12201
|
1 |
(* Title: ZF/Induct/Term.thy
|
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
3 |
Copyright 1994 University of Cambridge
|
|
4 |
*)
|
|
5 |
|
60770
|
6 |
section \<open>Terms over an alphabet\<close>
|
12201
|
7 |
|
16417
|
8 |
theory Term imports Main begin
|
12201
|
9 |
|
60770
|
10 |
text \<open>
|
61798
|
11 |
Illustrates the list functor (essentially the same type as in \<open>Trees_Forest\<close>).
|
60770
|
12 |
\<close>
|
12201
|
13 |
|
|
14 |
consts
|
|
15 |
"term" :: "i => i"
|
|
16 |
|
|
17 |
datatype "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 |
|
|
21 |
declare Apply [TC]
|
|
22 |
|
24893
|
23 |
definition
|
|
24 |
term_rec :: "[i, [i, i, i] => i] => i" where
|
12201
|
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 |
|
24893
|
28 |
definition
|
|
29 |
term_map :: "[i => i, i] => i" where
|
12201
|
30 |
"term_map(f,t) == term_rec(t, \<lambda>x zs rs. Apply(f(x), rs))"
|
|
31 |
|
24893
|
32 |
definition
|
|
33 |
term_size :: "i => i" where
|
12201
|
34 |
"term_size(t) == term_rec(t, \<lambda>x zs rs. succ(list_add(rs)))"
|
|
35 |
|
24893
|
36 |
definition
|
|
37 |
reflect :: "i => i" where
|
12201
|
38 |
"reflect(t) == term_rec(t, \<lambda>x zs rs. Apply(x, rev(rs)))"
|
|
39 |
|
24893
|
40 |
definition
|
|
41 |
preorder :: "i => i" where
|
12201
|
42 |
"preorder(t) == term_rec(t, \<lambda>x zs rs. Cons(x, flat(rs)))"
|
|
43 |
|
24893
|
44 |
definition
|
|
45 |
postorder :: "i => i" where
|
12201
|
46 |
"postorder(t) == term_rec(t, \<lambda>x zs rs. flat(rs) @ [x])"
|
|
47 |
|
|
48 |
lemma 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 |
|
|
52 |
lemma 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)"
|
61798
|
58 |
\<comment> \<open>Induction on @{term "term(A)"} followed by induction on @{term list}.\<close>
|
12201
|
59 |
apply (induct_tac t)
|
|
60 |
apply (erule list.induct)
|
|
61 |
apply (auto dest: list_CollectD)
|
|
62 |
done
|
|
63 |
|
18415
|
64 |
lemma term_induct_eqn [consumes 1, case_names Apply]:
|
12201
|
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)"
|
61798
|
69 |
\<comment> \<open>Induction on @{term "term(A)"} to prove an equation.\<close>
|
12201
|
70 |
apply (induct_tac t)
|
|
71 |
apply (auto dest: map_list_Collect list_CollectD)
|
|
72 |
done
|
|
73 |
|
60770
|
74 |
text \<open>
|
12201
|
75 |
\medskip Lemmas to justify using @{term "term"} in other recursive
|
|
76 |
type definitions.
|
60770
|
77 |
\<close>
|
12201
|
78 |
|
|
79 |
lemma 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 |
|
|
86 |
lemma term_univ: "term(univ(A)) \<subseteq> univ(A)"
|
61798
|
87 |
\<comment> \<open>Easily provable by induction also\<close>
|
12201
|
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 |
|
|
95 |
lemma 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 |
|
|
101 |
lemma term_into_univ: "[| t \<in> term(A); A \<subseteq> univ(B) |] ==> t \<in> univ(B)"
|
|
102 |
by (rule term_subset_univ [THEN subsetD])
|
|
103 |
|
60770
|
104 |
text \<open>
|
61798
|
105 |
\medskip \<open>term_rec\<close> -- by \<open>Vset\<close> recursion.
|
60770
|
106 |
\<close>
|
12201
|
107 |
|
|
108 |
lemma 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)"
|
61798
|
110 |
\<comment> \<open>@{term map} works correctly on the underlying list of terms.\<close>
|
12201
|
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 |
|
|
119 |
lemma 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))"
|
61798
|
121 |
\<comment> \<open>Typing premise is necessary to invoke \<open>map_lemma\<close>.\<close>
|
12201
|
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 |
|
|
127 |
lemma term_rec_type:
|
18415
|
128 |
assumes t: "t \<in> term(A)"
|
|
129 |
and a: "!!x zs r. [| x \<in> A; zs: list(term(A));
|
12201
|
130 |
r \<in> list(\<Union>t \<in> term(A). C(t)) |]
|
|
131 |
==> d(x, zs, r): C(Apply(x,zs))"
|
18415
|
132 |
shows "term_rec(t,d) \<in> C(t)"
|
61798
|
133 |
\<comment> \<open>Slightly odd typing condition on \<open>r\<close> in the second premise!\<close>
|
18415
|
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)
|
46900
|
140 |
apply auto
|
18415
|
141 |
done
|
12201
|
142 |
|
|
143 |
lemma 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 |
|
|
150 |
lemma 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 |
|
60770
|
161 |
text \<open>
|
12201
|
162 |
\medskip @{term term_map}.
|
60770
|
163 |
\<close>
|
12201
|
164 |
|
|
165 |
lemma term_map [simp]:
|
12610
|
166 |
"ts \<in> list(A) ==>
|
|
167 |
term_map(f, Apply(a, ts)) = Apply(f(a), map(term_map(f), ts))"
|
12201
|
168 |
by (rule term_map_def [THEN def_term_rec])
|
|
169 |
|
|
170 |
lemma 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 |
|
|
177 |
lemma 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 |
|
60770
|
183 |
text \<open>
|
12201
|
184 |
\medskip @{term term_size}.
|
60770
|
185 |
\<close>
|
12201
|
186 |
|
|
187 |
lemma term_size [simp]:
|
12216
|
188 |
"ts \<in> list(A) ==> term_size(Apply(a, ts)) = succ(list_add(map(term_size, ts)))"
|
12201
|
189 |
by (rule term_size_def [THEN def_term_rec])
|
|
190 |
|
|
191 |
lemma term_size_type [TC]: "t \<in> term(A) ==> term_size(t) \<in> nat"
|
|
192 |
by (auto simp add: term_size_def)
|
|
193 |
|
|
194 |
|
60770
|
195 |
text \<open>
|
61798
|
196 |
\medskip \<open>reflect\<close>.
|
60770
|
197 |
\<close>
|
12201
|
198 |
|
|
199 |
lemma reflect [simp]:
|
12216
|
200 |
"ts \<in> list(A) ==> reflect(Apply(a, ts)) = Apply(a, rev(map(reflect, ts)))"
|
12201
|
201 |
by (rule reflect_def [THEN def_term_rec])
|
|
202 |
|
|
203 |
lemma reflect_type [TC]: "t \<in> term(A) ==> reflect(t) \<in> term(A)"
|
|
204 |
by (auto simp add: reflect_def)
|
|
205 |
|
|
206 |
|
60770
|
207 |
text \<open>
|
61798
|
208 |
\medskip \<open>preorder\<close>.
|
60770
|
209 |
\<close>
|
12201
|
210 |
|
|
211 |
lemma preorder [simp]:
|
12216
|
212 |
"ts \<in> list(A) ==> preorder(Apply(a, ts)) = Cons(a, flat(map(preorder, ts)))"
|
12201
|
213 |
by (rule preorder_def [THEN def_term_rec])
|
|
214 |
|
|
215 |
lemma preorder_type [TC]: "t \<in> term(A) ==> preorder(t) \<in> list(A)"
|
|
216 |
by (simp add: preorder_def)
|
|
217 |
|
|
218 |
|
60770
|
219 |
text \<open>
|
61798
|
220 |
\medskip \<open>postorder\<close>.
|
60770
|
221 |
\<close>
|
12201
|
222 |
|
|
223 |
lemma postorder [simp]:
|
12216
|
224 |
"ts \<in> list(A) ==> postorder(Apply(a, ts)) = flat(map(postorder, ts)) @ [a]"
|
12201
|
225 |
by (rule postorder_def [THEN def_term_rec])
|
|
226 |
|
|
227 |
lemma postorder_type [TC]: "t \<in> term(A) ==> postorder(t) \<in> list(A)"
|
|
228 |
by (simp add: postorder_def)
|
|
229 |
|
|
230 |
|
60770
|
231 |
text \<open>
|
61798
|
232 |
\medskip Theorems about \<open>term_map\<close>.
|
60770
|
233 |
\<close>
|
12201
|
234 |
|
26059
|
235 |
declare map_compose [simp]
|
12201
|
236 |
|
|
237 |
lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t"
|
18415
|
238 |
by (induct rule: term_induct_eqn) simp
|
12201
|
239 |
|
|
240 |
lemma term_map_compose:
|
|
241 |
"t \<in> term(A) ==> term_map(f, term_map(g,t)) = term_map(\<lambda>u. f(g(u)), t)"
|
18415
|
242 |
by (induct rule: term_induct_eqn) simp
|
12201
|
243 |
|
|
244 |
lemma term_map_reflect:
|
|
245 |
"t \<in> term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"
|
18415
|
246 |
by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric])
|
12201
|
247 |
|
|
248 |
|
60770
|
249 |
text \<open>
|
61798
|
250 |
\medskip Theorems about \<open>term_size\<close>.
|
60770
|
251 |
\<close>
|
12201
|
252 |
|
|
253 |
lemma term_size_term_map: "t \<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)"
|
18415
|
254 |
by (induct rule: term_induct_eqn) simp
|
12201
|
255 |
|
|
256 |
lemma term_size_reflect: "t \<in> term(A) ==> term_size(reflect(t)) = term_size(t)"
|
18415
|
257 |
by (induct rule: term_induct_eqn) (simp add: rev_map_distrib [symmetric] list_add_rev)
|
12201
|
258 |
|
|
259 |
lemma term_size_length: "t \<in> term(A) ==> term_size(t) = length(preorder(t))"
|
18415
|
260 |
by (induct rule: term_induct_eqn) (simp add: length_flat)
|
12201
|
261 |
|
|
262 |
|
60770
|
263 |
text \<open>
|
61798
|
264 |
\medskip Theorems about \<open>reflect\<close>.
|
60770
|
265 |
\<close>
|
12201
|
266 |
|
|
267 |
lemma reflect_reflect_ident: "t \<in> term(A) ==> reflect(reflect(t)) = t"
|
18415
|
268 |
by (induct rule: term_induct_eqn) (simp add: rev_map_distrib)
|
12201
|
269 |
|
|
270 |
|
60770
|
271 |
text \<open>
|
12201
|
272 |
\medskip Theorems about preorder.
|
60770
|
273 |
\<close>
|
12201
|
274 |
|
12610
|
275 |
lemma preorder_term_map:
|
|
276 |
"t \<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"
|
18415
|
277 |
by (induct rule: term_induct_eqn) (simp add: map_flat)
|
12201
|
278 |
|
|
279 |
lemma preorder_reflect_eq_rev_postorder:
|
|
280 |
"t \<in> term(A) ==> preorder(reflect(t)) = rev(postorder(t))"
|
18415
|
281 |
by (induct rule: term_induct_eqn)
|
|
282 |
(simp add: rev_app_distrib rev_flat rev_map_distrib [symmetric])
|
12201
|
283 |
|
|
284 |
end
|