1(* Title: ZF/Induct/Ntree.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1994 University of Cambridge 4*) 5 6section \<open>Datatype definition n-ary branching trees\<close> 7 8theory Ntree imports ZF begin 9 10text \<open> 11 Demonstrates a simple use of function space in a datatype 12 definition. Based upon theory \<open>Term\<close>. 13\<close> 14 15consts 16 ntree :: "i => i" 17 maptree :: "i => i" 18 maptree2 :: "[i, i] => i" 19 20datatype "ntree(A)" = Branch ("a \<in> A", "h \<in> (\<Union>n \<in> nat. n -> ntree(A))") 21 monos UN_mono [OF subset_refl Pi_mono] \<comment> \<open>MUST have this form\<close> 22 type_intros nat_fun_univ [THEN subsetD] 23 type_elims UN_E 24 25datatype "maptree(A)" = Sons ("a \<in> A", "h \<in> maptree(A) -||> maptree(A)") 26 monos FiniteFun_mono1 \<comment> \<open>Use monotonicity in BOTH args\<close> 27 type_intros FiniteFun_univ1 [THEN subsetD] 28 29datatype "maptree2(A, B)" = Sons2 ("a \<in> A", "h \<in> B -||> maptree2(A, B)") 30 monos FiniteFun_mono [OF subset_refl] 31 type_intros FiniteFun_in_univ' 32 33definition 34 ntree_rec :: "[[i, i, i] => i, i] => i" where 35 "ntree_rec(b) == 36 Vrecursor(\<lambda>pr. ntree_case(\<lambda>x h. b(x, h, \<lambda>i \<in> domain(h). pr`(h`i))))" 37 38definition 39 ntree_copy :: "i => i" where 40 "ntree_copy(z) == ntree_rec(\<lambda>x h r. Branch(x,r), z)" 41 42 43text \<open> 44 \medskip \<open>ntree\<close> 45\<close> 46 47lemma ntree_unfold: "ntree(A) = A \<times> (\<Union>n \<in> nat. n -> ntree(A))" 48 by (blast intro: ntree.intros [unfolded ntree.con_defs] 49 elim: ntree.cases [unfolded ntree.con_defs]) 50 51lemma ntree_induct [consumes 1, case_names Branch, induct set: ntree]: 52 assumes t: "t \<in> ntree(A)" 53 and step: "!!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); \<forall>i \<in> n. P(h`i) 54 |] ==> P(Branch(x,h))" 55 shows "P(t)" 56 \<comment> \<open>A nicer induction rule than the standard one.\<close> 57 using t 58 apply induct 59 apply (erule UN_E) 60 apply (assumption | rule step)+ 61 apply (fast elim: fun_weaken_type) 62 apply (fast dest: apply_type) 63 done 64 65lemma ntree_induct_eqn [consumes 1]: 66 assumes t: "t \<in> ntree(A)" 67 and f: "f \<in> ntree(A)->B" 68 and g: "g \<in> ntree(A)->B" 69 and step: "!!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); f O h = g O h |] ==> 70 f ` Branch(x,h) = g ` Branch(x,h)" 71 shows "f`t=g`t" 72 \<comment> \<open>Induction on \<^term>\<open>ntree(A)\<close> to prove an equation\<close> 73 using t 74 apply induct 75 apply (assumption | rule step)+ 76 apply (insert f g) 77 apply (rule fun_extension) 78 apply (assumption | rule comp_fun)+ 79 apply (simp add: comp_fun_apply) 80 done 81 82text \<open> 83 \medskip Lemmas to justify using \<open>Ntree\<close> in other recursive 84 type definitions. 85\<close> 86 87lemma ntree_mono: "A \<subseteq> B ==> ntree(A) \<subseteq> ntree(B)" 88 apply (unfold ntree.defs) 89 apply (rule lfp_mono) 90 apply (rule ntree.bnd_mono)+ 91 apply (assumption | rule univ_mono basic_monos)+ 92 done 93 94lemma ntree_univ: "ntree(univ(A)) \<subseteq> univ(A)" 95 \<comment> \<open>Easily provable by induction also\<close> 96 apply (unfold ntree.defs ntree.con_defs) 97 apply (rule lfp_lowerbound) 98 apply (rule_tac [2] A_subset_univ [THEN univ_mono]) 99 apply (blast intro: Pair_in_univ nat_fun_univ [THEN subsetD]) 100 done 101 102lemma ntree_subset_univ: "A \<subseteq> univ(B) ==> ntree(A) \<subseteq> univ(B)" 103 by (rule subset_trans [OF ntree_mono ntree_univ]) 104 105 106text \<open> 107 \medskip \<open>ntree\<close> recursion. 108\<close> 109 110lemma ntree_rec_Branch: 111 "function(h) ==> 112 ntree_rec(b, Branch(x,h)) = b(x, h, \<lambda>i \<in> domain(h). ntree_rec(b, h`i))" 113 apply (rule ntree_rec_def [THEN def_Vrecursor, THEN trans]) 114 apply (simp add: ntree.con_defs rank_pair2 [THEN [2] lt_trans] rank_apply) 115 done 116 117lemma ntree_copy_Branch [simp]: 118 "function(h) ==> 119 ntree_copy (Branch(x, h)) = Branch(x, \<lambda>i \<in> domain(h). ntree_copy (h`i))" 120 by (simp add: ntree_copy_def ntree_rec_Branch) 121 122lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z" 123 by (induct z set: ntree) 124 (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function) 125 126 127text \<open> 128 \medskip \<open>maptree\<close> 129\<close> 130 131lemma maptree_unfold: "maptree(A) = A \<times> (maptree(A) -||> maptree(A))" 132 by (fast intro!: maptree.intros [unfolded maptree.con_defs] 133 elim: maptree.cases [unfolded maptree.con_defs]) 134 135lemma maptree_induct [consumes 1, induct set: maptree]: 136 assumes t: "t \<in> maptree(A)" 137 and step: "!!x n h. [| x \<in> A; h \<in> maptree(A) -||> maptree(A); 138 \<forall>y \<in> field(h). P(y) 139 |] ==> P(Sons(x,h))" 140 shows "P(t)" 141 \<comment> \<open>A nicer induction rule than the standard one.\<close> 142 using t 143 apply induct 144 apply (assumption | rule step)+ 145 apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD]) 146 apply (drule FiniteFun.dom_subset [THEN subsetD]) 147 apply (drule Fin.dom_subset [THEN subsetD]) 148 apply fast 149 done 150 151 152text \<open> 153 \medskip \<open>maptree2\<close> 154\<close> 155 156lemma maptree2_unfold: "maptree2(A, B) = A \<times> (B -||> maptree2(A, B))" 157 by (fast intro!: maptree2.intros [unfolded maptree2.con_defs] 158 elim: maptree2.cases [unfolded maptree2.con_defs]) 159 160lemma maptree2_induct [consumes 1, induct set: maptree2]: 161 assumes t: "t \<in> maptree2(A, B)" 162 and step: "!!x n h. [| x \<in> A; h \<in> B -||> maptree2(A,B); \<forall>y \<in> range(h). P(y) 163 |] ==> P(Sons2(x,h))" 164 shows "P(t)" 165 using t 166 apply induct 167 apply (assumption | rule step)+ 168 apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD]) 169 apply (drule FiniteFun.dom_subset [THEN subsetD]) 170 apply (drule Fin.dom_subset [THEN subsetD]) 171 apply fast 172 done 173 174end 175