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