1(* Title: ZF/Induct/Term.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1994 University of Cambridge 4*) 5 6section \<open>Terms over an alphabet\<close> 7 8theory Term imports ZF begin 9 10text \<open> 11 Illustrates the list functor (essentially the same type as in \<open>Trees_Forest\<close>). 12\<close> 13 14consts 15 "term" :: "i => i" 16 17datatype "term(A)" = Apply ("a \<in> A", "l \<in> list(term(A))") 18 monos list_mono 19 type_elims list_univ [THEN subsetD, elim_format] 20 21declare Apply [TC] 22 23definition 24 term_rec :: "[i, [i, i, i] => i] => i" where 25 "term_rec(t,d) == 26 Vrec(t, \<lambda>t g. term_case(\<lambda>x zs. d(x, zs, map(\<lambda>z. g`z, zs)), t))" 27 28definition 29 term_map :: "[i => i, i] => i" where 30 "term_map(f,t) == term_rec(t, \<lambda>x zs rs. Apply(f(x), rs))" 31 32definition 33 term_size :: "i => i" where 34 "term_size(t) == term_rec(t, \<lambda>x zs rs. succ(list_add(rs)))" 35 36definition 37 reflect :: "i => i" where 38 "reflect(t) == term_rec(t, \<lambda>x zs rs. Apply(x, rev(rs)))" 39 40definition 41 preorder :: "i => i" where 42 "preorder(t) == term_rec(t, \<lambda>x zs rs. Cons(x, flat(rs)))" 43 44definition 45 postorder :: "i => i" where 46 "postorder(t) == term_rec(t, \<lambda>x zs rs. flat(rs) @ [x])" 47 48lemma term_unfold: "term(A) = A * list(term(A))" 49 by (fast intro!: term.intros [unfolded term.con_defs] 50 elim: term.cases [unfolded term.con_defs]) 51 52lemma term_induct2: 53 "[| t \<in> term(A); 54 !!x. [| x \<in> A |] ==> P(Apply(x,Nil)); 55 !!x z zs. [| x \<in> A; z \<in> term(A); zs: list(term(A)); P(Apply(x,zs)) 56 |] ==> P(Apply(x, Cons(z,zs))) 57 |] ==> P(t)" 58 \<comment> \<open>Induction on \<^term>\<open>term(A)\<close> followed by induction on \<^term>\<open>list\<close>.\<close> 59 apply (induct_tac t) 60 apply (erule list.induct) 61 apply (auto dest: list_CollectD) 62 done 63 64lemma term_induct_eqn [consumes 1, case_names Apply]: 65 "[| t \<in> term(A); 66 !!x zs. [| x \<in> A; zs: list(term(A)); map(f,zs) = map(g,zs) |] ==> 67 f(Apply(x,zs)) = g(Apply(x,zs)) 68 |] ==> f(t) = g(t)" 69 \<comment> \<open>Induction on \<^term>\<open>term(A)\<close> to prove an equation.\<close> 70 apply (induct_tac t) 71 apply (auto dest: map_list_Collect list_CollectD) 72 done 73 74text \<open> 75 \medskip Lemmas to justify using \<^term>\<open>term\<close> in other recursive 76 type definitions. 77\<close> 78 79lemma term_mono: "A \<subseteq> B ==> term(A) \<subseteq> term(B)" 80 apply (unfold term.defs) 81 apply (rule lfp_mono) 82 apply (rule term.bnd_mono)+ 83 apply (rule univ_mono basic_monos| assumption)+ 84 done 85 86lemma term_univ: "term(univ(A)) \<subseteq> univ(A)" 87 \<comment> \<open>Easily provable by induction also\<close> 88 apply (unfold term.defs term.con_defs) 89 apply (rule lfp_lowerbound) 90 apply (rule_tac [2] A_subset_univ [THEN univ_mono]) 91 apply safe 92 apply (assumption | rule Pair_in_univ list_univ [THEN subsetD])+ 93 done 94 95lemma term_subset_univ: "A \<subseteq> univ(B) ==> term(A) \<subseteq> univ(B)" 96 apply (rule subset_trans) 97 apply (erule term_mono) 98 apply (rule term_univ) 99 done 100 101lemma term_into_univ: "[| t \<in> term(A); A \<subseteq> univ(B) |] ==> t \<in> univ(B)" 102 by (rule term_subset_univ [THEN subsetD]) 103 104text \<open> 105 \medskip \<open>term_rec\<close> -- by \<open>Vset\<close> recursion. 106\<close> 107 108lemma map_lemma: "[| l \<in> list(A); Ord(i); rank(l)<i |] 109 ==> map(\<lambda>z. (\<lambda>x \<in> Vset(i).h(x)) ` z, l) = map(h,l)" 110 \<comment> \<open>\<^term>\<open>map\<close> works correctly on the underlying list of terms.\<close> 111 apply (induct set: list) 112 apply simp 113 apply (subgoal_tac "rank (a) <i & rank (l) < i") 114 apply (simp add: rank_of_Ord) 115 apply (simp add: list.con_defs) 116 apply (blast dest: rank_rls [THEN lt_trans]) 117 done 118 119lemma term_rec [simp]: "ts \<in> list(A) ==> 120 term_rec(Apply(a,ts), d) = d(a, ts, map (\<lambda>z. term_rec(z,d), ts))" 121 \<comment> \<open>Typing premise is necessary to invoke \<open>map_lemma\<close>.\<close> 122 apply (rule term_rec_def [THEN def_Vrec, THEN trans]) 123 apply (unfold term.con_defs) 124 apply (simp add: rank_pair2 map_lemma) 125 done 126 127lemma term_rec_type: 128 assumes t: "t \<in> term(A)" 129 and a: "!!x zs r. [| x \<in> A; zs: list(term(A)); 130 r \<in> list(\<Union>t \<in> term(A). C(t)) |] 131 ==> d(x, zs, r): C(Apply(x,zs))" 132 shows "term_rec(t,d) \<in> C(t)" 133 \<comment> \<open>Slightly odd typing condition on \<open>r\<close> in the second premise!\<close> 134 using t 135 apply induct 136 apply (frule list_CollectD) 137 apply (subst term_rec) 138 apply (assumption | rule a)+ 139 apply (erule list.induct) 140 apply auto 141 done 142 143lemma def_term_rec: 144 "[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> 145 j(Apply(a,ts)) = d(a, ts, map(\<lambda>Z. j(Z), ts))" 146 apply (simp only:) 147 apply (erule term_rec) 148 done 149 150lemma term_rec_simple_type [TC]: 151 "[| t \<in> term(A); 152 !!x zs r. [| x \<in> A; zs: list(term(A)); r \<in> list(C) |] 153 ==> d(x, zs, r): C 154 |] ==> term_rec(t,d) \<in> C" 155 apply (erule term_rec_type) 156 apply (drule subset_refl [THEN UN_least, THEN list_mono, THEN subsetD]) 157 apply simp 158 done 159 160 161text \<open> 162 \medskip \<^term>\<open>term_map\<close>. 163\<close> 164 165lemma term_map [simp]: 166 "ts \<in> list(A) ==> 167 term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))" 168 by (rule term_map_def [THEN def_term_rec]) 169 170lemma term_map_type [TC]: 171 "[| t \<in> term(A); !!x. x \<in> A ==> f(x): B |] ==> term_map(f,t) \<in> term(B)" 172 apply (unfold term_map_def) 173 apply (erule term_rec_simple_type) 174 apply fast 175 done 176 177lemma term_map_type2 [TC]: 178 "t \<in> term(A) ==> term_map(f,t) \<in> term({f(u). u \<in> A})" 179 apply (erule term_map_type) 180 apply (erule RepFunI) 181 done 182 183text \<open> 184 \medskip \<^term>\<open>term_size\<close>. 185\<close> 186 187lemma term_size [simp]: 188 "ts \<in> list(A) ==> term_size(Apply(a, ts)) = succ(list_add(map(term_size, ts)))" 189 by (rule term_size_def [THEN def_term_rec]) 190 191lemma term_size_type [TC]: "t \<in> term(A) ==> term_size(t) \<in> nat" 192 by (auto simp add: term_size_def) 193 194 195text \<open> 196 \medskip \<open>reflect\<close>. 197\<close> 198 199lemma reflect [simp]: 200 "ts \<in> list(A) ==> reflect(Apply(a, ts)) = Apply(a, rev(map(reflect, ts)))" 201 by (rule reflect_def [THEN def_term_rec]) 202 203lemma reflect_type [TC]: "t \<in> term(A) ==> reflect(t) \<in> term(A)" 204 by (auto simp add: reflect_def) 205 206 207text \<open> 208 \medskip \<open>preorder\<close>. 209\<close> 210 211lemma preorder [simp]: 212 "ts \<in> list(A) ==> preorder(Apply(a, ts)) = Cons(a, flat(map(preorder, ts)))" 213 by (rule preorder_def [THEN def_term_rec]) 214 215lemma preorder_type [TC]: "t \<in> term(A) ==> preorder(t) \<in> list(A)" 216 by (simp add: preorder_def) 217 218 219text \<open> 220 \medskip \<open>postorder\<close>. 221\<close> 222 223lemma postorder [simp]: 224 "ts \<in> list(A) ==> postorder(Apply(a, ts)) = flat(map(postorder, ts)) @ [a]" 225 by (rule postorder_def [THEN def_term_rec]) 226 227lemma postorder_type [TC]: "t \<in> term(A) ==> postorder(t) \<in> list(A)" 228 by (simp add: postorder_def) 229 230 231text \<open> 232 \medskip Theorems about \<open>term_map\<close>. 233\<close> 234 235declare map_compose [simp] 236 237lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t" 238 by (induct rule: term_induct_eqn) simp 239 240lemma term_map_compose: 241 "t \<in> term(A) ==> term_map(f, term_map(g,t)) = term_map(\<lambda>u. f(g(u)), t)" 242 by (induct rule: term_induct_eqn) simp 243 244lemma term_map_reflect: 245 "t \<in> term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))" 246 by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric]) 247 248 249text \<open> 250 \medskip Theorems about \<open>term_size\<close>. 251\<close> 252 253lemma term_size_term_map: "t \<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)" 254 by (induct rule: term_induct_eqn) simp 255 256lemma term_size_reflect: "t \<in> term(A) ==> term_size(reflect(t)) = term_size(t)" 257 by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric] list_add_rev) 258 259lemma term_size_length: "t \<in> term(A) ==> term_size(t) = length(preorder(t))" 260 by (induct rule: term_induct_eqn) (simp add: length_flat) 261 262 263text \<open> 264 \medskip Theorems about \<open>reflect\<close>. 265\<close> 266 267lemma reflect_reflect_ident: "t \<in> term(A) ==> reflect(reflect(t)) = t" 268 by (induct rule: term_induct_eqn) (simp add: rev_map_distrib) 269 270 271text \<open> 272 \medskip Theorems about preorder. 273\<close> 274 275lemma preorder_term_map: 276 "t \<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))" 277 by (induct rule: term_induct_eqn) (simp add: map_flat) 278 279lemma preorder_reflect_eq_rev_postorder: 280 "t \<in> term(A) ==> preorder(reflect(t)) = rev(postorder(t))" 281 by (induct rule: term_induct_eqn) 282 (simp add: rev_app_distrib rev_flat rev_map_distrib [symmetric]) 283 284end 285