1 (* Title: HOL/ex/mt.ML |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Based upon the article |
|
7 Robin Milner and Mads Tofte, |
|
8 Co-induction in Relational Semantics, |
|
9 Theoretical Computer Science 87 (1991), pages 209-220. |
|
10 |
|
11 Written up as |
|
12 Jacob Frost, A Case Study of Co-induction in Isabelle/HOL |
|
13 Report 308, Computer Lab, University of Cambridge (1993). |
|
14 |
|
15 NEEDS TO USE INDUCTIVE DEFS PACKAGE |
|
16 *) |
|
17 |
|
18 open MT; |
|
19 |
|
20 val prems = goal MT.thy "~a:{b} ==> ~a=b"; |
|
21 by (cut_facts_tac prems 1); |
|
22 by (rtac notI 1); |
|
23 by (dtac notE 1); |
|
24 by (hyp_subst_tac 1); |
|
25 by (rtac singletonI 1); |
|
26 by (assume_tac 1); |
|
27 qed "notsingletonI"; |
|
28 |
|
29 (* ############################################################ *) |
|
30 (* Inference systems *) |
|
31 (* ############################################################ *) |
|
32 |
|
33 val infsys_mono_tac = |
|
34 (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN |
|
35 (rtac CollectI 1) THEN (dtac CollectD 1) THEN |
|
36 REPEAT |
|
37 ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN |
|
38 (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1) |
|
39 ); |
|
40 |
|
41 val prems = goal MT.thy "P(a,b) ==> P(fst(<a,b>),snd(<a,b>))"; |
|
42 by (simp_tac (prod_ss addsimps prems) 1); |
|
43 qed "infsys_p1"; |
|
44 |
|
45 val prems = goal MT.thy "!!a b. P(fst(<a,b>),snd(<a,b>)) ==> P(a,b)"; |
|
46 by (asm_full_simp_tac prod_ss 1); |
|
47 qed "infsys_p2"; |
|
48 |
|
49 val prems = goal MT.thy |
|
50 "P(a,b,c) ==> P(fst(fst(<<a,b>,c>)),snd(fst(<<a,b>,c>)),snd(<<a,b>,c>))"; |
|
51 by (simp_tac (prod_ss addsimps prems) 1); |
|
52 qed "infsys_pp1"; |
|
53 |
|
54 goal MT.thy |
|
55 "!!a.P(fst(fst(<<a,b>,c>)),snd(fst(<<a,b>,c>)),snd(<<a,b>,c>)) ==> P(a,b,c)"; |
|
56 by (asm_full_simp_tac prod_ss 1); |
|
57 qed "infsys_pp2"; |
|
58 |
|
59 (* ############################################################ *) |
|
60 (* Fixpoints *) |
|
61 (* ############################################################ *) |
|
62 |
|
63 (* Least fixpoints *) |
|
64 |
|
65 val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)"; |
|
66 by (rtac subsetD 1); |
|
67 by (rtac lfp_lemma2 1); |
|
68 by (resolve_tac prems 1); |
|
69 by (resolve_tac prems 1); |
|
70 qed "lfp_intro2"; |
|
71 |
|
72 val prems = goal MT.thy |
|
73 " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \ |
|
74 \ P(x)"; |
|
75 by (cut_facts_tac prems 1); |
|
76 by (resolve_tac prems 1); |
|
77 by (rtac subsetD 1); |
|
78 by (rtac lfp_lemma3 1); |
|
79 by (assume_tac 1); |
|
80 by (assume_tac 1); |
|
81 qed "lfp_elim2"; |
|
82 |
|
83 val prems = goal MT.thy |
|
84 " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \ |
|
85 \ P(x)"; |
|
86 by (cut_facts_tac prems 1); |
|
87 by (etac induct 1); |
|
88 by (assume_tac 1); |
|
89 by (eresolve_tac prems 1); |
|
90 qed "lfp_ind2"; |
|
91 |
|
92 (* Greatest fixpoints *) |
|
93 |
|
94 (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *) |
|
95 |
|
96 val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)"; |
|
97 by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1); |
|
98 by (rtac (monoh RS monoD) 1); |
|
99 by (rtac (UnE RS subsetI) 1); |
|
100 by (assume_tac 1); |
|
101 by (fast_tac (set_cs addSIs [cih]) 1); |
|
102 by (rtac (monoh RS monoD RS subsetD) 1); |
|
103 by (rtac Un_upper2 1); |
|
104 by (etac (monoh RS gfp_lemma2 RS subsetD) 1); |
|
105 qed "gfp_coind2"; |
|
106 |
|
107 val [gfph,monoh,caseh] = goal MT.thy |
|
108 "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)"; |
|
109 by (rtac caseh 1); |
|
110 by (rtac subsetD 1); |
|
111 by (rtac gfp_lemma2 1); |
|
112 by (rtac monoh 1); |
|
113 by (rtac gfph 1); |
|
114 qed "gfp_elim2"; |
|
115 |
|
116 (* ############################################################ *) |
|
117 (* Expressions *) |
|
118 (* ############################################################ *) |
|
119 |
|
120 val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj]; |
|
121 |
|
122 val e_disjs = |
|
123 [ e_disj_const_var, |
|
124 e_disj_const_fn, |
|
125 e_disj_const_fix, |
|
126 e_disj_const_app, |
|
127 e_disj_var_fn, |
|
128 e_disj_var_fix, |
|
129 e_disj_var_app, |
|
130 e_disj_fn_fix, |
|
131 e_disj_fn_app, |
|
132 e_disj_fix_app |
|
133 ]; |
|
134 |
|
135 val e_disj_si = e_disjs @ (e_disjs RL [not_sym]); |
|
136 val e_disj_se = (e_disj_si RL [notE]); |
|
137 |
|
138 fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs; |
|
139 |
|
140 (* ############################################################ *) |
|
141 (* Values *) |
|
142 (* ############################################################ *) |
|
143 |
|
144 val v_disjs = [v_disj_const_clos]; |
|
145 val v_disj_si = v_disjs @ (v_disjs RL [not_sym]); |
|
146 val v_disj_se = (v_disj_si RL [notE]); |
|
147 |
|
148 val v_injs = [v_const_inj, v_clos_inj]; |
|
149 |
|
150 fun v_ext_cs cs = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs; |
|
151 |
|
152 (* ############################################################ *) |
|
153 (* Evaluations *) |
|
154 (* ############################################################ *) |
|
155 |
|
156 (* Monotonicity of eval_fun *) |
|
157 |
|
158 goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)"; |
|
159 (*Causes the most horrendous flexflex-trace.*) |
|
160 by infsys_mono_tac; |
|
161 qed "eval_fun_mono"; |
|
162 |
|
163 (* Introduction rules *) |
|
164 |
|
165 goalw MT.thy [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)"; |
|
166 by (rtac lfp_intro2 1); |
|
167 by (rtac eval_fun_mono 1); |
|
168 by (rewtac eval_fun_def); |
|
169 by (fast_tac set_cs 1); |
|
170 qed "eval_const"; |
|
171 |
|
172 val prems = goalw MT.thy [eval_def, eval_rel_def] |
|
173 "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app(ve,ev)"; |
|
174 by (cut_facts_tac prems 1); |
|
175 by (rtac lfp_intro2 1); |
|
176 by (rtac eval_fun_mono 1); |
|
177 by (rewtac eval_fun_def); |
|
178 by (fast_tac set_cs 1); |
|
179 qed "eval_var"; |
|
180 |
|
181 val prems = goalw MT.thy [eval_def, eval_rel_def] |
|
182 "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)"; |
|
183 by (cut_facts_tac prems 1); |
|
184 by (rtac lfp_intro2 1); |
|
185 by (rtac eval_fun_mono 1); |
|
186 by (rewtac eval_fun_def); |
|
187 by (fast_tac set_cs 1); |
|
188 qed "eval_fn"; |
|
189 |
|
190 val prems = goalw MT.thy [eval_def, eval_rel_def] |
|
191 " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \ |
|
192 \ ve |- fix ev2(ev1) = e ---> v_clos(cl)"; |
|
193 by (cut_facts_tac prems 1); |
|
194 by (rtac lfp_intro2 1); |
|
195 by (rtac eval_fun_mono 1); |
|
196 by (rewtac eval_fun_def); |
|
197 by (fast_tac set_cs 1); |
|
198 qed "eval_fix"; |
|
199 |
|
200 val prems = goalw MT.thy [eval_def, eval_rel_def] |
|
201 " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \ |
|
202 \ ve |- e1 @ e2 ---> v_const(c_app(c1,c2))"; |
|
203 by (cut_facts_tac prems 1); |
|
204 by (rtac lfp_intro2 1); |
|
205 by (rtac eval_fun_mono 1); |
|
206 by (rewtac eval_fun_def); |
|
207 by (fast_tac set_cs 1); |
|
208 qed "eval_app1"; |
|
209 |
|
210 val prems = goalw MT.thy [eval_def, eval_rel_def] |
|
211 " [| ve |- e1 ---> v_clos(<|xm,em,vem|>); \ |
|
212 \ ve |- e2 ---> v2; \ |
|
213 \ vem + {xm |-> v2} |- em ---> v \ |
|
214 \ |] ==> \ |
|
215 \ ve |- e1 @ e2 ---> v"; |
|
216 by (cut_facts_tac prems 1); |
|
217 by (rtac lfp_intro2 1); |
|
218 by (rtac eval_fun_mono 1); |
|
219 by (rewtac eval_fun_def); |
|
220 by (fast_tac (set_cs addSIs [disjI2]) 1); |
|
221 qed "eval_app2"; |
|
222 |
|
223 (* Strong elimination, induction on evaluations *) |
|
224 |
|
225 val prems = goalw MT.thy [eval_def, eval_rel_def] |
|
226 " [| ve |- e ---> v; \ |
|
227 \ !!ve c. P(<<ve,e_const(c)>,v_const(c)>); \ |
|
228 \ !!ev ve. ev:ve_dom(ve) ==> P(<<ve,e_var(ev)>,ve_app(ve,ev)>); \ |
|
229 \ !!ev ve e. P(<<ve,fn ev => e>,v_clos(<|ev,e,ve|>)>); \ |
|
230 \ !!ev1 ev2 ve cl e. \ |
|
231 \ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \ |
|
232 \ P(<<ve,fix ev2(ev1) = e>,v_clos(cl)>); \ |
|
233 \ !!ve c1 c2 e1 e2. \ |
|
234 \ [| P(<<ve,e1>,v_const(c1)>); P(<<ve,e2>,v_const(c2)>) |] ==> \ |
|
235 \ P(<<ve,e1 @ e2>,v_const(c_app(c1,c2))>); \ |
|
236 \ !!ve vem xm e1 e2 em v v2. \ |
|
237 \ [| P(<<ve,e1>,v_clos(<|xm,em,vem|>)>); \ |
|
238 \ P(<<ve,e2>,v2>); \ |
|
239 \ P(<<vem + {xm |-> v2},em>,v>) \ |
|
240 \ |] ==> \ |
|
241 \ P(<<ve,e1 @ e2>,v>) \ |
|
242 \ |] ==> \ |
|
243 \ P(<<ve,e>,v>)"; |
|
244 by (resolve_tac (prems RL [lfp_ind2]) 1); |
|
245 by (rtac eval_fun_mono 1); |
|
246 by (rewtac eval_fun_def); |
|
247 by (dtac CollectD 1); |
|
248 by (safe_tac HOL_cs); |
|
249 by (ALLGOALS (resolve_tac prems)); |
|
250 by (ALLGOALS (fast_tac set_cs)); |
|
251 qed "eval_ind0"; |
|
252 |
|
253 val prems = goal MT.thy |
|
254 " [| ve |- e ---> v; \ |
|
255 \ !!ve c. P(ve,e_const(c),v_const(c)); \ |
|
256 \ !!ev ve. ev:ve_dom(ve) ==> P(ve,e_var(ev),ve_app(ve,ev)); \ |
|
257 \ !!ev ve e. P(ve,fn ev => e,v_clos(<|ev,e,ve|>)); \ |
|
258 \ !!ev1 ev2 ve cl e. \ |
|
259 \ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \ |
|
260 \ P(ve,fix ev2(ev1) = e,v_clos(cl)); \ |
|
261 \ !!ve c1 c2 e1 e2. \ |
|
262 \ [| P(ve,e1,v_const(c1)); P(ve,e2,v_const(c2)) |] ==> \ |
|
263 \ P(ve,e1 @ e2,v_const(c_app(c1,c2))); \ |
|
264 \ !!ve vem evm e1 e2 em v v2. \ |
|
265 \ [| P(ve,e1,v_clos(<|evm,em,vem|>)); \ |
|
266 \ P(ve,e2,v2); \ |
|
267 \ P(vem + {evm |-> v2},em,v) \ |
|
268 \ |] ==> P(ve,e1 @ e2,v) \ |
|
269 \ |] ==> P(ve,e,v)"; |
|
270 by (res_inst_tac [("P","P")] infsys_pp2 1); |
|
271 by (rtac eval_ind0 1); |
|
272 by (ALLGOALS (rtac infsys_pp1)); |
|
273 by (ALLGOALS (resolve_tac prems)); |
|
274 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); |
|
275 qed "eval_ind"; |
|
276 |
|
277 (* ############################################################ *) |
|
278 (* Elaborations *) |
|
279 (* ############################################################ *) |
|
280 |
|
281 goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)"; |
|
282 by infsys_mono_tac; |
|
283 qed "elab_fun_mono"; |
|
284 |
|
285 (* Introduction rules *) |
|
286 |
|
287 val prems = goalw MT.thy [elab_def, elab_rel_def] |
|
288 "c isof ty ==> te |- e_const(c) ===> ty"; |
|
289 by (cut_facts_tac prems 1); |
|
290 by (rtac lfp_intro2 1); |
|
291 by (rtac elab_fun_mono 1); |
|
292 by (rewtac elab_fun_def); |
|
293 by (fast_tac set_cs 1); |
|
294 qed "elab_const"; |
|
295 |
|
296 val prems = goalw MT.thy [elab_def, elab_rel_def] |
|
297 "x:te_dom(te) ==> te |- e_var(x) ===> te_app(te,x)"; |
|
298 by (cut_facts_tac prems 1); |
|
299 by (rtac lfp_intro2 1); |
|
300 by (rtac elab_fun_mono 1); |
|
301 by (rewtac elab_fun_def); |
|
302 by (fast_tac set_cs 1); |
|
303 qed "elab_var"; |
|
304 |
|
305 val prems = goalw MT.thy [elab_def, elab_rel_def] |
|
306 "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2"; |
|
307 by (cut_facts_tac prems 1); |
|
308 by (rtac lfp_intro2 1); |
|
309 by (rtac elab_fun_mono 1); |
|
310 by (rewtac elab_fun_def); |
|
311 by (fast_tac set_cs 1); |
|
312 qed "elab_fn"; |
|
313 |
|
314 val prems = goalw MT.thy [elab_def, elab_rel_def] |
|
315 " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \ |
|
316 \ te |- fix f(x) = e ===> ty1->ty2"; |
|
317 by (cut_facts_tac prems 1); |
|
318 by (rtac lfp_intro2 1); |
|
319 by (rtac elab_fun_mono 1); |
|
320 by (rewtac elab_fun_def); |
|
321 by (rtac CollectI 1); |
|
322 by (rtac disjI2 1); |
|
323 by (rtac disjI2 1); |
|
324 by (rtac disjI2 1); |
|
325 by (rtac disjI1 1); |
|
326 by (fast_tac HOL_cs 1); |
|
327 qed "elab_fix"; |
|
328 |
|
329 val prems = goalw MT.thy [elab_def, elab_rel_def] |
|
330 " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \ |
|
331 \ te |- e1 @ e2 ===> ty2"; |
|
332 by (cut_facts_tac prems 1); |
|
333 by (rtac lfp_intro2 1); |
|
334 by (rtac elab_fun_mono 1); |
|
335 by (rewtac elab_fun_def); |
|
336 by (fast_tac (set_cs addSIs [disjI2]) 1); |
|
337 qed "elab_app"; |
|
338 |
|
339 (* Strong elimination, induction on elaborations *) |
|
340 |
|
341 val prems = goalw MT.thy [elab_def, elab_rel_def] |
|
342 " [| te |- e ===> t; \ |
|
343 \ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \ |
|
344 \ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app(te,x)>); \ |
|
345 \ !!te x e t1 t2. \ |
|
346 \ [| te + {x |=> t1} |- e ===> t2; P(<<te + {x |=> t1},e>,t2>) |] ==> \ |
|
347 \ P(<<te,fn x => e>,t1->t2>); \ |
|
348 \ !!te f x e t1 t2. \ |
|
349 \ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \ |
|
350 \ P(<<te + {f |=> t1->t2} + {x |=> t1},e>,t2>) \ |
|
351 \ |] ==> \ |
|
352 \ P(<<te,fix f(x) = e>,t1->t2>); \ |
|
353 \ !!te e1 e2 t1 t2. \ |
|
354 \ [| te |- e1 ===> t1->t2; P(<<te,e1>,t1->t2>); \ |
|
355 \ te |- e2 ===> t1; P(<<te,e2>,t1>) \ |
|
356 \ |] ==> \ |
|
357 \ P(<<te,e1 @ e2>,t2>) \ |
|
358 \ |] ==> \ |
|
359 \ P(<<te,e>,t>)"; |
|
360 by (resolve_tac (prems RL [lfp_ind2]) 1); |
|
361 by (rtac elab_fun_mono 1); |
|
362 by (rewtac elab_fun_def); |
|
363 by (dtac CollectD 1); |
|
364 by (safe_tac HOL_cs); |
|
365 by (ALLGOALS (resolve_tac prems)); |
|
366 by (ALLGOALS (fast_tac set_cs)); |
|
367 qed "elab_ind0"; |
|
368 |
|
369 val prems = goal MT.thy |
|
370 " [| te |- e ===> t; \ |
|
371 \ !!te c t. c isof t ==> P(te,e_const(c),t); \ |
|
372 \ !!te x. x:te_dom(te) ==> P(te,e_var(x),te_app(te,x)); \ |
|
373 \ !!te x e t1 t2. \ |
|
374 \ [| te + {x |=> t1} |- e ===> t2; P(te + {x |=> t1},e,t2) |] ==> \ |
|
375 \ P(te,fn x => e,t1->t2); \ |
|
376 \ !!te f x e t1 t2. \ |
|
377 \ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \ |
|
378 \ P(te + {f |=> t1->t2} + {x |=> t1},e,t2) \ |
|
379 \ |] ==> \ |
|
380 \ P(te,fix f(x) = e,t1->t2); \ |
|
381 \ !!te e1 e2 t1 t2. \ |
|
382 \ [| te |- e1 ===> t1->t2; P(te,e1,t1->t2); \ |
|
383 \ te |- e2 ===> t1; P(te,e2,t1) \ |
|
384 \ |] ==> \ |
|
385 \ P(te,e1 @ e2,t2) \ |
|
386 \ |] ==> \ |
|
387 \ P(te,e,t)"; |
|
388 by (res_inst_tac [("P","P")] infsys_pp2 1); |
|
389 by (rtac elab_ind0 1); |
|
390 by (ALLGOALS (rtac infsys_pp1)); |
|
391 by (ALLGOALS (resolve_tac prems)); |
|
392 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); |
|
393 qed "elab_ind"; |
|
394 |
|
395 (* Weak elimination, case analysis on elaborations *) |
|
396 |
|
397 val prems = goalw MT.thy [elab_def, elab_rel_def] |
|
398 " [| te |- e ===> t; \ |
|
399 \ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \ |
|
400 \ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app(te,x)>); \ |
|
401 \ !!te x e t1 t2. \ |
|
402 \ te + {x |=> t1} |- e ===> t2 ==> P(<<te,fn x => e>,t1->t2>); \ |
|
403 \ !!te f x e t1 t2. \ |
|
404 \ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \ |
|
405 \ P(<<te,fix f(x) = e>,t1->t2>); \ |
|
406 \ !!te e1 e2 t1 t2. \ |
|
407 \ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \ |
|
408 \ P(<<te,e1 @ e2>,t2>) \ |
|
409 \ |] ==> \ |
|
410 \ P(<<te,e>,t>)"; |
|
411 by (resolve_tac (prems RL [lfp_elim2]) 1); |
|
412 by (rtac elab_fun_mono 1); |
|
413 by (rewtac elab_fun_def); |
|
414 by (dtac CollectD 1); |
|
415 by (safe_tac HOL_cs); |
|
416 by (ALLGOALS (resolve_tac prems)); |
|
417 by (ALLGOALS (fast_tac set_cs)); |
|
418 qed "elab_elim0"; |
|
419 |
|
420 val prems = goal MT.thy |
|
421 " [| te |- e ===> t; \ |
|
422 \ !!te c t. c isof t ==> P(te,e_const(c),t); \ |
|
423 \ !!te x. x:te_dom(te) ==> P(te,e_var(x),te_app(te,x)); \ |
|
424 \ !!te x e t1 t2. \ |
|
425 \ te + {x |=> t1} |- e ===> t2 ==> P(te,fn x => e,t1->t2); \ |
|
426 \ !!te f x e t1 t2. \ |
|
427 \ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \ |
|
428 \ P(te,fix f(x) = e,t1->t2); \ |
|
429 \ !!te e1 e2 t1 t2. \ |
|
430 \ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \ |
|
431 \ P(te,e1 @ e2,t2) \ |
|
432 \ |] ==> \ |
|
433 \ P(te,e,t)"; |
|
434 by (res_inst_tac [("P","P")] infsys_pp2 1); |
|
435 by (rtac elab_elim0 1); |
|
436 by (ALLGOALS (rtac infsys_pp1)); |
|
437 by (ALLGOALS (resolve_tac prems)); |
|
438 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); |
|
439 qed "elab_elim"; |
|
440 |
|
441 (* Elimination rules for each expression *) |
|
442 |
|
443 fun elab_e_elim_tac p = |
|
444 ( (rtac elab_elim 1) THEN |
|
445 (resolve_tac p 1) THEN |
|
446 (REPEAT (fast_tac (e_ext_cs HOL_cs) 1)) |
|
447 ); |
|
448 |
|
449 val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)"; |
|
450 by (elab_e_elim_tac prems); |
|
451 qed "elab_const_elim_lem"; |
|
452 |
|
453 val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t"; |
|
454 by (cut_facts_tac prems 1); |
|
455 by (dtac elab_const_elim_lem 1); |
|
456 by (fast_tac prop_cs 1); |
|
457 qed "elab_const_elim"; |
|
458 |
|
459 val prems = goal MT.thy |
|
460 "te |- e ===> t ==> (e = e_var(x) --> t=te_app(te,x) & x:te_dom(te))"; |
|
461 by (elab_e_elim_tac prems); |
|
462 qed "elab_var_elim_lem"; |
|
463 |
|
464 val prems = goal MT.thy |
|
465 "te |- e_var(ev) ===> t ==> t=te_app(te,ev) & ev : te_dom(te)"; |
|
466 by (cut_facts_tac prems 1); |
|
467 by (dtac elab_var_elim_lem 1); |
|
468 by (fast_tac prop_cs 1); |
|
469 qed "elab_var_elim"; |
|
470 |
|
471 val prems = goal MT.thy |
|
472 " te |- e ===> t ==> \ |
|
473 \ ( e = fn x1 => e1 --> \ |
|
474 \ (? t1 t2.t=t_fun(t1,t2) & te + {x1 |=> t1} |- e1 ===> t2) \ |
|
475 \ )"; |
|
476 by (elab_e_elim_tac prems); |
|
477 qed "elab_fn_elim_lem"; |
|
478 |
|
479 val prems = goal MT.thy |
|
480 " te |- fn x1 => e1 ===> t ==> \ |
|
481 \ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)"; |
|
482 by (cut_facts_tac prems 1); |
|
483 by (dtac elab_fn_elim_lem 1); |
|
484 by (fast_tac prop_cs 1); |
|
485 qed "elab_fn_elim"; |
|
486 |
|
487 val prems = goal MT.thy |
|
488 " te |- e ===> t ==> \ |
|
489 \ (e = fix f(x) = e1 --> \ |
|
490 \ (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; |
|
491 by (elab_e_elim_tac prems); |
|
492 qed "elab_fix_elim_lem"; |
|
493 |
|
494 val prems = goal MT.thy |
|
495 " te |- fix ev1(ev2) = e1 ===> t ==> \ |
|
496 \ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)"; |
|
497 by (cut_facts_tac prems 1); |
|
498 by (dtac elab_fix_elim_lem 1); |
|
499 by (fast_tac prop_cs 1); |
|
500 qed "elab_fix_elim"; |
|
501 |
|
502 val prems = goal MT.thy |
|
503 " te |- e ===> t2 ==> \ |
|
504 \ (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; |
|
505 by (elab_e_elim_tac prems); |
|
506 qed "elab_app_elim_lem"; |
|
507 |
|
508 val prems = goal MT.thy |
|
509 "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; |
|
510 by (cut_facts_tac prems 1); |
|
511 by (dtac elab_app_elim_lem 1); |
|
512 by (fast_tac prop_cs 1); |
|
513 qed "elab_app_elim"; |
|
514 |
|
515 (* ############################################################ *) |
|
516 (* The extended correspondence relation *) |
|
517 (* ############################################################ *) |
|
518 |
|
519 (* Monotonicity of hasty_fun *) |
|
520 |
|
521 goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)"; |
|
522 by infsys_mono_tac; |
|
523 bind_thm("mono_hasty_fun", result()); |
|
524 |
|
525 (* |
|
526 Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it |
|
527 enjoys two strong indtroduction (co-induction) rules and an elimination rule. |
|
528 *) |
|
529 |
|
530 (* First strong indtroduction (co-induction) rule for hasty_rel *) |
|
531 |
|
532 val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> <v_const(c),t> : hasty_rel"; |
|
533 by (cut_facts_tac prems 1); |
|
534 by (rtac gfp_coind2 1); |
|
535 by (rewtac MT.hasty_fun_def); |
|
536 by (rtac CollectI 1); |
|
537 by (rtac disjI1 1); |
|
538 by (fast_tac HOL_cs 1); |
|
539 by (rtac mono_hasty_fun 1); |
|
540 qed "hasty_rel_const_coind"; |
|
541 |
|
542 (* Second strong introduction (co-induction) rule for hasty_rel *) |
|
543 |
|
544 val prems = goalw MT.thy [hasty_rel_def] |
|
545 " [| te |- fn ev => e ===> t; \ |
|
546 \ ve_dom(ve) = te_dom(te); \ |
|
547 \ ! ev1. \ |
|
548 \ ev1:ve_dom(ve) --> \ |
|
549 \ <ve_app(ve,ev1),te_app(te,ev1)> : {<v_clos(<|ev,e,ve|>),t>} Un hasty_rel \ |
|
550 \ |] ==> \ |
|
551 \ <v_clos(<|ev,e,ve|>),t> : hasty_rel"; |
|
552 by (cut_facts_tac prems 1); |
|
553 by (rtac gfp_coind2 1); |
|
554 by (rewtac hasty_fun_def); |
|
555 by (rtac CollectI 1); |
|
556 by (rtac disjI2 1); |
|
557 by (fast_tac HOL_cs 1); |
|
558 by (rtac mono_hasty_fun 1); |
|
559 qed "hasty_rel_clos_coind"; |
|
560 |
|
561 (* Elimination rule for hasty_rel *) |
|
562 |
|
563 val prems = goalw MT.thy [hasty_rel_def] |
|
564 " [| !! c t.c isof t ==> P(<v_const(c),t>); \ |
|
565 \ !! te ev e t ve. \ |
|
566 \ [| te |- fn ev => e ===> t; \ |
|
567 \ ve_dom(ve) = te_dom(te); \ |
|
568 \ !ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : hasty_rel \ |
|
569 \ |] ==> P(<v_clos(<|ev,e,ve|>),t>); \ |
|
570 \ <v,t> : hasty_rel \ |
|
571 \ |] ==> P(<v,t>)"; |
|
572 by (cut_facts_tac prems 1); |
|
573 by (etac gfp_elim2 1); |
|
574 by (rtac mono_hasty_fun 1); |
|
575 by (rewtac hasty_fun_def); |
|
576 by (dtac CollectD 1); |
|
577 by (fold_goals_tac [hasty_fun_def]); |
|
578 by (safe_tac HOL_cs); |
|
579 by (ALLGOALS (resolve_tac prems)); |
|
580 by (ALLGOALS (fast_tac set_cs)); |
|
581 qed "hasty_rel_elim0"; |
|
582 |
|
583 val prems = goal MT.thy |
|
584 " [| <v,t> : hasty_rel; \ |
|
585 \ !! c t.c isof t ==> P(v_const(c),t); \ |
|
586 \ !! te ev e t ve. \ |
|
587 \ [| te |- fn ev => e ===> t; \ |
|
588 \ ve_dom(ve) = te_dom(te); \ |
|
589 \ !ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : hasty_rel \ |
|
590 \ |] ==> P(v_clos(<|ev,e,ve|>),t) \ |
|
591 \ |] ==> P(v,t)"; |
|
592 by (res_inst_tac [("P","P")] infsys_p2 1); |
|
593 by (rtac hasty_rel_elim0 1); |
|
594 by (ALLGOALS (rtac infsys_p1)); |
|
595 by (ALLGOALS (resolve_tac prems)); |
|
596 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1))); |
|
597 qed "hasty_rel_elim"; |
|
598 |
|
599 (* Introduction rules for hasty *) |
|
600 |
|
601 val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t"; |
|
602 by (resolve_tac (prems RL [hasty_rel_const_coind]) 1); |
|
603 qed "hasty_const"; |
|
604 |
|
605 val prems = goalw MT.thy [hasty_def,hasty_env_def] |
|
606 "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t"; |
|
607 by (cut_facts_tac prems 1); |
|
608 by (rtac hasty_rel_clos_coind 1); |
|
609 by (ALLGOALS (fast_tac set_cs)); |
|
610 qed "hasty_clos"; |
|
611 |
|
612 (* Elimination on constants for hasty *) |
|
613 |
|
614 val prems = goalw MT.thy [hasty_def] |
|
615 "v hasty t ==> (!c.(v = v_const(c) --> c isof t))"; |
|
616 by (cut_facts_tac prems 1); |
|
617 by (rtac hasty_rel_elim 1); |
|
618 by (ALLGOALS (fast_tac (v_ext_cs HOL_cs))); |
|
619 qed "hasty_elim_const_lem"; |
|
620 |
|
621 val prems = goal MT.thy "v_const(c) hasty t ==> c isof t"; |
|
622 by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1); |
|
623 by (fast_tac HOL_cs 1); |
|
624 qed "hasty_elim_const"; |
|
625 |
|
626 (* Elimination on closures for hasty *) |
|
627 |
|
628 val prems = goalw MT.thy [hasty_env_def,hasty_def] |
|
629 " v hasty t ==> \ |
|
630 \ ! x e ve. \ |
|
631 \ v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)"; |
|
632 by (cut_facts_tac prems 1); |
|
633 by (rtac hasty_rel_elim 1); |
|
634 by (ALLGOALS (fast_tac (v_ext_cs HOL_cs))); |
|
635 qed "hasty_elim_clos_lem"; |
|
636 |
|
637 val prems = goal MT.thy |
|
638 "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===> t & ve hastyenv te "; |
|
639 by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1); |
|
640 by (fast_tac HOL_cs 1); |
|
641 qed "hasty_elim_clos"; |
|
642 |
|
643 (* ############################################################ *) |
|
644 (* The pointwise extension of hasty to environments *) |
|
645 (* ############################################################ *) |
|
646 |
|
647 goal MT.thy |
|
648 "!!ve. [| ve hastyenv te; v hasty t |] ==> \ |
|
649 \ ve + {ev |-> v} hastyenv te + {ev |=> t}"; |
|
650 by (rewtac hasty_env_def); |
|
651 by (asm_full_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1); |
|
652 by (safe_tac HOL_cs); |
|
653 by (excluded_middle_tac "ev=x" 1); |
|
654 by (asm_full_simp_tac (HOL_ss addsimps [ve_app_owr2, te_app_owr2]) 1); |
|
655 by (fast_tac set_cs 1); |
|
656 by (asm_simp_tac (HOL_ss addsimps [ve_app_owr1, te_app_owr1]) 1); |
|
657 qed "hasty_env1"; |
|
658 |
|
659 (* ############################################################ *) |
|
660 (* The Consistency theorem *) |
|
661 (* ############################################################ *) |
|
662 |
|
663 val prems = goal MT.thy |
|
664 "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t"; |
|
665 by (cut_facts_tac prems 1); |
|
666 by (dtac elab_const_elim 1); |
|
667 by (etac hasty_const 1); |
|
668 qed "consistency_const"; |
|
669 |
|
670 val prems = goalw MT.thy [hasty_env_def] |
|
671 " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \ |
|
672 \ ve_app(ve,ev) hasty t"; |
|
673 by (cut_facts_tac prems 1); |
|
674 by (dtac elab_var_elim 1); |
|
675 by (fast_tac HOL_cs 1); |
|
676 qed "consistency_var"; |
|
677 |
|
678 val prems = goal MT.thy |
|
679 " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \ |
|
680 \ v_clos(<| ev, e, ve |>) hasty t"; |
|
681 by (cut_facts_tac prems 1); |
|
682 by (rtac hasty_clos 1); |
|
683 by (fast_tac prop_cs 1); |
|
684 qed "consistency_fn"; |
|
685 |
|
686 val prems = goalw MT.thy [hasty_env_def,hasty_def] |
|
687 " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \ |
|
688 \ ve hastyenv te ; \ |
|
689 \ te |- fix ev2 ev1 = e ===> t \ |
|
690 \ |] ==> \ |
|
691 \ v_clos(cl) hasty t"; |
|
692 by (cut_facts_tac prems 1); |
|
693 by (dtac elab_fix_elim 1); |
|
694 by (safe_tac HOL_cs); |
|
695 (*Do a single unfolding of cl*) |
|
696 by ((forward_tac [ssubst] 1) THEN (assume_tac 2)); |
|
697 by (rtac hasty_rel_clos_coind 1); |
|
698 by (etac elab_fn 1); |
|
699 by (asm_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1); |
|
700 |
|
701 by (asm_simp_tac (HOL_ss addsimps [ve_dom_owr]) 1); |
|
702 by (safe_tac HOL_cs); |
|
703 by (excluded_middle_tac "ev2=ev1a" 1); |
|
704 by (asm_full_simp_tac (HOL_ss addsimps [ve_app_owr2, te_app_owr2]) 1); |
|
705 by (fast_tac set_cs 1); |
|
706 |
|
707 by (asm_simp_tac (HOL_ss addsimps [ve_app_owr1, te_app_owr1]) 1); |
|
708 by (hyp_subst_tac 1); |
|
709 by (etac subst 1); |
|
710 by (fast_tac set_cs 1); |
|
711 qed "consistency_fix"; |
|
712 |
|
713 val prems = goal MT.thy |
|
714 " [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t; \ |
|
715 \ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \ |
|
716 \ ve hastyenv te ; te |- e1 @ e2 ===> t \ |
|
717 \ |] ==> \ |
|
718 \ v_const(c_app(c1,c2)) hasty t"; |
|
719 by (cut_facts_tac prems 1); |
|
720 by (dtac elab_app_elim 1); |
|
721 by (safe_tac HOL_cs); |
|
722 by (rtac hasty_const 1); |
|
723 by (rtac isof_app 1); |
|
724 by (rtac hasty_elim_const 1); |
|
725 by (fast_tac HOL_cs 1); |
|
726 by (rtac hasty_elim_const 1); |
|
727 by (fast_tac HOL_cs 1); |
|
728 qed "consistency_app1"; |
|
729 |
|
730 val prems = goal MT.thy |
|
731 " [| ! t te. \ |
|
732 \ ve hastyenv te --> \ |
|
733 \ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \ |
|
734 \ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \ |
|
735 \ ! t te. \ |
|
736 \ vem + { evm |-> v2 } hastyenv te --> te |- em ===> t --> v hasty t; \ |
|
737 \ ve hastyenv te ; \ |
|
738 \ te |- e1 @ e2 ===> t \ |
|
739 \ |] ==> \ |
|
740 \ v hasty t"; |
|
741 by (cut_facts_tac prems 1); |
|
742 by (dtac elab_app_elim 1); |
|
743 by (safe_tac HOL_cs); |
|
744 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1)); |
|
745 by (assume_tac 1); |
|
746 by (etac impE 1); |
|
747 by (assume_tac 1); |
|
748 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1)); |
|
749 by (assume_tac 1); |
|
750 by (etac impE 1); |
|
751 by (assume_tac 1); |
|
752 by (dtac hasty_elim_clos 1); |
|
753 by (safe_tac HOL_cs); |
|
754 by (dtac elab_fn_elim 1); |
|
755 by (safe_tac HOL_cs); |
|
756 by (dtac t_fun_inj 1); |
|
757 by (safe_tac prop_cs); |
|
758 by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1)); |
|
759 qed "consistency_app2"; |
|
760 |
|
761 val [major] = goal MT.thy |
|
762 "ve |- e ---> v ==> \ |
|
763 \ (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)"; |
|
764 |
|
765 (* Proof by induction on the structure of evaluations *) |
|
766 |
|
767 by (rtac (major RS eval_ind) 1); |
|
768 by (safe_tac HOL_cs); |
|
769 by (DEPTH_SOLVE |
|
770 (ares_tac [consistency_const, consistency_var, consistency_fn, |
|
771 consistency_fix, consistency_app1, consistency_app2] 1)); |
|
772 qed "consistency"; |
|
773 |
|
774 (* ############################################################ *) |
|
775 (* The Basic Consistency theorem *) |
|
776 (* ############################################################ *) |
|
777 |
|
778 val prems = goalw MT.thy [isof_env_def,hasty_env_def] |
|
779 "ve isofenv te ==> ve hastyenv te"; |
|
780 by (cut_facts_tac prems 1); |
|
781 by (safe_tac HOL_cs); |
|
782 by (etac allE 1); |
|
783 by (etac impE 1); |
|
784 by (assume_tac 1); |
|
785 by (etac exE 1); |
|
786 by (etac conjE 1); |
|
787 by (dtac hasty_const 1); |
|
788 by (asm_simp_tac HOL_ss 1); |
|
789 qed "basic_consistency_lem"; |
|
790 |
|
791 val prems = goal MT.thy |
|
792 "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t"; |
|
793 by (cut_facts_tac prems 1); |
|
794 by (rtac hasty_elim_const 1); |
|
795 by (dtac consistency 1); |
|
796 by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1); |
|
797 qed "basic_consistency"; |
|
798 |
|
799 |
|