author  wenzelm 
Mon, 03 Nov 1997 12:13:18 +0100  
changeset 4089  96fba19bcbe2 
parent 3842  b55686a7b22c 
child 4153  e534c4c32d54 
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 
open MT; 

19 

20 
(* ############################################################ *) 

21 
(* Inference systems *) 

22 
(* ############################################################ *) 

23 

2935  24 
val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1)); 
969  25 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

26 
val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))"; 
4089  27 
by (simp_tac (simpset() addsimps prems) 1); 
969  28 
qed "infsys_p1"; 
29 

1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

30 
val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b"; 
1266  31 
by (Asm_full_simp_tac 1); 
969  32 
qed "infsys_p2"; 
33 

34 
val prems = goal MT.thy 

1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

35 
"!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))"; 
1266  36 
by (Asm_full_simp_tac 1); 
969  37 
qed "infsys_pp1"; 
38 

39 
val prems = goal MT.thy 

1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

40 
"!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c"; 
1266  41 
by (Asm_full_simp_tac 1); 
969  42 
qed "infsys_pp2"; 
43 

44 
(* ############################################################ *) 

45 
(* Fixpoints *) 

46 
(* ############################################################ *) 

47 

48 
(* Least fixpoints *) 

49 

50 
val prems = goal MT.thy "[ mono(f); x:f(lfp(f)) ] ==> x:lfp(f)"; 

51 
by (rtac subsetD 1); 

52 
by (rtac lfp_lemma2 1); 

1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

53 
by (resolve_tac prems 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

54 
by (resolve_tac prems 1); 
969  55 
qed "lfp_intro2"; 
56 

57 
val prems = goal MT.thy 

58 
" [ x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) ] ==> \ 

59 
\ P(x)"; 

60 
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

61 
by (resolve_tac prems 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

62 
by (rtac subsetD 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

63 
by (rtac lfp_lemma3 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

64 
by (assume_tac 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

65 
by (assume_tac 1); 
969  66 
qed "lfp_elim2"; 
67 

68 
val prems = goal MT.thy 

3842  69 
" [ x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) ] ==> \ 
969  70 
\ P(x)"; 
71 
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

72 
by (etac induct 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

73 
by (assume_tac 1); 
969  74 
by (eresolve_tac prems 1); 
75 
qed "lfp_ind2"; 

76 

77 
(* Greatest fixpoints *) 

78 

79 
(* Note : "[ x:S; S <= f(S Un gfp(f)); mono(f) ] ==> x:gfp(f)" *) 

80 

81 
val [cih,monoh] = goal MT.thy "[ x:f({x} Un gfp(f)); mono(f) ] ==> x:gfp(f)"; 

82 
by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1); 

83 
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

84 
by (rtac (UnE RS subsetI) 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

85 
by (assume_tac 1); 
4089  86 
by (blast_tac (claset() addSIs [cih]) 1); 
969  87 
by (rtac (monoh RS monoD RS subsetD) 1); 
88 
by (rtac Un_upper2 1); 

89 
by (etac (monoh RS gfp_lemma2 RS subsetD) 1); 

90 
qed "gfp_coind2"; 

91 

92 
val [gfph,monoh,caseh] = goal MT.thy 

93 
"[ 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

94 
by (rtac caseh 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

95 
by (rtac subsetD 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

96 
by (rtac gfp_lemma2 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

97 
by (rtac monoh 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

98 
by (rtac gfph 1); 
969  99 
qed "gfp_elim2"; 
100 

101 
(* ############################################################ *) 

102 
(* Expressions *) 

103 
(* ############################################################ *) 

104 

105 
val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj]; 

106 

107 
val e_disjs = 

108 
[ e_disj_const_var, 

109 
e_disj_const_fn, 

110 
e_disj_const_fix, 

111 
e_disj_const_app, 

112 
e_disj_var_fn, 

113 
e_disj_var_fix, 

114 
e_disj_var_app, 

115 
e_disj_fn_fix, 

116 
e_disj_fn_app, 

117 
e_disj_fix_app 

118 
]; 

119 

120 
val e_disj_si = e_disjs @ (e_disjs RL [not_sym]); 

121 
val e_disj_se = (e_disj_si RL [notE]); 

122 

123 
fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs; 

124 

125 
(* ############################################################ *) 

126 
(* Values *) 

127 
(* ############################################################ *) 

128 

129 
val v_disjs = [v_disj_const_clos]; 

130 
val v_disj_si = v_disjs @ (v_disjs RL [not_sym]); 

131 
val v_disj_se = (v_disj_si RL [notE]); 

132 

133 
val v_injs = [v_const_inj, v_clos_inj]; 

134 

135 
fun v_ext_cs cs = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs; 

136 

137 
(* ############################################################ *) 

138 
(* Evaluations *) 

139 
(* ############################################################ *) 

140 

141 
(* Monotonicity of eval_fun *) 

142 

143 
goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)"; 

144 
by infsys_mono_tac; 

145 
qed "eval_fun_mono"; 

146 

147 
(* Introduction rules *) 

148 

149 
goalw MT.thy [eval_def, eval_rel_def] "ve  e_const(c) > v_const(c)"; 

150 
by (rtac lfp_intro2 1); 

151 
by (rtac eval_fun_mono 1); 

152 
by (rewtac eval_fun_def); 

2935  153 
(*Naughty! But the quantifiers are nested VERY deeply...*) 
4089  154 
by (blast_tac (claset() addSIs [exI]) 1); 
969  155 
qed "eval_const"; 
156 

157 
val prems = goalw MT.thy [eval_def, eval_rel_def] 

158 
"ev:ve_dom(ve) ==> ve  e_var(ev) > ve_app ve ev"; 

159 
by (cut_facts_tac prems 1); 

160 
by (rtac lfp_intro2 1); 

161 
by (rtac eval_fun_mono 1); 

162 
by (rewtac eval_fun_def); 

4089  163 
by (blast_tac (claset() addSIs [exI]) 1); 
1266  164 
qed "eval_var2"; 
969  165 

166 
val prems = goalw MT.thy [eval_def, eval_rel_def] 

167 
"ve  fn ev => e > v_clos(<ev,e,ve>)"; 

168 
by (cut_facts_tac prems 1); 

169 
by (rtac lfp_intro2 1); 

170 
by (rtac eval_fun_mono 1); 

171 
by (rewtac eval_fun_def); 

4089  172 
by (blast_tac (claset() addSIs [exI]) 1); 
969  173 
qed "eval_fn"; 
174 

175 
val prems = goalw MT.thy [eval_def, eval_rel_def] 

176 
" cl = < ev1, e, ve + {ev2 > v_clos(cl)} > ==> \ 

177 
\ ve  fix ev2(ev1) = e > v_clos(cl)"; 

178 
by (cut_facts_tac prems 1); 

179 
by (rtac lfp_intro2 1); 

180 
by (rtac eval_fun_mono 1); 

181 
by (rewtac eval_fun_def); 

4089  182 
by (blast_tac (claset() addSIs [exI]) 1); 
969  183 
qed "eval_fix"; 
184 

185 
val prems = goalw MT.thy [eval_def, eval_rel_def] 

186 
" [ ve  e1 > v_const(c1); ve  e2 > v_const(c2) ] ==> \ 

187 
\ ve  e1 @ e2 > v_const(c_app c1 c2)"; 

188 
by (cut_facts_tac prems 1); 

189 
by (rtac lfp_intro2 1); 

190 
by (rtac eval_fun_mono 1); 

191 
by (rewtac eval_fun_def); 

4089  192 
by (blast_tac (claset() addSIs [exI]) 1); 
969  193 
qed "eval_app1"; 
194 

195 
val prems = goalw MT.thy [eval_def, eval_rel_def] 

196 
" [ ve  e1 > v_clos(<xm,em,vem>); \ 

197 
\ ve  e2 > v2; \ 

198 
\ vem + {xm > v2}  em > v \ 

199 
\ ] ==> \ 

200 
\ ve  e1 @ e2 > v"; 

201 
by (cut_facts_tac prems 1); 

202 
by (rtac lfp_intro2 1); 

203 
by (rtac eval_fun_mono 1); 

204 
by (rewtac eval_fun_def); 

4089  205 
by (blast_tac (claset() addSIs [disjI2]) 1); 
969  206 
qed "eval_app2"; 
207 

208 
(* Strong elimination, induction on evaluations *) 

209 

210 
val prems = goalw MT.thy [eval_def, eval_rel_def] 

211 
" [ ve  e > v; \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

212 
\ !!ve c. P(((ve,e_const(c)),v_const(c))); \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

213 
\ !!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

214 
\ !!ev ve e. P(((ve,fn ev => e),v_clos(<ev,e,ve>))); \ 
969  215 
\ !!ev1 ev2 ve cl e. \ 
216 
\ cl = < ev1, e, ve + {ev2 > v_clos(cl)} > ==> \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

217 
\ P(((ve,fix ev2(ev1) = e),v_clos(cl))); \ 
969  218 
\ !!ve c1 c2 e1 e2. \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

219 
\ [ P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) ] ==> \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

220 
\ P(((ve,e1 @ e2),v_const(c_app c1 c2))); \ 
969  221 
\ !!ve vem xm e1 e2 em v v2. \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

222 
\ [ P(((ve,e1),v_clos(<xm,em,vem>))); \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

223 
\ P(((ve,e2),v2)); \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

224 
\ P(((vem + {xm > v2},em),v)) \ 
969  225 
\ ] ==> \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

226 
\ P(((ve,e1 @ e2),v)) \ 
969  227 
\ ] ==> \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

228 
\ P(((ve,e),v))"; 
969  229 
by (resolve_tac (prems RL [lfp_ind2]) 1); 
230 
by (rtac eval_fun_mono 1); 

231 
by (rewtac eval_fun_def); 

232 
by (dtac CollectD 1); 

4089  233 
by (safe_tac (claset())); 
969  234 
by (ALLGOALS (resolve_tac prems)); 
2935  235 
by (ALLGOALS (Blast_tac)); 
969  236 
qed "eval_ind0"; 
237 

238 
val prems = goal MT.thy 

239 
" [ ve  e > v; \ 

240 
\ !!ve c. P ve (e_const c) (v_const c); \ 

241 
\ !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \ 

242 
\ !!ev ve e. P ve (fn ev => e) (v_clos <ev,e,ve>); \ 

243 
\ !!ev1 ev2 ve cl e. \ 

244 
\ cl = < ev1, e, ve + {ev2 > v_clos(cl)} > ==> \ 

245 
\ P ve (fix ev2(ev1) = e) (v_clos cl); \ 

246 
\ !!ve c1 c2 e1 e2. \ 

247 
\ [ P ve e1 (v_const c1); P ve e2 (v_const c2) ] ==> \ 

248 
\ P ve (e1 @ e2) (v_const(c_app c1 c2)); \ 

249 
\ !!ve vem evm e1 e2 em v v2. \ 

250 
\ [ P ve e1 (v_clos <evm,em,vem>); \ 

251 
\ P ve e2 v2; \ 

252 
\ P (vem + {evm > v2}) em v \ 

253 
\ ] ==> P ve (e1 @ e2) v \ 

254 
\ ] ==> P ve e v"; 

255 
by (res_inst_tac [("P","P")] infsys_pp2 1); 

256 
by (rtac eval_ind0 1); 

257 
by (ALLGOALS (rtac infsys_pp1)); 

258 
by (ALLGOALS (resolve_tac prems)); 

259 
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); 

260 
qed "eval_ind"; 

261 

262 
(* ############################################################ *) 

263 
(* Elaborations *) 

264 
(* ############################################################ *) 

265 

266 
goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)"; 

267 
by infsys_mono_tac; 

268 
qed "elab_fun_mono"; 

269 

270 
(* Introduction rules *) 

271 

2935  272 
goalw MT.thy [elab_def, elab_rel_def] 
273 
"!!te. c isof ty ==> te  e_const(c) ===> ty"; 

969  274 
by (rtac lfp_intro2 1); 
275 
by (rtac elab_fun_mono 1); 

276 
by (rewtac elab_fun_def); 

4089  277 
by (blast_tac (claset() addSIs [exI]) 1); 
969  278 
qed "elab_const"; 
279 

2935  280 
goalw MT.thy [elab_def, elab_rel_def] 
281 
"!!te. x:te_dom(te) ==> te  e_var(x) ===> te_app te x"; 

969  282 
by (rtac lfp_intro2 1); 
283 
by (rtac elab_fun_mono 1); 

284 
by (rewtac elab_fun_def); 

4089  285 
by (blast_tac (claset() addSIs [exI]) 1); 
969  286 
qed "elab_var"; 
287 

2935  288 
goalw MT.thy [elab_def, elab_rel_def] 
289 
"!!te. te + {x => ty1}  e ===> ty2 ==> te  fn 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_fn"; 
295 

2935  296 
goalw MT.thy [elab_def, elab_rel_def] 
297 
"!!te. te + {f => ty1>ty2} + {x => ty1}  e ===> ty2 ==> \ 

298 
\ te  fix f(x) = e ===> ty1>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 [exI]) 1); 
969  303 
qed "elab_fix"; 
304 

2935  305 
goalw MT.thy [elab_def, elab_rel_def] 
306 
"!!te. [ te  e1 ===> ty1>ty2; te  e2 ===> ty1 ] ==> \ 

307 
\ te  e1 @ e2 ===> ty2"; 

969  308 
by (rtac lfp_intro2 1); 
309 
by (rtac elab_fun_mono 1); 

310 
by (rewtac elab_fun_def); 

4089  311 
by (blast_tac (claset() addSIs [disjI2]) 1); 
969  312 
qed "elab_app"; 
313 

314 
(* Strong elimination, induction on elaborations *) 

315 

316 
val prems = goalw MT.thy [elab_def, elab_rel_def] 

317 
" [ te  e ===> t; \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

318 
\ !!te c t. c isof t ==> P(((te,e_const(c)),t)); \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

319 
\ !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \ 
969  320 
\ !!te x e t1 t2. \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

321 
\ [ te + {x => t1}  e ===> t2; P(((te + {x => t1},e),t2)) ] ==> \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

322 
\ P(((te,fn x => e),t1>t2)); \ 
969  323 
\ !!te f x e t1 t2. \ 
324 
\ [ te + {f => t1>t2} + {x => t1}  e ===> t2; \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

325 
\ P(((te + {f => t1>t2} + {x => t1},e),t2)) \ 
969  326 
\ ] ==> \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

327 
\ P(((te,fix f(x) = e),t1>t2)); \ 
969  328 
\ !!te e1 e2 t1 t2. \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

329 
\ [ te  e1 ===> t1>t2; P(((te,e1),t1>t2)); \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

330 
\ te  e2 ===> t1; P(((te,e2),t1)) \ 
969  331 
\ ] ==> \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

332 
\ P(((te,e1 @ e2),t2)) \ 
969  333 
\ ] ==> \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

334 
\ P(((te,e),t))"; 
969  335 
by (resolve_tac (prems RL [lfp_ind2]) 1); 
336 
by (rtac elab_fun_mono 1); 

337 
by (rewtac elab_fun_def); 

338 
by (dtac CollectD 1); 

4089  339 
by (safe_tac (claset())); 
969  340 
by (ALLGOALS (resolve_tac prems)); 
2935  341 
by (ALLGOALS (Blast_tac)); 
969  342 
qed "elab_ind0"; 
343 

344 
val prems = goal MT.thy 

345 
" [ te  e ===> t; \ 

346 
\ !!te c t. c isof t ==> P te (e_const c) t; \ 

347 
\ !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \ 

348 
\ !!te x e t1 t2. \ 

349 
\ [ te + {x => t1}  e ===> t2; P (te + {x => t1}) e t2 ] ==> \ 

350 
\ P te (fn x => e) (t1>t2); \ 

351 
\ !!te f x e t1 t2. \ 

352 
\ [ te + {f => t1>t2} + {x => t1}  e ===> t2; \ 

353 
\ P (te + {f => t1>t2} + {x => t1}) e t2 \ 

354 
\ ] ==> \ 

355 
\ P te (fix f(x) = e) (t1>t2); \ 

356 
\ !!te e1 e2 t1 t2. \ 

357 
\ [ te  e1 ===> t1>t2; P te e1 (t1>t2); \ 

358 
\ te  e2 ===> t1; P te e2 t1 \ 

359 
\ ] ==> \ 

360 
\ P te (e1 @ e2) t2 \ 

361 
\ ] ==> \ 

362 
\ P te e t"; 

363 
by (res_inst_tac [("P","P")] infsys_pp2 1); 

364 
by (rtac elab_ind0 1); 

365 
by (ALLGOALS (rtac infsys_pp1)); 

366 
by (ALLGOALS (resolve_tac prems)); 

367 
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); 

368 
qed "elab_ind"; 

369 

370 
(* Weak elimination, case analysis on elaborations *) 

371 

372 
val prems = goalw MT.thy [elab_def, elab_rel_def] 

373 
" [ te  e ===> t; \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

374 
\ !!te c t. c isof t ==> P(((te,e_const(c)),t)); \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

375 
\ !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \ 
969  376 
\ !!te x e t1 t2. \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

377 
\ te + {x => t1}  e ===> t2 ==> P(((te,fn x => e),t1>t2)); \ 
969  378 
\ !!te f x e t1 t2. \ 
379 
\ te + {f => t1>t2} + {x => t1}  e ===> t2 ==> \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

380 
\ P(((te,fix f(x) = e),t1>t2)); \ 
969  381 
\ !!te e1 e2 t1 t2. \ 
382 
\ [ te  e1 ===> t1>t2; te  e2 ===> t1 ] ==> \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

383 
\ P(((te,e1 @ e2),t2)) \ 
969  384 
\ ] ==> \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

385 
\ P(((te,e),t))"; 
969  386 
by (resolve_tac (prems RL [lfp_elim2]) 1); 
387 
by (rtac elab_fun_mono 1); 

388 
by (rewtac elab_fun_def); 

389 
by (dtac CollectD 1); 

4089  390 
by (safe_tac (claset())); 
969  391 
by (ALLGOALS (resolve_tac prems)); 
2935  392 
by (ALLGOALS (Blast_tac)); 
969  393 
qed "elab_elim0"; 
394 

395 
val prems = goal MT.thy 

396 
" [ te  e ===> t; \ 

397 
\ !!te c t. c isof t ==> P te (e_const c) t; \ 

398 
\ !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \ 

399 
\ !!te x e t1 t2. \ 

400 
\ te + {x => t1}  e ===> t2 ==> P te (fn x => e) (t1>t2); \ 

401 
\ !!te f x e t1 t2. \ 

402 
\ te + {f => t1>t2} + {x => t1}  e ===> t2 ==> \ 

403 
\ P te (fix f(x) = e) (t1>t2); \ 

404 
\ !!te e1 e2 t1 t2. \ 

405 
\ [ te  e1 ===> t1>t2; te  e2 ===> t1 ] ==> \ 

406 
\ P te (e1 @ e2) t2 \ 

407 
\ ] ==> \ 

408 
\ P te e t"; 

409 
by (res_inst_tac [("P","P")] infsys_pp2 1); 

410 
by (rtac elab_elim0 1); 

411 
by (ALLGOALS (rtac infsys_pp1)); 

412 
by (ALLGOALS (resolve_tac prems)); 

413 
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); 

414 
qed "elab_elim"; 

415 

416 
(* Elimination rules for each expression *) 

417 

418 
fun elab_e_elim_tac p = 

419 
( (rtac elab_elim 1) THEN 

420 
(resolve_tac p 1) THEN 

2935  421 
(REPEAT (blast_tac (e_ext_cs HOL_cs) 1)) 
969  422 
); 
423 

424 
val prems = goal MT.thy "te  e ===> t ==> (e = e_const(c) > c isof t)"; 

425 
by (elab_e_elim_tac prems); 

426 
qed "elab_const_elim_lem"; 

427 

428 
val prems = goal MT.thy "te  e_const(c) ===> t ==> c isof t"; 

429 
by (cut_facts_tac prems 1); 

430 
by (dtac elab_const_elim_lem 1); 

2935  431 
by (Blast_tac 1); 
969  432 
qed "elab_const_elim"; 
433 

434 
val prems = goal MT.thy 

435 
"te  e ===> t ==> (e = e_var(x) > t=te_app te x & x:te_dom(te))"; 

436 
by (elab_e_elim_tac prems); 

437 
qed "elab_var_elim_lem"; 

438 

439 
val prems = goal MT.thy 

440 
"te  e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)"; 

441 
by (cut_facts_tac prems 1); 

442 
by (dtac elab_var_elim_lem 1); 

2935  443 
by (Blast_tac 1); 
969  444 
qed "elab_var_elim"; 
445 

446 
val prems = goal MT.thy 

447 
" te  e ===> t ==> \ 

448 
\ ( e = fn x1 => e1 > \ 

3842  449 
\ (? t1 t2. t=t_fun t1 t2 & te + {x1 => t1}  e1 ===> t2) \ 
969  450 
\ )"; 
451 
by (elab_e_elim_tac prems); 

452 
qed "elab_fn_elim_lem"; 

453 

454 
val prems = goal MT.thy 

455 
" te  fn x1 => e1 ===> t ==> \ 

456 
\ (? t1 t2. t=t1>t2 & te + {x1 => t1}  e1 ===> t2)"; 

457 
by (cut_facts_tac prems 1); 

458 
by (dtac elab_fn_elim_lem 1); 

2935  459 
by (Blast_tac 1); 
969  460 
qed "elab_fn_elim"; 
461 

462 
val prems = goal MT.thy 

463 
" te  e ===> t ==> \ 

464 
\ (e = fix f(x) = e1 > \ 

465 
\ (? t1 t2. t=t1>t2 & te + {f => t1>t2} + {x => t1}  e1 ===> t2))"; 

466 
by (elab_e_elim_tac prems); 

467 
qed "elab_fix_elim_lem"; 

468 

469 
val prems = goal MT.thy 

470 
" te  fix ev1(ev2) = e1 ===> t ==> \ 

471 
\ (? t1 t2. t=t1>t2 & te + {ev1 => t1>t2} + {ev2 => t1}  e1 ===> t2)"; 

472 
by (cut_facts_tac prems 1); 

473 
by (dtac elab_fix_elim_lem 1); 

2935  474 
by (Blast_tac 1); 
969  475 
qed "elab_fix_elim"; 
476 

477 
val prems = goal MT.thy 

478 
" te  e ===> t2 ==> \ 

479 
\ (e = e1 @ e2 > (? t1 . te  e1 ===> t1>t2 & te  e2 ===> t1))"; 

480 
by (elab_e_elim_tac prems); 

481 
qed "elab_app_elim_lem"; 

482 

1266  483 
val prems = goal MT.thy 
484 
"te  e1 @ e2 ===> t2 ==> (? t1 . te  e1 ===> t1>t2 & te  e2 ===> t1)"; 

969  485 
by (cut_facts_tac prems 1); 
486 
by (dtac elab_app_elim_lem 1); 

2935  487 
by (Blast_tac 1); 
969  488 
qed "elab_app_elim"; 
489 

490 
(* ############################################################ *) 

491 
(* The extended correspondence relation *) 

492 
(* ############################################################ *) 

493 

494 
(* Monotonicity of hasty_fun *) 

495 

496 
goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)"; 

497 
by infsys_mono_tac; 

2935  498 
by (Blast_tac 1); 
499 
qed "mono_hasty_fun"; 

969  500 

501 
(* 

502 
Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 

503 
enjoys two strong indtroduction (coinduction) rules and an elimination rule. 

504 
*) 

505 

506 
(* First strong indtroduction (coinduction) rule for hasty_rel *) 

507 

1266  508 
val prems = 
509 
goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel"; 

969  510 
by (cut_facts_tac prems 1); 
511 
by (rtac gfp_coind2 1); 

512 
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

513 
by (rtac CollectI 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

514 
by (rtac disjI1 1); 
2935  515 
by (Blast_tac 1); 
969  516 
by (rtac mono_hasty_fun 1); 
517 
qed "hasty_rel_const_coind"; 

518 

519 
(* Second strong introduction (coinduction) rule for hasty_rel *) 

520 

521 
val prems = goalw MT.thy [hasty_rel_def] 

522 
" [ te  fn ev => e ===> t; \ 

523 
\ ve_dom(ve) = te_dom(te); \ 

524 
\ ! ev1. \ 

525 
\ ev1:ve_dom(ve) > \ 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

526 
\ (ve_app ve ev1,te_app te ev1) : {(v_clos(<ev,e,ve>),t)} Un hasty_rel \ 
969  527 
\ ] ==> \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

528 
\ (v_clos(<ev,e,ve>),t) : hasty_rel"; 
969  529 
by (cut_facts_tac prems 1); 
530 
by (rtac gfp_coind2 1); 

531 
by (rewtac hasty_fun_def); 

1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

532 
by (rtac CollectI 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

533 
by (rtac disjI2 1); 
2935  534 
by (blast_tac HOL_cs 1); 
969  535 
by (rtac mono_hasty_fun 1); 
536 
qed "hasty_rel_clos_coind"; 

537 

538 
(* Elimination rule for hasty_rel *) 

539 

540 
val prems = goalw MT.thy [hasty_rel_def] 

3842  541 
" [ !! c t. c isof t ==> P((v_const(c),t)); \ 
969  542 
\ !! te ev e t ve. \ 
543 
\ [ te  fn ev => e ===> t; \ 

544 
\ ve_dom(ve) = te_dom(te); \ 

3842  545 
\ !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

546 
\ ] ==> P((v_clos(<ev,e,ve>),t)); \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

547 
\ (v,t) : hasty_rel \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

548 
\ ] ==> P((v,t))"; 
969  549 
by (cut_facts_tac prems 1); 
550 
by (etac gfp_elim2 1); 

551 
by (rtac mono_hasty_fun 1); 

552 
by (rewtac hasty_fun_def); 

553 
by (dtac CollectD 1); 

554 
by (fold_goals_tac [hasty_fun_def]); 

4089  555 
by (safe_tac (claset())); 
2935  556 
by (REPEAT (ares_tac prems 1)); 
969  557 
qed "hasty_rel_elim0"; 
558 

559 
val prems = goal MT.thy 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset

560 
" [ (v,t) : hasty_rel; \ 
3842  561 
\ !! c t. c isof t ==> P (v_const c) t; \ 
969  562 
\ !! te ev e t ve. \ 
563 
\ [ te  fn ev => e ===> t; \ 

564 
\ ve_dom(ve) = te_dom(te); \ 

3842  565 
\ !ev1. ev1:ve_dom(ve) > (ve_app ve ev1,te_app te ev1) : hasty_rel \ 
969  566 
\ ] ==> P (v_clos <ev,e,ve>) t \ 
567 
\ ] ==> P v t"; 

568 
by (res_inst_tac [("P","P")] infsys_p2 1); 

569 
by (rtac hasty_rel_elim0 1); 

570 
by (ALLGOALS (rtac infsys_p1)); 

571 
by (ALLGOALS (resolve_tac prems)); 

572 
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1))); 

573 
qed "hasty_rel_elim"; 

574 

575 
(* Introduction rules for hasty *) 

576 

2935  577 
goalw MT.thy [hasty_def] "!!c. c isof t ==> v_const(c) hasty t"; 
578 
by (etac hasty_rel_const_coind 1); 

969  579 
qed "hasty_const"; 
580 

2935  581 
goalw MT.thy [hasty_def,hasty_env_def] 
582 
"!!t. te  fn ev => e ===> t & ve hastyenv te ==> v_clos(<ev,e,ve>) hasty t"; 

969  583 
by (rtac hasty_rel_clos_coind 1); 
4089  584 
by (ALLGOALS (blast_tac (claset() delrules [equalityI]))); 
969  585 
qed "hasty_clos"; 
586 

587 
(* Elimination on constants for hasty *) 

588 

2935  589 
goalw MT.thy [hasty_def] 
590 
"!!v. v hasty t ==> (!c.(v = v_const(c) > c isof t))"; 

969  591 
by (rtac hasty_rel_elim 1); 
2935  592 
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs))); 
969  593 
qed "hasty_elim_const_lem"; 
594 

2935  595 
goal MT.thy "!!c. v_const(c) hasty t ==> c isof t"; 
596 
by (dtac hasty_elim_const_lem 1); 

597 
by (Blast_tac 1); 

969  598 
qed "hasty_elim_const"; 
599 

600 
(* Elimination on closures for hasty *) 

601 

602 
val prems = goalw MT.thy [hasty_env_def,hasty_def] 

603 
" v hasty t ==> \ 

604 
\ ! x e ve. \ 

3842  605 
\ v=v_clos(<x,e,ve>) > (? te. te  fn x => e ===> t & ve hastyenv te)"; 
969  606 
by (cut_facts_tac prems 1); 
607 
by (rtac hasty_rel_elim 1); 

2935  608 
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs))); 
969  609 
qed "hasty_elim_clos_lem"; 
610 

2935  611 
goal MT.thy 
612 
"!!t. v_clos(<ev,e,ve>) hasty t ==> \ 

3842  613 
\ ? te. te  fn ev => e ===> t & ve hastyenv te "; 
2935  614 
by (dtac hasty_elim_clos_lem 1); 
615 
by (Blast_tac 1); 

969  616 
qed "hasty_elim_clos"; 
617 

618 
(* ############################################################ *) 

619 
(* The pointwise extension of hasty to environments *) 

620 
(* ############################################################ *) 

621 

1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

622 
goal MT.thy 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

623 
"!!ve. [ ve hastyenv te; v hasty t ] ==> \ 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

624 
\ 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

625 
by (rewtac hasty_env_def); 
4089  626 
by (asm_full_simp_tac (simpset() delsimps mem_simps 
1266  627 
addsimps [ve_dom_owr, te_dom_owr]) 1); 
2935  628 
by (safe_tac HOL_cs); 
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

629 
by (excluded_middle_tac "ev=x" 1); 
4089  630 
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1); 
2935  631 
by (Blast_tac 1); 
4089  632 
by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1); 
969  633 
qed "hasty_env1"; 
634 

635 
(* ############################################################ *) 

636 
(* The Consistency theorem *) 

637 
(* ############################################################ *) 

638 

2935  639 
goal MT.thy 
640 
"!!t. [ ve hastyenv te ; te  e_const(c) ===> t ] ==> v_const(c) hasty t"; 

969  641 
by (dtac elab_const_elim 1); 
642 
by (etac hasty_const 1); 

643 
qed "consistency_const"; 

644 

2935  645 
goalw MT.thy [hasty_env_def] 
646 
"!!t. [ ev : ve_dom(ve); ve hastyenv te ; te  e_var(ev) ===> t ] ==> \ 

647 
\ ve_app ve ev hasty t"; 

969  648 
by (dtac elab_var_elim 1); 
2935  649 
by (Blast_tac 1); 
969  650 
qed "consistency_var"; 
651 

2935  652 
goal MT.thy 
653 
"!!t. [ ve hastyenv te ; te  fn ev => e ===> t ] ==> \ 

654 
\ v_clos(< ev, e, ve >) hasty t"; 

969  655 
by (rtac hasty_clos 1); 
2935  656 
by (Blast_tac 1); 
969  657 
qed "consistency_fn"; 
658 

2935  659 
goalw MT.thy [hasty_env_def,hasty_def] 
660 
"!!t. [ cl = < ev1, e, ve + { ev2 > v_clos(cl) } >; \ 

969  661 
\ ve hastyenv te ; \ 
662 
\ te  fix ev2 ev1 = e ===> t \ 

663 
\ ] ==> \ 

664 
\ v_clos(cl) hasty t"; 

665 
by (dtac elab_fix_elim 1); 

2935  666 
by (safe_tac HOL_cs); 
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

667 
(*Do a single unfolding of cl*) 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

668 
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

669 
by (rtac hasty_rel_clos_coind 1); 
969  670 
by (etac elab_fn 1); 
4089  671 
by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1); 
969  672 

4089  673 
by (asm_simp_tac (simpset() delsimps mem_simps addsimps [ve_dom_owr]) 1); 
2935  674 
by (safe_tac HOL_cs); 
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

675 
by (excluded_middle_tac "ev2=ev1a" 1); 
4089  676 
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1); 
2935  677 
by (Blast_tac 1); 
969  678 

4089  679 
by (asm_simp_tac (simpset() delsimps mem_simps 
1266  680 
addsimps [ve_app_owr1, te_app_owr1]) 1); 
969  681 
by (hyp_subst_tac 1); 
682 
by (etac subst 1); 

2935  683 
by (Blast_tac 1); 
969  684 
qed "consistency_fix"; 
685 

2935  686 
goal MT.thy 
687 
"!!t. [ ! t te. ve hastyenv te > te  e1 ===> t > v_const(c1) hasty t;\ 

969  688 
\ ! t te. ve hastyenv te > te  e2 ===> t > v_const(c2) hasty t; \ 
689 
\ ve hastyenv te ; te  e1 @ e2 ===> t \ 

690 
\ ] ==> \ 

691 
\ v_const(c_app c1 c2) hasty t"; 

692 
by (dtac elab_app_elim 1); 

4089  693 
by (safe_tac (claset())); 
969  694 
by (rtac hasty_const 1); 
695 
by (rtac isof_app 1); 

696 
by (rtac hasty_elim_const 1); 

2935  697 
by (Blast_tac 1); 
969  698 
by (rtac hasty_elim_const 1); 
2935  699 
by (Blast_tac 1); 
969  700 
qed "consistency_app1"; 
701 

2935  702 
goal MT.thy 
703 
"!!t. [ ! t te. \ 

969  704 
\ ve hastyenv te > \ 
705 
\ te  e1 ===> t > v_clos(<evm, em, vem>) hasty t; \ 

706 
\ ! t te. ve hastyenv te > te  e2 ===> t > v2 hasty t; \ 

707 
\ ! t te. \ 

708 
\ vem + { evm > v2 } hastyenv te > te  em ===> t > v hasty t; \ 

709 
\ ve hastyenv te ; \ 

710 
\ te  e1 @ e2 ===> t \ 

711 
\ ] ==> \ 

712 
\ v hasty t"; 

713 
by (dtac elab_app_elim 1); 

4089  714 
by (safe_tac (claset())); 
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

715 
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

716 
by (assume_tac 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

717 
by (etac impE 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

718 
by (assume_tac 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

719 
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

720 
by (assume_tac 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); 
969  723 
by (dtac hasty_elim_clos 1); 
4089  724 
by (safe_tac (claset())); 
969  725 
by (dtac elab_fn_elim 1); 
4089  726 
by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1); 
969  727 
qed "consistency_app2"; 
728 

1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

729 
val [major] = goal MT.thy 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

730 
"ve  e > v ==> \ 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

731 
\ (! t te. ve hastyenv te > te  e ===> t > v hasty t)"; 
969  732 

733 
(* Proof by induction on the structure of evaluations *) 

734 

1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

735 
by (rtac (major RS eval_ind) 1); 
4089  736 
by (safe_tac (claset())); 
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

737 
by (DEPTH_SOLVE 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

738 
(ares_tac [consistency_const, consistency_var, consistency_fn, 
1465  739 
consistency_fix, consistency_app1, consistency_app2] 1)); 
969  740 
qed "consistency"; 
741 

742 
(* ############################################################ *) 

743 
(* The Basic Consistency theorem *) 

744 
(* ############################################################ *) 

745 

746 
val prems = goalw MT.thy [isof_env_def,hasty_env_def] 

747 
"ve isofenv te ==> ve hastyenv te"; 

748 
by (cut_facts_tac prems 1); 

4089  749 
by (safe_tac (claset())); 
1047
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

750 
by (etac allE 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

751 
by (etac impE 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

752 
by (assume_tac 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

753 
by (etac exE 1); 
5133479a37cf
Simplified some proofs and made them work for new hyp_subst_tac.
lcp
parents:
972
diff
changeset

754 
by (etac conjE 1); 
969  755 
by (dtac hasty_const 1); 
1266  756 
by (Asm_simp_tac 1); 
969  757 
qed "basic_consistency_lem"; 
758 

759 
val prems = goal MT.thy 

760 
"[ ve isofenv te; ve  e > v_const(c); te  e ===> t ] ==> c isof t"; 

761 
by (cut_facts_tac prems 1); 

762 
by (rtac hasty_elim_const 1); 

763 
by (dtac consistency 1); 

4089  764 
by (blast_tac (claset() addSIs [basic_consistency_lem]) 1); 
969  765 
qed "basic_consistency"; 
1584  766 

767 
writeln"Reached end of file."; 