--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Brouwer.thy Fri Nov 16 22:11:19 2001 +0100
@@ -0,0 +1,85 @@
+(* Title: ZF/Induct/Brouwer.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+*)
+
+header {* Infinite branching datatype definitions *}
+
+theory Brouwer = Main:
+
+subsection {* The Brouwer ordinals *}
+
+consts
+ brouwer :: i
+
+datatype \<subseteq> "Vfrom(0, csucc(nat))"
+ "brouwer" = Zero | Suc ("b \<in> brouwer") | Lim ("h \<in> nat -> brouwer")
+ monos Pi_mono
+ type_intros inf_datatype_intrs
+
+lemma brouwer_unfold: "brouwer = {0} + brouwer + (nat -> brouwer)"
+ by (fast intro!: brouwer.intros [unfolded brouwer.con_defs]
+ elim: brouwer.cases [unfolded brouwer.con_defs])
+
+lemma brouwer_induct2:
+ "[| b \<in> brouwer;
+ P(Zero);
+ !!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b));
+ !!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i)
+ |] ==> P(Lim(h))
+ |] ==> P(b)"
+ -- {* A nicer induction rule than the standard one. *}
+proof -
+ case rule_context
+ assume "b \<in> brouwer"
+ thus ?thesis
+ apply induct
+ apply (assumption | rule rule_context)+
+ apply (fast elim: fun_weaken_type)
+ apply (fast dest: apply_type)
+ done
+qed
+
+
+subsection {* The Martin-Löf wellordering type *}
+
+consts
+ Well :: "[i, i => i] => i"
+
+datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))"
+ -- {* The union with @{text nat} ensures that the cardinal is infinite. *}
+ "Well(A, B)" = Sup ("a \<in> A", "f \<in> B(a) -> Well(A, B)")
+ monos Pi_mono
+ type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intrs
+
+lemma Well_unfold: "Well(A, B) = (\<Sigma>x \<in> A. B(x) -> Well(A, B))"
+ by (fast intro!: Well.intros [unfolded Well.con_defs]
+ elim: Well.cases [unfolded Well.con_defs])
+
+
+lemma Well_induct2:
+ "[| w \<in> Well(A, B);
+ !!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y)
+ |] ==> P(Sup(a,f))
+ |] ==> P(w)"
+ -- {* A nicer induction rule than the standard one. *}
+proof -
+ case rule_context
+ assume "w \<in> Well(A, B)"
+ thus ?thesis
+ apply induct
+ apply (assumption | rule rule_context)+
+ apply (fast elim: fun_weaken_type)
+ apply (fast dest: apply_type)
+ done
+qed
+
+lemma Well_bool_unfold: "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))"
+ -- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
+ -- {* for @{text Well} to prove this. *}
+ apply (rule Well_unfold [THEN trans])
+ apply (simp add: Sigma_bool Pi_empty1 succ_def)
+ done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Ntree.thy Fri Nov 16 22:11:19 2001 +0100
@@ -0,0 +1,190 @@
+(* Title: ZF/Induct/Ntree.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+*)
+
+header {* Datatype definition n-ary branching trees *}
+
+theory Ntree = Main:
+
+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 \<in> A", "h \<in> (\<Union>n \<in> 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 \<in> A", "h \<in> maptree(A) -||> maptree(A)")
+ monos FiniteFun_mono1 -- {* Use monotonicity in BOTH args *}
+ type_intros FiniteFun_univ1 [THEN subsetD]
+
+datatype "maptree2(A, B)" = Sons2 ("a \<in> A", "h \<in> 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, \<lambda>i \<in> 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 \<times> (\<Union>n \<in> nat. n -> ntree(A))"
+ by (fast intro!: ntree.intros [unfolded ntree.con_defs]
+ elim: ntree.cases [unfolded ntree.con_defs])
+
+lemma ntree_induct [induct set: ntree]:
+ "[| t \<in> ntree(A);
+ !!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); \<forall>i \<in> n. P(h`i)
+ |] ==> P(Branch(x,h))
+ |] ==> P(t)"
+ -- {* A nicer induction rule than the standard one. *}
+proof -
+ case rule_context
+ assume "t \<in> 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 \<in> ntree(A); f \<in> ntree(A)->B; g \<in> ntree(A)->B;
+ !!x n h. [| x \<in> A; n \<in> nat; h \<in> 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 \<in> 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 \<subseteq> B ==> ntree(A) \<subseteq> 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)) \<subseteq> 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 \<subseteq> univ(B) ==> ntree(A) \<subseteq> univ(B)"
+ by (rule subset_trans [OF ntree_mono ntree_univ])
+
+
+text {*
+ \medskip @{text ntree} recursion.
+*}
+
+lemma ntree_rec_Branch: "ntree_rec(b, Branch(x,h))
+ = b(x, h, \<lambda>i \<in> 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]:
+ "ntree_copy (Branch(x, h)) = Branch(x, \<lambda>i \<in> domain(h). ntree_copy (h`i))"
+ apply (unfold ntree_copy_def)
+ apply (rule ntree_rec_Branch)
+ done
+
+lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z"
+ apply (induct_tac z)
+ apply (auto simp add: domain_of_fun Pi_Collect_iff)
+ done
+
+
+text {*
+ \medskip @{text maptree}
+*}
+
+lemma maptree_unfold: "maptree(A) = A \<times> (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 \<in> maptree(A);
+ !!x n h. [| x \<in> A; h \<in> maptree(A) -||> maptree(A);
+ \<forall>y \<in> field(h). P(y)
+ |] ==> P(Sons(x,h))
+ |] ==> P(t)"
+ -- {* A nicer induction rule than the standard one. *}
+proof -
+ case rule_context
+ assume "t \<in> 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 \<times> (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 \<in> maptree2(A, B);
+ !!x n h. [| x \<in> A; h \<in> B -||> maptree2(A,B); \<forall>y \<in> range(h). P(y)
+ |] ==> P(Sons2(x,h))
+ |] ==> P(t)"
+proof -
+ case rule_context
+ assume "t \<in> 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
--- a/src/ZF/Induct/ROOT.ML Fri Nov 16 22:10:27 2001 +0100
+++ b/src/ZF/Induct/ROOT.ML Fri Nov 16 22:11:19 2001 +0100
@@ -6,10 +6,13 @@
Inductive definitions.
*)
-time_use_thy "Datatypes";
-time_use_thy "Binary_Trees";
+(** Datatypes **)
+time_use_thy "Datatypes"; (*sample datatypes*)
+time_use_thy "Binary_Trees"; (*binary trees*)
time_use_thy "Term"; (*recursion over the list functor*)
+time_use_thy "Ntree"; (*variable-branching trees; function demo*)
time_use_thy "Tree_Forest"; (*mutual recursion*)
+time_use_thy "Brouwer"; (*Infinite-branching trees*)
time_use_thy "Mutil"; (*mutilated chess board*)
(*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for
--- a/src/ZF/IsaMakefile Fri Nov 16 22:10:27 2001 +0100
+++ b/src/ZF/IsaMakefile Fri Nov 16 22:11:19 2001 +0100
@@ -125,10 +125,10 @@
ZF-Induct: ZF $(LOG)/ZF-Induct.gz
$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
- Induct/Binary_Trees.thy Induct/Comb.ML Induct/Comb.thy Induct/Datatypes.thy \
- Induct/FoldSet.ML Induct/FoldSet.thy Induct/ListN.ML Induct/ListN.thy \
- Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
- Induct/Primrec_defs.ML Induct/Primrec_defs.thy \
+ Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.ML Induct/Comb.thy \
+ Induct/Datatypes.thy Induct/FoldSet.ML Induct/FoldSet.thy Induct/ListN.ML \
+ Induct/ListN.thy Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
+ Induct/Ntree.thy Induct/Primrec_defs.ML Induct/Primrec_defs.thy \
Induct/Primrec.ML Induct/Primrec.thy \
Induct/PropLog.ML Induct/PropLog.thy Induct/Rmap.ML Induct/Rmap.thy \
Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
@@ -140,10 +140,8 @@
ZF-ex: ZF $(LOG)/ZF-ex.gz
$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \
- ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
- ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
- ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy \
- ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
+ ex/BinEx.thy ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
+ ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy ex/Primes.ML ex/Primes.thy \
ex/NatSum.ML ex/NatSum.thy ex/Ramsey.ML ex/Ramsey.thy ex/misc.thy
@$(ISATOOL) usedir $(OUT)/ZF ex
--- a/src/ZF/ex/Brouwer.ML Fri Nov 16 22:10:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-(* Title: ZF/ex/Brouwer.ML
- ID: $ $
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Infinite branching datatype definitions
- (1) the Brouwer ordinals
- (2) the Martin-Löf wellordering type
-*)
-
-open Brouwer;
-
-(** The Brouwer ordinals **)
-
-Goal "brouwer = {0} + brouwer + (nat -> brouwer)";
-let open brouwer; val rew = rewrite_rule con_defs in
-by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
-end;
-qed "brouwer_unfold";
-
-(*A nicer induction rule than the standard one*)
-val major::prems = goal Brouwer.thy
- "[| b \\<in> brouwer; \
-\ P(Zero); \
-\ !!b. [| b \\<in> brouwer; P(b) |] ==> P(Suc(b)); \
-\ !!h. [| h \\<in> nat -> brouwer; \\<forall>i \\<in> nat. P(h`i) \
-\ |] ==> P(Lim(h)) \
-\ |] ==> P(b)";
-by (rtac (major RS brouwer.induct) 1);
-by (REPEAT_SOME (ares_tac prems));
-by (fast_tac (claset() addEs [fun_weaken_type]) 1);
-by (fast_tac (claset() addDs [apply_type]) 1);
-qed "brouwer_induct2";
-
-
-(** The Martin-Löf wellordering type **)
-
-Goal "Well(A,B) = (\\<Sigma>x \\<in> A. B(x) -> Well(A,B))";
-let open Well; val rew = rewrite_rule con_defs in
-by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
-end;
-qed "Well_unfold";
-
-(*A nicer induction rule than the standard one*)
-val major::prems = goal Brouwer.thy
- "[| w \\<in> Well(A,B); \
-\ !!a f. [| a \\<in> A; f \\<in> B(a) -> Well(A,B); \\<forall>y \\<in> B(a). P(f`y) \
-\ |] ==> P(Sup(a,f)) \
-\ |] ==> P(w)";
-by (rtac (major RS Well.induct) 1);
-by (REPEAT_SOME (ares_tac prems));
-by (fast_tac (claset() addEs [fun_weaken_type]) 1);
-by (fast_tac (claset() addDs [apply_type]) 1);
-qed "Well_induct2";
-
-
-(*In fact it's isomorphic to nat, but we need a recursion operator for
- Well to prove this.*)
-Goal "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))";
-by (resolve_tac [Well_unfold RS trans] 1);
-by (simp_tac (simpset() addsimps [Sigma_bool, Pi_empty1, succ_def]) 1);
-qed "Well_bool_unfold";
--- a/src/ZF/ex/Brouwer.thy Fri Nov 16 22:10:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: ZF/ex/Brouwer.thy
- ID: $ $
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Infinite branching datatype definitions
- (1) the Brouwer ordinals
- (2) the Martin-Löf wellordering type
-*)
-
-Brouwer = Main +
-
-consts
- brouwer :: i
- Well :: [i,i=>i]=>i
-
-datatype <= "Vfrom(0, csucc(nat))"
- "brouwer" = Zero | Suc ("b \\<in> brouwer") | Lim ("h \\<in> nat -> brouwer")
- monos Pi_mono
- type_intrs "inf_datatype_intrs"
-
-(*The union with nat ensures that the cardinal is infinite*)
-datatype <= "Vfrom(A Un (\\<Union>x \\<in> A. B(x)), csucc(nat Un |\\<Union>x \\<in> A. B(x)|))"
- "Well(A,B)" = Sup ("a \\<in> A", "f \\<in> B(a) -> Well(A,B)")
- monos Pi_mono
- type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]
- @ inf_datatype_intrs"
-
-
-end
--- a/src/ZF/ex/Ntree.ML Fri Nov 16 22:10:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,137 +0,0 @@
-(* Title: ZF/ex/Ntree.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Datatype definition n-ary branching trees
-Demonstrates a simple use of function space in a datatype definition
-
-Based upon ex/Term.ML
-*)
-
-(** ntree **)
-
-Goal "ntree(A) = A * (\\<Union>n \\<in> nat. n -> ntree(A))";
-let open ntree; val rew = rewrite_rule con_defs in
-by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
-end;
-qed "ntree_unfold";
-
-(*A nicer induction rule than the standard one*)
-val major::prems = goal Ntree.thy
- "[| t \\<in> ntree(A); \
-\ !!x n h. [| x \\<in> A; n \\<in> nat; h \\<in> n -> ntree(A); \\<forall>i \\<in> n. P(h`i) \
-\ |] ==> P(Branch(x,h)) \
-\ |] ==> P(t)";
-by (rtac (major RS ntree.induct) 1);
-by (etac UN_E 1);
-by (REPEAT_SOME (ares_tac prems));
-by (fast_tac (claset() addEs [fun_weaken_type]) 1);
-by (fast_tac (claset() addDs [apply_type]) 1);
-qed "ntree_induct";
-
-(*Induction on ntree(A) to prove an equation*)
-val major::prems = goal Ntree.thy
- "[| t \\<in> ntree(A); f \\<in> ntree(A)->B; g \\<in> ntree(A)->B; \
-\ !!x n h. [| x \\<in> A; n \\<in> nat; h \\<in> n -> ntree(A); f O h = g O h |] ==> \
-\ f ` Branch(x,h) = g ` Branch(x,h) \
-\ |] ==> f`t=g`t";
-by (rtac (major RS ntree_induct) 1);
-by (REPEAT_SOME (ares_tac prems));
-by (cut_facts_tac prems 1);
-by (rtac fun_extension 1);
-by (REPEAT_SOME (ares_tac [comp_fun]));
-by (asm_simp_tac (simpset() addsimps [comp_fun_apply]) 1);
-qed "ntree_induct_eqn";
-
-(** Lemmas to justify using "Ntree" in other recursive type definitions **)
-
-Goalw ntree.defs "A \\<subseteq> B ==> ntree(A) \\<subseteq> ntree(B)";
-by (rtac lfp_mono 1);
-by (REPEAT (rtac ntree.bnd_mono 1));
-by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
-qed "ntree_mono";
-
-(*Easily provable by induction also*)
-Goalw (ntree.defs@ntree.con_defs) "ntree(univ(A)) \\<subseteq> univ(A)";
-by (rtac lfp_lowerbound 1);
-by (rtac (A_subset_univ RS univ_mono) 2);
-by Safe_tac;
-by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1));
-qed "ntree_univ";
-
-val ntree_subset_univ = [ntree_mono, ntree_univ] MRS subset_trans |> standard;
-
-
-(** ntree recursion **)
-
-Goal "ntree_rec(b, Branch(x,h)) \
-\ = b(x, h, \\<lambda>i \\<in> domain(h). ntree_rec(b, h`i))";
-by (rtac (ntree_rec_def RS def_Vrecursor RS trans) 1);
-by (Simp_tac 1);
-by (rewrite_goals_tac ntree.con_defs);
-by (asm_simp_tac (simpset() addsimps [rank_pair2 RSN (2, lt_trans),
- rank_apply]) 1);;
-qed "ntree_rec_Branch";
-
-Goalw [ntree_copy_def]
- "ntree_copy (Branch(x, h)) = Branch(x, \\<lambda>i \\<in> domain(h). ntree_copy (h`i))";
-by (rtac ntree_rec_Branch 1);
-qed "ntree_copy_Branch";
-
-Addsimps [ntree_copy_Branch];
-
-Goal "z \\<in> ntree(A) ==> ntree_copy(z) = z";
-by (induct_tac "z" 1);
-by (auto_tac (claset(), simpset() addsimps [domain_of_fun, Pi_Collect_iff]));
-qed "ntree_copy_is_ident";
-
-
-
-(** maptree **)
-
-Goal "maptree(A) = A * (maptree(A) -||> maptree(A))";
-let open maptree; val rew = rewrite_rule con_defs in
-by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
-end;
-qed "maptree_unfold";
-
-(*A nicer induction rule than the standard one*)
-val major::prems = goal Ntree.thy
- "[| t \\<in> maptree(A); \
-\ !!x n h. [| x \\<in> A; h \\<in> maptree(A) -||> maptree(A); \
-\ \\<forall>y \\<in> field(h). P(y) \
-\ |] ==> P(Sons(x,h)) \
-\ |] ==> P(t)";
-by (rtac (major RS maptree.induct) 1);
-by (REPEAT_SOME (ares_tac prems));
-by (eresolve_tac [Collect_subset RS FiniteFun_mono1 RS subsetD] 1);
-by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1);
-by (dresolve_tac [Fin.dom_subset RS subsetD] 1);
-by (Fast_tac 1);
-qed "maptree_induct";
-
-
-(** maptree2 **)
-
-Goal "maptree2(A,B) = A * (B -||> maptree2(A,B))";
-let open maptree2; val rew = rewrite_rule con_defs in
-by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
-end;
-qed "maptree2_unfold";
-
-(*A nicer induction rule than the standard one*)
-val major::prems = goal Ntree.thy
- "[| t \\<in> maptree2(A,B); \
-\ !!x n h. [| x \\<in> A; h \\<in> B -||> maptree2(A,B); \\<forall>y \\<in> range(h). P(y) \
-\ |] ==> P(Sons2(x,h)) \
-\ |] ==> P(t)";
-by (rtac (major RS maptree2.induct) 1);
-by (REPEAT_SOME (ares_tac prems));
-by (eresolve_tac [[subset_refl, Collect_subset] MRS
- FiniteFun_mono RS subsetD] 1);
-by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1);
-by (dresolve_tac [Fin.dom_subset RS subsetD] 1);
-by (Fast_tac 1);
-qed "maptree2_induct";
-
--- a/src/ZF/ex/Ntree.thy Fri Nov 16 22:10:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(* Title: ZF/ex/Ntree.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Datatype definition n-ary branching trees
-Demonstrates a simple use of function space in a datatype definition
-
-Based upon ex/Term.thy
-*)
-
-Ntree = Main +
-consts
- ntree :: i=>i
- maptree :: i=>i
- maptree2 :: [i,i] => i
-
-datatype
- "ntree(A)" = Branch ("a \\<in> A", "h \\<in> (\\<Union>n \\<in> nat. n -> ntree(A))")
- monos "[[subset_refl, Pi_mono] MRS UN_mono]" (*MUST have this form*)
- type_intrs "[nat_fun_univ RS subsetD]"
- type_elims UN_E
-
-datatype
- "maptree(A)" = Sons ("a \\<in> A", "h \\<in> maptree(A) -||> maptree(A)")
- monos FiniteFun_mono1 (*Use monotonicity in BOTH args*)
- type_intrs "[FiniteFun_univ1 RS subsetD]"
-
-datatype
- "maptree2(A,B)" = Sons2 ("a \\<in> A", "h \\<in> B -||> maptree2(A,B)")
- monos "[subset_refl RS FiniteFun_mono]"
- type_intrs FiniteFun_in_univ'
-
-
-constdefs
- ntree_rec :: [[i,i,i]=>i, i] => i
- "ntree_rec(b) ==
- Vrecursor(%pr. ntree_case(%x h. b(x, h, \\<lambda>i \\<in> domain(h). pr`(h`i))))"
-
-constdefs
- ntree_copy :: i=>i
- "ntree_copy(z) == ntree_rec(%x h r. Branch(x,r), z)"
-
-end
--- a/src/ZF/ex/ROOT.ML Fri Nov 16 22:10:27 2001 +0100
+++ b/src/ZF/ex/ROOT.ML Fri Nov 16 22:11:19 2001 +0100
@@ -14,10 +14,6 @@
time_use_thy "Limit"; (*Inverse limit construction of domains*)
time_use_thy "BinEx"; (*Binary integer arithmetic*)
-(** Datatypes **)
-time_use_thy "Ntree"; (*variable-branching trees; function demo*)
-time_use_thy "Brouwer"; (*Infinite-branching trees*)
-
(** CoDatatypes **)
time_use_thy "LList";
time_use_thy "CoUnit";