1169691Skan(* Title: ZF/Induct/Tree_Forest.thy 2169691Skan Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3169691Skan Copyright 1994 University of Cambridge 4169691Skan*) 5169691Skan 6169691Skansection \<open>Trees and forests, a mutually recursive type definition\<close> 7169691Skan 8169691Skantheory Tree_Forest imports ZF begin 9169691Skan 10169691Skansubsection \<open>Datatype definition\<close> 11169691Skan 12169691Skanconsts 13169691Skan tree :: "i => i" 14169691Skan forest :: "i => i" 15169691Skan tree_forest :: "i => i" 16169691Skan 17169691Skandatatype "tree(A)" = Tcons ("a \<in> A", "f \<in> forest(A)") 18169691Skan and "forest(A)" = Fnil | Fcons ("t \<in> tree(A)", "f \<in> forest(A)") 19169691Skan 20169691Skan(* FIXME *) 21169691Skanlemmas tree'induct = 22169691Skan tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, consumes 1] 23169691Skan and forest'induct = 24169691Skan tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, consumes 1] 25169691Skan for t f 26169691Skan 27169691Skandeclare tree_forest.intros [simp, TC] 28169691Skan 29169691Skanlemma tree_def: "tree(A) == Part(tree_forest(A), Inl)" 30169691Skan by (simp only: tree_forest.defs) 31169691Skan 32169691Skanlemma forest_def: "forest(A) == Part(tree_forest(A), Inr)" 33169691Skan by (simp only: tree_forest.defs) 34169691Skan 35169691Skan 36169691Skantext \<open> 37169691Skan \medskip \<^term>\<open>tree_forest(A)\<close> as the union of \<^term>\<open>tree(A)\<close> 38169691Skan and \<^term>\<open>forest(A)\<close>. 39169691Skan\<close> 40169691Skan 41169691Skanlemma tree_subset_TF: "tree(A) \<subseteq> tree_forest(A)" 42169691Skan apply (unfold tree_forest.defs) 43169691Skan apply (rule Part_subset) 44169691Skan done 45169691Skan 46169691Skanlemma treeI [TC]: "x \<in> tree(A) ==> x \<in> tree_forest(A)" 47169691Skan by (rule tree_subset_TF [THEN subsetD]) 48169691Skan 49169691Skanlemma forest_subset_TF: "forest(A) \<subseteq> tree_forest(A)" 50169691Skan apply (unfold tree_forest.defs) 51169691Skan apply (rule Part_subset) 52169691Skan done 53169691Skan 54169691Skanlemma treeI' [TC]: "x \<in> forest(A) ==> x \<in> tree_forest(A)" 55169691Skan by (rule forest_subset_TF [THEN subsetD]) 56169691Skan 57169691Skanlemma TF_equals_Un: "tree(A) \<union> forest(A) = tree_forest(A)" 58169691Skan apply (insert tree_subset_TF forest_subset_TF) 59169691Skan apply (auto intro!: equalityI tree_forest.intros elim: tree_forest.cases) 60169691Skan done 61169691Skan 62169691Skanlemma tree_forest_unfold: 63169691Skan "tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))" 64169691Skan \<comment> \<open>NOT useful, but interesting \dots\<close> 65169691Skan supply rews = tree_forest.con_defs tree_def forest_def 66 apply (unfold tree_def forest_def) 67 apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1] 68 elim: tree_forest.cases [unfolded rews]) 69 done 70 71lemma tree_forest_unfold': 72 "tree_forest(A) = 73 A \<times> Part(tree_forest(A), \<lambda>w. Inr(w)) + 74 {0} + Part(tree_forest(A), \<lambda>w. Inl(w)) * Part(tree_forest(A), \<lambda>w. Inr(w))" 75 by (rule tree_forest_unfold [unfolded tree_def forest_def]) 76 77lemma tree_unfold: "tree(A) = {Inl(x). x \<in> A \<times> forest(A)}" 78 apply (unfold tree_def forest_def) 79 apply (rule Part_Inl [THEN subst]) 80 apply (rule tree_forest_unfold' [THEN subst_context]) 81 done 82 83lemma forest_unfold: "forest(A) = {Inr(x). x \<in> {0} + tree(A)*forest(A)}" 84 apply (unfold tree_def forest_def) 85 apply (rule Part_Inr [THEN subst]) 86 apply (rule tree_forest_unfold' [THEN subst_context]) 87 done 88 89text \<open> 90 \medskip Type checking for recursor: Not needed; possibly interesting? 91\<close> 92 93lemma TF_rec_type: 94 "[| z \<in> tree_forest(A); 95 !!x f r. [| x \<in> A; f \<in> forest(A); r \<in> C(f) 96 |] ==> b(x,f,r) \<in> C(Tcons(x,f)); 97 c \<in> C(Fnil); 98 !!t f r1 r2. [| t \<in> tree(A); f \<in> forest(A); r1 \<in> C(t); r2 \<in> C(f) 99 |] ==> d(t,f,r1,r2) \<in> C(Fcons(t,f)) 100 |] ==> tree_forest_rec(b,c,d,z) \<in> C(z)" 101 by (induct_tac z) simp_all 102 103lemma tree_forest_rec_type: 104 "[| !!x f r. [| x \<in> A; f \<in> forest(A); r \<in> D(f) 105 |] ==> b(x,f,r) \<in> C(Tcons(x,f)); 106 c \<in> D(Fnil); 107 !!t f r1 r2. [| t \<in> tree(A); f \<in> forest(A); r1 \<in> C(t); r2 \<in> D(f) 108 |] ==> d(t,f,r1,r2) \<in> D(Fcons(t,f)) 109 |] ==> (\<forall>t \<in> tree(A). tree_forest_rec(b,c,d,t) \<in> C(t)) \<and> 110 (\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))" 111 \<comment> \<open>Mutually recursive version.\<close> 112 apply (unfold Ball_def) 113 apply (rule tree_forest.mutual_induct) 114 apply simp_all 115 done 116 117 118subsection \<open>Operations\<close> 119 120consts 121 map :: "[i => i, i] => i" 122 size :: "i => i" 123 preorder :: "i => i" 124 list_of_TF :: "i => i" 125 of_list :: "i => i" 126 reflect :: "i => i" 127 128primrec 129 "list_of_TF (Tcons(x,f)) = [Tcons(x,f)]" 130 "list_of_TF (Fnil) = []" 131 "list_of_TF (Fcons(t,tf)) = Cons (t, list_of_TF(tf))" 132 133primrec 134 "of_list([]) = Fnil" 135 "of_list(Cons(t,l)) = Fcons(t, of_list(l))" 136 137primrec 138 "map (h, Tcons(x,f)) = Tcons(h(x), map(h,f))" 139 "map (h, Fnil) = Fnil" 140 "map (h, Fcons(t,tf)) = Fcons (map(h, t), map(h, tf))" 141 142primrec 143 "size (Tcons(x,f)) = succ(size(f))" 144 "size (Fnil) = 0" 145 "size (Fcons(t,tf)) = size(t) #+ size(tf)" 146 147primrec 148 "preorder (Tcons(x,f)) = Cons(x, preorder(f))" 149 "preorder (Fnil) = Nil" 150 "preorder (Fcons(t,tf)) = preorder(t) @ preorder(tf)" 151 152primrec 153 "reflect (Tcons(x,f)) = Tcons(x, reflect(f))" 154 "reflect (Fnil) = Fnil" 155 "reflect (Fcons(t,tf)) = 156 of_list (list_of_TF (reflect(tf)) @ Cons(reflect(t), Nil))" 157 158 159text \<open> 160 \medskip \<open>list_of_TF\<close> and \<open>of_list\<close>. 161\<close> 162 163lemma list_of_TF_type [TC]: 164 "z \<in> tree_forest(A) ==> list_of_TF(z) \<in> list(tree(A))" 165 by (induct set: tree_forest) simp_all 166 167lemma of_list_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)" 168 by (induct set: list) simp_all 169 170text \<open> 171 \medskip \<open>map\<close>. 172\<close> 173 174lemma 175 assumes "!!x. x \<in> A ==> h(x): B" 176 shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)" 177 and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)" 178 using assms 179 by (induct rule: tree'induct forest'induct) simp_all 180 181text \<open> 182 \medskip \<open>size\<close>. 183\<close> 184 185lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat" 186 by (induct set: tree_forest) simp_all 187 188 189text \<open> 190 \medskip \<open>preorder\<close>. 191\<close> 192 193lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)" 194 by (induct set: tree_forest) simp_all 195 196 197text \<open> 198 \medskip Theorems about \<open>list_of_TF\<close> and \<open>of_list\<close>. 199\<close> 200 201lemma forest_induct [consumes 1, case_names Fnil Fcons]: 202 "[| f \<in> forest(A); 203 R(Fnil); 204 !!t f. [| t \<in> tree(A); f \<in> forest(A); R(f) |] ==> R(Fcons(t,f)) 205 |] ==> R(f)" 206 \<comment> \<open>Essentially the same as list induction.\<close> 207 apply (erule tree_forest.mutual_induct 208 [THEN conjunct2, THEN spec, THEN [2] rev_mp]) 209 apply (rule TrueI) 210 apply simp 211 apply simp 212 done 213 214lemma forest_iso: "f \<in> forest(A) ==> of_list(list_of_TF(f)) = f" 215 by (induct rule: forest_induct) simp_all 216 217lemma tree_list_iso: "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts" 218 by (induct set: list) simp_all 219 220 221text \<open> 222 \medskip Theorems about \<open>map\<close>. 223\<close> 224 225lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z" 226 by (induct set: tree_forest) simp_all 227 228lemma map_compose: 229 "z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)" 230 by (induct set: tree_forest) simp_all 231 232 233text \<open> 234 \medskip Theorems about \<open>size\<close>. 235\<close> 236 237lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)" 238 by (induct set: tree_forest) simp_all 239 240lemma size_length: "z \<in> tree_forest(A) ==> size(z) = length(preorder(z))" 241 by (induct set: tree_forest) (simp_all add: length_app) 242 243text \<open> 244 \medskip Theorems about \<open>preorder\<close>. 245\<close> 246 247lemma preorder_map: 248 "z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))" 249 by (induct set: tree_forest) (simp_all add: map_app_distrib) 250 251end 252