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