1 (* Title: HOL/ex/MT.thy |
|
2 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
3 Copyright 1993 University of Cambridge |
|
4 |
|
5 Based upon the article |
|
6 Robin Milner and Mads Tofte, |
|
7 Co-induction in Relational Semantics, |
|
8 Theoretical Computer Science 87 (1991), pages 209-220. |
|
9 |
|
10 Written up as |
|
11 Jacob Frost, A Case Study of Co_induction in Isabelle/HOL |
|
12 Report 308, Computer Lab, University of Cambridge (1993). |
|
13 *) |
|
14 |
|
15 section \<open>Milner-Tofte: Co-induction in Relational Semantics\<close> |
|
16 |
|
17 theory MT |
|
18 imports Main |
|
19 begin |
|
20 |
|
21 typedecl Const |
|
22 |
|
23 typedecl ExVar |
|
24 typedecl Ex |
|
25 |
|
26 typedecl TyConst |
|
27 typedecl Ty |
|
28 |
|
29 typedecl Clos |
|
30 typedecl Val |
|
31 |
|
32 typedecl ValEnv |
|
33 typedecl TyEnv |
|
34 |
|
35 consts |
|
36 c_app :: "[Const, Const] => Const" |
|
37 |
|
38 e_const :: "Const => Ex" |
|
39 e_var :: "ExVar => Ex" |
|
40 e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000) |
|
41 e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000) |
|
42 e_app :: "[Ex, Ex] => Ex" ("_ @@ _" [51,51] 1000) |
|
43 e_const_fst :: "Ex => Const" |
|
44 |
|
45 t_const :: "TyConst => Ty" |
|
46 t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000) |
|
47 |
|
48 v_const :: "Const => Val" |
|
49 v_clos :: "Clos => Val" |
|
50 |
|
51 ve_emp :: ValEnv |
|
52 ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50) |
|
53 ve_dom :: "ValEnv => ExVar set" |
|
54 ve_app :: "[ValEnv, ExVar] => Val" |
|
55 |
|
56 clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000) |
|
57 |
|
58 te_emp :: TyEnv |
|
59 te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50) |
|
60 te_app :: "[TyEnv, ExVar] => Ty" |
|
61 te_dom :: "TyEnv => ExVar set" |
|
62 |
|
63 isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50) |
|
64 |
|
65 (* |
|
66 Expression constructors must be injective, distinct and it must be possible |
|
67 to do induction over expressions. |
|
68 *) |
|
69 |
|
70 (* All the constructors are injective *) |
|
71 axiomatization where |
|
72 e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2" and |
|
73 e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2" and |
|
74 e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2" and |
|
75 e_fix_inj: |
|
76 " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> |
|
77 ev11 = ev21 & ev12 = ev22 & e1 = e2" and |
|
78 e_app_inj: "e11 @@ e12 = e21 @@ e22 ==> e11 = e21 & e12 = e22" |
|
79 |
|
80 (* All constructors are distinct *) |
|
81 |
|
82 axiomatization where |
|
83 e_disj_const_var: "~e_const(c) = e_var(ev)" and |
|
84 e_disj_const_fn: "~e_const(c) = fn ev => e" and |
|
85 e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e" and |
|
86 e_disj_const_app: "~e_const(c) = e1 @@ e2" and |
|
87 e_disj_var_fn: "~e_var(ev1) = fn ev2 => e" and |
|
88 e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e" and |
|
89 e_disj_var_app: "~e_var(ev) = e1 @@ e2" and |
|
90 e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2" and |
|
91 e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22" and |
|
92 e_disj_fix_app: "~fix ev11(ev12) = e1 = e21 @@ e22" |
|
93 |
|
94 (* Strong elimination, induction on expressions *) |
|
95 |
|
96 axiomatization where |
|
97 e_ind: |
|
98 " [| !!ev. P(e_var(ev)); |
|
99 !!c. P(e_const(c)); |
|
100 !!ev e. P(e) ==> P(fn ev => e); |
|
101 !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); |
|
102 !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @@ e2) |
|
103 |] ==> |
|
104 P(e) |
|
105 " |
|
106 |
|
107 (* Types - same scheme as for expressions *) |
|
108 |
|
109 (* All constructors are injective *) |
|
110 |
|
111 axiomatization where |
|
112 t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2" and |
|
113 t_fun_inj: "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22" |
|
114 |
|
115 (* All constructors are distinct, not needed so far ... *) |
|
116 |
|
117 (* Strong elimination, induction on types *) |
|
118 |
|
119 axiomatization where |
|
120 t_ind: |
|
121 "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] |
|
122 ==> P(t)" |
|
123 |
|
124 |
|
125 (* Values - same scheme again *) |
|
126 |
|
127 (* All constructors are injective *) |
|
128 |
|
129 axiomatization where |
|
130 v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2" and |
|
131 v_clos_inj: |
|
132 " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> |
|
133 ev1 = ev2 & e1 = e2 & ve1 = ve2" |
|
134 |
|
135 (* All constructors are distinct *) |
|
136 |
|
137 axiomatization where |
|
138 v_disj_const_clos: "~v_const(c) = v_clos(cl)" |
|
139 |
|
140 (* No induction on values: they are a codatatype! ... *) |
|
141 |
|
142 |
|
143 (* |
|
144 Value environments bind variables to values. Only the following trivial |
|
145 properties are needed. |
|
146 *) |
|
147 |
|
148 axiomatization where |
|
149 ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}" and |
|
150 |
|
151 ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v" and |
|
152 ve_app_owr2: "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2" |
|
153 |
|
154 |
|
155 (* Type Environments bind variables to types. The following trivial |
|
156 properties are needed. *) |
|
157 |
|
158 axiomatization where |
|
159 te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}" and |
|
160 |
|
161 te_app_owr1: "te_app (te + {ev |=> t}) ev=t" and |
|
162 te_app_owr2: "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2" |
|
163 |
|
164 |
|
165 (* The dynamic semantics is defined inductively by a set of inference |
|
166 rules. These inference rules allows one to draw conclusions of the form ve |
|
167 |- e ---> v, read the expression e evaluates to the value v in the value |
|
168 environment ve. Therefore the relation _ |- _ ---> _ is defined in Isabelle |
|
169 as the least fixpoint of the functor eval_fun below. From this definition |
|
170 introduction rules and a strong elimination (induction) rule can be |
|
171 derived. |
|
172 *) |
|
173 |
|
174 definition eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set" |
|
175 where "eval_fun(s) == |
|
176 { pp. |
|
177 (? ve c. pp=((ve,e_const(c)),v_const(c))) | |
|
178 (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) | |
|
179 (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| |
|
180 ( ? ve e x f cl. |
|
181 pp=((ve,fix f(x) = e),v_clos(cl)) & |
|
182 cl=<|x, e, ve+{f |-> v_clos(cl)} |> |
|
183 ) | |
|
184 ( ? ve e1 e2 c1 c2. |
|
185 pp=((ve,e1 @@ e2),v_const(c_app c1 c2)) & |
|
186 ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s |
|
187 ) | |
|
188 ( ? ve vem e1 e2 em xm v v2. |
|
189 pp=((ve,e1 @@ e2),v) & |
|
190 ((ve,e1),v_clos(<|xm,em,vem|>)):s & |
|
191 ((ve,e2),v2):s & |
|
192 ((vem+{xm |-> v2},em),v):s |
|
193 ) |
|
194 }" |
|
195 |
|
196 definition eval_rel :: "((ValEnv * Ex) * Val) set" |
|
197 where "eval_rel == lfp(eval_fun)" |
|
198 |
|
199 definition eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50) |
|
200 where "ve |- e ---> v == ((ve,e),v) \<in> eval_rel" |
|
201 |
|
202 (* The static semantics is defined in the same way as the dynamic |
|
203 semantics. The relation te |- e ===> t express the expression e has the |
|
204 type t in the type environment te. |
|
205 *) |
|
206 |
|
207 definition elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set" |
|
208 where "elab_fun(s) == |
|
209 { pp. |
|
210 (? te c t. pp=((te,e_const(c)),t) & c isof t) | |
|
211 (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | |
|
212 (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | |
|
213 (? te f x e t1 t2. |
|
214 pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s |
|
215 ) | |
|
216 (? te e1 e2 t1 t2. |
|
217 pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s |
|
218 ) |
|
219 }" |
|
220 |
|
221 definition elab_rel :: "((TyEnv * Ex) * Ty) set" |
|
222 where "elab_rel == lfp(elab_fun)" |
|
223 |
|
224 definition elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50) |
|
225 where "te |- e ===> t == ((te,e),t):elab_rel" |
|
226 |
|
227 |
|
228 (* The original correspondence relation *) |
|
229 |
|
230 definition isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _") |
|
231 where "ve isofenv te == |
|
232 ve_dom(ve) = te_dom(te) & |
|
233 (! x. |
|
234 x:ve_dom(ve) --> |
|
235 (? c. ve_app ve x = v_const(c) & c isof te_app te x))" |
|
236 |
|
237 axiomatization where |
|
238 isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2" |
|
239 |
|
240 |
|
241 (* The extented correspondence relation *) |
|
242 |
|
243 definition hasty_fun :: "(Val * Ty) set => (Val * Ty) set" |
|
244 where "hasty_fun(r) == |
|
245 { p. |
|
246 ( ? c t. p = (v_const(c),t) & c isof t) | |
|
247 ( ? ev e ve t te. |
|
248 p = (v_clos(<|ev,e,ve|>),t) & |
|
249 te |- fn ev => e ===> t & |
|
250 ve_dom(ve) = te_dom(te) & |
|
251 (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) |
|
252 ) |
|
253 }" |
|
254 |
|
255 definition hasty_rel :: "(Val * Ty) set" |
|
256 where "hasty_rel == gfp(hasty_fun)" |
|
257 |
|
258 definition hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50) |
|
259 where "v hasty t == (v,t) : hasty_rel" |
|
260 |
|
261 definition hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35) |
|
262 where "ve hastyenv te == |
|
263 ve_dom(ve) = te_dom(te) & |
|
264 (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)" |
|
265 |
|
266 |
|
267 (* ############################################################ *) |
|
268 (* Inference systems *) |
|
269 (* ############################################################ *) |
|
270 |
|
271 ML \<open> |
|
272 fun infsys_mono_tac ctxt = REPEAT (ares_tac ctxt (@{thms basic_monos} @ [allI, impI]) 1) |
|
273 \<close> |
|
274 |
|
275 lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))" |
|
276 by simp |
|
277 |
|
278 lemma infsys_p2: "P (fst (a,b)) (snd (a,b)) ==> P a b" |
|
279 by simp |
|
280 |
|
281 lemma infsys_pp1: "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))" |
|
282 by simp |
|
283 |
|
284 lemma infsys_pp2: "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c" |
|
285 by simp |
|
286 |
|
287 |
|
288 (* ############################################################ *) |
|
289 (* Fixpoints *) |
|
290 (* ############################################################ *) |
|
291 |
|
292 (* Least fixpoints *) |
|
293 |
|
294 lemma lfp_intro2: "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)" |
|
295 apply (rule subsetD) |
|
296 apply (rule lfp_lemma2) |
|
297 apply assumption+ |
|
298 done |
|
299 |
|
300 lemma lfp_elim2: |
|
301 assumes lfp: "x:lfp(f)" |
|
302 and mono: "mono(f)" |
|
303 and r: "!!y. y:f(lfp(f)) ==> P(y)" |
|
304 shows "P(x)" |
|
305 apply (rule r) |
|
306 apply (rule subsetD) |
|
307 apply (rule lfp_lemma3) |
|
308 apply (rule mono) |
|
309 apply (rule lfp) |
|
310 done |
|
311 |
|
312 lemma lfp_ind2: |
|
313 assumes lfp: "x:lfp(f)" |
|
314 and mono: "mono(f)" |
|
315 and r: "!!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y)" |
|
316 shows "P(x)" |
|
317 apply (rule lfp_induct_set [OF lfp mono]) |
|
318 apply (erule r) |
|
319 done |
|
320 |
|
321 (* Greatest fixpoints *) |
|
322 |
|
323 (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *) |
|
324 |
|
325 lemma gfp_coind2: |
|
326 assumes cih: "x:f({x} Un gfp(f))" |
|
327 and monoh: "mono(f)" |
|
328 shows "x:gfp(f)" |
|
329 apply (rule cih [THEN [2] gfp_upperbound [THEN subsetD]]) |
|
330 apply (rule monoh [THEN monoD]) |
|
331 apply (rule UnE [THEN subsetI]) |
|
332 apply assumption |
|
333 apply (blast intro!: cih) |
|
334 apply (rule monoh [THEN monoD [THEN subsetD]]) |
|
335 apply (rule Un_upper2) |
|
336 apply (erule monoh [THEN gfp_lemma2, THEN subsetD]) |
|
337 done |
|
338 |
|
339 lemma gfp_elim2: |
|
340 assumes gfph: "x:gfp(f)" |
|
341 and monoh: "mono(f)" |
|
342 and caseh: "!!y. y:f(gfp(f)) ==> P(y)" |
|
343 shows "P(x)" |
|
344 apply (rule caseh) |
|
345 apply (rule subsetD) |
|
346 apply (rule gfp_lemma2) |
|
347 apply (rule monoh) |
|
348 apply (rule gfph) |
|
349 done |
|
350 |
|
351 (* ############################################################ *) |
|
352 (* Expressions *) |
|
353 (* ############################################################ *) |
|
354 |
|
355 lemmas e_injs = e_const_inj e_var_inj e_fn_inj e_fix_inj e_app_inj |
|
356 |
|
357 lemmas e_disjs = |
|
358 e_disj_const_var |
|
359 e_disj_const_fn |
|
360 e_disj_const_fix |
|
361 e_disj_const_app |
|
362 e_disj_var_fn |
|
363 e_disj_var_fix |
|
364 e_disj_var_app |
|
365 e_disj_fn_fix |
|
366 e_disj_fn_app |
|
367 e_disj_fix_app |
|
368 |
|
369 lemmas e_disj_si = e_disjs e_disjs [symmetric] |
|
370 |
|
371 lemmas e_disj_se = e_disj_si [THEN notE] |
|
372 |
|
373 (* ############################################################ *) |
|
374 (* Values *) |
|
375 (* ############################################################ *) |
|
376 |
|
377 lemmas v_disjs = v_disj_const_clos |
|
378 lemmas v_disj_si = v_disjs v_disjs [symmetric] |
|
379 lemmas v_disj_se = v_disj_si [THEN notE] |
|
380 |
|
381 lemmas v_injs = v_const_inj v_clos_inj |
|
382 |
|
383 (* ############################################################ *) |
|
384 (* Evaluations *) |
|
385 (* ############################################################ *) |
|
386 |
|
387 (* Monotonicity of eval_fun *) |
|
388 |
|
389 lemma eval_fun_mono: "mono(eval_fun)" |
|
390 unfolding mono_def eval_fun_def |
|
391 apply (tactic "infsys_mono_tac @{context}") |
|
392 done |
|
393 |
|
394 (* Introduction rules *) |
|
395 |
|
396 lemma eval_const: "ve |- e_const(c) ---> v_const(c)" |
|
397 unfolding eval_def eval_rel_def |
|
398 apply (rule lfp_intro2) |
|
399 apply (rule eval_fun_mono) |
|
400 apply (unfold eval_fun_def) |
|
401 (*Naughty! But the quantifiers are nested VERY deeply...*) |
|
402 apply (blast intro!: exI) |
|
403 done |
|
404 |
|
405 lemma eval_var2: |
|
406 "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev" |
|
407 apply (unfold eval_def eval_rel_def) |
|
408 apply (rule lfp_intro2) |
|
409 apply (rule eval_fun_mono) |
|
410 apply (unfold eval_fun_def) |
|
411 apply (blast intro!: exI) |
|
412 done |
|
413 |
|
414 lemma eval_fn: |
|
415 "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)" |
|
416 apply (unfold eval_def eval_rel_def) |
|
417 apply (rule lfp_intro2) |
|
418 apply (rule eval_fun_mono) |
|
419 apply (unfold eval_fun_def) |
|
420 apply (blast intro!: exI) |
|
421 done |
|
422 |
|
423 lemma eval_fix: |
|
424 " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> |
|
425 ve |- fix ev2(ev1) = e ---> v_clos(cl)" |
|
426 apply (unfold eval_def eval_rel_def) |
|
427 apply (rule lfp_intro2) |
|
428 apply (rule eval_fun_mono) |
|
429 apply (unfold eval_fun_def) |
|
430 apply (blast intro!: exI) |
|
431 done |
|
432 |
|
433 lemma eval_app1: |
|
434 " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> |
|
435 ve |- e1 @@ e2 ---> v_const(c_app c1 c2)" |
|
436 apply (unfold eval_def eval_rel_def) |
|
437 apply (rule lfp_intro2) |
|
438 apply (rule eval_fun_mono) |
|
439 apply (unfold eval_fun_def) |
|
440 apply (blast intro!: exI) |
|
441 done |
|
442 |
|
443 lemma eval_app2: |
|
444 " [| ve |- e1 ---> v_clos(<|xm,em,vem|>); |
|
445 ve |- e2 ---> v2; |
|
446 vem + {xm |-> v2} |- em ---> v |
|
447 |] ==> |
|
448 ve |- e1 @@ e2 ---> v" |
|
449 apply (unfold eval_def eval_rel_def) |
|
450 apply (rule lfp_intro2) |
|
451 apply (rule eval_fun_mono) |
|
452 apply (unfold eval_fun_def) |
|
453 apply (blast intro!: disjI2) |
|
454 done |
|
455 |
|
456 (* Strong elimination, induction on evaluations *) |
|
457 |
|
458 lemma eval_ind0: |
|
459 " [| ve |- e ---> v; |
|
460 !!ve c. P(((ve,e_const(c)),v_const(c))); |
|
461 !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); |
|
462 !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); |
|
463 !!ev1 ev2 ve cl e. |
|
464 cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> |
|
465 P(((ve,fix ev2(ev1) = e),v_clos(cl))); |
|
466 !!ve c1 c2 e1 e2. |
|
467 [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> |
|
468 P(((ve,e1 @@ e2),v_const(c_app c1 c2))); |
|
469 !!ve vem xm e1 e2 em v v2. |
|
470 [| P(((ve,e1),v_clos(<|xm,em,vem|>))); |
|
471 P(((ve,e2),v2)); |
|
472 P(((vem + {xm |-> v2},em),v)) |
|
473 |] ==> |
|
474 P(((ve,e1 @@ e2),v)) |
|
475 |] ==> |
|
476 P(((ve,e),v))" |
|
477 unfolding eval_def eval_rel_def |
|
478 apply (erule lfp_ind2) |
|
479 apply (rule eval_fun_mono) |
|
480 apply (unfold eval_fun_def) |
|
481 apply (drule CollectD) |
|
482 apply safe |
|
483 apply auto |
|
484 done |
|
485 |
|
486 lemma eval_ind: |
|
487 " [| ve |- e ---> v; |
|
488 !!ve c. P ve (e_const c) (v_const c); |
|
489 !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); |
|
490 !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); |
|
491 !!ev1 ev2 ve cl e. |
|
492 cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> |
|
493 P ve (fix ev2(ev1) = e) (v_clos cl); |
|
494 !!ve c1 c2 e1 e2. |
|
495 [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> |
|
496 P ve (e1 @@ e2) (v_const(c_app c1 c2)); |
|
497 !!ve vem evm e1 e2 em v v2. |
|
498 [| P ve e1 (v_clos <|evm,em,vem|>); |
|
499 P ve e2 v2; |
|
500 P (vem + {evm |-> v2}) em v |
|
501 |] ==> P ve (e1 @@ e2) v |
|
502 |] ==> P ve e v" |
|
503 apply (rule_tac P = "P" in infsys_pp2) |
|
504 apply (rule eval_ind0) |
|
505 apply (rule infsys_pp1) |
|
506 apply auto |
|
507 done |
|
508 |
|
509 (* ############################################################ *) |
|
510 (* Elaborations *) |
|
511 (* ############################################################ *) |
|
512 |
|
513 lemma elab_fun_mono: "mono(elab_fun)" |
|
514 unfolding mono_def elab_fun_def |
|
515 apply (tactic "infsys_mono_tac @{context}") |
|
516 done |
|
517 |
|
518 (* Introduction rules *) |
|
519 |
|
520 lemma elab_const: |
|
521 "c isof ty ==> te |- e_const(c) ===> ty" |
|
522 apply (unfold elab_def elab_rel_def) |
|
523 apply (rule lfp_intro2) |
|
524 apply (rule elab_fun_mono) |
|
525 apply (unfold elab_fun_def) |
|
526 apply (blast intro!: exI) |
|
527 done |
|
528 |
|
529 lemma elab_var: |
|
530 "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x" |
|
531 apply (unfold elab_def elab_rel_def) |
|
532 apply (rule lfp_intro2) |
|
533 apply (rule elab_fun_mono) |
|
534 apply (unfold elab_fun_def) |
|
535 apply (blast intro!: exI) |
|
536 done |
|
537 |
|
538 lemma elab_fn: |
|
539 "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2" |
|
540 apply (unfold elab_def elab_rel_def) |
|
541 apply (rule lfp_intro2) |
|
542 apply (rule elab_fun_mono) |
|
543 apply (unfold elab_fun_def) |
|
544 apply (blast intro!: exI) |
|
545 done |
|
546 |
|
547 lemma elab_fix: |
|
548 "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> |
|
549 te |- fix f(x) = e ===> ty1->ty2" |
|
550 apply (unfold elab_def elab_rel_def) |
|
551 apply (rule lfp_intro2) |
|
552 apply (rule elab_fun_mono) |
|
553 apply (unfold elab_fun_def) |
|
554 apply (blast intro!: exI) |
|
555 done |
|
556 |
|
557 lemma elab_app: |
|
558 "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> |
|
559 te |- e1 @@ e2 ===> ty2" |
|
560 apply (unfold elab_def elab_rel_def) |
|
561 apply (rule lfp_intro2) |
|
562 apply (rule elab_fun_mono) |
|
563 apply (unfold elab_fun_def) |
|
564 apply (blast intro!: disjI2) |
|
565 done |
|
566 |
|
567 (* Strong elimination, induction on elaborations *) |
|
568 |
|
569 lemma elab_ind0: |
|
570 assumes 1: "te |- e ===> t" |
|
571 and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))" |
|
572 and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))" |
|
573 and 4: "!!te x e t1 t2. |
|
574 [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> |
|
575 P(((te,fn x => e),t1->t2))" |
|
576 and 5: "!!te f x e t1 t2. |
|
577 [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; |
|
578 P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) |
|
579 |] ==> |
|
580 P(((te,fix f(x) = e),t1->t2))" |
|
581 and 6: "!!te e1 e2 t1 t2. |
|
582 [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); |
|
583 te |- e2 ===> t1; P(((te,e2),t1)) |
|
584 |] ==> |
|
585 P(((te,e1 @@ e2),t2))" |
|
586 shows "P(((te,e),t))" |
|
587 apply (rule lfp_ind2 [OF 1 [unfolded elab_def elab_rel_def]]) |
|
588 apply (rule elab_fun_mono) |
|
589 apply (unfold elab_fun_def) |
|
590 apply (drule CollectD) |
|
591 apply safe |
|
592 apply (erule 2) |
|
593 apply (erule 3) |
|
594 apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+ |
|
595 apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+ |
|
596 apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+ |
|
597 done |
|
598 |
|
599 lemma elab_ind: |
|
600 " [| te |- e ===> t; |
|
601 !!te c t. c isof t ==> P te (e_const c) t; |
|
602 !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); |
|
603 !!te x e t1 t2. |
|
604 [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> |
|
605 P te (fn x => e) (t1->t2); |
|
606 !!te f x e t1 t2. |
|
607 [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; |
|
608 P (te + {f |=> t1->t2} + {x |=> t1}) e t2 |
|
609 |] ==> |
|
610 P te (fix f(x) = e) (t1->t2); |
|
611 !!te e1 e2 t1 t2. |
|
612 [| te |- e1 ===> t1->t2; P te e1 (t1->t2); |
|
613 te |- e2 ===> t1; P te e2 t1 |
|
614 |] ==> |
|
615 P te (e1 @@ e2) t2 |
|
616 |] ==> |
|
617 P te e t" |
|
618 apply (rule_tac P = "P" in infsys_pp2) |
|
619 apply (erule elab_ind0) |
|
620 apply (rule_tac [!] infsys_pp1) |
|
621 apply auto |
|
622 done |
|
623 |
|
624 (* Weak elimination, case analysis on elaborations *) |
|
625 |
|
626 lemma elab_elim0: |
|
627 assumes 1: "te |- e ===> t" |
|
628 and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))" |
|
629 and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))" |
|
630 and 4: "!!te x e t1 t2. |
|
631 te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2))" |
|
632 and 5: "!!te f x e t1 t2. |
|
633 te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> |
|
634 P(((te,fix f(x) = e),t1->t2))" |
|
635 and 6: "!!te e1 e2 t1 t2. |
|
636 [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> |
|
637 P(((te,e1 @@ e2),t2))" |
|
638 shows "P(((te,e),t))" |
|
639 apply (rule lfp_elim2 [OF 1 [unfolded elab_def elab_rel_def]]) |
|
640 apply (rule elab_fun_mono) |
|
641 apply (unfold elab_fun_def) |
|
642 apply (drule CollectD) |
|
643 apply safe |
|
644 apply (erule 2) |
|
645 apply (erule 3) |
|
646 apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+ |
|
647 apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+ |
|
648 apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+ |
|
649 done |
|
650 |
|
651 lemma elab_elim: |
|
652 " [| te |- e ===> t; |
|
653 !!te c t. c isof t ==> P te (e_const c) t; |
|
654 !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); |
|
655 !!te x e t1 t2. |
|
656 te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); |
|
657 !!te f x e t1 t2. |
|
658 te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> |
|
659 P te (fix f(x) = e) (t1->t2); |
|
660 !!te e1 e2 t1 t2. |
|
661 [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> |
|
662 P te (e1 @@ e2) t2 |
|
663 |] ==> |
|
664 P te e t" |
|
665 apply (rule_tac P = "P" in infsys_pp2) |
|
666 apply (rule elab_elim0) |
|
667 apply auto |
|
668 done |
|
669 |
|
670 (* Elimination rules for each expression *) |
|
671 |
|
672 lemma elab_const_elim_lem: |
|
673 "te |- e ===> t ==> (e = e_const(c) --> c isof t)" |
|
674 apply (erule elab_elim) |
|
675 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+ |
|
676 done |
|
677 |
|
678 lemma elab_const_elim: "te |- e_const(c) ===> t ==> c isof t" |
|
679 apply (drule elab_const_elim_lem) |
|
680 apply blast |
|
681 done |
|
682 |
|
683 lemma elab_var_elim_lem: |
|
684 "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))" |
|
685 apply (erule elab_elim) |
|
686 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+ |
|
687 done |
|
688 |
|
689 lemma elab_var_elim: "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)" |
|
690 apply (drule elab_var_elim_lem) |
|
691 apply blast |
|
692 done |
|
693 |
|
694 lemma elab_fn_elim_lem: |
|
695 " te |- e ===> t ==> |
|
696 ( e = fn x1 => e1 --> |
|
697 (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) |
|
698 )" |
|
699 apply (erule elab_elim) |
|
700 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+ |
|
701 done |
|
702 |
|
703 lemma elab_fn_elim: " te |- fn x1 => e1 ===> t ==> |
|
704 (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)" |
|
705 apply (drule elab_fn_elim_lem) |
|
706 apply blast |
|
707 done |
|
708 |
|
709 lemma elab_fix_elim_lem: |
|
710 " te |- e ===> t ==> |
|
711 (e = fix f(x) = e1 --> |
|
712 (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))" |
|
713 apply (erule elab_elim) |
|
714 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+ |
|
715 done |
|
716 |
|
717 lemma elab_fix_elim: " te |- fix ev1(ev2) = e1 ===> t ==> |
|
718 (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)" |
|
719 apply (drule elab_fix_elim_lem) |
|
720 apply blast |
|
721 done |
|
722 |
|
723 lemma elab_app_elim_lem: |
|
724 " te |- e ===> t2 ==> |
|
725 (e = e1 @@ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))" |
|
726 apply (erule elab_elim) |
|
727 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+ |
|
728 done |
|
729 |
|
730 lemma elab_app_elim: "te |- e1 @@ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)" |
|
731 apply (drule elab_app_elim_lem) |
|
732 apply blast |
|
733 done |
|
734 |
|
735 (* ############################################################ *) |
|
736 (* The extended correspondence relation *) |
|
737 (* ############################################################ *) |
|
738 |
|
739 (* Monotonicity of hasty_fun *) |
|
740 |
|
741 lemma mono_hasty_fun: "mono(hasty_fun)" |
|
742 unfolding mono_def hasty_fun_def |
|
743 apply (tactic "infsys_mono_tac @{context}") |
|
744 apply blast |
|
745 done |
|
746 |
|
747 (* |
|
748 Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it |
|
749 enjoys two strong indtroduction (co-induction) rules and an elimination rule. |
|
750 *) |
|
751 |
|
752 (* First strong indtroduction (co-induction) rule for hasty_rel *) |
|
753 |
|
754 lemma hasty_rel_const_coind: "c isof t ==> (v_const(c),t) : hasty_rel" |
|
755 apply (unfold hasty_rel_def) |
|
756 apply (rule gfp_coind2) |
|
757 apply (unfold hasty_fun_def) |
|
758 apply (rule CollectI) |
|
759 apply (rule disjI1) |
|
760 apply blast |
|
761 apply (rule mono_hasty_fun) |
|
762 done |
|
763 |
|
764 (* Second strong introduction (co-induction) rule for hasty_rel *) |
|
765 |
|
766 lemma hasty_rel_clos_coind: |
|
767 " [| te |- fn ev => e ===> t; |
|
768 ve_dom(ve) = te_dom(te); |
|
769 ! ev1. |
|
770 ev1:ve_dom(ve) --> |
|
771 (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel |
|
772 |] ==> |
|
773 (v_clos(<|ev,e,ve|>),t) : hasty_rel" |
|
774 apply (unfold hasty_rel_def) |
|
775 apply (rule gfp_coind2) |
|
776 apply (unfold hasty_fun_def) |
|
777 apply (rule CollectI) |
|
778 apply (rule disjI2) |
|
779 apply blast |
|
780 apply (rule mono_hasty_fun) |
|
781 done |
|
782 |
|
783 (* Elimination rule for hasty_rel *) |
|
784 |
|
785 lemma hasty_rel_elim0: |
|
786 " [| !! c t. c isof t ==> P((v_const(c),t)); |
|
787 !! te ev e t ve. |
|
788 [| te |- fn ev => e ===> t; |
|
789 ve_dom(ve) = te_dom(te); |
|
790 !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel |
|
791 |] ==> P((v_clos(<|ev,e,ve|>),t)); |
|
792 (v,t) : hasty_rel |
|
793 |] ==> P(v,t)" |
|
794 unfolding hasty_rel_def |
|
795 apply (erule gfp_elim2) |
|
796 apply (rule mono_hasty_fun) |
|
797 apply (unfold hasty_fun_def) |
|
798 apply (drule CollectD) |
|
799 apply (fold hasty_fun_def) |
|
800 apply auto |
|
801 done |
|
802 |
|
803 lemma hasty_rel_elim: |
|
804 " [| (v,t) : hasty_rel; |
|
805 !! c t. c isof t ==> P (v_const c) t; |
|
806 !! te ev e t ve. |
|
807 [| te |- fn ev => e ===> t; |
|
808 ve_dom(ve) = te_dom(te); |
|
809 !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel |
|
810 |] ==> P (v_clos <|ev,e,ve|>) t |
|
811 |] ==> P v t" |
|
812 apply (rule_tac P = "P" in infsys_p2) |
|
813 apply (rule hasty_rel_elim0) |
|
814 apply auto |
|
815 done |
|
816 |
|
817 (* Introduction rules for hasty *) |
|
818 |
|
819 lemma hasty_const: "c isof t ==> v_const(c) hasty t" |
|
820 apply (unfold hasty_def) |
|
821 apply (erule hasty_rel_const_coind) |
|
822 done |
|
823 |
|
824 lemma hasty_clos: |
|
825 "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t" |
|
826 apply (unfold hasty_def hasty_env_def) |
|
827 apply (rule hasty_rel_clos_coind) |
|
828 apply (blast del: equalityI)+ |
|
829 done |
|
830 |
|
831 (* Elimination on constants for hasty *) |
|
832 |
|
833 lemma hasty_elim_const_lem: |
|
834 "v hasty t ==> (!c.(v = v_const(c) --> c isof t))" |
|
835 apply (unfold hasty_def) |
|
836 apply (rule hasty_rel_elim) |
|
837 apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+ |
|
838 done |
|
839 |
|
840 lemma hasty_elim_const: "v_const(c) hasty t ==> c isof t" |
|
841 apply (drule hasty_elim_const_lem) |
|
842 apply blast |
|
843 done |
|
844 |
|
845 (* Elimination on closures for hasty *) |
|
846 |
|
847 lemma hasty_elim_clos_lem: |
|
848 " v hasty t ==> |
|
849 ! x e ve. |
|
850 v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)" |
|
851 apply (unfold hasty_env_def hasty_def) |
|
852 apply (rule hasty_rel_elim) |
|
853 apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+ |
|
854 done |
|
855 |
|
856 lemma hasty_elim_clos: "v_clos(<|ev,e,ve|>) hasty t ==> |
|
857 ? te. te |- fn ev => e ===> t & ve hastyenv te " |
|
858 apply (drule hasty_elim_clos_lem) |
|
859 apply blast |
|
860 done |
|
861 |
|
862 (* ############################################################ *) |
|
863 (* The pointwise extension of hasty to environments *) |
|
864 (* ############################################################ *) |
|
865 |
|
866 lemma hasty_env1: "[| ve hastyenv te; v hasty t |] ==> |
|
867 ve + {ev |-> v} hastyenv te + {ev |=> t}" |
|
868 apply (unfold hasty_env_def) |
|
869 apply (simp del: mem_simps add: ve_dom_owr te_dom_owr) |
|
870 apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>) |
|
871 apply (case_tac "ev=x") |
|
872 apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1) |
|
873 apply (simp add: ve_app_owr2 te_app_owr2) |
|
874 done |
|
875 |
|
876 (* ############################################################ *) |
|
877 (* The Consistency theorem *) |
|
878 (* ############################################################ *) |
|
879 |
|
880 lemma consistency_const: "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t" |
|
881 apply (drule elab_const_elim) |
|
882 apply (erule hasty_const) |
|
883 done |
|
884 |
|
885 lemma consistency_var: |
|
886 "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> |
|
887 ve_app ve ev hasty t" |
|
888 apply (unfold hasty_env_def) |
|
889 apply (drule elab_var_elim) |
|
890 apply blast |
|
891 done |
|
892 |
|
893 lemma consistency_fn: "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> |
|
894 v_clos(<| ev, e, ve |>) hasty t" |
|
895 apply (rule hasty_clos) |
|
896 apply blast |
|
897 done |
|
898 |
|
899 lemma consistency_fix: |
|
900 "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; |
|
901 ve hastyenv te ; |
|
902 te |- fix ev2 ev1 = e ===> t |
|
903 |] ==> |
|
904 v_clos(cl) hasty t" |
|
905 apply (unfold hasty_env_def hasty_def) |
|
906 apply (drule elab_fix_elim) |
|
907 apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>) |
|
908 (*Do a single unfolding of cl*) |
|
909 apply (frule ssubst) prefer 2 apply assumption |
|
910 apply (rule hasty_rel_clos_coind) |
|
911 apply (erule elab_fn) |
|
912 apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr) |
|
913 |
|
914 apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr) |
|
915 apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>) |
|
916 apply (case_tac "ev2=ev1a") |
|
917 apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1) |
|
918 apply blast |
|
919 apply (simp add: ve_app_owr2 te_app_owr2) |
|
920 done |
|
921 |
|
922 lemma consistency_app1: "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t; |
|
923 ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; |
|
924 ve hastyenv te ; te |- e1 @@ e2 ===> t |
|
925 |] ==> |
|
926 v_const(c_app c1 c2) hasty t" |
|
927 apply (drule elab_app_elim) |
|
928 apply safe |
|
929 apply (rule hasty_const) |
|
930 apply (rule isof_app) |
|
931 apply (rule hasty_elim_const) |
|
932 apply blast |
|
933 apply (rule hasty_elim_const) |
|
934 apply blast |
|
935 done |
|
936 |
|
937 lemma consistency_app2: "[| ! t te. |
|
938 ve hastyenv te --> |
|
939 te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; |
|
940 ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; |
|
941 ! t te. |
|
942 vem + { evm |-> v2 } hastyenv te --> te |- em ===> t --> v hasty t; |
|
943 ve hastyenv te ; |
|
944 te |- e1 @@ e2 ===> t |
|
945 |] ==> |
|
946 v hasty t" |
|
947 apply (drule elab_app_elim) |
|
948 apply safe |
|
949 apply (erule allE, erule allE, erule impE) |
|
950 apply assumption |
|
951 apply (erule impE) |
|
952 apply assumption |
|
953 apply (erule allE, erule allE, erule impE) |
|
954 apply assumption |
|
955 apply (erule impE) |
|
956 apply assumption |
|
957 apply (drule hasty_elim_clos) |
|
958 apply safe |
|
959 apply (drule elab_fn_elim) |
|
960 apply (blast intro: hasty_env1 dest!: t_fun_inj) |
|
961 done |
|
962 |
|
963 lemma consistency: "ve |- e ---> v ==> |
|
964 (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)" |
|
965 |
|
966 (* Proof by induction on the structure of evaluations *) |
|
967 |
|
968 apply (erule eval_ind) |
|
969 apply safe |
|
970 apply (blast intro: consistency_const consistency_var consistency_fn consistency_fix consistency_app1 consistency_app2)+ |
|
971 done |
|
972 |
|
973 (* ############################################################ *) |
|
974 (* The Basic Consistency theorem *) |
|
975 (* ############################################################ *) |
|
976 |
|
977 lemma basic_consistency_lem: |
|
978 "ve isofenv te ==> ve hastyenv te" |
|
979 apply (unfold isof_env_def hasty_env_def) |
|
980 apply safe |
|
981 apply (erule allE) |
|
982 apply (erule impE) |
|
983 apply assumption |
|
984 apply (erule exE) |
|
985 apply (erule conjE) |
|
986 apply (drule hasty_const) |
|
987 apply (simp (no_asm_simp)) |
|
988 done |
|
989 |
|
990 lemma basic_consistency: |
|
991 "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t" |
|
992 apply (rule hasty_elim_const) |
|
993 apply (drule consistency) |
|
994 apply (blast intro!: basic_consistency_lem) |
|
995 done |
|
996 |
|
997 end |
|