# Theory Ntree

Up to index of Isabelle/ZF/Induct

theory Ntree
imports Main
begin

    (*  Title:      ZF/Induct/Ntree.thy
        ID:         $Id: Ntree.thy,v 1.5 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header {* Datatype definition n-ary branching trees *}

    theory Ntree imports Main begin

    text {*
      Demonstrates a simple use of function space in a datatype
      definition.  Based upon theory @{text Term}.
    *}

    consts
      ntree :: "i => i"
      maptree :: "i => i"
      maptree2 :: "[i, i] => i"

    datatype "ntree(A)" = Branch ("a ∈ A", "h ∈ (\<Union>n ∈ nat. n -> ntree(A))")
      monos UN_mono [OF subset_refl Pi_mono]  -- {* MUST have this form *}
      type_intros nat_fun_univ [THEN subsetD]
      type_elims UN_E

    datatype "maptree(A)" = Sons ("a ∈ A", "h ∈ maptree(A) -||> maptree(A)")
      monos FiniteFun_mono1  -- {* Use monotonicity in BOTH args *}
      type_intros FiniteFun_univ1 [THEN subsetD]

    datatype "maptree2(A, B)" = Sons2 ("a ∈ A", "h ∈ B -||> maptree2(A, B)")
      monos FiniteFun_mono [OF subset_refl]
      type_intros FiniteFun_in_univ'

    constdefs
      ntree_rec :: "[[i, i, i] => i, i] => i"
      "ntree_rec(b) ==
        Vrecursor(λpr. ntree_case(λx h. b(x, h, λi ∈ domain(h). pr`(h`i))))"

    constdefs
      ntree_copy :: "i => i"
      "ntree_copy(z) == ntree_rec(λx h r. Branch(x,r), z)"

    text {*
      \medskip @{text ntree}
    *}

    lemma ntree_unfold: "ntree(A) = A × (\<Union>n ∈ nat. n -> ntree(A))"
      by (blast intro: ntree.intros [unfolded ntree.con_defs]
        elim: ntree.cases [unfolded ntree.con_defs])

    lemma ntree_induct [induct set: ntree]:
      "[| t ∈ ntree(A);
          !!x n h. [| x ∈ A;  n ∈ nat;  h ∈ n -> ntree(A);  ∀i ∈ n. P(h`i)
                   |] ==> P(Branch(x,h))
       |] ==> P(t)"
      -- {* A nicer induction rule than the standard one. *}
    proof -
      case rule_context
      assume "t ∈ ntree(A)"
      thus ?thesis
        apply induct
        apply (erule UN_E)
        apply (assumption | rule rule_context)+
         apply (fast elim: fun_weaken_type)
        apply (fast dest: apply_type)
        done
    qed

    lemma ntree_induct_eqn:
      "[| t ∈ ntree(A);  f ∈ ntree(A)->B;  g ∈ ntree(A)->B;
          !!x n h. [| x ∈ A;  n ∈ nat;  h ∈ n -> ntree(A);  f O h = g O h |] ==>
                   f ` Branch(x,h) = g ` Branch(x,h)
       |] ==> f`t=g`t"
      -- {* Induction on @{term "ntree(A)"} to prove an equation *}
    proof -
      case rule_context
      assume "t ∈ ntree(A)"
      thus ?thesis
        apply induct
        apply (assumption | rule rule_context)+
        apply (insert rule_context)
        apply (rule fun_extension)
          apply (assumption | rule comp_fun)+
        apply (simp add: comp_fun_apply)
      done
    qed

    text {*
      \medskip Lemmas to justify using @{text Ntree} in other recursive
      type definitions.
    *}

    lemma ntree_mono: "A ⊆ B ==> ntree(A) ⊆ ntree(B)"
      apply (unfold ntree.defs)
      apply (rule lfp_mono)
        apply (rule ntree.bnd_mono)+
      apply (assumption | rule univ_mono basic_monos)+
      done

    lemma ntree_univ: "ntree(univ(A)) ⊆ univ(A)"
      -- {* Easily provable by induction also *}
      apply (unfold ntree.defs ntree.con_defs)
      apply (rule lfp_lowerbound)
       apply (rule_tac [2] A_subset_univ [THEN univ_mono])
      apply (blast intro: Pair_in_univ nat_fun_univ [THEN subsetD])
      done

    lemma ntree_subset_univ: "A ⊆ univ(B) ==> ntree(A) ⊆ univ(B)"
      by (rule subset_trans [OF ntree_mono ntree_univ])

    text {*
      \medskip @{text ntree} recursion.
    *}

    lemma ntree_rec_Branch:
        "function(h) ==>
         ntree_rec(b, Branch(x,h)) = b(x, h, λi ∈ domain(h). ntree_rec(b, h`i))"
      apply (rule ntree_rec_def [THEN def_Vrecursor, THEN trans])
      apply (simp add: ntree.con_defs rank_pair2 [THEN [2] lt_trans] rank_apply)
      done

    lemma ntree_copy_Branch [simp]:
        "function(h) ==>
         ntree_copy (Branch(x, h)) = Branch(x, λi ∈ domain(h). ntree_copy (h`i))"
      by (simp add: ntree_copy_def ntree_rec_Branch)

    lemma ntree_copy_is_ident: "z ∈ ntree(A) ==> ntree_copy(z) = z"
      apply (induct_tac z)
      apply (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
      done

    text {*
      \medskip @{text maptree}
    *}

    lemma maptree_unfold: "maptree(A) = A × (maptree(A) -||> maptree(A))"
      by (fast intro!: maptree.intros [unfolded maptree.con_defs]
        elim: maptree.cases [unfolded maptree.con_defs])

    lemma maptree_induct [induct set: maptree]:
      "[| t ∈ maptree(A);
          !!x n h. [| x ∈ A;  h ∈ maptree(A) -||> maptree(A);
                      ∀y ∈ field(h). P(y)
                   |] ==> P(Sons(x,h))
       |] ==> P(t)"
      -- {* A nicer induction rule than the standard one. *}
    proof -
      case rule_context
      assume "t ∈ maptree(A)"
      thus ?thesis
        apply induct
        apply (assumption | rule rule_context)+
         apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD])
        apply (drule FiniteFun.dom_subset [THEN subsetD])
        apply (drule Fin.dom_subset [THEN subsetD])
        apply fast
        done
    qed

    text {*
      \medskip @{text maptree2}
    *}

    lemma maptree2_unfold: "maptree2(A, B) = A × (B -||> maptree2(A, B))"
      by (fast intro!: maptree2.intros [unfolded maptree2.con_defs]
        elim: maptree2.cases [unfolded maptree2.con_defs])

    lemma maptree2_induct [induct set: maptree2]:
      "[| t ∈ maptree2(A, B);
          !!x n h. [| x ∈ A;  h ∈ B -||> maptree2(A,B);  ∀y ∈ range(h). P(y)
                   |] ==> P(Sons2(x,h))
       |] ==> P(t)"
    proof -
      case rule_context
      assume "t ∈ maptree2(A, B)"
      thus ?thesis
        apply induct
        apply (assumption | rule rule_context)+
         apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD])
        apply (drule FiniteFun.dom_subset [THEN subsetD])
        apply (drule Fin.dom_subset [THEN subsetD])
        apply fast
        done
    qed

    end

lemma ntree_unfold:

      ntree(A) = A × (\<Union>n∈nat. n -> ntree(A))

lemma ntree_induct:

      [| t ∈ ntree(A);
         !!x n h.
            [| x ∈ A; n ∈ nat; h ∈ n -> ntree(A); ∀i∈n. P(h ` i) |]
            ==> P(Branch(x, h)) |]
      ==> P(t)

lemma ntree_induct_eqn:

      [| t ∈ ntree(A); f ∈ ntree(A) -> B; g ∈ ntree(A) -> B;
         !!x n h.
            [| x ∈ A; n ∈ nat; h ∈ n -> ntree(A); f O h = g O h |]
            ==> f ` Branch(x, h) = g ` Branch(x, h) |]
      ==> f ` t = g ` t

lemma ntree_mono:

      A ⊆ B ==> ntree(A) ⊆ ntree(B)

lemma ntree_univ:

      ntree(univ(A)) ⊆ univ(A)

lemma ntree_subset_univ:

      A ⊆ univ(B) ==> ntree(A) ⊆ univ(B)

lemma ntree_rec_Branch:

      function(h)
      ==> ntree_rec(b, Branch(x, h)) = b(x, h, λi∈domain(h). ntree_rec(b, h ` i))

lemma ntree_copy_Branch:

      function(h)
      ==> ntree_copy(Branch(x, h)) = Branch(x, λi∈domain(h). ntree_copy(h ` i))

lemma ntree_copy_is_ident:

      z ∈ ntree(A) ==> ntree_copy(z) = z

lemma maptree_unfold:

      maptree(A) = A × (maptree(A) -||> maptree(A))

lemma maptree_induct:

      [| t ∈ maptree(A);
         !!x n h.
            [| x ∈ A; h ∈ maptree(A) -||> maptree(A); ∀y∈field(h). P(y) |]
            ==> P(Sons(x, h)) |]
      ==> P(t)

lemma maptree2_unfold:

      maptree2(A, B) = A × (B -||> maptree2(A, B))

lemma maptree2_induct:

      [| t ∈ maptree2(A, B);
         !!x n h.
            [| x ∈ A; h ∈ B -||> maptree2(A, B); ∀y∈range(h). P(y) |]
            ==> P(Sons2(x, h)) |]
      ==> P(t)