# HG changeset patch # User wenzelm # Date 1005945079 -3600 # Node ID bfba0eb5124bd934e4d46a02eb9e2532fe6a7be8 # Parent 9e5d3c96111a30c81fde70d2a2008a545bd5f056 Ntree and Brouwer converted and moved to ZF/Induct; diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/Induct/Brouwer.thy --- /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 \ "Vfrom(0, csucc(nat))" + "brouwer" = Zero | Suc ("b \ brouwer") | Lim ("h \ 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 \ brouwer; + P(Zero); + !!b. [| b \ brouwer; P(b) |] ==> P(Suc(b)); + !!h. [| h \ nat -> brouwer; \i \ nat. P(h`i) + |] ==> P(Lim(h)) + |] ==> P(b)" + -- {* A nicer induction rule than the standard one. *} +proof - + case rule_context + assume "b \ 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 \ "Vfrom(A \ (\x \ A. B(x)), csucc(nat \ |\x \ A. B(x)|))" + -- {* The union with @{text nat} ensures that the cardinal is infinite. *} + "Well(A, B)" = Sup ("a \ A", "f \ 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) = (\x \ 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 \ Well(A, B); + !!a f. [| a \ A; f \ B(a) -> Well(A,B); \y \ 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 \ 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 diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/Induct/Ntree.thy --- /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 \ A", "h \ (\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 \ (\n \ 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 \ 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: "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]: + "ntree_copy (Branch(x, h)) = Branch(x, \i \ domain(h). ntree_copy (h`i))" + apply (unfold ntree_copy_def) + apply (rule ntree_rec_Branch) + done + +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) + 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 diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/Induct/ROOT.ML --- 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 diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/IsaMakefile --- 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 diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/ex/Brouwer.ML --- 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 \\ brouwer; \ -\ P(Zero); \ -\ !!b. [| b \\ brouwer; P(b) |] ==> P(Suc(b)); \ -\ !!h. [| h \\ nat -> brouwer; \\i \\ 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) = (\\x \\ 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 \\ Well(A,B); \ -\ !!a f. [| a \\ A; f \\ B(a) -> Well(A,B); \\y \\ 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"; diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/ex/Brouwer.thy --- 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 \\ brouwer") | Lim ("h \\ nat -> brouwer") - monos Pi_mono - type_intrs "inf_datatype_intrs" - -(*The union with nat ensures that the cardinal is infinite*) -datatype <= "Vfrom(A Un (\\x \\ A. B(x)), csucc(nat Un |\\x \\ A. B(x)|))" - "Well(A,B)" = Sup ("a \\ A", "f \\ B(a) -> Well(A,B)") - monos Pi_mono - type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans] - @ inf_datatype_intrs" - - -end diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/ex/Ntree.ML --- 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 * (\\n \\ 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 \\ ntree(A); \ -\ !!x n h. [| x \\ A; n \\ nat; h \\ n -> ntree(A); \\i \\ 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 \\ 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"; -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 \\ B ==> ntree(A) \\ 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)) \\ 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, \\i \\ 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, \\i \\ domain(h). ntree_copy (h`i))"; -by (rtac ntree_rec_Branch 1); -qed "ntree_copy_Branch"; - -Addsimps [ntree_copy_Branch]; - -Goal "z \\ 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 \\ maptree(A); \ -\ !!x n h. [| x \\ A; h \\ maptree(A) -||> maptree(A); \ -\ \\y \\ 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 \\ maptree2(A,B); \ -\ !!x n h. [| x \\ A; h \\ B -||> maptree2(A,B); \\y \\ 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"; - diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/ex/Ntree.thy --- 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 \\ A", "h \\ (\\n \\ 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 \\ A", "h \\ maptree(A) -||> maptree(A)") - monos FiniteFun_mono1 (*Use monotonicity in BOTH args*) - type_intrs "[FiniteFun_univ1 RS subsetD]" - -datatype - "maptree2(A,B)" = Sons2 ("a \\ A", "h \\ 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, \\i \\ domain(h). pr`(h`i))))" - -constdefs - ntree_copy :: i=>i - "ntree_copy(z) == ntree_rec(%x h r. Branch(x,r), z)" - -end diff -r 9e5d3c96111a -r bfba0eb5124b src/ZF/ex/ROOT.ML --- 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";