author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10202  9e8b4bebc940 
child 15386  06757406d8cf 
permissions  rwrr 
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 
Coinduction in Relational Semantics, 

9 
Theoretical Computer Science 87 (1991), pages 209220. 

10 

11 
Written up as 

12 
Jacob Frost, A Case Study of Coinduction 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); 

10202  68 
by (etac lfp_induct 1); 
1047
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 (coinduction) rules and an elimination rule. 

486 
*) 

487 

488 
(* First strong indtroduction (coinduction) 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 (coinduction) 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."; 