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