1 (* Title: ZF/ex/Term.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Datatype definition of terms over an alphabet. |
|
7 Illustrates the list functor (essentially the same type as in Trees & Forests) |
|
8 *) |
|
9 |
|
10 AddTCs [term.Apply_I]; |
|
11 |
|
12 Goal "term(A) = A * list(term(A))"; |
|
13 let open term; val rew = rewrite_rule con_defs in |
|
14 by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) |
|
15 end; |
|
16 qed "term_unfold"; |
|
17 |
|
18 (*Induction on term(A) followed by induction on List *) |
|
19 val major::prems = Goal |
|
20 "[| t \\<in> term(A); \ |
|
21 \ !!x. [| x \\<in> A |] ==> P(Apply(x,Nil)); \ |
|
22 \ !!x z zs. [| x \\<in> A; z \\<in> term(A); zs: list(term(A)); P(Apply(x,zs)) \ |
|
23 \ |] ==> P(Apply(x, Cons(z,zs))) \ |
|
24 \ |] ==> P(t)"; |
|
25 by (rtac (major RS term.induct) 1); |
|
26 by (etac list.induct 1); |
|
27 by (etac CollectE 2); |
|
28 by (REPEAT (ares_tac (prems@[list_CollectD]) 1)); |
|
29 qed "term_induct2"; |
|
30 |
|
31 (*Induction on term(A) to prove an equation*) |
|
32 val major::prems = Goal |
|
33 "[| t \\<in> term(A); \ |
|
34 \ !!x zs. [| x \\<in> A; zs: list(term(A)); map(f,zs) = map(g,zs) |] ==> \ |
|
35 \ f(Apply(x,zs)) = g(Apply(x,zs)) \ |
|
36 \ |] ==> f(t)=g(t)"; |
|
37 by (rtac (major RS term.induct) 1); |
|
38 by (resolve_tac prems 1); |
|
39 by (REPEAT (eresolve_tac [asm_rl, map_list_Collect, list_CollectD] 1)); |
|
40 qed "term_induct_eqn"; |
|
41 |
|
42 (** Lemmas to justify using "term" in other recursive type definitions **) |
|
43 |
|
44 Goalw term.defs "A \\<subseteq> B ==> term(A) \\<subseteq> term(B)"; |
|
45 by (rtac lfp_mono 1); |
|
46 by (REPEAT (rtac term.bnd_mono 1)); |
|
47 by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
|
48 qed "term_mono"; |
|
49 |
|
50 (*Easily provable by induction also*) |
|
51 Goalw (term.defs@term.con_defs) "term(univ(A)) \\<subseteq> univ(A)"; |
|
52 by (rtac lfp_lowerbound 1); |
|
53 by (rtac (A_subset_univ RS univ_mono) 2); |
|
54 by Safe_tac; |
|
55 by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1)); |
|
56 qed "term_univ"; |
|
57 |
|
58 val term_subset_univ = |
|
59 term_mono RS (term_univ RSN (2,subset_trans)) |> standard; |
|
60 |
|
61 Goal "[| t \\<in> term(A); A \\<subseteq> univ(B) |] ==> t \\<in> univ(B)"; |
|
62 by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1)); |
|
63 qed "term_into_univ"; |
|
64 |
|
65 |
|
66 (*** term_rec -- by Vset recursion ***) |
|
67 |
|
68 (*Lemma: map works correctly on the underlying list of terms*) |
|
69 Goal "[| l \\<in> list(A); Ord(i) |] ==> \ |
|
70 \ rank(l)<i --> map(%z. (\\<lambda>x \\<in> Vset(i).h(x)) ` z, l) = map(h,l)"; |
|
71 by (etac list.induct 1); |
|
72 by (Simp_tac 1); |
|
73 by (rtac impI 1); |
|
74 by (subgoal_tac "rank(a)<i & rank(l) < i" 1); |
|
75 by (asm_simp_tac (simpset() addsimps [rank_of_Ord]) 1); |
|
76 by (full_simp_tac (simpset() addsimps list.con_defs) 1); |
|
77 by (blast_tac (claset() addDs (rank_rls RL [lt_trans])) 1); |
|
78 qed "map_lemma"; |
|
79 |
|
80 (*Typing premise is necessary to invoke map_lemma*) |
|
81 Goal "ts \\<in> list(A) ==> \ |
|
82 \ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))"; |
|
83 by (rtac (term_rec_def RS def_Vrec RS trans) 1); |
|
84 by (rewrite_goals_tac term.con_defs); |
|
85 by (asm_simp_tac (simpset() addsimps [rank_pair2, map_lemma]) 1);; |
|
86 qed "term_rec"; |
|
87 |
|
88 (*Slightly odd typing condition on r in the second premise!*) |
|
89 val major::prems = Goal |
|
90 "[| t \\<in> term(A); \ |
|
91 \ !!x zs r. [| x \\<in> A; zs: list(term(A)); \ |
|
92 \ r \\<in> list(\\<Union>t \\<in> term(A). C(t)) |] \ |
|
93 \ ==> d(x, zs, r): C(Apply(x,zs)) \ |
|
94 \ |] ==> term_rec(t,d) \\<in> C(t)"; |
|
95 by (rtac (major RS term.induct) 1); |
|
96 by (ftac list_CollectD 1); |
|
97 by (stac term_rec 1); |
|
98 by (REPEAT (ares_tac prems 1)); |
|
99 by (etac list.induct 1); |
|
100 by (ALLGOALS (asm_simp_tac (simpset() addsimps [term_rec]))); |
|
101 by Auto_tac; |
|
102 qed "term_rec_type"; |
|
103 |
|
104 val [rew,tslist] = Goal |
|
105 "[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \ |
|
106 \ j(Apply(a,ts)) = d(a, ts, map(%Z. j(Z), ts))"; |
|
107 by (rewtac rew); |
|
108 by (rtac (tslist RS term_rec) 1); |
|
109 qed "def_term_rec"; |
|
110 |
|
111 val prems = Goal |
|
112 "[| t \\<in> term(A); \ |
|
113 \ !!x zs r. [| x \\<in> A; zs: list(term(A)); r \\<in> list(C) |] \ |
|
114 \ ==> d(x, zs, r): C \ |
|
115 \ |] ==> term_rec(t,d) \\<in> C"; |
|
116 by (REPEAT (ares_tac (term_rec_type::prems) 1)); |
|
117 by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1); |
|
118 qed "term_rec_simple_type"; |
|
119 |
|
120 AddTCs [term_rec_simple_type]; |
|
121 |
|
122 (** term_map **) |
|
123 |
|
124 bind_thm ("term_map", term_map_def RS def_term_rec); |
|
125 |
|
126 val prems = Goalw [term_map_def] |
|
127 "[| t \\<in> term(A); !!x. x \\<in> A ==> f(x): B |] ==> term_map(f,t) \\<in> term(B)"; |
|
128 by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1)); |
|
129 qed "term_map_type"; |
|
130 |
|
131 Goal "t \\<in> term(A) ==> term_map(f,t) \\<in> term({f(u). u \\<in> A})"; |
|
132 by (etac term_map_type 1); |
|
133 by (etac RepFunI 1); |
|
134 qed "term_map_type2"; |
|
135 |
|
136 |
|
137 (** term_size **) |
|
138 |
|
139 bind_thm ("term_size", term_size_def RS def_term_rec); |
|
140 |
|
141 Goalw [term_size_def] "t \\<in> term(A) ==> term_size(t) \\<in> nat"; |
|
142 by Auto_tac; |
|
143 qed "term_size_type"; |
|
144 |
|
145 |
|
146 (** reflect **) |
|
147 |
|
148 bind_thm ("reflect", reflect_def RS def_term_rec); |
|
149 |
|
150 Goalw [reflect_def] "t \\<in> term(A) ==> reflect(t) \\<in> term(A)"; |
|
151 by Auto_tac; |
|
152 qed "reflect_type"; |
|
153 |
|
154 (** preorder **) |
|
155 |
|
156 bind_thm ("preorder", preorder_def RS def_term_rec); |
|
157 |
|
158 Goalw [preorder_def] "t \\<in> term(A) ==> preorder(t) \\<in> list(A)"; |
|
159 by Auto_tac; |
|
160 qed "preorder_type"; |
|
161 |
|
162 (** postorder **) |
|
163 |
|
164 bind_thm ("postorder", postorder_def RS def_term_rec); |
|
165 |
|
166 Goalw [postorder_def] "t \\<in> term(A) ==> postorder(t) \\<in> list(A)"; |
|
167 by Auto_tac; |
|
168 qed "postorder_type"; |
|
169 |
|
170 |
|
171 (** Term simplification **) |
|
172 |
|
173 AddTCs [term_map_type, term_map_type2, term_size_type, |
|
174 reflect_type, preorder_type, postorder_type]; |
|
175 |
|
176 (*map_type2 and term_map_type2 instantiate variables*) |
|
177 Addsimps [term_rec, term_map, term_size, reflect, preorder, postorder]; |
|
178 |
|
179 |
|
180 (** theorems about term_map **) |
|
181 |
|
182 Addsimps [thm "List.map_compose"]; (*there is also TF.map_compose*) |
|
183 |
|
184 Goal "t \\<in> term(A) ==> term_map(%u. u, t) = t"; |
|
185 by (etac term_induct_eqn 1); |
|
186 by (Asm_simp_tac 1); |
|
187 qed "term_map_ident"; |
|
188 |
|
189 Goal "t \\<in> term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)"; |
|
190 by (etac term_induct_eqn 1); |
|
191 by (Asm_simp_tac 1); |
|
192 qed "term_map_compose"; |
|
193 |
|
194 Goal "t \\<in> term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))"; |
|
195 by (etac term_induct_eqn 1); |
|
196 by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym]) 1); |
|
197 qed "term_map_reflect"; |
|
198 |
|
199 |
|
200 (** theorems about term_size **) |
|
201 |
|
202 Goal "t \\<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)"; |
|
203 by (etac term_induct_eqn 1); |
|
204 by (Asm_simp_tac 1); |
|
205 qed "term_size_term_map"; |
|
206 |
|
207 Goal "t \\<in> term(A) ==> term_size(reflect(t)) = term_size(t)"; |
|
208 by (etac term_induct_eqn 1); |
|
209 by (asm_simp_tac(simpset() addsimps [rev_map_distrib RS sym, list_add_rev]) 1); |
|
210 qed "term_size_reflect"; |
|
211 |
|
212 Goal "t \\<in> term(A) ==> term_size(t) = length(preorder(t))"; |
|
213 by (etac term_induct_eqn 1); |
|
214 by (asm_simp_tac (simpset() addsimps [length_flat]) 1); |
|
215 qed "term_size_length"; |
|
216 |
|
217 |
|
218 (** theorems about reflect **) |
|
219 |
|
220 Goal "t \\<in> term(A) ==> reflect(reflect(t)) = t"; |
|
221 by (etac term_induct_eqn 1); |
|
222 by (asm_simp_tac (simpset() addsimps [rev_map_distrib]) 1); |
|
223 qed "reflect_reflect_ident"; |
|
224 |
|
225 |
|
226 (** theorems about preorder **) |
|
227 |
|
228 Goal "t \\<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))"; |
|
229 by (etac term_induct_eqn 1); |
|
230 by (asm_simp_tac (simpset() addsimps [map_flat]) 1); |
|
231 qed "preorder_term_map"; |
|
232 |
|
233 Goal "t \\<in> term(A) ==> preorder(reflect(t)) = rev(postorder(t))"; |
|
234 by (etac term_induct_eqn 1); |
|
235 by (asm_simp_tac(simpset() addsimps [rev_app_distrib, rev_flat, |
|
236 rev_map_distrib RS sym]) 1); |
|
237 qed "preorder_reflect_eq_rev_postorder"; |
|
238 |
|
239 |
|
240 writeln"Reached end of file."; |
|