author | paulson |
Tue, 23 May 2000 18:08:52 +0200 | |
changeset 8936 | a1c426541757 |
parent 8114 | 09a7a180cc99 |
child 10202 | 9e8b4bebc940 |
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 |
||
5278 | 442 |
Goal " te |- fn x1 => e1 ===> t ==> \ |
969 | 443 |
\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)"; |
444 |
by (dtac elab_fn_elim_lem 1); |
|
2935 | 445 |
by (Blast_tac 1); |
969 | 446 |
qed "elab_fn_elim"; |
447 |
||
448 |
val prems = goal MT.thy |
|
449 |
" te |- e ===> t ==> \ |
|
450 |
\ (e = fix f(x) = e1 --> \ |
|
451 |
\ (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; |
|
452 |
by (elab_e_elim_tac prems); |
|
453 |
qed "elab_fix_elim_lem"; |
|
454 |
||
5278 | 455 |
Goal " te |- fix ev1(ev2) = e1 ===> t ==> \ |
969 | 456 |
\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)"; |
457 |
by (dtac elab_fix_elim_lem 1); |
|
2935 | 458 |
by (Blast_tac 1); |
969 | 459 |
qed "elab_fix_elim"; |
460 |
||
461 |
val prems = goal MT.thy |
|
462 |
" te |- e ===> t2 ==> \ |
|
463 |
\ (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; |
|
464 |
by (elab_e_elim_tac prems); |
|
465 |
qed "elab_app_elim_lem"; |
|
466 |
||
5278 | 467 |
Goal "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; |
969 | 468 |
by (dtac elab_app_elim_lem 1); |
2935 | 469 |
by (Blast_tac 1); |
969 | 470 |
qed "elab_app_elim"; |
471 |
||
472 |
(* ############################################################ *) |
|
473 |
(* The extended correspondence relation *) |
|
474 |
(* ############################################################ *) |
|
475 |
||
476 |
(* Monotonicity of hasty_fun *) |
|
477 |
||
5069 | 478 |
Goalw [mono_def,MT.hasty_fun_def] "mono(hasty_fun)"; |
969 | 479 |
by infsys_mono_tac; |
2935 | 480 |
by (Blast_tac 1); |
481 |
qed "mono_hasty_fun"; |
|
969 | 482 |
|
483 |
(* |
|
484 |
Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it |
|
485 |
enjoys two strong indtroduction (co-induction) rules and an elimination rule. |
|
486 |
*) |
|
487 |
||
488 |
(* First strong indtroduction (co-induction) rule for hasty_rel *) |
|
489 |
||
5069 | 490 |
Goalw [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel"; |
969 | 491 |
by (rtac gfp_coind2 1); |
492 |
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
|
493 |
by (rtac CollectI 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
494 |
by (rtac disjI1 1); |
2935 | 495 |
by (Blast_tac 1); |
969 | 496 |
by (rtac mono_hasty_fun 1); |
497 |
qed "hasty_rel_const_coind"; |
|
498 |
||
499 |
(* Second strong introduction (co-induction) rule for hasty_rel *) |
|
500 |
||
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
501 |
Goalw [hasty_rel_def] |
969 | 502 |
" [| te |- fn ev => e ===> t; \ |
503 |
\ ve_dom(ve) = te_dom(te); \ |
|
504 |
\ ! ev1. \ |
|
505 |
\ ev1:ve_dom(ve) --> \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset
|
506 |
\ (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \ |
969 | 507 |
\ |] ==> \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset
|
508 |
\ (v_clos(<|ev,e,ve|>),t) : hasty_rel"; |
969 | 509 |
by (rtac gfp_coind2 1); |
510 |
by (rewtac hasty_fun_def); |
|
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
511 |
by (rtac CollectI 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
512 |
by (rtac disjI2 1); |
2935 | 513 |
by (blast_tac HOL_cs 1); |
969 | 514 |
by (rtac mono_hasty_fun 1); |
515 |
qed "hasty_rel_clos_coind"; |
|
516 |
||
517 |
(* Elimination rule for hasty_rel *) |
|
518 |
||
519 |
val prems = goalw MT.thy [hasty_rel_def] |
|
3842 | 520 |
" [| !! c t. c isof t ==> P((v_const(c),t)); \ |
969 | 521 |
\ !! te ev e t ve. \ |
522 |
\ [| te |- fn ev => e ===> t; \ |
|
523 |
\ ve_dom(ve) = te_dom(te); \ |
|
3842 | 524 |
\ !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
|
525 |
\ |] ==> P((v_clos(<|ev,e,ve|>),t)); \ |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset
|
526 |
\ (v,t) : hasty_rel \ |
8114 | 527 |
\ |] ==> P(v,t)"; |
969 | 528 |
by (cut_facts_tac prems 1); |
529 |
by (etac gfp_elim2 1); |
|
530 |
by (rtac mono_hasty_fun 1); |
|
531 |
by (rewtac hasty_fun_def); |
|
532 |
by (dtac CollectD 1); |
|
533 |
by (fold_goals_tac [hasty_fun_def]); |
|
4153 | 534 |
by Safe_tac; |
2935 | 535 |
by (REPEAT (ares_tac prems 1)); |
969 | 536 |
qed "hasty_rel_elim0"; |
537 |
||
538 |
val prems = goal MT.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset
|
539 |
" [| (v,t) : hasty_rel; \ |
3842 | 540 |
\ !! c t. c isof t ==> P (v_const c) t; \ |
969 | 541 |
\ !! te ev e t ve. \ |
542 |
\ [| te |- fn ev => e ===> t; \ |
|
543 |
\ ve_dom(ve) = te_dom(te); \ |
|
3842 | 544 |
\ !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \ |
969 | 545 |
\ |] ==> P (v_clos <|ev,e,ve|>) t \ |
546 |
\ |] ==> P v t"; |
|
547 |
by (res_inst_tac [("P","P")] infsys_p2 1); |
|
548 |
by (rtac hasty_rel_elim0 1); |
|
549 |
by (ALLGOALS (rtac infsys_p1)); |
|
550 |
by (ALLGOALS (resolve_tac prems)); |
|
551 |
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1))); |
|
552 |
qed "hasty_rel_elim"; |
|
553 |
||
554 |
(* Introduction rules for hasty *) |
|
555 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
556 |
Goalw [hasty_def] "c isof t ==> v_const(c) hasty t"; |
2935 | 557 |
by (etac hasty_rel_const_coind 1); |
969 | 558 |
qed "hasty_const"; |
559 |
||
5069 | 560 |
Goalw [hasty_def,hasty_env_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
561 |
"te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t"; |
969 | 562 |
by (rtac hasty_rel_clos_coind 1); |
4089 | 563 |
by (ALLGOALS (blast_tac (claset() delrules [equalityI]))); |
969 | 564 |
qed "hasty_clos"; |
565 |
||
566 |
(* Elimination on constants for hasty *) |
|
567 |
||
5069 | 568 |
Goalw [hasty_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
569 |
"v hasty t ==> (!c.(v = v_const(c) --> c isof t))"; |
969 | 570 |
by (rtac hasty_rel_elim 1); |
2935 | 571 |
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs))); |
969 | 572 |
qed "hasty_elim_const_lem"; |
573 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
574 |
Goal "v_const(c) hasty t ==> c isof t"; |
2935 | 575 |
by (dtac hasty_elim_const_lem 1); |
576 |
by (Blast_tac 1); |
|
969 | 577 |
qed "hasty_elim_const"; |
578 |
||
579 |
(* Elimination on closures for hasty *) |
|
580 |
||
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
581 |
Goalw [hasty_env_def,hasty_def] |
969 | 582 |
" v hasty t ==> \ |
583 |
\ ! x e ve. \ |
|
3842 | 584 |
\ v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)"; |
969 | 585 |
by (rtac hasty_rel_elim 1); |
2935 | 586 |
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs))); |
969 | 587 |
qed "hasty_elim_clos_lem"; |
588 |
||
5278 | 589 |
Goal "v_clos(<|ev,e,ve|>) hasty t ==> \ |
3842 | 590 |
\ ? te. te |- fn ev => e ===> t & ve hastyenv te "; |
2935 | 591 |
by (dtac hasty_elim_clos_lem 1); |
592 |
by (Blast_tac 1); |
|
969 | 593 |
qed "hasty_elim_clos"; |
594 |
||
595 |
(* ############################################################ *) |
|
596 |
(* The pointwise extension of hasty to environments *) |
|
597 |
(* ############################################################ *) |
|
598 |
||
5278 | 599 |
Goal "[| 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
|
600 |
\ 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
|
601 |
by (rewtac hasty_env_def); |
4089 | 602 |
by (asm_full_simp_tac (simpset() delsimps mem_simps |
1266 | 603 |
addsimps [ve_dom_owr, te_dom_owr]) 1); |
2935 | 604 |
by (safe_tac HOL_cs); |
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
605 |
by (excluded_middle_tac "ev=x" 1); |
4089 | 606 |
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1); |
2935 | 607 |
by (Blast_tac 1); |
4089 | 608 |
by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1); |
969 | 609 |
qed "hasty_env1"; |
610 |
||
611 |
(* ############################################################ *) |
|
612 |
(* The Consistency theorem *) |
|
613 |
(* ############################################################ *) |
|
614 |
||
5278 | 615 |
Goal "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t"; |
969 | 616 |
by (dtac elab_const_elim 1); |
617 |
by (etac hasty_const 1); |
|
618 |
qed "consistency_const"; |
|
619 |
||
5069 | 620 |
Goalw [hasty_env_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
621 |
"[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \ |
2935 | 622 |
\ ve_app ve ev hasty t"; |
969 | 623 |
by (dtac elab_var_elim 1); |
2935 | 624 |
by (Blast_tac 1); |
969 | 625 |
qed "consistency_var"; |
626 |
||
5278 | 627 |
Goal "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \ |
2935 | 628 |
\ v_clos(<| ev, e, ve |>) hasty t"; |
969 | 629 |
by (rtac hasty_clos 1); |
2935 | 630 |
by (Blast_tac 1); |
969 | 631 |
qed "consistency_fn"; |
632 |
||
5069 | 633 |
Goalw [hasty_env_def,hasty_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
634 |
"[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \ |
969 | 635 |
\ ve hastyenv te ; \ |
636 |
\ te |- fix ev2 ev1 = e ===> t \ |
|
637 |
\ |] ==> \ |
|
638 |
\ v_clos(cl) hasty t"; |
|
639 |
by (dtac elab_fix_elim 1); |
|
2935 | 640 |
by (safe_tac HOL_cs); |
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
641 |
(*Do a single unfolding of cl*) |
7499 | 642 |
by ((ftac ssubst 1) THEN (assume_tac 2)); |
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
643 |
by (rtac hasty_rel_clos_coind 1); |
969 | 644 |
by (etac elab_fn 1); |
4089 | 645 |
by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1); |
969 | 646 |
|
4089 | 647 |
by (asm_simp_tac (simpset() delsimps mem_simps addsimps [ve_dom_owr]) 1); |
2935 | 648 |
by (safe_tac HOL_cs); |
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
649 |
by (excluded_middle_tac "ev2=ev1a" 1); |
4089 | 650 |
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1); |
2935 | 651 |
by (Blast_tac 1); |
969 | 652 |
|
4089 | 653 |
by (asm_simp_tac (simpset() delsimps mem_simps |
1266 | 654 |
addsimps [ve_app_owr1, te_app_owr1]) 1); |
969 | 655 |
by (hyp_subst_tac 1); |
656 |
by (etac subst 1); |
|
2935 | 657 |
by (Blast_tac 1); |
969 | 658 |
qed "consistency_fix"; |
659 |
||
5278 | 660 |
Goal "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\ |
969 | 661 |
\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \ |
662 |
\ ve hastyenv te ; te |- e1 @ e2 ===> t \ |
|
663 |
\ |] ==> \ |
|
664 |
\ v_const(c_app c1 c2) hasty t"; |
|
665 |
by (dtac elab_app_elim 1); |
|
4153 | 666 |
by Safe_tac; |
969 | 667 |
by (rtac hasty_const 1); |
668 |
by (rtac isof_app 1); |
|
669 |
by (rtac hasty_elim_const 1); |
|
2935 | 670 |
by (Blast_tac 1); |
969 | 671 |
by (rtac hasty_elim_const 1); |
2935 | 672 |
by (Blast_tac 1); |
969 | 673 |
qed "consistency_app1"; |
674 |
||
5278 | 675 |
Goal "[| ! t te. \ |
969 | 676 |
\ ve hastyenv te --> \ |
677 |
\ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \ |
|
678 |
\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \ |
|
679 |
\ ! t te. \ |
|
680 |
\ vem + { evm |-> v2 } hastyenv te --> te |- em ===> t --> v hasty t; \ |
|
681 |
\ ve hastyenv te ; \ |
|
682 |
\ te |- e1 @ e2 ===> t \ |
|
683 |
\ |] ==> \ |
|
684 |
\ v hasty t"; |
|
685 |
by (dtac elab_app_elim 1); |
|
4153 | 686 |
by Safe_tac; |
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
687 |
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
|
688 |
by (assume_tac 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
689 |
by (etac impE 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
690 |
by (assume_tac 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
691 |
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
|
692 |
by (assume_tac 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
693 |
by (etac impE 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
694 |
by (assume_tac 1); |
969 | 695 |
by (dtac hasty_elim_clos 1); |
4153 | 696 |
by Safe_tac; |
969 | 697 |
by (dtac elab_fn_elim 1); |
4089 | 698 |
by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1); |
969 | 699 |
qed "consistency_app2"; |
700 |
||
5278 | 701 |
Goal "ve |- e ---> v ==> \ |
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
702 |
\ (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)"; |
969 | 703 |
|
704 |
(* Proof by induction on the structure of evaluations *) |
|
705 |
||
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
706 |
by (etac eval_ind 1); |
4153 | 707 |
by Safe_tac; |
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
708 |
by (DEPTH_SOLVE |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
709 |
(ares_tac [consistency_const, consistency_var, consistency_fn, |
1465 | 710 |
consistency_fix, consistency_app1, consistency_app2] 1)); |
969 | 711 |
qed "consistency"; |
712 |
||
713 |
(* ############################################################ *) |
|
714 |
(* The Basic Consistency theorem *) |
|
715 |
(* ############################################################ *) |
|
716 |
||
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
717 |
Goalw [isof_env_def,hasty_env_def] |
969 | 718 |
"ve isofenv te ==> ve hastyenv te"; |
4153 | 719 |
by Safe_tac; |
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
720 |
by (etac allE 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
721 |
by (etac impE 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
722 |
by (assume_tac 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
723 |
by (etac exE 1); |
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset
|
724 |
by (etac conjE 1); |
969 | 725 |
by (dtac hasty_const 1); |
1266 | 726 |
by (Asm_simp_tac 1); |
969 | 727 |
qed "basic_consistency_lem"; |
728 |
||
5278 | 729 |
Goal "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t"; |
969 | 730 |
by (rtac hasty_elim_const 1); |
731 |
by (dtac consistency 1); |
|
4089 | 732 |
by (blast_tac (claset() addSIs [basic_consistency_lem]) 1); |
969 | 733 |
qed "basic_consistency"; |
1584 | 734 |
|
735 |
writeln"Reached end of file."; |