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