|
1 (* Title: Substitutions/uterm.ML |
|
2 Author: Martin Coen, Cambridge University Computer Laboratory |
|
3 Copyright 1993 University of Cambridge |
|
4 |
|
5 For uterm.thy. |
|
6 *) |
|
7 |
|
8 open UTerm; |
|
9 |
|
10 (** the uterm functional **) |
|
11 |
|
12 goal UTerm.thy "mono(%Z. A <+> A <+> Z <*> Z)"; |
|
13 by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono] 1)); |
|
14 val UTerm_fun_mono = result(); |
|
15 |
|
16 val UTerm_unfold = UTerm_fun_mono RS (UTerm_def RS def_lfp_Tarski); |
|
17 |
|
18 (*This justifies using UTerm in other recursive type definitions*) |
|
19 val prems = goalw UTerm.thy [UTerm_def] "[| A<=B |] ==> UTerm(A) <= UTerm(B)"; |
|
20 by (REPEAT (ares_tac (prems@[monoI, subset_refl, lfp_mono, |
|
21 usum_mono, uprod_mono]) 1)); |
|
22 val UTerm_mono = result(); |
|
23 |
|
24 (** Type checking rules -- UTerm creates well-founded sets **) |
|
25 |
|
26 val prems = goalw UTerm.thy [UTerm_def] "UTerm(Sexp) <= Sexp"; |
|
27 by (rtac lfp_lowerbound 1); |
|
28 by (fast_tac (univ_cs addIs [Sexp_In0I,Sexp_In1I,Sexp_SconsI]) 1); |
|
29 val UTerm_Sexp = result(); |
|
30 |
|
31 (* A <= Sexp ==> UTerm(A) <= Sexp *) |
|
32 val UTerm_subset_Sexp = standard |
|
33 (UTerm_mono RS (UTerm_Sexp RSN (2,subset_trans))); |
|
34 |
|
35 (** Induction **) |
|
36 |
|
37 (*Induction for the set UTerm(A) *) |
|
38 val major::prems = goalw UTerm.thy [VAR_def,CONST_def,COMB_def] |
|
39 "[| M: UTerm(A); !!M.M : A ==> P(VAR(M)); !!M.M : A ==> P(CONST(M)); \ |
|
40 \ !!M N. [| M: UTerm(A); N: UTerm(A); P(M); P(N) |] ==> P(COMB(M,N)) |] \ |
|
41 \ ==> P(M)"; |
|
42 by (rtac (major RS (UTerm_def RS def_induct)) 1); |
|
43 by (rtac UTerm_fun_mono 1); |
|
44 by (fast_tac (set_cs addIs prems addEs [usumE,uprodE]) 1); |
|
45 val UTerm_induct = result(); |
|
46 |
|
47 (*Induction for the type 'a uterm *) |
|
48 val prems = goalw UTerm.thy [Var_def,Const_def,Comb_def] |
|
49 "[| !!x.P(Var(x)); !!x.P(Const(x)); \ |
|
50 \ !!u v. [| P(u); P(v) |] ==> P(Comb(u,v)) |] ==> P(t)"; |
|
51 by (rtac (Rep_UTerm_inverse RS subst) 1); (*types force good instantiation*) |
|
52 by (rtac (Rep_UTerm RS UTerm_induct) 1); |
|
53 by (REPEAT (ares_tac prems 1 |
|
54 ORELSE eresolve_tac [rangeE, ssubst, Abs_UTerm_inverse RS subst] 1)); |
|
55 val uterm_induct = result(); |
|
56 |
|
57 (*Perform induction on xs. *) |
|
58 fun uterm_ind_tac a M = |
|
59 EVERY [res_inst_tac [("t",a)] uterm_induct M, |
|
60 rename_last_tac a ["1"] (M+1)]; |
|
61 |
|
62 (** Introduction rules for UTerm constructors **) |
|
63 |
|
64 (* c : A <+> A <+> UTerm(A) <*> UTerm(A) ==> c : UTerm(A) *) |
|
65 val UTermI = UTerm_unfold RS equalityD2 RS subsetD; |
|
66 |
|
67 (* Nil is a UTerm -- this also justifies the type definition*) |
|
68 val prems = goalw UTerm.thy [VAR_def] "v:A ==> VAR(v) : UTerm(A)"; |
|
69 by (REPEAT (resolve_tac ([singletonI, UTermI, usum_In0I]@prems) 1)); |
|
70 val VAR_I = result(); |
|
71 |
|
72 val prems = goalw UTerm.thy [CONST_def] "c:A ==> CONST(c) : UTerm(A)"; |
|
73 by (REPEAT (resolve_tac ([singletonI, UTermI, usum_In0I, usum_In1I]@prems) 1)); |
|
74 val CONST_I = result(); |
|
75 |
|
76 val prems = goalw UTerm.thy [COMB_def] |
|
77 "[| M:UTerm(A); N:UTerm(A) |] ==> COMB(M,N) : UTerm(A)"; |
|
78 by (REPEAT (resolve_tac (prems@[UTermI, uprodI, usum_In1I]) 1)); |
|
79 val COMB_I = result(); |
|
80 |
|
81 (*** Isomorphisms ***) |
|
82 |
|
83 goal UTerm.thy "inj(Rep_UTerm)"; |
|
84 by (rtac inj_inverseI 1); |
|
85 by (rtac Rep_UTerm_inverse 1); |
|
86 val inj_Rep_UTerm = result(); |
|
87 |
|
88 goal UTerm.thy "inj_onto(Abs_UTerm,UTerm(range(Leaf)))"; |
|
89 by (rtac inj_onto_inverseI 1); |
|
90 by (etac Abs_UTerm_inverse 1); |
|
91 val inj_onto_Abs_UTerm = result(); |
|
92 |
|
93 (** Distinctness of constructors **) |
|
94 |
|
95 goalw UTerm.thy [CONST_def,COMB_def] "~ CONST(c) = COMB(u,v)"; |
|
96 by (rtac notI 1); |
|
97 by (etac (In1_inject RS (In0_not_In1 RS notE)) 1); |
|
98 val CONST_not_COMB = result(); |
|
99 val COMB_not_CONST = standard (CONST_not_COMB RS not_sym); |
|
100 val CONST_neq_COMB = standard (CONST_not_COMB RS notE); |
|
101 val COMB_neq_CONST = sym RS CONST_neq_COMB; |
|
102 |
|
103 goalw UTerm.thy [COMB_def,VAR_def] "~ COMB(u,v) = VAR(x)"; |
|
104 by (rtac In1_not_In0 1); |
|
105 val COMB_not_VAR = result(); |
|
106 val VAR_not_COMB = standard (COMB_not_VAR RS not_sym); |
|
107 val COMB_neq_VAR = standard (COMB_not_VAR RS notE); |
|
108 val VAR_neq_COMB = sym RS COMB_neq_VAR; |
|
109 |
|
110 goalw UTerm.thy [VAR_def,CONST_def] "~ VAR(x) = CONST(c)"; |
|
111 by (rtac In0_not_In1 1); |
|
112 val VAR_not_CONST = result(); |
|
113 val CONST_not_VAR = standard (VAR_not_CONST RS not_sym); |
|
114 val VAR_neq_CONST = standard (VAR_not_CONST RS notE); |
|
115 val CONST_neq_VAR = sym RS VAR_neq_CONST; |
|
116 |
|
117 |
|
118 goalw UTerm.thy [Const_def,Comb_def] "~ Const(c) = Comb(u,v)"; |
|
119 by (rtac (CONST_not_COMB RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1); |
|
120 by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1)); |
|
121 val Const_not_Comb = result(); |
|
122 val Comb_not_Const = standard (Const_not_Comb RS not_sym); |
|
123 val Const_neq_Comb = standard (Const_not_Comb RS notE); |
|
124 val Comb_neq_Const = sym RS Const_neq_Comb; |
|
125 |
|
126 goalw UTerm.thy [Comb_def,Var_def] "~ Comb(u,v) = Var(x)"; |
|
127 by (rtac (COMB_not_VAR RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1); |
|
128 by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1)); |
|
129 val Comb_not_Var = result(); |
|
130 val Var_not_Comb = standard (Comb_not_Var RS not_sym); |
|
131 val Comb_neq_Var = standard (Comb_not_Var RS notE); |
|
132 val Var_neq_Comb = sym RS Comb_neq_Var; |
|
133 |
|
134 goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)"; |
|
135 by (rtac (VAR_not_CONST RS (inj_onto_Abs_UTerm RS inj_onto_contraD)) 1); |
|
136 by (REPEAT (resolve_tac [rangeI, VAR_I, CONST_I, COMB_I, Rep_UTerm] 1)); |
|
137 val Var_not_Const = result(); |
|
138 val Const_not_Var = standard (Var_not_Const RS not_sym); |
|
139 val Var_neq_Const = standard (Var_not_Const RS notE); |
|
140 val Const_neq_Var = sym RS Var_neq_Const; |
|
141 |
|
142 |
|
143 (** Injectiveness of CONST and Const **) |
|
144 |
|
145 val inject_cs = HOL_cs addSEs [Scons_inject] |
|
146 addSDs [In0_inject,In1_inject]; |
|
147 |
|
148 goalw UTerm.thy [VAR_def] "(VAR(M)=VAR(N)) = (M=N)"; |
|
149 by (fast_tac inject_cs 1); |
|
150 val VAR_VAR_eq = result(); |
|
151 |
|
152 goalw UTerm.thy [CONST_def] "(CONST(M)=CONST(N)) = (M=N)"; |
|
153 by (fast_tac inject_cs 1); |
|
154 val CONST_CONST_eq = result(); |
|
155 |
|
156 goalw UTerm.thy [COMB_def] "(COMB(K,L)=COMB(M,N)) = (K=M & L=N)"; |
|
157 by (fast_tac inject_cs 1); |
|
158 val COMB_COMB_eq = result(); |
|
159 |
|
160 val VAR_inject = standard (VAR_VAR_eq RS iffD1); |
|
161 val CONST_inject = standard (CONST_CONST_eq RS iffD1); |
|
162 val COMB_inject = standard (COMB_COMB_eq RS iffD1 RS conjE); |
|
163 |
|
164 |
|
165 (*For reasoning about abstract uterm constructors*) |
|
166 val UTerm_cs = set_cs addIs [Rep_UTerm, VAR_I, CONST_I, COMB_I] |
|
167 addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST, |
|
168 COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR, |
|
169 COMB_inject] |
|
170 addSDs [VAR_inject,CONST_inject, |
|
171 inj_onto_Abs_UTerm RS inj_ontoD, |
|
172 inj_Rep_UTerm RS injD, Leaf_inject]; |
|
173 |
|
174 goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)"; |
|
175 by (fast_tac UTerm_cs 1); |
|
176 val Var_Var_eq = result(); |
|
177 val Var_inject = standard (Var_Var_eq RS iffD1); |
|
178 |
|
179 goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)"; |
|
180 by (fast_tac UTerm_cs 1); |
|
181 val Const_Const_eq = result(); |
|
182 val Const_inject = standard (Const_Const_eq RS iffD1); |
|
183 |
|
184 goalw UTerm.thy [Comb_def] "(Comb(u,v)=Comb(x,y)) = (u=x & v=y)"; |
|
185 by (fast_tac UTerm_cs 1); |
|
186 val Comb_Comb_eq = result(); |
|
187 val Comb_inject = standard (Comb_Comb_eq RS iffD1 RS conjE); |
|
188 |
|
189 val [major] = goal UTerm.thy "VAR(M): UTerm(A) ==> M : A"; |
|
190 by (rtac (major RS setup_induction) 1); |
|
191 by (etac UTerm_induct 1); |
|
192 by (ALLGOALS (fast_tac UTerm_cs)); |
|
193 val VAR_D = result(); |
|
194 |
|
195 val [major] = goal UTerm.thy "CONST(M): UTerm(A) ==> M : A"; |
|
196 by (rtac (major RS setup_induction) 1); |
|
197 by (etac UTerm_induct 1); |
|
198 by (ALLGOALS (fast_tac UTerm_cs)); |
|
199 val CONST_D = result(); |
|
200 |
|
201 val [major] = goal UTerm.thy |
|
202 "COMB(M,N): UTerm(A) ==> M: UTerm(A) & N: UTerm(A)"; |
|
203 by (rtac (major RS setup_induction) 1); |
|
204 by (etac UTerm_induct 1); |
|
205 by (ALLGOALS (fast_tac UTerm_cs)); |
|
206 val COMB_D = result(); |
|
207 |
|
208 (*Basic ss with constructors and their freeness*) |
|
209 val uterm_free_simps = [Const_not_Comb,Comb_not_Var,Var_not_Const, |
|
210 Comb_not_Const,Var_not_Comb,Const_not_Var, |
|
211 Var_Var_eq,Const_Const_eq,Comb_Comb_eq, |
|
212 CONST_not_COMB,COMB_not_VAR,VAR_not_CONST, |
|
213 COMB_not_CONST,VAR_not_COMB,CONST_not_VAR, |
|
214 VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq, |
|
215 VAR_I, CONST_I, COMB_I]; |
|
216 val uterm_free_ss = HOL_ss addsimps uterm_free_simps; |
|
217 |
|
218 goal UTerm.thy "!u. ~(t=Comb(t,u))"; |
|
219 by (uterm_ind_tac "t" 1); |
|
220 by (rtac (Var_not_Comb RS allI) 1); |
|
221 by (rtac (Const_not_Comb RS allI) 1); |
|
222 by (asm_simp_tac uterm_free_ss 1); |
|
223 val t_not_Comb_t = result(); |
|
224 |
|
225 goal UTerm.thy "!t. ~(u=Comb(t,u))"; |
|
226 by (uterm_ind_tac "u" 1); |
|
227 by (rtac (Var_not_Comb RS allI) 1); |
|
228 by (rtac (Const_not_Comb RS allI) 1); |
|
229 by (asm_simp_tac uterm_free_ss 1); |
|
230 val u_not_Comb_u = result(); |
|
231 |
|
232 |
|
233 (*** UTerm_rec -- by wf recursion on pred_Sexp ***) |
|
234 |
|
235 val UTerm_rec_unfold = |
|
236 wf_pred_Sexp RS wf_trancl RS (UTerm_rec_def RS def_wfrec); |
|
237 |
|
238 (** conversion rules **) |
|
239 |
|
240 goalw UTerm.thy [VAR_def] "UTerm_rec(VAR(x),b,c,d) = b(x)"; |
|
241 by (rtac (UTerm_rec_unfold RS trans) 1); |
|
242 by (rtac Case_In0 1); |
|
243 val UTerm_rec_VAR = result(); |
|
244 |
|
245 goalw UTerm.thy [CONST_def] "UTerm_rec(CONST(x),b,c,d) = c(x)"; |
|
246 by (rtac (UTerm_rec_unfold RS trans) 1); |
|
247 by (simp_tac (HOL_ss addsimps [Case_In0,Case_In1]) 1); |
|
248 val UTerm_rec_CONST = result(); |
|
249 |
|
250 val prems = goalw UTerm.thy [COMB_def] |
|
251 "[| M: Sexp; N: Sexp |] ==> \ |
|
252 \ UTerm_rec(COMB(M,N), b, c, d) = \ |
|
253 \ d(M, N, UTerm_rec(M,b,c,d), UTerm_rec(N,b,c,d))"; |
|
254 by (rtac (UTerm_rec_unfold RS trans) 1); |
|
255 by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1); |
|
256 by (simp_tac (pred_Sexp_ss addsimps (In1_def::prems)) 1); |
|
257 val UTerm_rec_COMB = result(); |
|
258 |
|
259 (*** uterm_rec -- by UTerm_rec ***) |
|
260 |
|
261 val Rep_UTerm_in_Sexp = |
|
262 Rep_UTerm RS (range_Leaf_subset_Sexp RS UTerm_subset_Sexp RS subsetD); |
|
263 |
|
264 val uterm_rec_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, |
|
265 Abs_UTerm_inverse, Rep_UTerm_inverse, VAR_I, CONST_I, COMB_I, |
|
266 Rep_UTerm, rangeI, inj_Leaf, Inv_f_f, Rep_UTerm_in_Sexp]; |
|
267 val uterm_rec_ss = HOL_ss addsimps uterm_rec_simps; |
|
268 |
|
269 goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec(Var(x),b,c,d) = b(x)"; |
|
270 by (simp_tac uterm_rec_ss 1); |
|
271 val uterm_rec_Var = result(); |
|
272 |
|
273 goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec(Const(x),b,c,d) = c(x)"; |
|
274 by (simp_tac uterm_rec_ss 1); |
|
275 val uterm_rec_Const = result(); |
|
276 |
|
277 goalw UTerm.thy [uterm_rec_def, Comb_def] |
|
278 "uterm_rec(Comb(u,v),b,c,d) = d(u,v,uterm_rec(u,b,c,d),uterm_rec(v,b,c,d))"; |
|
279 by (simp_tac uterm_rec_ss 1); |
|
280 val uterm_rec_Comb = result(); |
|
281 |
|
282 val uterm_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, |
|
283 uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb]; |
|
284 val uterm_ss = uterm_free_ss addsimps uterm_simps; |
|
285 |
|
286 (*Type checking. Useful?*) |
|
287 val major::A_subset_Sexp::prems = goal UTerm.thy |
|
288 "[| M: UTerm(A); \ |
|
289 \ A<=Sexp; \ |
|
290 \ !!x.x:A ==> b(x): C(VAR(x)); \ |
|
291 \ !!x.x:A ==> c(x): C(CONST(x)); \ |
|
292 \ !!x y q r. [| x: UTerm(A); y: UTerm(A); q: C(x); r: C(y) |] ==> \ |
|
293 \ d(x,y,q,r): C(COMB(x,y)) \ |
|
294 \ |] ==> UTerm_rec(M,b,c,d) : C(M)"; |
|
295 val Sexp_UTermA_I = A_subset_Sexp RS UTerm_subset_Sexp RS subsetD; |
|
296 val Sexp_A_I = A_subset_Sexp RS subsetD; |
|
297 by (rtac (major RS UTerm_induct) 1); |
|
298 by (ALLGOALS |
|
299 (asm_simp_tac (uterm_ss addsimps ([Sexp_A_I,Sexp_UTermA_I] @ prems)))); |
|
300 val UTerm_rec_type = result(); |
|
301 |
|
302 |
|
303 (**********) |
|
304 |
|
305 val uterm_rews = [uterm_rec_Var,uterm_rec_Const,uterm_rec_Comb, |
|
306 t_not_Comb_t,u_not_Comb_u, |
|
307 Const_not_Comb,Comb_not_Var,Var_not_Const, |
|
308 Comb_not_Const,Var_not_Comb,Const_not_Var, |
|
309 Var_Var_eq,Const_Const_eq,Comb_Comb_eq]; |
|
310 |
|
311 (* |
|
312 val prems = goal Subst.thy |
|
313 "[| !!x.P(Var(x)); !!x.P(Const(x)); \ |
|
314 \ !!u v. P(u) --> P(v) --> P(Comb(u,v)) |] ==> P(a)"; |
|
315 by (uterm_ind_tac "a" 1); |
|
316 by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs)); |
|
317 val uterm_induct2 = result(); |
|
318 |
|
319 add_inds uterm_induct2; |
|
320 *) |