summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Bali/DefiniteAssignmentCorrect.thy

author | wenzelm |

Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) | |

changeset 63915 | bab633745c7f |

parent 62042 | 6c6ccf573479 |

child 68451 | c34aa23a1fb6 |

permissions | -rw-r--r-- |

tuned proofs;

1 subsection \<open>Correctness of Definite Assignment\<close>

3 theory DefiniteAssignmentCorrect imports WellForm Eval begin

5 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]

7 lemma sxalloc_no_jump:

8 assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and

9 no_jmp: "abrupt s0 \<noteq> Some (Jump j)"

10 shows "abrupt s1 \<noteq> Some (Jump j)"

11 using sxalloc no_jmp

12 by cases simp_all

14 lemma sxalloc_no_jump':

15 assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and

16 jump: "abrupt s1 = Some (Jump j)"

17 shows "abrupt s0 = Some (Jump j)"

18 using sxalloc jump

19 by cases simp_all

21 lemma halloc_no_jump:

22 assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and

23 no_jmp: "abrupt s0 \<noteq> Some (Jump j)"

24 shows "abrupt s1 \<noteq> Some (Jump j)"

25 using halloc no_jmp

26 by cases simp_all

28 lemma halloc_no_jump':

29 assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and

30 jump: "abrupt s1 = Some (Jump j)"

31 shows "abrupt s0 = Some (Jump j)"

32 using halloc jump

33 by cases simp_all

35 lemma Body_no_jump:

36 assumes eval: "G\<turnstile>s0 \<midarrow>Body D c-\<succ>v\<rightarrow>s1" and

37 jump: "abrupt s0 \<noteq> Some (Jump j)"

38 shows "abrupt s1 \<noteq> Some (Jump j)"

39 proof (cases "normal s0")

40 case True

41 with eval obtain s0' where eval': "G\<turnstile>Norm s0' \<midarrow>Body D c-\<succ>v\<rightarrow>s1" and

42 s0: "s0 = Norm s0'"

43 by (cases s0) simp

44 from eval' obtain s2 where

45 s1: "s1 = abupd (absorb Ret)

46 (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>

47 abrupt s2 = Some (Jump (Cont l))

48 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)"

49 by cases simp

50 show ?thesis

51 proof (cases "\<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>

52 abrupt s2 = Some (Jump (Cont l))")

53 case True

54 with s1 have "abrupt s1 = Some (Error CrossMethodJump)"

55 by (cases s2) simp

56 thus ?thesis by simp

57 next

58 case False

59 with s1 have "s1=abupd (absorb Ret) s2"

60 by simp

61 with False show ?thesis

62 by (cases s2,cases j) (auto simp add: absorb_def)

63 qed

64 next

65 case False

66 with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Body D c-\<succ>v\<rightarrow>s1"

67 "s0 = (Some abr, s0')"

68 by (cases s0) fastforce

69 with this jump

70 show ?thesis

71 by (cases) (simp)

72 qed

74 lemma Methd_no_jump:

75 assumes eval: "G\<turnstile>s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1" and

76 jump: "abrupt s0 \<noteq> Some (Jump j)"

77 shows "abrupt s1 \<noteq> Some (Jump j)"

78 proof (cases "normal s0")

79 case True

80 with eval obtain s0' where "G\<turnstile>Norm s0' \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1"

81 "s0 = Norm s0'"

82 by (cases s0) simp

83 then obtain D' body where "G\<turnstile>s0 \<midarrow>Body D' body-\<succ>v\<rightarrow>s1"

84 by (cases) (simp add: body_def2)

85 from this jump

86 show ?thesis

87 by (rule Body_no_jump)

88 next

89 case False

90 with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1"

91 "s0 = (Some abr, s0')"

92 by (cases s0) fastforce

93 with this jump

94 show ?thesis

95 by (cases) (simp)

96 qed

98 lemma jumpNestingOkS_mono:

99 assumes jumpNestingOk_l': "jumpNestingOkS jmps' c"

100 and subset: "jmps' \<subseteq> jmps"

101 shows "jumpNestingOkS jmps c"

102 proof -

103 have True and True and

104 "\<And> jmps' jmps. \<lbrakk>jumpNestingOkS jmps' c; jmps' \<subseteq> jmps\<rbrakk> \<Longrightarrow> jumpNestingOkS jmps c"

105 proof (induct rule: var.induct expr.induct stmt.induct)

106 case (Lab j c jmps' jmps)

107 note jmpOk = \<open>jumpNestingOkS jmps' (j\<bullet> c)\<close>

108 note jmps = \<open>jmps' \<subseteq> jmps\<close>

109 with jmpOk have "jumpNestingOkS ({j} \<union> jmps') c" by simp

110 moreover from jmps have "({j} \<union> jmps') \<subseteq> ({j} \<union> jmps)" by auto

111 ultimately

112 have "jumpNestingOkS ({j} \<union> jmps) c"

113 by (rule Lab.hyps)

114 thus ?case

115 by simp

116 next

117 case (Jmp j jmps' jmps)

118 thus ?case

119 by (cases j) auto

120 next

121 case (Comp c1 c2 jmps' jmps)

122 from Comp.prems

123 have "jumpNestingOkS jmps c1" by - (rule Comp.hyps,auto)

124 moreover from Comp.prems

125 have "jumpNestingOkS jmps c2" by - (rule Comp.hyps,auto)

126 ultimately show ?case

127 by simp

128 next

129 case (If' e c1 c2 jmps' jmps)

130 from If'.prems

131 have "jumpNestingOkS jmps c1" by - (rule If'.hyps,auto)

132 moreover from If'.prems

133 have "jumpNestingOkS jmps c2" by - (rule If'.hyps,auto)

134 ultimately show ?case

135 by simp

136 next

137 case (Loop l e c jmps' jmps)

138 from \<open>jumpNestingOkS jmps' (l\<bullet> While(e) c)\<close>

139 have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp

140 moreover

141 from \<open>jmps' \<subseteq> jmps\<close>

142 have "{Cont l} \<union> jmps' \<subseteq> {Cont l} \<union> jmps" by auto

143 ultimately

144 have "jumpNestingOkS ({Cont l} \<union> jmps) c"

145 by (rule Loop.hyps)

146 thus ?case by simp

147 next

148 case (TryC c1 C vn c2 jmps' jmps)

149 from TryC.prems

150 have "jumpNestingOkS jmps c1" by - (rule TryC.hyps,auto)

151 moreover from TryC.prems

152 have "jumpNestingOkS jmps c2" by - (rule TryC.hyps,auto)

153 ultimately show ?case

154 by simp

155 next

156 case (Fin c1 c2 jmps' jmps)

157 from Fin.prems

158 have "jumpNestingOkS jmps c1" by - (rule Fin.hyps,auto)

159 moreover from Fin.prems

160 have "jumpNestingOkS jmps c2" by - (rule Fin.hyps,auto)

161 ultimately show ?case

162 by simp

163 qed (simp_all)

164 with jumpNestingOk_l' subset

165 show ?thesis

166 by iprover

167 qed

169 corollary jumpNestingOk_mono:

170 assumes jmpOk: "jumpNestingOk jmps' t"

171 and subset: "jmps' \<subseteq> jmps"

172 shows "jumpNestingOk jmps t"

173 proof (cases t)

174 case (In1 expr_stmt)

175 show ?thesis

176 proof (cases expr_stmt)

177 case (Inl e)

178 with In1 show ?thesis by simp

179 next

180 case (Inr s)

181 with In1 jmpOk subset show ?thesis by (auto intro: jumpNestingOkS_mono)

182 qed

183 qed (simp_all)

185 lemma assign_abrupt_propagation:

186 assumes f_ok: "abrupt (f n s) \<noteq> x"

187 and ass: "abrupt (assign f n s) = x"

188 shows "abrupt s = x"

189 proof (cases x)

190 case None

191 with ass show ?thesis

192 by (cases s) (simp add: assign_def Let_def)

193 next

194 case (Some xcpt)

195 from f_ok

196 obtain xf sf where "f n s = (xf,sf)"

197 by (cases "f n s")

198 with Some ass f_ok show ?thesis

199 by (cases s) (simp add: assign_def Let_def)

200 qed

202 lemma wt_init_comp_ty':

203 "is_acc_type (prg Env) (pid (cls Env)) T \<Longrightarrow> Env\<turnstile>init_comp_ty T\<Colon>\<surd>"

204 apply (unfold init_comp_ty_def)

205 apply (clarsimp simp add: accessible_in_RefT_simp

206 is_acc_type_def is_acc_class_def)

207 done

209 lemma fvar_upd_no_jump:

210 assumes upd: "upd = snd (fst (fvar statDeclC stat fn a s'))"

211 and noJmp: "abrupt s \<noteq> Some (Jump j)"

212 shows "abrupt (upd val s) \<noteq> Some (Jump j)"

213 proof (cases "stat")

214 case True

215 with noJmp upd

216 show ?thesis

217 by (cases s) (simp add: fvar_def2)

218 next

219 case False

220 with noJmp upd

221 show ?thesis

222 by (cases s) (simp add: fvar_def2)

223 qed

226 lemma avar_state_no_jump:

227 assumes jmp: "abrupt (snd (avar G i a s)) = Some (Jump j)"

228 shows "abrupt s = Some (Jump j)"

229 proof (cases "normal s")

230 case True with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def)

231 next

232 case False with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def)

233 qed

235 lemma avar_upd_no_jump:

236 assumes upd: "upd = snd (fst (avar G i a s'))"

237 and noJmp: "abrupt s \<noteq> Some (Jump j)"

238 shows "abrupt (upd val s) \<noteq> Some (Jump j)"

239 using upd noJmp

240 by (cases s) (simp add: avar_def2 abrupt_if_def)

243 text \<open>

244 The next theorem expresses: If jumps (breaks, continues, returns) are nested

245 correctly, we won't find an unexpected jump in the result state of the

246 evaluation. For exeample, a break can't leave its enclosing loop, an return

247 cant leave its enclosing method.

248 To proove this, the method call is critical. Allthough the

249 wellformedness of the whole program guarantees that the jumps (breaks,continues

250 and returns) are nested

251 correctly in all method bodies, the call rule alone does not guarantee that I

252 will call a method or even a class that is part of the program due to dynamic

253 binding! To be able to enshure this we need a kind of conformance of the

254 state, like in the typesafety proof. But then we will redo the typesafty

255 proof here. It would be nice if we could find an easy precondition that will

256 guarantee that all calls will actually call classes and methods of the current

257 program, which can be instantiated in the typesafty proof later on.

258 To fix this problem, I have instrumented the semantic definition of a call

259 to filter out any breaks in the state and to throw an error instead.

261 To get an induction hypothesis which is strong enough to perform the

262 proof, we can't just

263 assume @{term jumpNestingOk} for the empty set and conlcude, that no jump at

264 all will be in the resulting state, because the set is altered by

265 the statements @{term Lab} and @{term While}.

267 The wellformedness of the program is used to enshure that for all

268 classinitialisations and methods the nesting of jumps is wellformed, too.

269 \<close>

270 theorem jumpNestingOk_eval:

271 assumes eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"

272 and jmpOk: "jumpNestingOk jmps t"

273 and wt: "Env\<turnstile>t\<Colon>T"

274 and wf: "wf_prog G"

275 and G: "prg Env = G"

276 and no_jmp: "\<forall>j. abrupt s0 = Some (Jump j) \<longrightarrow> j \<in> jmps"

277 (is "?Jmp jmps s0")

278 shows "(\<forall>j. fst s1 = Some (Jump j) \<longrightarrow> j \<in> jmps) \<and>

279 (normal s1 \<longrightarrow>

280 (\<forall> w upd. v=In2 (w,upd)

281 \<longrightarrow> (\<forall> s j val.

282 abrupt s \<noteq> Some (Jump j) \<longrightarrow>

283 abrupt (upd val s) \<noteq> Some (Jump j))))"

284 (is "?Jmp jmps s1 \<and> ?Upd v s1")

285 proof -

286 let ?HypObj = "\<lambda> t s0 s1 v.

287 (\<forall> jmps T Env.

288 ?Jmp jmps s0 \<longrightarrow> jumpNestingOk jmps t \<longrightarrow> Env\<turnstile>t\<Colon>T \<longrightarrow> prg Env=G\<longrightarrow>

289 ?Jmp jmps s1 \<and> ?Upd v s1)"

290 \<comment> \<open>Variable \<open>?HypObj\<close> is the following goal spelled in terms of

291 the object logic, instead of the meta logic. It is needed in some

292 cases of the induction were, the atomize-rulify process of induct

293 does not work fine, because the eval rules mix up object and meta

294 logic. See for example the case for the loop.\<close>

295 from eval

296 have "\<And> jmps T Env. \<lbrakk>?Jmp jmps s0; jumpNestingOk jmps t; Env\<turnstile>t\<Colon>T;prg Env=G\<rbrakk>

297 \<Longrightarrow> ?Jmp jmps s1 \<and> ?Upd v s1"

298 (is "PROP ?Hyp t s0 s1 v")

299 \<comment> \<open>We need to abstract over @{term jmps} since @{term jmps} are extended

300 during analysis of @{term Lab}. Also we need to abstract over

301 @{term T} and @{term Env} since they are altered in various

302 typing judgements.\<close>

303 proof (induct)

304 case Abrupt thus ?case by simp

305 next

306 case Skip thus ?case by simp

307 next

308 case Expr thus ?case by (elim wt_elim_cases) simp

309 next

310 case (Lab s0 c s1 jmp jmps T Env)

311 note jmpOK = \<open>jumpNestingOk jmps (In1r (jmp\<bullet> c))\<close>

312 note G = \<open>prg Env = G\<close>

313 have wt_c: "Env\<turnstile>c\<Colon>\<surd>"

314 using Lab.prems by (elim wt_elim_cases)

315 {

316 fix j

317 assume ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)"

318 have "j\<in>jmps"

319 proof -

320 from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"

321 by (cases s1) (simp add: absorb_def)

322 note hyp_c = \<open>PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>\<close>

323 from ab_s1 have "j \<noteq> jmp"

324 by (cases s1) (simp add: absorb_def)

325 moreover have "j \<in> {jmp} \<union> jmps"

326 proof -

327 from jmpOK

328 have "jumpNestingOk ({jmp} \<union> jmps) (In1r c)" by simp

329 with wt_c jmp_s1 G hyp_c

330 show ?thesis

331 by - (rule hyp_c [THEN conjunct1,rule_format],simp)

332 qed

333 ultimately show ?thesis

334 by simp

335 qed

336 }

337 thus ?case by simp

338 next

339 case (Comp s0 c1 s1 c2 s2 jmps T Env)

340 note jmpOk = \<open>jumpNestingOk jmps (In1r (c1;; c2))\<close>

341 note G = \<open>prg Env = G\<close>

342 from Comp.prems obtain

343 wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

344 by (elim wt_elim_cases)

345 {

346 fix j

347 assume abr_s2: "abrupt s2 = Some (Jump j)"

348 have "j\<in>jmps"

349 proof -

350 have jmp: "?Jmp jmps s1"

351 proof -

352 note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>\<close>

353 with wt_c1 jmpOk G

354 show ?thesis by simp

355 qed

356 moreover note hyp_c2 = \<open>PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)\<close>

357 have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp

358 moreover note wt_c2 G abr_s2

359 ultimately show "j \<in> jmps"

360 by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])

361 qed

362 } thus ?case by simp

363 next

364 case (If s0 e b s1 c1 c2 s2 jmps T Env)

365 note jmpOk = \<open>jumpNestingOk jmps (In1r (If(e) c1 Else c2))\<close>

366 note G = \<open>prg Env = G\<close>

367 from If.prems obtain

368 wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and

369 wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"

370 by (elim wt_elim_cases) simp

371 {

372 fix j

373 assume jmp: "abrupt s2 = Some (Jump j)"

374 have "j\<in>jmps"

375 proof -

376 note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>

377 with wt_e G have "?Jmp jmps s1"

378 by simp

379 moreover note hyp_then_else =

380 \<open>PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>\<close>

381 have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"

382 using jmpOk by (cases "the_Bool b") simp_all

383 moreover note wt_then_else G jmp

384 ultimately show "j\<in> jmps"

385 by (rule hyp_then_else [THEN conjunct1,rule_format (no_asm)])

386 qed

387 }

388 thus ?case by simp

389 next

390 case (Loop s0 e b s1 c s2 l s3 jmps T Env)

391 note jmpOk = \<open>jumpNestingOk jmps (In1r (l\<bullet> While(e) c))\<close>

392 note G = \<open>prg Env = G\<close>

393 note wt = \<open>Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T\<close>

394 then obtain

395 wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and

396 wt_c: "Env\<turnstile>c\<Colon>\<surd>"

397 by (elim wt_elim_cases)

398 {

399 fix j

400 assume jmp: "abrupt s3 = Some (Jump j)"

401 have "j\<in>jmps"

402 proof -

403 note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>

404 with wt_e G have jmp_s1: "?Jmp jmps s1"

405 by simp

406 show ?thesis

407 proof (cases "the_Bool b")

408 case False

409 from Loop.hyps

410 have "s3=s1"

411 by (simp (no_asm_use) only: if_False False)

412 with jmp_s1 jmp have "j \<in> jmps" by simp

413 thus ?thesis by simp

414 next

415 case True

416 from Loop.hyps

417 (* Because of the mixture of object and pure logic in the rule

418 eval.If the atomization-rulification of the induct method

419 leaves the hypothesis in object logic *)

420 have "?HypObj (In1r c) s1 s2 (\<diamondsuit>::vals)"

421 apply (simp (no_asm_use) only: True if_True )

422 apply (erule conjE)+

423 apply assumption

424 done

425 note hyp_c = this [rule_format (no_asm)]

426 moreover from jmpOk have "jumpNestingOk ({Cont l} \<union> jmps) (In1r c)"

427 by simp

428 moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp

429 ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2"

430 using wt_c G by iprover

431 have "?Jmp jmps (abupd (absorb (Cont l)) s2)"

432 proof -

433 {

434 fix j'

435 assume abs: "abrupt (abupd (absorb (Cont l)) s2)=Some (Jump j')"

436 have "j' \<in> jmps"

437 proof (cases "j' = Cont l")

438 case True

439 with abs show ?thesis

440 by (cases s2) (simp add: absorb_def)

441 next

442 case False

443 with abs have "abrupt s2 = Some (Jump j')"

444 by (cases s2) (simp add: absorb_def)

445 with jmp_s2 False show ?thesis

446 by simp

447 qed

448 }

449 thus ?thesis by simp

450 qed

451 moreover

452 from Loop.hyps

453 have "?HypObj (In1r (l\<bullet> While(e) c))

454 (abupd (absorb (Cont l)) s2) s3 (\<diamondsuit>::vals)"

455 apply (simp (no_asm_use) only: True if_True)

456 apply (erule conjE)+

457 apply assumption

458 done

459 note hyp_w = this [rule_format (no_asm)]

460 note jmpOk wt G jmp

461 ultimately show "j\<in> jmps"

462 by (rule hyp_w [THEN conjunct1,rule_format (no_asm)])

463 qed

464 qed

465 }

466 thus ?case by simp

467 next

468 case (Jmp s j jmps T Env) thus ?case by simp

469 next

470 case (Throw s0 e a s1 jmps T Env)

471 note jmpOk = \<open>jumpNestingOk jmps (In1r (Throw e))\<close>

472 note G = \<open>prg Env = G\<close>

473 from Throw.prems obtain Te where

474 wt_e: "Env\<turnstile>e\<Colon>-Te"

475 by (elim wt_elim_cases)

476 {

477 fix j

478 assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"

479 have "j\<in>jmps"

480 proof -

481 from \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>

482 have "?Jmp jmps s1" using wt_e G by simp

483 moreover

484 from jmp

485 have "abrupt s1 = Some (Jump j)"

486 by (cases s1) (simp add: throw_def abrupt_if_def)

487 ultimately show "j \<in> jmps" by simp

488 qed

489 }

490 thus ?case by simp

491 next

492 case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)

493 note jmpOk = \<open>jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))\<close>

494 note G = \<open>prg Env = G\<close>

495 from Try.prems obtain

496 wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and

497 wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"

498 by (elim wt_elim_cases)

499 {

500 fix j

501 assume jmp: "abrupt s3 = Some (Jump j)"

502 have "j\<in>jmps"

503 proof -

504 note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)\<close>

505 with jmpOk wt_c1 G

506 have jmp_s1: "?Jmp jmps s1" by simp

507 note s2 = \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>

508 show "j \<in> jmps"

509 proof (cases "G,s2\<turnstile>catch C")

510 case False

511 from Try.hyps have "s3=s2"

512 by (simp (no_asm_use) only: False if_False)

513 with jmp have "abrupt s1 = Some (Jump j)"

514 using sxalloc_no_jump' [OF s2] by simp

515 with jmp_s1

516 show ?thesis by simp

517 next

518 case True

519 with Try.hyps

520 have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3 (\<diamondsuit>::vals)"

521 apply (simp (no_asm_use) only: True if_True simp_thms)

522 apply (erule conjE)+

523 apply assumption

524 done

525 note hyp_c2 = this [rule_format (no_asm)]

526 from jmp_s1 sxalloc_no_jump' [OF s2]

527 have "?Jmp jmps s2"

528 by simp

529 hence "?Jmp jmps (new_xcpt_var vn s2)"

530 by (cases s2) simp

531 moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp

532 moreover note wt_c2

533 moreover from G

534 have "prg (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) = G"

535 by simp

536 moreover note jmp

537 ultimately show ?thesis

538 by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])

539 qed

540 qed

541 }

542 thus ?case by simp

543 next

544 case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)

545 note jmpOk = \<open>jumpNestingOk jmps (In1r (c1 Finally c2))\<close>

546 note G = \<open>prg Env = G\<close>

547 from Fin.prems obtain

548 wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

549 by (elim wt_elim_cases)

550 {

551 fix j

552 assume jmp: "abrupt s3 = Some (Jump j)"

553 have "j \<in> jmps"

554 proof (cases "x1=Some (Jump j)")

555 case True

556 note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>\<close>

557 with True jmpOk wt_c1 G show ?thesis

558 by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)

559 next

560 case False

561 note hyp_c2 = \<open>PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>\<close>

562 note \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)

563 else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close>

564 with False jmp have "abrupt s2 = Some (Jump j)"

565 by (cases s2) (simp add: abrupt_if_def)

566 with jmpOk wt_c2 G show ?thesis

567 by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all)

568 qed

569 }

570 thus ?case by simp

571 next

572 case (Init C c s0 s3 s1 s2 jmps T Env)

573 note \<open>jumpNestingOk jmps (In1r (Init C))\<close>

574 note G = \<open>prg Env = G\<close>

575 note \<open>the (class G C) = c\<close>

576 with Init.prems have c: "class G C = Some c"

577 by (elim wt_elim_cases) auto

578 {

579 fix j

580 assume jmp: "abrupt s3 = (Some (Jump j))"

581 have "j\<in>jmps"

582 proof (cases "inited C (globs s0)")

583 case True

584 with Init.hyps have "s3=Norm s0"

585 by simp

586 with jmp

587 have "False" by simp thus ?thesis ..

588 next

589 case False

590 from wf c G

591 have wf_cdecl: "wf_cdecl G (C,c)"

592 by (simp add: wf_prog_cdecl)

593 from Init.hyps

594 have "?HypObj (In1r (if C = Object then Skip else Init (super c)))

595 (Norm ((init_class_obj G C) s0)) s1 (\<diamondsuit>::vals)"

596 apply (simp (no_asm_use) only: False if_False simp_thms)

597 apply (erule conjE)+

598 apply assumption

599 done

600 note hyp_s1 = this [rule_format (no_asm)]

601 from wf_cdecl G have

602 wt_super: "Env\<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"

603 by (cases "C=Object")

604 (auto dest: wf_cdecl_supD is_acc_classD)

605 from hyp_s1 [OF _ _ wt_super G]

606 have "?Jmp jmps s1"

607 by simp

608 hence jmp_s1: "?Jmp jmps ((set_lvars empty) s1)" by (cases s1) simp

609 from False Init.hyps

610 have "?HypObj (In1r (init c)) ((set_lvars empty) s1) s2 (\<diamondsuit>::vals)"

611 apply (simp (no_asm_use) only: False if_False simp_thms)

612 apply (erule conjE)+

613 apply assumption

614 done

615 note hyp_init_c = this [rule_format (no_asm)]

616 from wf_cdecl

617 have wt_init_c: "\<lparr>prg = G, cls = C, lcl = empty\<rparr>\<turnstile>init c\<Colon>\<surd>"

618 by (rule wf_cdecl_wt_init)

619 from wf_cdecl have "jumpNestingOkS {} (init c)"

620 by (cases rule: wf_cdeclE)

621 hence "jumpNestingOkS jmps (init c)"

622 by (rule jumpNestingOkS_mono) simp

623 moreover

624 have "abrupt s2 = Some (Jump j)"

625 proof -

626 from False Init.hyps

627 have "s3 = (set_lvars (locals (store s1))) s2" by simp

628 with jmp show ?thesis by (cases s2) simp

629 qed

630 ultimately show ?thesis

631 using hyp_init_c [OF jmp_s1 _ wt_init_c]

632 by simp

633 qed

634 }

635 thus ?case by simp

636 next

637 case (NewC s0 C s1 a s2 jmps T Env)

638 {

639 fix j

640 assume jmp: "abrupt s2 = Some (Jump j)"

641 have "j\<in>jmps"

642 proof -

643 note \<open>prg Env = G\<close>

644 moreover note hyp_init = \<open>PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>\<close>

645 moreover from wf NewC.prems

646 have "Env\<turnstile>(Init C)\<Colon>\<surd>"

647 by (elim wt_elim_cases) (drule is_acc_classD,simp)

648 moreover

649 have "abrupt s1 = Some (Jump j)"

650 proof -

651 from \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close> and jmp show ?thesis

652 by (rule halloc_no_jump')

653 qed

654 ultimately show "j \<in> jmps"

655 by - (rule hyp_init [THEN conjunct1,rule_format (no_asm)],auto)

656 qed

657 }

658 thus ?case by simp

659 next

660 case (NewA s0 elT s1 e i s2 a s3 jmps T Env)

661 {

662 fix j

663 assume jmp: "abrupt s3 = Some (Jump j)"

664 have "j\<in>jmps"

665 proof -

666 note G = \<open>prg Env = G\<close>

667 from NewA.prems

668 obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and

669 wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"

670 by (elim wt_elim_cases) (auto dest: wt_init_comp_ty')

671 note \<open>PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>\<close>

672 with wt_init G

673 have "?Jmp jmps s1"

674 by (simp add: init_comp_ty_def)

675 moreover

676 note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 i)\<close>

677 have "abrupt s2 = Some (Jump j)"

678 proof -

679 note \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3\<close>

680 moreover note jmp

681 ultimately

682 have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"

683 by (rule halloc_no_jump')

684 thus ?thesis by (cases s2) auto

685 qed

686 ultimately show "j\<in>jmps" using wt_size G

687 by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all)

688 qed

689 }

690 thus ?case by simp

691 next

692 case (Cast s0 e v s1 s2 cT jmps T Env)

693 {

694 fix j

695 assume jmp: "abrupt s2 = Some (Jump j)"

696 have "j\<in>jmps"

697 proof -

698 note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>

699 note \<open>prg Env = G\<close>

700 moreover from Cast.prems

701 obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)

702 moreover

703 have "abrupt s1 = Some (Jump j)"

704 proof -

705 note \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close>

706 moreover note jmp

707 ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)

708 qed

709 ultimately show ?thesis

710 by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)

711 qed

712 }

713 thus ?case by simp

714 next

715 case (Inst s0 e v s1 b eT jmps T Env)

716 {

717 fix j

718 assume jmp: "abrupt s1 = Some (Jump j)"

719 have "j\<in>jmps"

720 proof -

721 note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>

722 note \<open>prg Env = G\<close>

723 moreover from Inst.prems

724 obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)

725 moreover note jmp

726 ultimately show "j\<in>jmps"

727 by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)

728 qed

729 }

730 thus ?case by simp

731 next

732 case Lit thus ?case by simp

733 next

734 case (UnOp s0 e v s1 unop jmps T Env)

735 {

736 fix j

737 assume jmp: "abrupt s1 = Some (Jump j)"

738 have "j\<in>jmps"

739 proof -

740 note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>

741 note \<open>prg Env = G\<close>

742 moreover from UnOp.prems

743 obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)

744 moreover note jmp

745 ultimately show "j\<in>jmps"

746 by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)

747 qed

748 }

749 thus ?case by simp

750 next

751 case (BinOp s0 e1 v1 s1 binop e2 v2 s2 jmps T Env)

752 {

753 fix j

754 assume jmp: "abrupt s2 = Some (Jump j)"

755 have "j\<in>jmps"

756 proof -

757 note G = \<open>prg Env = G\<close>

758 from BinOp.prems

759 obtain e1T e2T where

760 wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and

761 wt_e2: "Env\<turnstile>e2\<Colon>-e2T"

762 by (elim wt_elim_cases)

763 note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)\<close>

764 with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp

765 note hyp_e2 =

766 \<open>PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)

767 s1 s2 (In1 v2)\<close>

768 show "j\<in>jmps"

769 proof (cases "need_second_arg binop v1")

770 case True with jmp_s1 wt_e2 jmp G

771 show ?thesis

772 by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)

773 next

774 case False with jmp_s1 jmp G

775 show ?thesis

776 by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],auto)

777 qed

778 qed

779 }

780 thus ?case by simp

781 next

782 case Super thus ?case by simp

783 next

784 case (Acc s0 va v f s1 jmps T Env)

785 {

786 fix j

787 assume jmp: "abrupt s1 = Some (Jump j)"

788 have "j\<in>jmps"

789 proof -

790 note hyp_va = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))\<close>

791 note \<open>prg Env = G\<close>

792 moreover from Acc.prems

793 obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)

794 moreover note jmp

795 ultimately show "j\<in>jmps"

796 by - (rule hyp_va [THEN conjunct1,rule_format (no_asm)], simp_all)

797 qed

798 }

799 thus ?case by simp

800 next

801 case (Ass s0 va w f s1 e v s2 jmps T Env)

802 note G = \<open>prg Env = G\<close>

803 from Ass.prems

804 obtain vT eT where

805 wt_va: "Env\<turnstile>va\<Colon>=vT" and

806 wt_e: "Env\<turnstile>e\<Colon>-eT"

807 by (elim wt_elim_cases)

808 note hyp_v = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))\<close>

809 note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 v)\<close>

810 {

811 fix j

812 assume jmp: "abrupt (assign f v s2) = Some (Jump j)"

813 have "j\<in>jmps"

814 proof -

815 have "abrupt s2 = Some (Jump j)"

816 proof (cases "normal s2")

817 case True

818 from \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close> and True have nrm_s1: "normal s1"

819 by (rule eval_no_abrupt_lemma [rule_format])

820 with nrm_s1 wt_va G True

821 have "abrupt (f v s2) \<noteq> Some (Jump j)"

822 using hyp_v [THEN conjunct2,rule_format (no_asm)]

823 by simp

824 from this jmp

825 show ?thesis

826 by (rule assign_abrupt_propagation)

827 next

828 case False with jmp

829 show ?thesis by (cases s2) (simp add: assign_def Let_def)

830 qed

831 moreover from wt_va G

832 have "?Jmp jmps s1"

833 by - (rule hyp_v [THEN conjunct1],simp_all)

834 ultimately show ?thesis using G

835 by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e)

836 qed

837 }

838 thus ?case by simp

839 next

840 case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env)

841 note G = \<open>prg Env = G\<close>

842 note hyp_e0 = \<open>PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)\<close>

843 note hyp_e1_e2 = \<open>PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)\<close>

844 from Cond.prems

845 obtain e1T e2T

846 where wt_e0: "Env\<turnstile>e0\<Colon>-PrimT Boolean"

847 and wt_e1: "Env\<turnstile>e1\<Colon>-e1T"

848 and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"

849 by (elim wt_elim_cases)

850 {

851 fix j

852 assume jmp: "abrupt s2 = Some (Jump j)"

853 have "j\<in>jmps"

854 proof -

855 from wt_e0 G

856 have jmp_s1: "?Jmp jmps s1"

857 by - (rule hyp_e0 [THEN conjunct1],simp_all)

858 show ?thesis

859 proof (cases "the_Bool b")

860 case True

861 with jmp_s1 wt_e1 G jmp

862 show ?thesis

863 by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)

864 next

865 case False

866 with jmp_s1 wt_e2 G jmp

867 show ?thesis

868 by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)

869 qed

870 qed

871 }

872 thus ?case by simp

873 next

874 case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4

875 jmps T Env)

876 note G = \<open>prg Env = G\<close>

877 from Call.prems

878 obtain eT argsT

879 where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"

880 by (elim wt_elim_cases)

881 {

882 fix j

883 assume jmp: "abrupt ((set_lvars (locals (store s2))) s4)

884 = Some (Jump j)"

885 have "j\<in>jmps"

886 proof -

887 note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>

888 from wt_e G

889 have jmp_s1: "?Jmp jmps s1"

890 by - (rule hyp_e [THEN conjunct1],simp_all)

891 note hyp_args = \<open>PROP ?Hyp (In3 args) s1 s2 (In3 vs)\<close>

892 have "abrupt s2 = Some (Jump j)"

893 proof -

894 note \<open>G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4\<close>

895 moreover

896 from jmp have "abrupt s4 = Some (Jump j)"

897 by (cases s4) simp

898 ultimately have "abrupt s3' = Some (Jump j)"

899 by - (rule ccontr,drule (1) Methd_no_jump,simp)

900 moreover note \<open>s3' = check_method_access G accC statT mode

901 \<lparr>name = mn, parTs = pTs\<rparr> a s3\<close>

902 ultimately have "abrupt s3 = Some (Jump j)"

903 by (cases s3)

904 (simp add: check_method_access_def abrupt_if_def Let_def)

905 moreover

906 note \<open>s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2\<close>

907 ultimately show ?thesis

908 by (cases s2) (auto simp add: init_lvars_def2)

909 qed

910 with jmp_s1 wt_args G

911 show ?thesis

912 by - (rule hyp_args [THEN conjunct1,rule_format (no_asm)], simp_all)

913 qed

914 }

915 thus ?case by simp

916 next

917 case (Methd s0 D sig v s1 jmps T Env)

918 from \<open>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<close>

919 have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"

920 by (rule eval.Methd)

921 hence "\<And> j. abrupt s1 \<noteq> Some (Jump j)"

922 by (rule Methd_no_jump) simp

923 thus ?case by simp

924 next

925 case (Body s0 D s1 c s2 s3 jmps T Env)

926 have "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)

927 \<rightarrow> abupd (absorb Ret) s3"

928 by (rule eval.Body) (rule Body)+

929 hence "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"

930 by (rule Body_no_jump) simp

931 thus ?case by simp

932 next

933 case LVar

934 thus ?case by (simp add: lvar_def Let_def)

935 next

936 case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env)

937 note G = \<open>prg Env = G\<close>

938 from wf FVar.prems

939 obtain statC f where

940 wt_e: "Env\<turnstile>e\<Colon>-Class statC" and

941 accfield: "accfield (prg Env) accC statC fn = Some (statDeclC,f)"

942 by (elim wt_elim_cases) simp

943 have wt_init: "Env\<turnstile>Init statDeclC\<Colon>\<surd>"

944 proof -

945 from wf wt_e G

946 have "is_class (prg Env) statC"

947 by (auto dest: ty_expr_is_type type_is_class)

948 with wf accfield G

949 have "is_class (prg Env) statDeclC"

950 by (auto dest!: accfield_fields dest: fields_declC)

951 thus ?thesis

952 by simp

953 qed

954 note fvar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>

955 {

956 fix j

957 assume jmp: "abrupt s3 = Some (Jump j)"

958 have "j\<in>jmps"

959 proof -

960 note hyp_init = \<open>PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>\<close>

961 from G wt_init

962 have "?Jmp jmps s1"

963 by - (rule hyp_init [THEN conjunct1],auto)

964 moreover

965 note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 a)\<close>

966 have "abrupt s2 = Some (Jump j)"

967 proof -

968 note \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>

969 with jmp have "abrupt s2' = Some (Jump j)"

970 by (cases s2')

971 (simp add: check_field_access_def abrupt_if_def Let_def)

972 with fvar show "abrupt s2 = Some (Jump j)"

973 by (cases s2) (simp add: fvar_def2 abrupt_if_def)

974 qed

975 ultimately show ?thesis

976 using G wt_e

977 by - (rule hyp_e [THEN conjunct1, rule_format (no_asm)],simp_all)

978 qed

979 }

980 moreover

981 from fvar obtain upd w

982 where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and

983 v: "v=(w,upd)"

984 by (cases "fvar statDeclC stat fn a s2") simp

985 {

986 fix j val fix s::state

987 assume "normal s3"

988 assume no_jmp: "abrupt s \<noteq> Some (Jump j)"

989 with upd

990 have "abrupt (upd val s) \<noteq> Some (Jump j)"

991 by (rule fvar_upd_no_jump)

992 }

993 ultimately show ?case using v by simp

994 next

995 case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)

996 note G = \<open>prg Env = G\<close>

997 from AVar.prems

998 obtain e1T e2T where

999 wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"

1000 by (elim wt_elim_cases) simp

1001 note avar = \<open>(v, s2') = avar G i a s2\<close>

1002 {

1003 fix j

1004 assume jmp: "abrupt s2' = Some (Jump j)"

1005 have "j\<in>jmps"

1006 proof -

1007 note hyp_e1 = \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)\<close>

1008 from G wt_e1

1009 have "?Jmp jmps s1"

1010 by - (rule hyp_e1 [THEN conjunct1], auto)

1011 moreover

1012 note hyp_e2 = \<open>PROP ?Hyp (In1l e2) s1 s2 (In1 i)\<close>

1013 have "abrupt s2 = Some (Jump j)"

1014 proof -

1015 from avar have "s2' = snd (avar G i a s2)"

1016 by (cases "avar G i a s2") simp

1017 with jmp show ?thesis by - (rule avar_state_no_jump,simp)

1018 qed

1019 ultimately show ?thesis

1020 using wt_e2 G

1021 by - (rule hyp_e2 [THEN conjunct1, rule_format (no_asm)],simp_all)

1022 qed

1023 }

1024 moreover

1025 from avar obtain upd w

1026 where upd: "upd = snd (fst (avar G i a s2))" and

1027 v: "v=(w,upd)"

1028 by (cases "avar G i a s2") simp

1029 {

1030 fix j val fix s::state

1031 assume "normal s2'"

1032 assume no_jmp: "abrupt s \<noteq> Some (Jump j)"

1033 with upd

1034 have "abrupt (upd val s) \<noteq> Some (Jump j)"

1035 by (rule avar_upd_no_jump)

1036 }

1037 ultimately show ?case using v by simp

1038 next

1039 case Nil thus ?case by simp

1040 next

1041 case (Cons s0 e v s1 es vs s2 jmps T Env)

1042 note G = \<open>prg Env = G\<close>

1043 from Cons.prems obtain eT esT

1044 where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_e2: "Env\<turnstile>es\<Colon>\<doteq>esT"

1045 by (elim wt_elim_cases) simp

1046 {

1047 fix j

1048 assume jmp: "abrupt s2 = Some (Jump j)"

1049 have "j\<in>jmps"

1050 proof -

1051 note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>

1052 from G wt_e

1053 have "?Jmp jmps s1"

1054 by - (rule hyp_e [THEN conjunct1],simp_all)

1055 moreover

1056 note hyp_es = \<open>PROP ?Hyp (In3 es) s1 s2 (In3 vs)\<close>

1057 ultimately show ?thesis

1058 using wt_e2 G jmp

1059 by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],

1060 (assumption|simp (no_asm_simp))+)

1061 qed

1062 }

1063 thus ?case by simp

1064 qed

1065 note generalized = this

1066 from no_jmp jmpOk wt G

1067 show ?thesis

1068 by (rule generalized)

1069 qed

1071 lemmas jumpNestingOk_evalE = jumpNestingOk_eval [THEN conjE,rule_format]

1074 lemma jumpNestingOk_eval_no_jump:

1075 assumes eval: "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and

1076 jmpOk: "jumpNestingOk {} t" and

1077 no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and

1078 wt: "Env\<turnstile>t\<Colon>T" and

1079 wf: "wf_prog (prg Env)"

1080 shows "abrupt s1 \<noteq> Some (Jump j) \<and>

1081 (normal s1 \<longrightarrow> v=In2 (w,upd)

1082 \<longrightarrow> abrupt s \<noteq> Some (Jump j')

1083 \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j'))"

1084 proof (cases "\<exists> j'. abrupt s0 = Some (Jump j')")

1085 case True

1086 then obtain j' where jmp: "abrupt s0 = Some (Jump j')" ..

1087 with no_jmp have "j'\<noteq>j" by simp

1088 with eval jmp have "s1=s0" by auto

1089 with no_jmp jmp show ?thesis by simp

1090 next

1091 case False

1092 obtain G where G: "prg Env = G"

1093 by (cases Env) simp

1094 from G eval have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by simp

1095 moreover note jmpOk wt

1096 moreover from G wf have "wf_prog G" by simp

1097 moreover note G

1098 moreover from False have "\<And> j. abrupt s0 = Some (Jump j) \<Longrightarrow> j \<in> {}"

1099 by simp

1100 ultimately show ?thesis

1101 apply (rule jumpNestingOk_evalE)

1102 apply assumption

1103 apply simp

1104 apply fastforce

1105 done

1106 qed

1108 lemmas jumpNestingOk_eval_no_jumpE

1109 = jumpNestingOk_eval_no_jump [THEN conjE,rule_format]

1111 corollary eval_expression_no_jump:

1112 assumes eval: "prg Env\<turnstile>s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and

1113 no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and

1114 wt: "Env\<turnstile>e\<Colon>-T" and

1115 wf: "wf_prog (prg Env)"

1116 shows "abrupt s1 \<noteq> Some (Jump j)"

1117 using eval _ no_jmp wt wf

1118 by (rule jumpNestingOk_eval_no_jumpE, simp_all)

1120 corollary eval_var_no_jump:

1121 assumes eval: "prg Env\<turnstile>s0 \<midarrow>var=\<succ>(w,upd)\<rightarrow> s1" and

1122 no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and

1123 wt: "Env\<turnstile>var\<Colon>=T" and

1124 wf: "wf_prog (prg Env)"

1125 shows "abrupt s1 \<noteq> Some (Jump j) \<and>

1126 (normal s1 \<longrightarrow>

1127 (abrupt s \<noteq> Some (Jump j')

1128 \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j')))"

1129 apply (rule_tac upd="upd" and val="val" and s="s" and w="w" and j'=j'

1130 in jumpNestingOk_eval_no_jumpE [OF eval _ no_jmp wt wf])

1131 by simp_all

1133 lemmas eval_var_no_jumpE = eval_var_no_jump [THEN conjE,rule_format]

1135 corollary eval_statement_no_jump:

1136 assumes eval: "prg Env\<turnstile>s0 \<midarrow>c\<rightarrow> s1" and

1137 jmpOk: "jumpNestingOkS {} c" and

1138 no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and

1139 wt: "Env\<turnstile>c\<Colon>\<surd>" and

1140 wf: "wf_prog (prg Env)"

1141 shows "abrupt s1 \<noteq> Some (Jump j)"

1142 using eval _ no_jmp wt wf

1143 by (rule jumpNestingOk_eval_no_jumpE) (simp_all add: jmpOk)

1145 corollary eval_expression_list_no_jump:

1146 assumes eval: "prg Env\<turnstile>s0 \<midarrow>es\<doteq>\<succ>v\<rightarrow> s1" and

1147 no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and

1148 wt: "Env\<turnstile>es\<Colon>\<doteq>T" and

1149 wf: "wf_prog (prg Env)"

1150 shows "abrupt s1 \<noteq> Some (Jump j)"

1151 using eval _ no_jmp wt wf

1152 by (rule jumpNestingOk_eval_no_jumpE, simp_all)

1154 (* ### FIXME: Do i need this *)

1155 lemma union_subseteq_elim [elim]: "\<lbrakk>A \<union> B \<subseteq> C; \<lbrakk>A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"

1156 by blast

1158 lemma dom_locals_halloc_mono:

1159 assumes halloc: "G\<turnstile>s0\<midarrow>halloc oi\<succ>a\<rightarrow>s1"

1160 shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"

1161 proof -

1162 from halloc show ?thesis

1163 by cases simp_all

1164 qed

1166 lemma dom_locals_sxalloc_mono:

1167 assumes sxalloc: "G\<turnstile>s0\<midarrow>sxalloc\<rightarrow>s1"

1168 shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"

1169 proof -

1170 from sxalloc show ?thesis

1171 proof (cases)

1172 case Norm thus ?thesis by simp

1173 next

1174 case Jmp thus ?thesis by simp

1175 next

1176 case Error thus ?thesis by simp

1177 next

1178 case XcptL thus ?thesis by simp

1179 next

1180 case SXcpt thus ?thesis

1181 by - (drule dom_locals_halloc_mono,simp)

1182 qed

1183 qed

1186 lemma dom_locals_assign_mono:

1187 assumes f_ok: "dom (locals (store s)) \<subseteq> dom (locals (store (f n s)))"

1188 shows "dom (locals (store s)) \<subseteq> dom (locals (store (assign f n s)))"

1189 proof (cases "normal s")

1190 case False thus ?thesis

1191 by (cases s) (auto simp add: assign_def Let_def)

1192 next

1193 case True

1194 then obtain s' where s': "s = (None,s')"

1195 by auto

1196 moreover

1197 obtain x1 s1 where "f n s = (x1,s1)"

1198 by (cases "f n s")

1199 ultimately

1200 show ?thesis

1201 using f_ok

1202 by (simp add: assign_def Let_def)

1203 qed

1205 (*

1206 lemma dom_locals_init_lvars_mono:

1207 "dom (locals (store s))

1208 \<subseteq> dom (locals (store (init_lvars G D sig mode a vs s)))"

1209 proof (cases "mode = Static")

1210 case True

1211 thus ?thesis

1212 apply (cases s)

1213 apply (simp add: init_lvars_def Let_def)

1214 *)

1216 lemma dom_locals_lvar_mono:

1217 "dom (locals (store s)) \<subseteq> dom (locals (store (snd (lvar vn s') val s)))"

1218 by (simp add: lvar_def) blast

1221 lemma dom_locals_fvar_vvar_mono:

1222 "dom (locals (store s))

1223 \<subseteq> dom (locals (store (snd (fst (fvar statDeclC stat fn a s')) val s)))"

1224 proof (cases stat)

1225 case True

1226 thus ?thesis

1227 by (cases s) (simp add: fvar_def2)

1228 next

1229 case False

1230 thus ?thesis

1231 by (cases s) (simp add: fvar_def2)

1232 qed

1234 lemma dom_locals_fvar_mono:

1235 "dom (locals (store s))

1236 \<subseteq> dom (locals (store (snd (fvar statDeclC stat fn a s))))"

1237 proof (cases stat)

1238 case True

1239 thus ?thesis

1240 by (cases s) (simp add: fvar_def2)

1241 next

1242 case False

1243 thus ?thesis

1244 by (cases s) (simp add: fvar_def2)

1245 qed

1248 lemma dom_locals_avar_vvar_mono:

1249 "dom (locals (store s))

1250 \<subseteq> dom (locals (store (snd (fst (avar G i a s')) val s)))"

1251 by (cases s, simp add: avar_def2)

1253 lemma dom_locals_avar_mono:

1254 "dom (locals (store s))

1255 \<subseteq> dom (locals (store (snd (avar G i a s))))"

1256 by (cases s, simp add: avar_def2)

1258 text \<open>

1259 Since assignments are modelled as functions from states to states, we

1260 must take into account these functions. They appear only in the assignment

1261 rule and as result from evaluating a variable. Thats why we need the

1262 complicated second part of the conjunction in the goal.

1263 The reason for the very generic way to treat assignments was the aim

1264 to omit redundancy. There is only one evaluation rule for each kind of

1265 variable (locals, fields, arrays). These rules are used for both accessing

1266 variables and updating variables. Thats why the evaluation rules for variables

1267 result in a pair consisting of a value and an update function. Of course we

1268 could also think of a pair of a value and a reference in the store, instead of

1269 the generic update function. But as only array updates can cause a special

1270 exception (if the types mismatch) and not array reads we then have to introduce

1271 two different rules to handle array reads and updates\<close>

1272 lemma dom_locals_eval_mono:

1273 assumes eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"

1274 shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1)) \<and>

1275 (\<forall> vv. v=In2 vv \<and> normal s1

1276 \<longrightarrow> (\<forall> s val. dom (locals (store s))

1277 \<subseteq> dom (locals (store ((snd vv) val s)))))"

1278 proof -

1279 from eval show ?thesis

1280 proof (induct)

1281 case Abrupt thus ?case by simp

1282 next

1283 case Skip thus ?case by simp

1284 next

1285 case Expr thus ?case by simp

1286 next

1287 case Lab thus ?case by simp

1288 next

1289 case (Comp s0 c1 s1 c2 s2)

1290 from Comp.hyps

1291 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1292 by simp

1293 also

1294 from Comp.hyps

1295 have "\<dots> \<subseteq> dom (locals (store s2))"

1296 by simp

1297 finally show ?case by simp

1298 next

1299 case (If s0 e b s1 c1 c2 s2)

1300 from If.hyps

1301 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1302 by simp

1303 also

1304 from If.hyps

1305 have "\<dots> \<subseteq> dom (locals (store s2))"

1306 by simp

1307 finally show ?case by simp

1308 next

1309 case (Loop s0 e b s1 c s2 l s3)

1310 show ?case

1311 proof (cases "the_Bool b")

1312 case True

1313 with Loop.hyps

1314 obtain

1315 s0_s1:

1316 "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" and

1317 s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" and

1318 s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"

1319 by simp

1320 note s0_s1 also note s1_s2 also note s2_s3

1321 finally show ?thesis

1322 by simp

1323 next

1324 case False

1325 with Loop.hyps show ?thesis

1326 by simp

1327 qed

1328 next

1329 case Jmp thus ?case by simp

1330 next

1331 case Throw thus ?case by simp

1332 next

1333 case (Try s0 c1 s1 s2 C vn c2 s3)

1334 then

1335 have s0_s1: "dom (locals (store ((Norm s0)::state)))

1336 \<subseteq> dom (locals (store s1))" by simp

1337 from \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>

1338 have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"

1339 by (rule dom_locals_sxalloc_mono)

1340 thus ?case

1341 proof (cases "G,s2\<turnstile>catch C")

1342 case True

1343 note s0_s1 also note s1_s2

1344 also

1345 from True Try.hyps

1346 have "dom (locals (store (new_xcpt_var vn s2)))

1347 \<subseteq> dom (locals (store s3))"

1348 by simp

1349 hence "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"

1350 by (cases s2, simp )

1351 finally show ?thesis by simp

1352 next

1353 case False

1354 note s0_s1 also note s1_s2

1355 finally

1356 show ?thesis

1357 using False Try.hyps by simp

1358 qed

1359 next

1360 case (Fin s0 c1 x1 s1 c2 s2 s3)

1361 show ?case

1362 proof (cases "\<exists>err. x1 = Some (Error err)")

1363 case True

1364 with Fin.hyps show ?thesis

1365 by simp

1366 next

1367 case False

1368 from Fin.hyps

1369 have "dom (locals (store ((Norm s0)::state)))

1370 \<subseteq> dom (locals (store (x1, s1)))"

1371 by simp

1372 hence "dom (locals (store ((Norm s0)::state)))

1373 \<subseteq> dom (locals (store ((Norm s1)::state)))"

1374 by simp

1375 also

1376 from Fin.hyps

1377 have "\<dots> \<subseteq> dom (locals (store s2))"

1378 by simp

1379 finally show ?thesis

1380 using Fin.hyps by simp

1381 qed

1382 next

1383 case (Init C c s0 s3 s1 s2)

1384 show ?case

1385 proof (cases "inited C (globs s0)")

1386 case True

1387 with Init.hyps show ?thesis by simp

1388 next

1389 case False

1390 with Init.hyps

1391 obtain s0_s1: "dom (locals (store (Norm ((init_class_obj G C) s0))))

1392 \<subseteq> dom (locals (store s1))" and

1393 s3: "s3 = (set_lvars (locals (snd s1))) s2"

1394 by simp

1395 from s0_s1

1396 have "dom (locals (store (Norm s0))) \<subseteq> dom (locals (store s1))"

1397 by (cases s0) simp

1398 with s3

1399 have "dom (locals (store (Norm s0))) \<subseteq> dom (locals (store s3))"

1400 by (cases s2) simp

1401 thus ?thesis by simp

1402 qed

1403 next

1404 case (NewC s0 C s1 a s2)

1405 note halloc = \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close>

1406 from NewC.hyps

1407 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1408 by simp

1409 also

1410 from halloc

1411 have "\<dots> \<subseteq> dom (locals (store s2))" by (rule dom_locals_halloc_mono)

1412 finally show ?case by simp

1413 next

1414 case (NewA s0 T s1 e i s2 a s3)

1415 note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3\<close>

1416 from NewA.hyps

1417 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1418 by simp

1419 also

1420 from NewA.hyps

1421 have "\<dots> \<subseteq> dom (locals (store s2))" by simp

1422 also

1423 from halloc

1424 have "\<dots> \<subseteq> dom (locals (store s3))"

1425 by (rule dom_locals_halloc_mono [elim_format]) simp

1426 finally show ?case by simp

1427 next

1428 case Cast thus ?case by simp

1429 next

1430 case Inst thus ?case by simp

1431 next

1432 case Lit thus ?case by simp

1433 next

1434 case UnOp thus ?case by simp

1435 next

1436 case (BinOp s0 e1 v1 s1 binop e2 v2 s2)

1437 from BinOp.hyps

1438 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1439 by simp

1440 also

1441 from BinOp.hyps

1442 have "\<dots> \<subseteq> dom (locals (store s2))" by simp

1443 finally show ?case by simp

1444 next

1445 case Super thus ?case by simp

1446 next

1447 case Acc thus ?case by simp

1448 next

1449 case (Ass s0 va w f s1 e v s2)

1450 from Ass.hyps

1451 have s0_s1:

1452 "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1453 by simp

1454 show ?case

1455 proof (cases "normal s1")

1456 case True

1457 with Ass.hyps

1458 have ass_ok:

1459 "\<And> s val. dom (locals (store s)) \<subseteq> dom (locals (store (f val s)))"

1460 by simp

1461 note s0_s1

1462 also

1463 from Ass.hyps

1464 have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"

1465 by simp

1466 also

1467 from ass_ok

1468 have "\<dots> \<subseteq> dom (locals (store (assign f v s2)))"

1469 by (rule dom_locals_assign_mono [where f = f])

1470 finally show ?thesis by simp

1471 next

1472 case False

1473 with \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close>

1474 have "s2=s1"

1475 by auto

1476 with s0_s1 False

1477 have "dom (locals (store ((Norm s0)::state)))

1478 \<subseteq> dom (locals (store (assign f v s2)))"

1479 by simp

1480 thus ?thesis

1481 by simp

1482 qed

1483 next

1484 case (Cond s0 e0 b s1 e1 e2 v s2)

1485 from Cond.hyps

1486 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1487 by simp

1488 also

1489 from Cond.hyps

1490 have "\<dots> \<subseteq> dom (locals (store s2))"

1491 by simp

1492 finally show ?case by simp

1493 next

1494 case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)

1495 note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close>

1496 from Call.hyps

1497 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1498 by simp

1499 also

1500 from Call.hyps

1501 have "\<dots> \<subseteq> dom (locals (store s2))"

1502 by simp

1503 also

1504 have "\<dots> \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"

1505 by (cases s4) simp

1506 finally show ?case by simp

1507 next

1508 case Methd thus ?case by simp

1509 next

1510 case (Body s0 D s1 c s2 s3)

1511 from Body.hyps

1512 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1513 by simp

1514 also

1515 from Body.hyps

1516 have "\<dots> \<subseteq> dom (locals (store s2))"

1517 by simp

1518 also

1519 have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s2)))"

1520 by simp

1521 also

1522 have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"

1523 proof -

1524 from \<open>s3 =

1525 (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>

1526 abrupt s2 = Some (Jump (Cont l))

1527 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)\<close>

1528 show ?thesis

1529 by simp

1530 qed

1531 finally show ?case by simp

1532 next

1533 case LVar

1534 thus ?case

1535 using dom_locals_lvar_mono

1536 by simp

1537 next

1538 case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)

1539 from FVar.hyps

1540 obtain s2': "s2' = snd (fvar statDeclC stat fn a s2)" and

1541 v: "v = fst (fvar statDeclC stat fn a s2)"

1542 by (cases "fvar statDeclC stat fn a s2" ) simp

1543 from v

1544 have "\<forall>s val. dom (locals (store s))

1545 \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok")

1546 by (simp add: dom_locals_fvar_vvar_mono)

1547 hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s3 \<longrightarrow> ?V_ok)"

1548 by - (intro strip, simp)

1549 note s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>

1550 from FVar.hyps

1551 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1552 by simp

1553 also

1554 from FVar.hyps

1555 have "\<dots> \<subseteq> dom (locals (store s2))"

1556 by simp

1557 also

1558 from s2'

1559 have "\<dots> \<subseteq> dom (locals (store s2'))"

1560 by (simp add: dom_locals_fvar_mono)

1561 also

1562 from s3

1563 have "\<dots> \<subseteq> dom (locals (store s3))"

1564 by (simp add: check_field_access_def Let_def)

1565 finally

1566 show ?case

1567 using v_ok

1568 by simp

1569 next

1570 case (AVar s0 e1 a s1 e2 i s2 v s2')

1571 from AVar.hyps

1572 obtain s2': "s2' = snd (avar G i a s2)" and

1573 v: "v = fst (avar G i a s2)"

1574 by (cases "avar G i a s2") simp

1575 from v

1576 have "\<forall>s val. dom (locals (store s))

1577 \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok")

1578 by (simp add: dom_locals_avar_vvar_mono)

1579 hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s2' \<longrightarrow> ?V_ok)"

1580 by - (intro strip, simp)

1581 from AVar.hyps

1582 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1583 by simp

1584 also

1585 from AVar.hyps

1586 have "\<dots> \<subseteq> dom (locals (store s2))"

1587 by simp

1588 also

1589 from s2'

1590 have "\<dots> \<subseteq> dom (locals (store s2'))"

1591 by (simp add: dom_locals_avar_mono)

1592 finally

1593 show ?case using v_ok by simp

1594 next

1595 case Nil thus ?case by simp

1596 next

1597 case (Cons s0 e v s1 es vs s2)

1598 from Cons.hyps

1599 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

1600 by simp

1601 also

1602 from Cons.hyps

1603 have "\<dots> \<subseteq> dom (locals (store s2))"

1604 by simp

1605 finally show ?case by simp

1606 qed

1607 qed

1609 lemma dom_locals_eval_mono_elim:

1610 assumes eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"

1611 obtains "dom (locals (store s0)) \<subseteq> dom (locals (store s1))" and

1612 "\<And> vv s val. \<lbrakk>v=In2 vv; normal s1\<rbrakk>

1613 \<Longrightarrow> dom (locals (store s))

1614 \<subseteq> dom (locals (store ((snd vv) val s)))"

1615 using eval by (rule dom_locals_eval_mono [THEN conjE]) (rule that, auto)

1617 lemma halloc_no_abrupt:

1618 assumes halloc: "G\<turnstile>s0\<midarrow>halloc oi\<succ>a\<rightarrow>s1" and

1619 normal: "normal s1"

1620 shows "normal s0"

1621 proof -

1622 from halloc normal show ?thesis

1623 by cases simp_all

1624 qed

1626 lemma sxalloc_mono_no_abrupt:

1627 assumes sxalloc: "G\<turnstile>s0\<midarrow>sxalloc\<rightarrow>s1" and

1628 normal: "normal s1"

1629 shows "normal s0"

1630 proof -

1631 from sxalloc normal show ?thesis

1632 by cases simp_all

1633 qed

1635 lemma union_subseteqI: "\<lbrakk>A \<union> B \<subseteq> C; A' \<subseteq> A; B' \<subseteq> B\<rbrakk> \<Longrightarrow> A' \<union> B' \<subseteq> C"

1636 by blast

1638 lemma union_subseteqIl: "\<lbrakk>A \<union> B \<subseteq> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A' \<union> B \<subseteq> C"

1639 by blast

1641 lemma union_subseteqIr: "\<lbrakk>A \<union> B \<subseteq> C; B' \<subseteq> B\<rbrakk> \<Longrightarrow> A \<union> B' \<subseteq> C"

1642 by blast

1644 lemma subseteq_union_transl [trans]: "\<lbrakk>A \<subseteq> B; B \<union> C \<subseteq> D\<rbrakk> \<Longrightarrow> A \<union> C \<subseteq> D"

1645 by blast

1647 lemma subseteq_union_transr [trans]: "\<lbrakk>A \<subseteq> B; C \<union> B \<subseteq> D\<rbrakk> \<Longrightarrow> A \<union> C \<subseteq> D"

1648 by blast

1650 lemma union_subseteq_weaken: "\<lbrakk>A \<union> B \<subseteq> C; \<lbrakk>A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"

1651 by blast

1653 lemma assigns_good_approx:

1654 assumes

1655 eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and

1656 normal: "normal s1"

1657 shows "assigns t \<subseteq> dom (locals (store s1))"

1658 proof -

1659 from eval normal show ?thesis

1660 proof (induct)

1661 case Abrupt thus ?case by simp

1662 next \<comment> \<open>For statements its trivial, since then @{term "assigns t = {}"}\<close>

1663 case Skip show ?case by simp

1664 next

1665 case Expr show ?case by simp

1666 next

1667 case Lab show ?case by simp

1668 next

1669 case Comp show ?case by simp

1670 next

1671 case If show ?case by simp

1672 next

1673 case Loop show ?case by simp

1674 next

1675 case Jmp show ?case by simp

1676 next

1677 case Throw show ?case by simp

1678 next

1679 case Try show ?case by simp

1680 next

1681 case Fin show ?case by simp

1682 next

1683 case Init show ?case by simp

1684 next

1685 case NewC show ?case by simp

1686 next

1687 case (NewA s0 T s1 e i s2 a s3)

1688 note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3\<close>

1689 have "assigns (In1l e) \<subseteq> dom (locals (store s2))"

1690 proof -

1691 from NewA

1692 have "normal (abupd (check_neg i) s2)"

1693 by - (erule halloc_no_abrupt [rule_format])

1694 hence "normal s2" by (cases s2) simp

1695 with NewA.hyps

1696 show ?thesis by iprover

1697 qed

1698 also

1699 from halloc

1700 have "\<dots> \<subseteq> dom (locals (store s3))"

1701 by (rule dom_locals_halloc_mono [elim_format]) simp

1702 finally show ?case by simp

1703 next

1704 case (Cast s0 e v s1 s2 T)

1705 hence "normal s1" by (cases s1,simp)

1706 with Cast.hyps

1707 have "assigns (In1l e) \<subseteq> dom (locals (store s1))"

1708 by simp

1709 also

1710 from Cast.hyps

1711 have "\<dots> \<subseteq> dom (locals (store s2))"

1712 by simp

1713 finally

1714 show ?case

1715 by simp

1716 next

1717 case Inst thus ?case by simp

1718 next

1719 case Lit thus ?case by simp

1720 next

1721 case UnOp thus ?case by simp

1722 next

1723 case (BinOp s0 e1 v1 s1 binop e2 v2 s2)

1724 hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])

1725 with BinOp.hyps

1726 have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"

1727 by iprover

1728 also

1729 have "\<dots> \<subseteq> dom (locals (store s2))"

1730 proof -

1731 note \<open>G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2

1732 else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)\<close>

1733 thus ?thesis

1734 by (rule dom_locals_eval_mono_elim)

1735 qed

1736 finally have s2: "assigns (In1l e1) \<subseteq> dom (locals (store s2))" .

1737 show ?case

1738 proof (cases "binop=CondAnd \<or> binop=CondOr")

1739 case True

1740 with s2 show ?thesis by simp

1741 next

1742 case False

1743 with BinOp

1744 have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"

1745 by (simp add: need_second_arg_def)

1746 with s2

1747 show ?thesis using False by simp

1748 qed

1749 next

1750 case Super thus ?case by simp

1751 next

1752 case Acc thus ?case by simp

1753 next

1754 case (Ass s0 va w f s1 e v s2)

1755 note nrm_ass_s2 = \<open>normal (assign f v s2)\<close>

1756 hence nrm_s2: "normal s2"

1757 by (cases s2, simp add: assign_def Let_def)

1758 with Ass.hyps

1759 have nrm_s1: "normal s1"

1760 by - (erule eval_no_abrupt_lemma [rule_format])

1761 with Ass.hyps

1762 have "assigns (In2 va) \<subseteq> dom (locals (store s1))"

1763 by iprover

1764 also

1765 from Ass.hyps

1766 have "\<dots> \<subseteq> dom (locals (store s2))"

1767 by - (erule dom_locals_eval_mono_elim)

1768 also

1769 from nrm_s2 Ass.hyps

1770 have "assigns (In1l e) \<subseteq> dom (locals (store s2))"

1771 by iprover

1772 ultimately

1773 have "assigns (In2 va) \<union> assigns (In1l e) \<subseteq> dom (locals (store s2))"

1774 by (rule Un_least)

1775 also

1776 from Ass.hyps nrm_s1

1777 have "\<dots> \<subseteq> dom (locals (store (f v s2)))"

1778 by - (erule dom_locals_eval_mono_elim, cases s2,simp)

1779 then

1780 have "dom (locals (store s2)) \<subseteq> dom (locals (store (assign f v s2)))"

1781 by (rule dom_locals_assign_mono)

1782 finally

1783 have va_e: " assigns (In2 va) \<union> assigns (In1l e)

1784 \<subseteq> dom (locals (snd (assign f v s2)))" .

1785 show ?case

1786 proof (cases "\<exists> n. va = LVar n")

1787 case False

1788 with va_e show ?thesis

1789 by (simp add: Un_assoc)

1790 next

1791 case True

1792 then obtain n where va: "va = LVar n"

1793 by blast

1794 with Ass.hyps

1795 have "G\<turnstile>Norm s0 \<midarrow>LVar n=\<succ>(w,f)\<rightarrow> s1"

1796 by simp

1797 hence "(w,f) = lvar n s0"

1798 by (rule eval_elim_cases) simp

1799 with nrm_ass_s2

1800 have "n \<in> dom (locals (store (assign f v s2)))"

1801 by (cases s2) (simp add: assign_def Let_def lvar_def)

1802 with va_e True va

1803 show ?thesis by (simp add: Un_assoc)

1804 qed

1805 next

1806 case (Cond s0 e0 b s1 e1 e2 v s2)

1807 hence "normal s1"

1808 by - (erule eval_no_abrupt_lemma [rule_format])

1809 with Cond.hyps

1810 have "assigns (In1l e0) \<subseteq> dom (locals (store s1))"

1811 by iprover

1812 also from Cond.hyps

1813 have "\<dots> \<subseteq> dom (locals (store s2))"

1814 by - (erule dom_locals_eval_mono_elim)

1815 finally have e0: "assigns (In1l e0) \<subseteq> dom (locals (store s2))" .

1816 show ?case

1817 proof (cases "the_Bool b")

1818 case True

1819 with Cond

1820 have "assigns (In1l e1) \<subseteq> dom (locals (store s2))"

1821 by simp

1822 hence "assigns (In1l e1) \<inter> assigns (In1l e2) \<subseteq> \<dots>"

1823 by blast

1824 with e0

1825 have "assigns (In1l e0) \<union> assigns (In1l e1) \<inter> assigns (In1l e2)

1826 \<subseteq> dom (locals (store s2))"

1827 by (rule Un_least)

1828 thus ?thesis using True by simp

1829 next

1830 case False

1831 with Cond

1832 have " assigns (In1l e2) \<subseteq> dom (locals (store s2))"

1833 by simp

1834 hence "assigns (In1l e1) \<inter> assigns (In1l e2) \<subseteq> \<dots>"

1835 by blast

1836 with e0

1837 have "assigns (In1l e0) \<union> assigns (In1l e1) \<inter> assigns (In1l e2)

1838 \<subseteq> dom (locals (store s2))"

1839 by (rule Un_least)

1840 thus ?thesis using False by simp

1841 qed

1842 next

1843 case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)

1844 have nrm_s2: "normal s2"

1845 proof -

1846 from \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>

1847 have normal_s4: "normal s4" by simp

1848 hence "normal s3'" using Call.hyps

1849 by - (erule eval_no_abrupt_lemma [rule_format])

1850 moreover note

1851 \<open>s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3\<close>

1852 ultimately have "normal s3"

1853 by (cases s3) (simp add: check_method_access_def Let_def)

1854 moreover

1855 note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close>

1856 ultimately show "normal s2"

1857 by (cases s2) (simp add: init_lvars_def2)

1858 qed

1859 hence "normal s1" using Call.hyps

1860 by - (erule eval_no_abrupt_lemma [rule_format])

1861 with Call.hyps

1862 have "assigns (In1l e) \<subseteq> dom (locals (store s1))"

1863 by iprover

1864 also from Call.hyps

1865 have "\<dots> \<subseteq> dom (locals (store s2))"

1866 by - (erule dom_locals_eval_mono_elim)

1867 also

1868 from nrm_s2 Call.hyps

1869 have "assigns (In3 args) \<subseteq> dom (locals (store s2))"

1870 by iprover

1871 ultimately have "assigns (In1l e) \<union> assigns (In3 args) \<subseteq> \<dots>"

1872 by (rule Un_least)

1873 also

1874 have "\<dots> \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"

1875 by (cases s4) simp

1876 finally show ?case

1877 by simp

1878 next

1879 case Methd thus ?case by simp

1880 next

1881 case Body thus ?case by simp

1882 next

1883 case LVar thus ?case by simp

1884 next

1885 case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)

1886 note s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>

1887 note avar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>

1888 have nrm_s2: "normal s2"

1889 proof -

1890 note \<open>normal s3\<close>

1891 with s3 have "normal s2'"

1892 by (cases s2') (simp add: check_field_access_def Let_def)

1893 with avar show "normal s2"

1894 by (cases s2) (simp add: fvar_def2)

1895 qed

1896 with FVar.hyps

1897 have "assigns (In1l e) \<subseteq> dom (locals (store s2))"

1898 by iprover

1899 also

1900 have "\<dots> \<subseteq> dom (locals (store s2'))"

1901 proof -

1902 from avar

1903 have "s2' = snd (fvar statDeclC stat fn a s2)"

1904 by (cases "fvar statDeclC stat fn a s2") simp

1905 thus ?thesis

1906 by simp (rule dom_locals_fvar_mono)

1907 qed

1908 also from s3

1909 have "\<dots> \<subseteq> dom (locals (store s3))"

1910 by (cases s2') (simp add: check_field_access_def Let_def)

1911 finally show ?case

1912 by simp

1913 next

1914 case (AVar s0 e1 a s1 e2 i s2 v s2')

1915 note avar = \<open>(v, s2') = avar G i a s2\<close>

1916 have nrm_s2: "normal s2"

1917 proof -

1918 from avar and \<open>normal s2'\<close>

1919 show ?thesis by (cases s2) (simp add: avar_def2)

1920 qed

1921 with AVar.hyps

1922 have "normal s1"

1923 by - (erule eval_no_abrupt_lemma [rule_format])

1924 with AVar.hyps

1925 have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"

1926 by iprover

1927 also from AVar.hyps

1928 have "\<dots> \<subseteq> dom (locals (store s2))"

1929 by - (erule dom_locals_eval_mono_elim)

1930 also

1931 from AVar.hyps nrm_s2

1932 have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"

1933 by iprover

1934 ultimately

1935 have "assigns (In1l e1) \<union> assigns (In1l e2) \<subseteq> \<dots>"

1936 by (rule Un_least)

1937 also

1938 have "dom (locals (store s2)) \<subseteq> dom (locals (store s2'))"

1939 proof -

1940 from avar have "s2' = snd (avar G i a s2)"

1941 by (cases "avar G i a s2") simp

1942 thus ?thesis

1943 by simp (rule dom_locals_avar_mono)

1944 qed

1945 finally

1946 show ?case

1947 by simp

1948 next

1949 case Nil show ?case by simp

1950 next

1951 case (Cons s0 e v s1 es vs s2)

1952 have "assigns (In1l e) \<subseteq> dom (locals (store s1))"

1953 proof -

1954 from Cons

1955 have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])

1956 with Cons.hyps show ?thesis by iprover

1957 qed

1958 also from Cons.hyps

1959 have "\<dots> \<subseteq> dom (locals (store s2))"

1960 by - (erule dom_locals_eval_mono_elim)

1961 also from Cons

1962 have "assigns (In3 es) \<subseteq> dom (locals (store s2))"

1963 by iprover

1964 ultimately

1965 have "assigns (In1l e) \<union> assigns (In3 es) \<subseteq> dom (locals (store s2))"

1966 by (rule Un_least)

1967 thus ?case

1968 by simp

1969 qed

1970 qed

1972 corollary assignsE_good_approx:

1973 assumes

1974 eval: "prg Env\<turnstile> s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and

1975 normal: "normal s1"

1976 shows "assignsE e \<subseteq> dom (locals (store s1))"

1977 proof -

1978 from eval normal show ?thesis

1979 by (rule assigns_good_approx [elim_format]) simp

1980 qed

1982 corollary assignsV_good_approx:

1983 assumes

1984 eval: "prg Env\<turnstile> s0 \<midarrow>v=\<succ>vf\<rightarrow> s1" and

1985 normal: "normal s1"

1986 shows "assignsV v \<subseteq> dom (locals (store s1))"

1987 proof -

1988 from eval normal show ?thesis

1989 by (rule assigns_good_approx [elim_format]) simp

1990 qed

1992 corollary assignsEs_good_approx:

1993 assumes

1994 eval: "prg Env\<turnstile> s0 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s1" and

1995 normal: "normal s1"

1996 shows "assignsEs es \<subseteq> dom (locals (store s1))"

1997 proof -

1998 from eval normal show ?thesis

1999 by (rule assigns_good_approx [elim_format]) simp

2000 qed

2002 lemma constVal_eval:

2003 assumes const: "constVal e = Some c" and

2004 eval: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s"

2005 shows "v = c \<and> normal s"

2006 proof -

2007 have True and

2008 "\<And> c v s0 s. \<lbrakk> constVal e = Some c; G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s\<rbrakk>

2009 \<Longrightarrow> v = c \<and> normal s"

2010 and True

2011 proof (induct rule: var.induct expr.induct stmt.induct)

2012 case NewC hence False by simp thus ?case ..

2013 next

2014 case NewA hence False by simp thus ?case ..

2015 next

2016 case Cast hence False by simp thus ?case ..

2017 next

2018 case Inst hence False by simp thus ?case ..

2019 next

2020 case (Lit val c v s0 s)

2021 note \<open>constVal (Lit val) = Some c\<close>

2022 moreover

2023 from \<open>G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s\<close>

2024 obtain "v=val" and "normal s"

2025 by cases simp

2026 ultimately show "v=c \<and> normal s" by simp

2027 next

2028 case (UnOp unop e c v s0 s)

2029 note const = \<open>constVal (UnOp unop e) = Some c\<close>

2030 then obtain ce where ce: "constVal e = Some ce" by simp

2031 from \<open>G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s\<close>

2032 obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and

2033 v: "v = eval_unop unop ve"

2034 by cases simp

2035 from ce ve

2036 obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"

2037 by (rule UnOp.hyps [elim_format]) iprover

2038 from eq_ve_ce const ce v

2039 have "v=c"

2040 by simp

2041 from this nrm_s

2042 show ?case ..

2043 next

2044 case (BinOp binop e1 e2 c v s0 s)

2045 note const = \<open>constVal (BinOp binop e1 e2) = Some c\<close>

2046 then obtain c1 c2 where c1: "constVal e1 = Some c1" and

2047 c2: "constVal e2 = Some c2" and

2048 c: "c = eval_binop binop c1 c2"

2049 by simp

2050 from \<open>G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s\<close>

2051 obtain v1 s1 v2

2052 where v1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and

2053 v2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2

2054 else In1r Skip)\<succ>\<rightarrow> (In1 v2, s)" and

2055 v: "v = eval_binop binop v1 v2"

2056 by cases simp

2057 from c1 v1

2058 obtain eq_v1_c1: "v1 = c1" and

2059 nrm_s1: "normal s1"

2060 by (rule BinOp.hyps [elim_format]) iprover

2061 show ?case

2062 proof (cases "need_second_arg binop v1")

2063 case True

2064 with v2 nrm_s1 obtain s1'

2065 where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v2\<rightarrow> s"

2066 by (cases s1) simp

2067 with c2 obtain "v2 = c2" "normal s"

2068 by (rule BinOp.hyps [elim_format]) iprover

2069 with c c1 c2 eq_v1_c1 v

2070 show ?thesis by simp

2071 next

2072 case False

2073 with nrm_s1 v2

2074 have "s=s1"

2075 by (cases s1) (auto elim!: eval_elim_cases)

2076 moreover

2077 from False c v eq_v1_c1

2078 have "v = c"

2079 by (simp add: eval_binop_arg2_indep)

2080 ultimately

2081 show ?thesis

2082 using nrm_s1 by simp

2083 qed (* hallo ehco *)

2084 next

2085 case Super hence False by simp thus ?case ..

2086 next

2087 case Acc hence False by simp thus ?case ..

2088 next

2089 case Ass hence False by simp thus ?case ..

2090 next

2091 case (Cond b e1 e2 c v s0 s)

2092 note c = \<open>constVal (b ? e1 : e2) = Some c\<close>

2093 then obtain cb c1 c2 where

2094 cb: "constVal b = Some cb" and

2095 c1: "constVal e1 = Some c1" and

2096 c2: "constVal e2 = Some c2"

2097 by (auto split: bool.splits)

2098 from \<open>G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s\<close>

2099 obtain vb s1

2100 where vb: "G\<turnstile>Norm s0 \<midarrow>b-\<succ>vb\<rightarrow> s1" and

2101 eval_v: "G\<turnstile>s1 \<midarrow>(if the_Bool vb then e1 else e2)-\<succ>v\<rightarrow> s"

2102 by cases simp

2103 from cb vb

2104 obtain eq_vb_cb: "vb = cb" and nrm_s1: "normal s1"

2105 by (rule Cond.hyps [elim_format]) iprover

2106 show ?case

2107 proof (cases "the_Bool vb")

2108 case True

2109 with c cb c1 eq_vb_cb

2110 have "c = c1"

2111 by simp

2112 moreover

2113 from True eval_v nrm_s1 obtain s1'

2114 where "G\<turnstile>Norm s1' \<midarrow>e1-\<succ>v\<rightarrow> s"

2115 by (cases s1) simp

2116 with c1 obtain "c1 = v" "normal s"

2117 by (rule Cond.hyps [elim_format]) iprover

2118 ultimately show ?thesis by simp

2119 next

2120 case False

2121 with c cb c2 eq_vb_cb

2122 have "c = c2"

2123 by simp

2124 moreover

2125 from False eval_v nrm_s1 obtain s1'

2126 where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v\<rightarrow> s"

2127 by (cases s1) simp

2128 with c2 obtain "c2 = v" "normal s"

2129 by (rule Cond.hyps [elim_format]) iprover

2130 ultimately show ?thesis by simp

2131 qed

2132 next

2133 case Call hence False by simp thus ?case ..

2134 qed simp_all

2135 with const eval

2136 show ?thesis

2137 by iprover

2138 qed

2140 lemmas constVal_eval_elim = constVal_eval [THEN conjE]

2142 lemma eval_unop_type:

2143 "typeof dt (eval_unop unop v) = Some (PrimT (unop_type unop))"

2144 by (cases unop) simp_all

2146 lemma eval_binop_type:

2147 "typeof dt (eval_binop binop v1 v2) = Some (PrimT (binop_type binop))"

2148 by (cases binop) simp_all

2150 lemma constVal_Boolean:

2151 assumes const: "constVal e = Some c" and

2152 wt: "Env\<turnstile>e\<Colon>-PrimT Boolean"

2153 shows "typeof empty_dt c = Some (PrimT Boolean)"

2154 proof -

2155 have True and

2156 "\<And> c. \<lbrakk>constVal e = Some c;Env\<turnstile>e\<Colon>-PrimT Boolean\<rbrakk>

2157 \<Longrightarrow> typeof empty_dt c = Some (PrimT Boolean)"

2158 and True

2159 proof (induct rule: var.induct expr.induct stmt.induct)

2160 case NewC hence False by simp thus ?case ..

2161 next

2162 case NewA hence False by simp thus ?case ..

2163 next

2164 case Cast hence False by simp thus ?case ..

2165 next

2166 case Inst hence False by simp thus ?case ..

2167 next

2168 case (Lit v c)

2169 from \<open>constVal (Lit v) = Some c\<close>

2170 have "c=v" by simp

2171 moreover

2172 from \<open>Env\<turnstile>Lit v\<Colon>-PrimT Boolean\<close>

2173 have "typeof empty_dt v = Some (PrimT Boolean)"

2174 by cases simp

2175 ultimately show ?case by simp

2176 next

2177 case (UnOp unop e c)

2178 from \<open>Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean\<close>

2179 have "Boolean = unop_type unop" by cases simp

2180 moreover

2181 from \<open>constVal (UnOp unop e) = Some c\<close>

2182 obtain ce where "c = eval_unop unop ce" by auto

2183 ultimately show ?case by (simp add: eval_unop_type)

2184 next

2185 case (BinOp binop e1 e2 c)

2186 from \<open>Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean\<close>

2187 have "Boolean = binop_type binop" by cases simp

2188 moreover

2189 from \<open>constVal (BinOp binop e1 e2) = Some c\<close>

2190 obtain c1 c2 where "c = eval_binop binop c1 c2" by auto

2191 ultimately show ?case by (simp add: eval_binop_type)

2192 next

2193 case Super hence False by simp thus ?case ..

2194 next

2195 case Acc hence False by simp thus ?case ..

2196 next

2197 case Ass hence False by simp thus ?case ..

2198 next

2199 case (Cond b e1 e2 c)

2200 note c = \<open>constVal (b ? e1 : e2) = Some c\<close>

2201 then obtain cb c1 c2 where

2202 cb: "constVal b = Some cb" and

2203 c1: "constVal e1 = Some c1" and

2204 c2: "constVal e2 = Some c2"

2205 by (auto split: bool.splits)

2206 note wt = \<open>Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean\<close>

2207 then

2208 obtain T1 T2

2209 where "Env\<turnstile>b\<Colon>-PrimT Boolean" and

2210 wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and

2211 wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"

2212 by cases (auto dest: widen_Boolean2)

2213 show ?case

2214 proof (cases "the_Bool cb")

2215 case True

2216 from c1 wt_e1

2217 have "typeof empty_dt c1 = Some (PrimT Boolean)"

2218 by (rule Cond.hyps)

2219 with True c cb c1 show ?thesis by simp

2220 next

2221 case False

2222 from c2 wt_e2

2223 have "typeof empty_dt c2 = Some (PrimT Boolean)"

2224 by (rule Cond.hyps)

2225 with False c cb c2 show ?thesis by simp

2226 qed

2227 next

2228 case Call hence False by simp thus ?case ..

2229 qed simp_all

2230 with const wt

2231 show ?thesis

2232 by iprover

2233 qed

2235 lemma assigns_if_good_approx:

2236 assumes

2237 eval: "prg Env\<turnstile> s0 \<midarrow>e-\<succ>b\<rightarrow> s1" and

2238 normal: "normal s1" and

2239 bool: "Env\<turnstile> e\<Colon>-PrimT Boolean"

2240 shows "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"

2241 proof -

2242 \<comment> \<open>To properly perform induction on the evaluation relation we have to

2243 generalize the lemma to terms not only expressions.\<close>

2244 { fix t val

2245 assume eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"

2246 assume bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"

2247 assume expr: "\<exists> expr. t=In1l expr"

2248 have "assigns_if (the_Bool (the_In1 val)) (the_In1l t)

2249 \<subseteq> dom (locals (store s1))"

2250 using eval' normal bool' expr

2251 proof (induct)

2252 case Abrupt thus ?case by simp

2253 next

2254 case (NewC s0 C s1 a s2)

2255 from \<open>Env\<turnstile>NewC C\<Colon>-PrimT Boolean\<close>

2256 have False

2257 by cases simp

2258 thus ?case ..

2259 next

2260 case (NewA s0 T s1 e i s2 a s3)

2261 from \<open>Env\<turnstile>New T[e]\<Colon>-PrimT Boolean\<close>

2262 have False

2263 by cases simp

2264 thus ?case ..

2265 next

2266 case (Cast s0 e b s1 s2 T)

2267 note s2 = \<open>s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1\<close>

2268 have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"

2269 proof -

2270 from s2 and \<open>normal s2\<close>

2271 have "normal s1"

2272 by (cases s1) simp

2273 moreover

2274 from \<open>Env\<turnstile>Cast T e\<Colon>-PrimT Boolean\<close>

2275 have "Env\<turnstile>e\<Colon>- PrimT Boolean"

2276 by cases (auto dest: cast_Boolean2)

2277 ultimately show ?thesis

2278 by (rule Cast.hyps [elim_format]) auto

2279 qed

2280 also from s2

2281 have "\<dots> \<subseteq> dom (locals (store s2))"

2282 by simp

2283 finally show ?case by simp

2284 next

2285 case (Inst s0 e v s1 b T)

2286 from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close> and \<open>normal s1\<close>

2287 have "assignsE e \<subseteq> dom (locals (store s1))"

2288 by (rule assignsE_good_approx)

2289 thus ?case

2290 by simp

2291 next

2292 case (Lit s v)

2293 from \<open>Env\<turnstile>Lit v\<Colon>-PrimT Boolean\<close>

2294 have "typeof empty_dt v = Some (PrimT Boolean)"

2295 by cases simp

2296 then obtain b where "v=Bool b"

2297 by (cases v) (simp_all add: empty_dt_def)

2298 thus ?case

2299 by simp

2300 next

2301 case (UnOp s0 e v s1 unop)

2302 note bool = \<open>Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean\<close>

2303 hence bool_e: "Env\<turnstile>e\<Colon>-PrimT Boolean"

2304 by cases (cases unop,simp_all)

2305 show ?case

2306 proof (cases "constVal (UnOp unop e)")

2307 case None

2308 note \<open>normal s1\<close>

2309 moreover note bool_e

2310 ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"

2311 by (rule UnOp.hyps [elim_format]) auto

2312 moreover

2313 from bool have "unop = UNot"

2314 by cases (cases unop, simp_all)

2315 moreover note None

2316 ultimately

2317 have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e)

2318 \<subseteq> dom (locals (store s1))"

2319 by simp

2320 thus ?thesis by simp

2321 next

2322 case (Some c)

2323 moreover

2324 from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close>

2325 have "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1"

2326 by (rule eval.UnOp)

2327 with Some

2328 have "eval_unop unop v=c"

2329 by (rule constVal_eval_elim) simp

2330 moreover

2331 from Some bool

2332 obtain b where "c=Bool b"

2333 by (rule constVal_Boolean [elim_format])

2334 (cases c, simp_all add: empty_dt_def)

2335 ultimately

2336 have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) = {}"

2337 by simp

2338 thus ?thesis by simp

2339 qed

2340 next

2341 case (BinOp s0 e1 v1 s1 binop e2 v2 s2)

2342 note bool = \<open>Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean\<close>

2343 show ?case

2344 proof (cases "constVal (BinOp binop e1 e2)")

2345 case (Some c)

2346 moreover

2347 from BinOp.hyps

2348 have

2349 "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"

2350 by - (rule eval.BinOp)

2351 with Some

2352 have "eval_binop binop v1 v2=c"

2353 by (rule constVal_eval_elim) simp

2354 moreover

2355 from Some bool

2356 obtain b where "c = Bool b"

2357 by (rule constVal_Boolean [elim_format])

2358 (cases c, simp_all add: empty_dt_def)

2359 ultimately

2360 have "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2)

2361 = {}"

2362 by simp

2363 thus ?thesis by simp

2364 next

2365 case None

2366 show ?thesis

2367 proof (cases "binop=CondAnd \<or> binop=CondOr")

2368 case True

2369 from bool obtain bool_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and

2370 bool_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"

2371 using True by cases auto

2372 have "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s1))"

2373 proof -

2374 from BinOp have "normal s1"

2375 by - (erule eval_no_abrupt_lemma [rule_format])

2376 from this bool_e1

2377 show ?thesis

2378 by (rule BinOp.hyps [elim_format]) auto

2379 qed

2380 also

2381 from BinOp.hyps

2382 have "\<dots> \<subseteq> dom (locals (store s2))"

2383 by - (erule dom_locals_eval_mono_elim,simp)

2384 finally

2385 have e1_s2: "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s2))".

2386 from True show ?thesis

2387 proof

2388 assume condAnd: "binop = CondAnd"

2389 show ?thesis

2390 proof (cases "the_Bool (eval_binop binop v1 v2)")

2391 case True

2392 with condAnd

2393 have need_second: "need_second_arg binop v1"

2394 by (simp add: need_second_arg_def)

2395 from \<open>normal s2\<close>

2396 have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2397 by (rule BinOp.hyps [elim_format])

2398 (simp add: need_second bool_e2)+

2399 with e1_s2

2400 have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2

2401 \<subseteq> dom (locals (store s2))"

2402 by (rule Un_least)

2403 with True condAnd None show ?thesis

2404 by simp

2405 next

2406 case False

2407 note binop_False = this

2408 show ?thesis

2409 proof (cases "need_second_arg binop v1")

2410 case True

2411 with binop_False condAnd

2412 obtain "the_Bool v1=True" and "the_Bool v2 = False"

2413 by (simp add: need_second_arg_def)

2414 moreover

2415 from \<open>normal s2\<close>

2416 have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2417 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+

2418 with e1_s2

2419 have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2

2420 \<subseteq> dom (locals (store s2))"

2421 by (rule Un_least)

2422 moreover note binop_False condAnd None

2423 ultimately show ?thesis

2424 by auto

2425 next

2426 case False

2427 with binop_False condAnd

2428 have "the_Bool v1=False"

2429 by (simp add: need_second_arg_def)

2430 with e1_s2

2431 show ?thesis

2432 using binop_False condAnd None by auto

2433 qed

2434 qed

2435 next

2436 assume condOr: "binop = CondOr"

2437 show ?thesis

2438 proof (cases "the_Bool (eval_binop binop v1 v2)")

2439 case False

2440 with condOr

2441 have need_second: "need_second_arg binop v1"

2442 by (simp add: need_second_arg_def)

2443 from \<open>normal s2\<close>

2444 have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2445 by (rule BinOp.hyps [elim_format])

2446 (simp add: need_second bool_e2)+

2447 with e1_s2

2448 have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2

2449 \<subseteq> dom (locals (store s2))"

2450 by (rule Un_least)

2451 with False condOr None show ?thesis

2452 by simp

2453 next

2454 case True

2455 note binop_True = this

2456 show ?thesis

2457 proof (cases "need_second_arg binop v1")

2458 case True

2459 with binop_True condOr

2460 obtain "the_Bool v1=False" and "the_Bool v2 = True"

2461 by (simp add: need_second_arg_def)

2462 moreover

2463 from \<open>normal s2\<close>

2464 have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2465 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+

2466 with e1_s2

2467 have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2

2468 \<subseteq> dom (locals (store s2))"

2469 by (rule Un_least)

2470 moreover note binop_True condOr None

2471 ultimately show ?thesis

2472 by auto

2473 next

2474 case False

2475 with binop_True condOr

2476 have "the_Bool v1=True"

2477 by (simp add: need_second_arg_def)

2478 with e1_s2

2479 show ?thesis

2480 using binop_True condOr None by auto

2481 qed

2482 qed

2483 qed

2484 next

2485 case False

2486 note \<open>\<not> (binop = CondAnd \<or> binop = CondOr)\<close>

2487 from BinOp.hyps

2488 have

2489 "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"

2490 by - (rule eval.BinOp)

2491 moreover note \<open>normal s2\<close>

2492 ultimately

2493 have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"

2494 by (rule assignsE_good_approx)

2495 with False None

2496 show ?thesis

2497 by simp

2498 qed

2499 qed

2500 next

2501 case Super

2502 note \<open>Env\<turnstile>Super\<Colon>-PrimT Boolean\<close>

2503 hence False

2504 by cases simp

2505 thus ?case ..

2506 next

2507 case (Acc s0 va v f s1)

2508 from \<open>prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1\<close> and \<open>normal s1\<close>

2509 have "assignsV va \<subseteq> dom (locals (store s1))"

2510 by (rule assignsV_good_approx)

2511 thus ?case by simp

2512 next

2513 case (Ass s0 va w f s1 e v s2)

2514 hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"

2515 by - (rule eval.Ass)

2516 moreover note \<open>normal (assign f v s2)\<close>

2517 ultimately

2518 have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"

2519 by (rule assignsE_good_approx)

2520 thus ?case by simp

2521 next

2522 case (Cond s0 e0 b s1 e1 e2 v s2)

2523 from \<open>Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean\<close>

2524 obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and

2525 wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"

2526 by cases (auto dest: widen_Boolean2)

2527 note eval_e0 = \<open>prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1\<close>

2528 have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"

2529 proof -

2530 note eval_e0

2531 moreover

2532 from Cond.hyps and \<open>normal s2\<close> have "normal s1"

2533 by - (erule eval_no_abrupt_lemma [rule_format],simp)

2534 ultimately

2535 have "assignsE e0 \<subseteq> dom (locals (store s1))"

2536 by (rule assignsE_good_approx)

2537 also

2538 from Cond

2539 have "\<dots> \<subseteq> dom (locals (store s2))"

2540 by - (erule dom_locals_eval_mono [elim_format],simp)

2541 finally show ?thesis .

2542 qed

2543 show ?case

2544 proof (cases "constVal e0")

2545 case None

2546 have "assigns_if (the_Bool v) e1 \<inter> assigns_if (the_Bool v) e2

2547 \<subseteq> dom (locals (store s2))"

2548 proof (cases "the_Bool b")

2549 case True

2550 from \<open>normal s2\<close>

2551 have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"

2552 by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)

2553 thus ?thesis

2554 by blast

2555 next

2556 case False

2557 from \<open>normal s2\<close>

2558 have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"

2559 by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)

2560 thus ?thesis

2561 by blast

2562 qed

2563 with e0_s2

2564 have "assignsE e0 \<union>

2565 (assigns_if (the_Bool v) e1 \<inter> assigns_if (the_Bool v) e2)

2566 \<subseteq> dom (locals (store s2))"

2567 by (rule Un_least)

2568 with None show ?thesis

2569 by simp

2570 next

2571 case (Some c)

2572 from this eval_e0 have eq_b_c: "b=c"

2573 by (rule constVal_eval_elim)

2574 show ?thesis

2575 proof (cases "the_Bool c")

2576 case True

2577 from \<open>normal s2\<close>

2578 have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"

2579 by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1)

2580 with e0_s2

2581 have "assignsE e0 \<union> assigns_if (the_Bool v) e1 \<subseteq> \<dots>"

2582 by (rule Un_least)

2583 with Some True show ?thesis

2584 by simp

2585 next

2586 case False

2587 from \<open>normal s2\<close>

2588 have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"

2589 by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2)

2590 with e0_s2

2591 have "assignsE e0 \<union> assigns_if (the_Bool v) e2 \<subseteq> \<dots>"

2592 by (rule Un_least)

2593 with Some False show ?thesis

2594 by simp

2595 qed

2596 qed

2597 next

2598 case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)

2599 hence

2600 "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v\<rightarrow>

2601 (set_lvars (locals (store s2)) s4)"

2602 by - (rule eval.Call)

2603 hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args))

2604 \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"

2605 using \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>

2606 by (rule assignsE_good_approx)

2607 thus ?case by simp

2608 next

2609 case Methd show ?case by simp

2610 next

2611 case Body show ?case by simp

2612 qed simp+ \<comment> \<open>all the statements and variables\<close>

2613 }

2614 note generalized = this

2615 from eval bool show ?thesis

2616 by (rule generalized [elim_format]) simp+

2617 qed

2619 lemma assigns_if_good_approx':

2620 assumes eval: "G\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1"

2621 and normal: "normal s1"

2622 and bool: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>- (PrimT Boolean)"

2623 shows "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"

2624 proof -

2625 from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp

2626 from this normal bool show ?thesis

2627 by (rule assigns_if_good_approx)

2628 qed

2631 lemma subset_Intl: "A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"

2632 by blast

2634 lemma subset_Intr: "B \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"

2635 by blast

2637 lemma da_good_approx:

2638 assumes eval: "prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and

2639 wt: "Env\<turnstile>t\<Colon>T" (is "?Wt Env t T") and

2640 da: "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" (is "?Da Env s0 t A") and

2641 wf: "wf_prog (prg Env)"

2642 shows "(normal s1 \<longrightarrow> (nrm A \<subseteq> dom (locals (store s1)))) \<and>

2643 (\<forall> l. abrupt s1 = Some (Jump (Break l)) \<and> normal s0

2644 \<longrightarrow> (brk A l \<subseteq> dom (locals (store s1)))) \<and>

2645 (abrupt s1 = Some (Jump Ret) \<and> normal s0

2646 \<longrightarrow> Result \<in> dom (locals (store s1)))"

2647 (is "?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1")

2648 proof -

2649 note inj_term_simps [simp]

2650 obtain G where G: "prg Env = G" by (cases Env) simp

2651 with eval have eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by simp

2652 from G wf have wf: "wf_prog G" by simp

2653 let ?HypObj = "\<lambda> t s0 s1.

2654 \<forall> Env T A. ?Wt Env t T \<longrightarrow> ?Da Env s0 t A \<longrightarrow> prg Env = G

2655 \<longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1"

2656 \<comment> \<open>Goal in object logic variant\<close>

2657 let ?Hyp = "\<lambda>t s0 s1. (\<And> Env T A. \<lbrakk>?Wt Env t T; ?Da Env s0 t A; prg Env = G\<rbrakk>

2658 \<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1)"

2659 from eval and wt da G

2660 show ?thesis

2661 proof (induct arbitrary: Env T A)

2662 case (Abrupt xc s t Env T A)

2663 have da: "Env\<turnstile> dom (locals s) \<guillemotright>t\<guillemotright> A" using Abrupt.prems by simp

2664 have "?NormalAssigned (Some xc,s) A"

2665 by simp

2666 moreover

2667 have "?BreakAssigned (Some xc,s) (Some xc,s) A"

2668 by simp

2669 moreover have "?ResAssigned (Some xc,s) (Some xc,s)"

2670 by simp

2671 ultimately show ?case by (intro conjI)

2672 next

2673 case (Skip s Env T A)

2674 have da: "Env\<turnstile> dom (locals (store (Norm s))) \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"

2675 using Skip.prems by simp

2676 hence "nrm A = dom (locals (store (Norm s)))"

2677 by (rule da_elim_cases) simp

2678 hence "?NormalAssigned (Norm s) A"

2679 by auto

2680 moreover

2681 have "?BreakAssigned (Norm s) (Norm s) A"

2682 by simp

2683 moreover have "?ResAssigned (Norm s) (Norm s)"

2684 by simp

2685 ultimately show ?case by (intro conjI)

2686 next

2687 case (Expr s0 e v s1 Env T A)

2688 from Expr.prems

2689 show "?NormalAssigned s1 A \<and> ?BreakAssigned (Norm s0) s1 A

2690 \<and> ?ResAssigned (Norm s0) s1"

2691 by (elim wt_elim_cases da_elim_cases)

2692 (rule Expr.hyps, auto)

2693 next

2694 case (Lab s0 c s1 j Env T A)

2695 note G = \<open>prg Env = G\<close>

2696 from Lab.prems

2697 obtain C l where

2698 da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and

2699 A: "nrm A = nrm C \<inter> (brk C) l" "brk A = rmlab l (brk C)" and

2700 j: "j = Break l"

2701 by - (erule da_elim_cases, simp)

2702 from Lab.prems

2703 have wt_c: "Env\<turnstile>c\<Colon>\<surd>"

2704 by - (erule wt_elim_cases, simp)

2705 from wt_c da_c G and Lab.hyps

2706 have norm_c: "?NormalAssigned s1 C" and

2707 brk_c: "?BreakAssigned (Norm s0) s1 C" and

2708 res_c: "?ResAssigned (Norm s0) s1"

2709 by simp_all

2710 have "?NormalAssigned (abupd (absorb j) s1) A"

2711 proof

2712 assume normal: "normal (abupd (absorb j) s1)"

2713 show "nrm A \<subseteq> dom (locals (store (abupd (absorb j) s1)))"

2714 proof (cases "abrupt s1")

2715 case None

2716 with norm_c A

2717 show ?thesis

2718 by auto

2719 next

2720 case Some

2721 with normal j

2722 have "abrupt s1 = Some (Jump (Break l))"

2723 by (auto dest: absorb_Some_NoneD)

2724 with brk_c A

2725 show ?thesis

2726 by auto

2727 qed

2728 qed

2729 moreover

2730 have "?BreakAssigned (Norm s0) (abupd (absorb j) s1) A"

2731 proof -

2732 {

2733 fix l'

2734 assume break: "abrupt (abupd (absorb j) s1) = Some (Jump (Break l'))"

2735 with j

2736 have "l\<noteq>l'"

2737 by (cases s1) (auto dest!: absorb_Some_JumpD)

2738 hence "(rmlab l (brk C)) l'= (brk C) l'"

2739 by (simp)

2740 with break brk_c A

2741 have

2742 "(brk A l' \<subseteq> dom (locals (store (abupd (absorb j) s1))))"

2743 by (cases s1) auto

2744 }

2745 then show ?thesis

2746 by simp

2747 qed

2748 moreover

2749 from res_c have "?ResAssigned (Norm s0) (abupd (absorb j) s1)"

2750 by (cases s1) (simp add: absorb_def)

2751 ultimately show ?case by (intro conjI)

2752 next

2753 case (Comp s0 c1 s1 c2 s2 Env T A)

2754 note G = \<open>prg Env = G\<close>

2755 from Comp.prems

2756 obtain C1 C2

2757 where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

2758 da_c2: "Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

2759 A: "nrm A = nrm C2" "brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)"

2760 by (elim da_elim_cases) simp

2761 from Comp.prems

2762 obtain wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and

2763 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

2764 by (elim wt_elim_cases) simp

2765 note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1\<close>

2766 with wt_c1 da_c1 G

2767 obtain nrm_c1: "?NormalAssigned s1 C1" and

2768 brk_c1: "?BreakAssigned (Norm s0) s1 C1" and

2769 res_c1: "?ResAssigned (Norm s0) s1"

2770 by simp

2771 show ?case

2772 proof (cases "normal s1")

2773 case True

2774 with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by iprover

2775 with da_c2 obtain C2'

2776 where da_c2': "Env\<turnstile> dom (locals (snd s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

2777 nrm_c2: "nrm C2 \<subseteq> nrm C2'" and

2778 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"

2779 by (rule da_weakenE) iprover

2780 note \<open>PROP ?Hyp (In1r c2) s1 s2\<close>

2781 with wt_c2 da_c2' G

2782 obtain nrm_c2': "?NormalAssigned s2 C2'" and

2783 brk_c2': "?BreakAssigned s1 s2 C2'" and

2784 res_c2 : "?ResAssigned s1 s2"

2785 by simp

2786 from nrm_c2' nrm_c2 A

2787 have "?NormalAssigned s2 A"

2788 by blast

2789 moreover from brk_c2' brk_c2 A

2790 have "?BreakAssigned s1 s2 A"

2791 by fastforce

2792 with True

2793 have "?BreakAssigned (Norm s0) s2 A" by simp

2794 moreover from res_c2 True

2795 have "?ResAssigned (Norm s0) s2"

2796 by simp

2797 ultimately show ?thesis by (intro conjI)

2798 next

2799 case False

2800 with \<open>G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<close>

2801 have eq_s1_s2: "s2=s1" by auto

2802 with False have "?NormalAssigned s2 A" by blast

2803 moreover

2804 have "?BreakAssigned (Norm s0) s2 A"

2805 proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")

2806 case True

2807 then obtain l where l: "abrupt s1 = Some (Jump (Break l))" ..

2808 with brk_c1

2809 have "brk C1 l \<subseteq> dom (locals (store s1))"

2810 by simp

2811 with A eq_s1_s2

2812 have "brk A l \<subseteq> dom (locals (store s2))"

2813 by auto

2814 with l eq_s1_s2

2815 show ?thesis by simp

2816 next

2817 case False

2818 with eq_s1_s2 show ?thesis by simp

2819 qed

2820 moreover from False res_c1 eq_s1_s2

2821 have "?ResAssigned (Norm s0) s2"

2822 by simp

2823 ultimately show ?thesis by (intro conjI)

2824 qed

2825 next

2826 case (If s0 e b s1 c1 c2 s2 Env T A)

2827 note G = \<open>prg Env = G\<close>

2828 with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp

2829 from If.prems

2830 obtain E C1 C2 where

2831 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

2832 da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2833 \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

2834 da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2835 \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

2836 A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"

2837 by (elim da_elim_cases)

2838 from If.prems

2839 obtain

2840 wt_e: "Env\<turnstile>e\<Colon>- PrimT Boolean" and

2841 wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and

2842 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

2843 by (elim wt_elim_cases)

2844 from If.hyps have

2845 s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

2846 by (elim dom_locals_eval_mono_elim)

2847 show ?case

2848 proof (cases "normal s1")

2849 case True

2850 note normal_s1 = this

2851 show ?thesis

2852 proof (cases "the_Bool b")

2853 case True

2854 from eval_e normal_s1 wt_e

2855 have "assigns_if True e \<subseteq> dom (locals (store s1))"

2856 by (rule assigns_if_good_approx [elim_format]) (simp add: True)

2857 with s0_s1

2858 have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"

2859 by (rule Un_least)

2860 with da_c1 obtain C1'

2861 where da_c1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and

2862 nrm_c1: "nrm C1 \<subseteq> nrm C1'" and

2863 brk_c1: "\<forall> l. brk C1 l \<subseteq> brk C1' l"

2864 by (rule da_weakenE) iprover

2865 from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp

2866 with wt_c1 da_c1'

2867 obtain nrm_c1': "?NormalAssigned s2 C1'" and

2868 brk_c1': "?BreakAssigned s1 s2 C1'" and

2869 res_c1: "?ResAssigned s1 s2"

2870 using G by simp

2871 from nrm_c1' nrm_c1 A

2872 have "?NormalAssigned s2 A"

2873 by blast

2874 moreover from brk_c1' brk_c1 A

2875 have "?BreakAssigned s1 s2 A"

2876 by fastforce

2877 with normal_s1

2878 have "?BreakAssigned (Norm s0) s2 A" by simp

2879 moreover from res_c1 normal_s1 have "?ResAssigned (Norm s0) s2"

2880 by simp

2881 ultimately show ?thesis by (intro conjI)

2882 next

2883 case False

2884 from eval_e normal_s1 wt_e

2885 have "assigns_if False e \<subseteq> dom (locals (store s1))"

2886 by (rule assigns_if_good_approx [elim_format]) (simp add: False)

2887 with s0_s1

2888 have "dom (locals (store ((Norm s0)::state)))\<union> assigns_if False e \<subseteq> \<dots>"

2889 by (rule Un_least)

2890 with da_c2 obtain C2'

2891 where da_c2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

2892 nrm_c2: "nrm C2 \<subseteq> nrm C2'" and

2893 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"

2894 by (rule da_weakenE) iprover

2895 from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp

2896 with wt_c2 da_c2'

2897 obtain nrm_c2': "?NormalAssigned s2 C2'" and

2898 brk_c2': "?BreakAssigned s1 s2 C2'" and

2899 res_c2: "?ResAssigned s1 s2"

2900 using G by simp

2901 from nrm_c2' nrm_c2 A

2902 have "?NormalAssigned s2 A"

2903 by blast

2904 moreover from brk_c2' brk_c2 A

2905 have "?BreakAssigned s1 s2 A"

2906 by fastforce

2907 with normal_s1

2908 have "?BreakAssigned (Norm s0) s2 A" by simp

2909 moreover from res_c2 normal_s1 have "?ResAssigned (Norm s0) s2"

2910 by simp

2911 ultimately show ?thesis by (intro conjI)

2912 qed

2913 next

2914 case False

2915 then obtain abr where abr: "abrupt s1 = Some abr"

2916 by (cases s1) auto

2917 moreover

2918 from eval_e _ wt_e have "\<And> j. abrupt s1 \<noteq> Some (Jump j)"

2919 by (rule eval_expression_no_jump) (simp_all add: G wf)

2920 moreover

2921 have "s2 = s1"

2922 proof -

2923 from abr and \<open>G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<close>

2924 show ?thesis

2925 by (cases s1) simp

2926 qed

2927 ultimately show ?thesis by simp

2928 qed

2929 next

2930 case (Loop s0 e b s1 c s2 l s3 Env T A)

2931 note G = \<open>prg Env = G\<close>

2932 with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"

2933 by (simp (no_asm_simp))

2934 from Loop.prems

2935 obtain E C where

2936 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

2937 da_c: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2938 \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and

2939 A: "nrm A = nrm C \<inter>

2940 (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)"

2941 "brk A = brk C"

2942 by (elim da_elim_cases)

2943 from Loop.prems

2944 obtain

2945 wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and

2946 wt_c: "Env\<turnstile>c\<Colon>\<surd>"

2947 by (elim wt_elim_cases)

2948 from wt_e da_e G

2949 obtain res_s1: "?ResAssigned (Norm s0) s1"

2950 by (elim Loop.hyps [elim_format]) simp+

2951 from Loop.hyps have

2952 s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

2953 by (elim dom_locals_eval_mono_elim)

2954 show ?case

2955 proof (cases "normal s1")

2956 case True

2957 note normal_s1 = this

2958 show ?thesis

2959 proof (cases "the_Bool b")

2960 case True

2961 with Loop.hyps obtain

2962 eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and

2963 eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"

2964 by simp

2965 from Loop.hyps True

2966 have "?HypObj (In1r c) s1 s2" by simp

2967 note hyp_c = this [rule_format]

2968 from Loop.hyps True

2969 have "?HypObj (In1r (l\<bullet> While(e) c)) (abupd (absorb (Cont l)) s2) s3"

2970 by simp

2971 note hyp_while = this [rule_format]

2972 from eval_e normal_s1 wt_e

2973 have "assigns_if True e \<subseteq> dom (locals (store s1))"

2974 by (rule assigns_if_good_approx [elim_format]) (simp add: True)

2975 with s0_s1

2976 have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"

2977 by (rule Un_least)

2978 with da_c obtain C'

2979 where da_c': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and

2980 nrm_C_C': "nrm C \<subseteq> nrm C'" and

2981 brk_C_C': "\<forall> l. brk C l \<subseteq> brk C' l"

2982 by (rule da_weakenE) iprover

2983 from hyp_c wt_c da_c'

2984 obtain nrm_C': "?NormalAssigned s2 C'" and

2985 brk_C': "?BreakAssigned s1 s2 C'" and

2986 res_s2: "?ResAssigned s1 s2"

2987 using G by simp

2988 show ?thesis

2989 proof (cases "normal s2 \<or> abrupt s2 = Some (Jump (Cont l))")

2990 case True

2991 from Loop.prems obtain

2992 wt_while: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" and

2993 da_while: "Env\<turnstile> dom (locals (store ((Norm s0)::state)))

2994 \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"

2995 by simp

2996 have "dom (locals (store ((Norm s0)::state)))

2997 \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"

2998 proof -

2999 note s0_s1

3000 also from eval_c

3001 have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"

3002 by (rule dom_locals_eval_mono_elim)

3003 also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"

3004 by simp

3005 finally show ?thesis .

3006 qed

3007 with da_while obtain A'

3008 where

3009 da_while': "Env\<turnstile> dom (locals (store (abupd (absorb (Cont l)) s2)))

3010 \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"

3011 and nrm_A_A': "nrm A \<subseteq> nrm A'"

3012 and brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"

3013 by (rule da_weakenE) simp

3014 with wt_while hyp_while

3015 obtain nrm_A': "?NormalAssigned s3 A'" and

3016 brk_A': "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A'" and

3017 res_s3: "?ResAssigned (abupd (absorb (Cont l)) s2) s3"

3018 using G by simp

3019 from nrm_A_A' nrm_A'

3020 have "?NormalAssigned s3 A"

3021 by blast

3022 moreover

3023 have "?BreakAssigned (Norm s0) s3 A"

3024 proof -

3025 from brk_A_A' brk_A'

3026 have "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A"

3027 by fastforce

3028 moreover

3029 from True have "normal (abupd (absorb (Cont l)) s2)"

3030 by (cases s2) auto

3031 ultimately show ?thesis

3032 by simp

3033 qed

3034 moreover from res_s3 True have "?ResAssigned (Norm s0) s3"

3035 by auto

3036 ultimately show ?thesis by (intro conjI)

3037 next

3038 case False

3039 then obtain abr where

3040 "abrupt s2 = Some abr" and

3041 "abrupt (abupd (absorb (Cont l)) s2) = Some abr"

3042 by auto

3043 with eval_while

3044 have eq_s3_s2: "s3=s2"

3045 by auto

3046 with nrm_C_C' nrm_C' A

3047 have "?NormalAssigned s3 A"

3048 by auto

3049 moreover

3050 from eq_s3_s2 brk_C_C' brk_C' normal_s1 A

3051 have "?BreakAssigned (Norm s0) s3 A"

3052 by fastforce

3053 moreover

3054 from eq_s3_s2 res_s2 normal_s1 have "?ResAssigned (Norm s0) s3"

3055 by simp

3056 ultimately show ?thesis by (intro conjI)

3057 qed

3058 next

3059 case False

3060 with Loop.hyps have eq_s3_s1: "s3=s1"

3061 by simp

3062 from eq_s3_s1 res_s1

3063 have res_s3: "?ResAssigned (Norm s0) s3"

3064 by simp

3065 from eval_e True wt_e

3066 have "assigns_if False e \<subseteq> dom (locals (store s1))"

3067 by (rule assigns_if_good_approx [elim_format]) (simp add: False)

3068 with s0_s1

3069 have "dom (locals (store ((Norm s0)::state)))\<union>assigns_if False e \<subseteq> \<dots>"

3070 by (rule Un_least)

3071 hence "nrm C \<inter>

3072 (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)

3073 \<subseteq> dom (locals (store s1))"

3074 by (rule subset_Intr)

3075 with normal_s1 A eq_s3_s1

3076 have "?NormalAssigned s3 A"

3077 by simp

3078 moreover

3079 from normal_s1 eq_s3_s1

3080 have "?BreakAssigned (Norm s0) s3 A"

3081 by simp

3082 moreover note res_s3

3083 ultimately show ?thesis by (intro conjI)

3084 qed

3085 next

3086 case False

3087 then obtain abr where abr: "abrupt s1 = Some abr"

3088 by (cases s1) auto

3089 moreover

3090 from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"

3091 by (rule eval_expression_no_jump) (simp_all add: wf G)

3092 moreover

3093 have eq_s3_s1: "s3=s1"

3094 proof (cases "the_Bool b")

3095 case True

3096 with Loop.hyps obtain

3097 eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and

3098 eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"

3099 by simp

3100 from eval_c abr have "s2=s1" by auto

3101 moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"

3102 by (cases s1) (simp add: absorb_def)

3103 ultimately show ?thesis

3104 using eval_while abr

3105 by auto

3106 next

3107 case False

3108 with Loop.hyps show ?thesis by simp

3109 qed

3110 moreover

3111 from eq_s3_s1 res_s1

3112 have res_s3: "?ResAssigned (Norm s0) s3"

3113 by simp

3114 ultimately show ?thesis

3115 by simp

3116 qed

3117 next

3118 case (Jmp s j Env T A)

3119 have "?NormalAssigned (Some (Jump j),s) A" by simp

3120 moreover

3121 from Jmp.prems

3122 obtain ret: "j = Ret \<longrightarrow> Result \<in> dom (locals (store (Norm s)))" and

3123 brk: "brk A = (case j of

3124 Break l \<Rightarrow> \<lambda> k. if k=l

3125 then dom (locals (store ((Norm s)::state)))

3126 else UNIV

3127 | Cont l \<Rightarrow> \<lambda> k. UNIV

3128 | Ret \<Rightarrow> \<lambda> k. UNIV)"

3129 by (elim da_elim_cases) simp

3130 from brk have "?BreakAssigned (Norm s) (Some (Jump j),s) A"

3131 by simp

3132 moreover from ret have "?ResAssigned (Norm s) (Some (Jump j),s)"

3133 by simp

3134 ultimately show ?case by (intro conjI)

3135 next

3136 case (Throw s0 e a s1 Env T A)

3137 note G = \<open>prg Env = G\<close>

3138 from Throw.prems obtain E where

3139 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"

3140 by (elim da_elim_cases)

3141 from Throw.prems

3142 obtain eT where wt_e: "Env\<turnstile>e\<Colon>-eT"

3143 by (elim wt_elim_cases)

3144 have "?NormalAssigned (abupd (throw a) s1) A"

3145 by (cases s1) (simp add: throw_def)

3146 moreover

3147 have "?BreakAssigned (Norm s0) (abupd (throw a) s1) A"

3148 proof -

3149 from G Throw.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"

3150 by (simp (no_asm_simp))

3151 from eval_e _ wt_e

3152 have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"

3153 by (rule eval_expression_no_jump) (simp_all add: wf G)

3154 hence "\<And> l. abrupt (abupd (throw a) s1) \<noteq> Some (Jump (Break l))"

3155 by (cases s1) (simp add: throw_def abrupt_if_def)

3156 thus ?thesis

3157 by simp

3158 qed

3159 moreover

3160 from wt_e da_e G have "?ResAssigned (Norm s0) s1"

3161 by (elim Throw.hyps [elim_format]) simp+

3162 hence "?ResAssigned (Norm s0) (abupd (throw a) s1)"

3163 by (cases s1) (simp add: throw_def abrupt_if_def)

3164 ultimately show ?case by (intro conjI)

3165 next

3166 case (Try s0 c1 s1 s2 C vn c2 s3 Env T A)

3167 note G = \<open>prg Env = G\<close>

3168 from Try.prems obtain C1 C2 where

3169 da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

3170 da_c2:

3171 "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>

3172 \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

3173 A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"

3174 by (elim da_elim_cases) simp

3175 from Try.prems obtain

3176 wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and

3177 wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"

3178 by (elim wt_elim_cases)

3179 have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G

3180 by (simp (no_asm_simp))

3181 note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1\<close>

3182 with wt_c1 da_c1 G

3183 obtain nrm_C1: "?NormalAssigned s1 C1" and

3184 brk_C1: "?BreakAssigned (Norm s0) s1 C1" and

3185 res_s1: "?ResAssigned (Norm s0) s1"

3186 by simp

3187 show ?case

3188 proof (cases "normal s1")

3189 case True

3190 with nrm_C1 have "nrm C1 \<inter> nrm C2 \<subseteq> dom (locals (store s1))"

3191 by auto

3192 moreover

3193 have "s3=s1"

3194 proof -

3195 from sxalloc True have eq_s2_s1: "s2=s1"

3196 by (cases s1) (auto elim: sxalloc_elim_cases)

3197 with True have "\<not> G,s2\<turnstile>catch C"

3198 by (simp add: catch_def)

3199 with Try.hyps have "s3=s2"

3200 by simp

3201 with eq_s2_s1 show ?thesis by simp

3202 qed

3203 ultimately show ?thesis

3204 using True A res_s1 by simp

3205 next

3206 case False

3207 note not_normal_s1 = this

3208 show ?thesis

3209 proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")

3210 case True

3211 then obtain l where l: "abrupt s1 = Some (Jump (Break l))"

3212 by auto

3213 with brk_C1 have "(brk C1 \<Rightarrow>\<inter> brk C2) l \<subseteq> dom (locals (store s1))"

3214 by auto

3215 moreover have "s3=s1"

3216 proof -

3217 from sxalloc l have eq_s2_s1: "s2=s1"

3218 by (cases s1) (auto elim: sxalloc_elim_cases)

3219 with l have "\<not> G,s2\<turnstile>catch C"

3220 by (simp add: catch_def)

3221 with Try.hyps have "s3=s2"

3222 by simp

3223 with eq_s2_s1 show ?thesis by simp

3224 qed

3225 ultimately show ?thesis

3226 using l A res_s1 by simp

3227 next

3228 case False

3229 note abrupt_no_break = this

3230 show ?thesis

3231 proof (cases "G,s2\<turnstile>catch C")

3232 case True

3233 with Try.hyps have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3"

3234 by simp

3235 note hyp_c2 = this [rule_format]

3236 have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn})

3237 \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"

3238 proof -

3239 from \<open>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1\<close>

3240 have "dom (locals (store ((Norm s0)::state)))

3241 \<subseteq> dom (locals (store s1))"

3242 by (rule dom_locals_eval_mono_elim)

3243 also

3244 from sxalloc

3245 have "\<dots> \<subseteq> dom (locals (store s2))"

3246 by (rule dom_locals_sxalloc_mono)

3247 also

3248 have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"

3249 by (cases s2) (simp add: new_xcpt_var_def, blast)

3250 also

3251 have "{VName vn} \<subseteq> \<dots>"

3252 by (cases s2) simp

3253 ultimately show ?thesis

3254 by (rule Un_least)

3255 qed

3256 with da_c2

3257 obtain C2' where

3258 da_C2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>

3259 \<turnstile> dom (locals (store (new_xcpt_var vn s2))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"

3260 and nrm_C2': "nrm C2 \<subseteq> nrm C2'"

3261 and brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"

3262 by (rule da_weakenE) simp

3263 from wt_c2 da_C2' G and hyp_c2

3264 obtain nrmAss_C2: "?NormalAssigned s3 C2'" and

3265 brkAss_C2: "?BreakAssigned (new_xcpt_var vn s2) s3 C2'" and

3266 resAss_s3: "?ResAssigned (new_xcpt_var vn s2) s3"

3267 by simp

3268 from nrmAss_C2 nrm_C2' A

3269 have "?NormalAssigned s3 A"

3270 by auto

3271 moreover

3272 have "?BreakAssigned (Norm s0) s3 A"

3273 proof -

3274 from brkAss_C2 have "?BreakAssigned (Norm s0) s3 C2'"

3275 by (cases s2) (auto simp add: new_xcpt_var_def)

3276 with brk_C2' A show ?thesis

3277 by fastforce

3278 qed

3279 moreover

3280 from resAss_s3 have "?ResAssigned (Norm s0) s3"

3281 by (cases s2) ( simp add: new_xcpt_var_def)

3282 ultimately show ?thesis by (intro conjI)

3283 next

3284 case False

3285 with Try.hyps

3286 have eq_s3_s2: "s3=s2" by simp

3287 moreover from sxalloc not_normal_s1 abrupt_no_break

3288 obtain "\<not> normal s2"

3289 "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l))"

3290 by - (rule sxalloc_cases,auto)

3291 ultimately obtain

3292 "?NormalAssigned s3 A" and "?BreakAssigned (Norm s0) s3 A"

3293 by (cases s2) auto

3294 moreover have "?ResAssigned (Norm s0) s3"

3295 proof (cases "abrupt s1 = Some (Jump Ret)")

3296 case True

3297 with sxalloc have "s2=s1"

3298 by (elim sxalloc_cases) auto

3299 with res_s1 eq_s3_s2 show ?thesis by simp

3300 next

3301 case False

3302 with sxalloc

3303 have "abrupt s2 \<noteq> Some (Jump Ret)"

3304 by (rule sxalloc_no_jump)

3305 with eq_s3_s2 show ?thesis

3306 by simp

3307 qed

3308 ultimately show ?thesis by (intro conjI)

3309 qed

3310 qed

3311 qed

3312 next

3313 case (Fin s0 c1 x1 s1 c2 s2 s3 Env T A)

3314 note G = \<open>prg Env = G\<close>

3315 from Fin.prems obtain C1 C2 where

3316 da_C1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

3317 da_C2: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

3318 nrm_A: "nrm A = nrm C1 \<union> nrm C2" and

3319 brk_A: "brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)"

3320 by (elim da_elim_cases) simp

3321 from Fin.prems obtain

3322 wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and

3323 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

3324 by (elim wt_elim_cases)

3325 note \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)\<close>

3326 with wt_c1 da_C1 G

3327 obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and

3328 brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and

3329 resAss_s1: "?ResAssigned (Norm s0) (x1,s1)"

3330 by simp

3331 obtain nrmAss_C2: "?NormalAssigned s2 C2" and

3332 brkAss_C2: "?BreakAssigned (Norm s1) s2 C2" and

3333 resAss_s2: "?ResAssigned (Norm s1) s2"

3334 proof -

3335 from Fin.hyps

3336 have "dom (locals (store ((Norm s0)::state)))

3337 \<subseteq> dom (locals (store (x1,s1)))"

3338 by - (rule dom_locals_eval_mono_elim)

3339 with da_C2 obtain C2'

3340 where

3341 da_C2': "Env\<turnstile> dom (locals (store (x1,s1))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

3342 nrm_C2': "nrm C2 \<subseteq> nrm C2'" and

3343 brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"

3344 by (rule da_weakenE) simp

3345 note \<open>PROP ?Hyp (In1r c2) (Norm s1) s2\<close>

3346 with wt_c2 da_C2' G

3347 obtain nrmAss_C2': "?NormalAssigned s2 C2'" and

3348 brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and

3349 resAss_s2': "?ResAssigned (Norm s1) s2"

3350 by simp

3351 from nrmAss_C2' nrm_C2' have "?NormalAssigned s2 C2"

3352 by blast

3353 moreover

3354 from brkAss_C2' brk_C2' have "?BreakAssigned (Norm s1) s2 C2"

3355 by fastforce

3356 ultimately

3357 show ?thesis

3358 using that resAss_s2' by simp

3359 qed

3360 note s3 = \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)

3361 else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close>

3362 have s1_s2: "dom (locals s1) \<subseteq> dom (locals (store s2))"

3363 proof -

3364 from \<open>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<close>

3365 show ?thesis

3366 by (rule dom_locals_eval_mono_elim) simp

3367 qed

3369 have "?NormalAssigned s3 A"

3370 proof

3371 assume normal_s3: "normal s3"

3372 show "nrm A \<subseteq> dom (locals (snd s3))"

3373 proof -

3374 have "nrm C1 \<subseteq> dom (locals (snd s3))"

3375 proof -

3376 from normal_s3 s3

3377 have "normal (x1,s1)"

3378 by (cases s2) (simp add: abrupt_if_def)

3379 with normal_s3 nrmAss_C1 s3 s1_s2

3380 show ?thesis

3381 by fastforce

3382 qed

3383 moreover

3384 have "nrm C2 \<subseteq> dom (locals (snd s3))"

3385 proof -

3386 from normal_s3 s3

3387 have "normal s2"

3388 by (cases s2) (simp add: abrupt_if_def)

3389 with normal_s3 nrmAss_C2 s3 s1_s2

3390 show ?thesis

3391 by fastforce

3392 qed

3393 ultimately have "nrm C1 \<union> nrm C2 \<subseteq> \<dots>"

3394 by (rule Un_least)

3395 with nrm_A show ?thesis

3396 by simp

3397 qed

3398 qed

3399 moreover

3400 {

3401 fix l assume brk_s3: "abrupt s3 = Some (Jump (Break l))"

3402 have "brk A l \<subseteq> dom (locals (store s3))"

3403 proof (cases "normal s2")

3404 case True

3405 with brk_s3 s3

3406 have s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"

3407 by simp

3408 have "brk C1 l \<subseteq> dom (locals (store s3))"

3409 proof -

3410 from True brk_s3 s3 have "x1=Some (Jump (Break l))"

3411 by (cases s2) (simp add: abrupt_if_def)

3412 with brkAss_C1 s1_s2 s2_s3

3413 show ?thesis

3414 by simp

3415 qed

3416 moreover from True nrmAss_C2 s2_s3

3417 have "nrm C2 \<subseteq> dom (locals (store s3))"

3418 by - (rule subset_trans, simp_all)

3419 ultimately

3420 have "((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) l \<subseteq> \<dots>"

3421 by blast

3422 with brk_A show ?thesis

3423 by simp blast

3424 next

3425 case False

3426 note not_normal_s2 = this

3427 have "s3=s2"

3428 proof (cases "normal (x1,s1)")

3429 case True with not_normal_s2 s3 show ?thesis

3430 by (cases s2) (simp add: abrupt_if_def)

3431 next

3432 case False with not_normal_s2 s3 brk_s3 show ?thesis

3433 by (cases s2) (simp add: abrupt_if_def)

3434 qed

3435 with brkAss_C2 brk_s3

3436 have "brk C2 l \<subseteq> dom (locals (store s3))"

3437 by simp

3438 with brk_A show ?thesis

3439 by simp blast

3440 qed

3441 }

3442 hence "?BreakAssigned (Norm s0) s3 A"

3443 by simp

3444 moreover

3445 {

3446 assume abr_s3: "abrupt s3 = Some (Jump Ret)"

3447 have "Result \<in> dom (locals (store s3))"

3448 proof (cases "x1 = Some (Jump Ret)")

3449 case True

3450 note ret_x1 = this

3451 with resAss_s1 have res_s1: "Result \<in> dom (locals s1)"

3452 by simp

3453 moreover have "dom (locals (store ((Norm s1)::state)))

3454 \<subseteq> dom (locals (store s2))"

3455 by (rule dom_locals_eval_mono_elim) (rule Fin.hyps)

3456 ultimately have "Result \<in> dom (locals (store s2))"

3457 by - (rule subsetD,auto)

3458 with res_s1 s3 show ?thesis

3459 by simp

3460 next

3461 case False

3462 with s3 abr_s3 obtain "abrupt s2 = Some (Jump Ret)" and "s3=s2"

3463 by (cases s2) (simp add: abrupt_if_def)

3464 with resAss_s2 show ?thesis

3465 by simp

3466 qed

3467 }

3468 hence "?ResAssigned (Norm s0) s3"

3469 by simp

3470 ultimately show ?case by (intro conjI)

3471 next

3472 case (Init C c s0 s3 s1 s2 Env T A)

3473 note G = \<open>prg Env = G\<close>

3474 from Init.hyps

3475 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Init C\<rightarrow> s3"

3476 apply (simp only: G)

3477 apply (rule eval.Init, assumption)

3478 apply (cases "inited C (globs s0) ")

3479 apply simp

3480 apply (simp only: if_False )

3481 apply (elim conjE,intro conjI,assumption+,simp)

3482 done (* auto or simp alone always do too much *)

3483 from Init.prems and \<open>the (class G C) = c\<close>

3484 have c: "class G C = Some c"

3485 by (elim wt_elim_cases) auto

3486 from Init.prems obtain

3487 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"

3488 by (elim da_elim_cases) simp

3489 show ?case

3490 proof (cases "inited C (globs s0)")

3491 case True

3492 with Init.hyps have "s3=Norm s0" by simp

3493 thus ?thesis

3494 using nrm_A by simp

3495 next

3496 case False

3497 from Init.hyps False G

3498 obtain eval_initC:

3499 "prg Env\<turnstile>Norm ((init_class_obj G C) s0)

3500 \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and

3501 eval_init: "prg Env\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and

3502 s3: "s3=(set_lvars (locals (store s1))) s2"

3503 by simp

3504 have "?NormalAssigned s3 A"

3505 proof

3506 show "nrm A \<subseteq> dom (locals (store s3))"

3507 proof -

3508 from nrm_A have "nrm A \<subseteq> dom (locals (init_class_obj G C s0))"

3509 by simp

3510 also from eval_initC have "\<dots> \<subseteq> dom (locals (store s1))"

3511 by (rule dom_locals_eval_mono_elim) simp

3512 also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"

3513 by (cases s1) (cases s2, simp add: init_lvars_def2)

3514 finally show ?thesis .

3515 qed

3516 qed

3517 moreover

3518 from eval

3519 have "\<And> j. abrupt s3 \<noteq> Some (Jump j)"

3520 by (rule eval_statement_no_jump) (auto simp add: wf c G)

3521 then obtain "?BreakAssigned (Norm s0) s3 A"

3522 and "?ResAssigned (Norm s0) s3"

3523 by simp

3524 ultimately show ?thesis by (intro conjI)

3525 qed

3526 next

3527 case (NewC s0 C s1 a s2 Env T A)

3528 note G = \<open>prg Env = G\<close>

3529 from NewC.prems

3530 obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))"

3531 "brk A = (\<lambda> l. UNIV)"

3532 by (elim da_elim_cases) simp

3533 from wf NewC.prems

3534 have wt_init: "Env\<turnstile>(Init C)\<Colon>\<surd>"

3535 by (elim wt_elim_cases) (drule is_acc_classD,simp)

3536 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s2))"

3537 proof -

3538 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

3539 by (rule dom_locals_eval_mono_elim) (rule NewC.hyps)

3540 also

3541 have "\<dots> \<subseteq> dom (locals (store s2))"

3542 by (rule dom_locals_halloc_mono) (rule NewC.hyps)

3543 finally show ?thesis .

3544 qed

3545 with A have "?NormalAssigned s2 A"

3546 by simp

3547 moreover

3548 {

3549 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3550 proof -

3551 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"

3552 unfolding G by (rule eval.NewC NewC.hyps)+

3553 from NewC.prems

3554 obtain T' where "T=Inl T'"

3555 by (elim wt_elim_cases) simp

3556 with NewC.prems have "Env\<turnstile>NewC C\<Colon>-T'"

3557 by simp

3558 from eval _ this

3559 show ?thesis

3560 by (rule eval_expression_no_jump) (simp_all add: G wf)

3561 qed

3562 }

3563 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3564 by simp_all

3565 ultimately show ?case by (intro conjI)

3566 next

3567 case (NewA s0 elT s1 e i s2 a s3 Env T A)

3568 note G = \<open>prg Env = G\<close>

3569 from NewA.prems obtain

3570 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3571 by (elim da_elim_cases)

3572 from NewA.prems obtain

3573 wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and

3574 wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"

3575 by (elim wt_elim_cases) (auto dest: wt_init_comp_ty')

3576 note halloc = \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3\<close>

3577 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"

3578 by (rule dom_locals_eval_mono_elim) (rule NewA.hyps)

3579 with da_e obtain A' where

3580 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"

3581 and nrm_A_A': "nrm A \<subseteq> nrm A'"

3582 and brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"

3583 by (rule da_weakenE) simp

3584 note \<open>PROP ?Hyp (In1l e) s1 s2\<close>

3585 with wt_size da_e' G obtain

3586 nrmAss_A': "?NormalAssigned s2 A'" and

3587 brkAss_A': "?BreakAssigned s1 s2 A'"

3588 by simp

3589 have s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"

3590 proof -

3591 have "dom (locals (store s2))

3592 \<subseteq> dom (locals (store (abupd (check_neg i) s2)))"

3593 by (simp)

3594 also have "\<dots> \<subseteq> dom (locals (store s3))"

3595 by (rule dom_locals_halloc_mono) (rule NewA.hyps)

3596 finally show ?thesis .

3597 qed

3598 have "?NormalAssigned s3 A"

3599 proof

3600 assume normal_s3: "normal s3"

3601 show "nrm A \<subseteq> dom (locals (store s3))"

3602 proof -

3603 from halloc normal_s3

3604 have "normal (abupd (check_neg i) s2)"

3605 by cases simp_all

3606 hence "normal s2"

3607 by (cases s2) simp

3608 with nrmAss_A' nrm_A_A' s2_s3 show ?thesis

3609 by blast

3610 qed

3611 qed

3612 moreover

3613 {

3614 fix j have "abrupt s3 \<noteq> Some (Jump j)"

3615 proof -

3616 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"

3617 unfolding G by (rule eval.NewA NewA.hyps)+

3618 from NewA.prems

3619 obtain T' where "T=Inl T'"

3620 by (elim wt_elim_cases) simp

3621 with NewA.prems have "Env\<turnstile>New elT[e]\<Colon>-T'"

3622 by simp

3623 from eval _ this

3624 show ?thesis

3625 by (rule eval_expression_no_jump) (simp_all add: G wf)

3626 qed

3627 }

3628 hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"

3629 by simp_all

3630 ultimately show ?case by (intro conjI)

3631 next

3632 case (Cast s0 e v s1 s2 cT Env T A)

3633 note G = \<open>prg Env = G\<close>

3634 from Cast.prems obtain

3635 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3636 by (elim da_elim_cases)

3637 from Cast.prems obtain eT where

3638 wt_e: "Env\<turnstile>e\<Colon>-eT"

3639 by (elim wt_elim_cases)

3640 note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>

3641 with wt_e da_e G obtain

3642 nrmAss_A: "?NormalAssigned s1 A" and

3643 brkAss_A: "?BreakAssigned (Norm s0) s1 A"

3644 by simp

3645 note s2 = \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close>

3646 hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"

3647 by simp

3648 have "?NormalAssigned s2 A"

3649 proof

3650 assume "normal s2"

3651 with s2 have "normal s1"

3652 by (cases s1) simp

3653 with nrmAss_A s1_s2

3654 show "nrm A \<subseteq> dom (locals (store s2))"

3655 by blast

3656 qed

3657 moreover

3658 {

3659 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3660 proof -

3661 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"

3662 unfolding G by (rule eval.Cast Cast.hyps)+

3663 from Cast.prems

3664 obtain T' where "T=Inl T'"

3665 by (elim wt_elim_cases) simp

3666 with Cast.prems have "Env\<turnstile>Cast cT e\<Colon>-T'"

3667 by simp

3668 from eval _ this

3669 show ?thesis

3670 by (rule eval_expression_no_jump) (simp_all add: G wf)

3671 qed

3672 }

3673 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3674 by simp_all

3675 ultimately show ?case by (intro conjI)

3676 next

3677 case (Inst s0 e v s1 b iT Env T A)

3678 note G = \<open>prg Env = G\<close>

3679 from Inst.prems obtain

3680 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3681 by (elim da_elim_cases)

3682 from Inst.prems obtain eT where

3683 wt_e: "Env\<turnstile>e\<Colon>-eT"

3684 by (elim wt_elim_cases)

3685 note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>

3686 with wt_e da_e G obtain

3687 "?NormalAssigned s1 A" and

3688 "?BreakAssigned (Norm s0) s1 A" and

3689 "?ResAssigned (Norm s0) s1"

3690 by simp

3691 thus ?case by (intro conjI)

3692 next

3693 case (Lit s v Env T A)

3694 from Lit.prems

3695 have "nrm A = dom (locals (store ((Norm s)::state)))"

3696 by (elim da_elim_cases) simp

3697 thus ?case by simp

3698 next

3699 case (UnOp s0 e v s1 unop Env T A)

3700 note G = \<open>prg Env = G\<close>

3701 from UnOp.prems obtain

3702 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3703 by (elim da_elim_cases)

3704 from UnOp.prems obtain eT where

3705 wt_e: "Env\<turnstile>e\<Colon>-eT"

3706 by (elim wt_elim_cases)

3707 note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>

3708 with wt_e da_e G obtain

3709 "?NormalAssigned s1 A" and

3710 "?BreakAssigned (Norm s0) s1 A" and

3711 "?ResAssigned (Norm s0) s1"

3712 by simp

3713 thus ?case by (intro conjI)

3714 next

3715 case (BinOp s0 e1 v1 s1 binop e2 v2 s2 Env T A)

3716 note G = \<open>prg Env = G\<close>

3717 from BinOp.hyps

3718 have

3719 eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"

3720 by (simp only: G) (rule eval.BinOp)

3721 have s0_s1: "dom (locals (store ((Norm s0)::state)))

3722 \<subseteq> dom (locals (store s1))"

3723 by (rule dom_locals_eval_mono_elim) (rule BinOp)

3724 also have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"

3725 by (rule dom_locals_eval_mono_elim) (rule BinOp)

3726 finally

3727 have s0_s2: "dom (locals (store ((Norm s0)::state)))

3728 \<subseteq> dom (locals (store s2))" .

3729 from BinOp.prems obtain e1T e2T

3730 where wt_e1: "Env\<turnstile>e1\<Colon>-e1T"

3731 and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"

3732 and wt_binop: "wt_binop (prg Env) binop e1T e2T"

3733 and T: "T=Inl (PrimT (binop_type binop))"

3734 by (elim wt_elim_cases) simp

3735 have "?NormalAssigned s2 A"

3736 proof

3737 assume normal_s2: "normal s2"

3738 have normal_s1: "normal s1"

3739 by (rule eval_no_abrupt_lemma [rule_format]) (rule BinOp.hyps, rule normal_s2)

3740 show "nrm A \<subseteq> dom (locals (store s2))"

3741 proof (cases "binop=CondAnd")

3742 case True

3743 note CondAnd = this

3744 from BinOp.prems obtain

3745 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

3746 \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>

3747 assigns_if False (BinOp CondAnd e1 e2))"

3748 by (elim da_elim_cases) (simp_all add: CondAnd)

3749 from T BinOp.prems CondAnd

3750 have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean"

3751 by (simp)

3752 with eval normal_s2

3753 have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2))

3754 (BinOp binop e1 e2)

3755 \<subseteq> dom (locals (store s2))"

3756 by (rule assigns_if_good_approx)

3757 have "(assigns_if True (BinOp CondAnd e1 e2) \<inter>

3758 assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"

3759 proof (cases "the_Bool (eval_binop binop v1 v2)")

3760 case True

3761 with ass_if CondAnd

3762 have "assigns_if True (BinOp CondAnd e1 e2)

3763 \<subseteq> dom (locals (store s2))"

3764 by simp

3765 thus ?thesis by blast

3766 next

3767 case False

3768 with ass_if CondAnd

3769 have "assigns_if False (BinOp CondAnd e1 e2)

3770 \<subseteq> dom (locals (store s2))"

3771 by (simp only: False)

3772 thus ?thesis by blast

3773 qed

3774 with s0_s2

3775 have "dom (locals (store ((Norm s0)::state)))

3776 \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>

3777 assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"

3778 by (rule Un_least)

3779 thus ?thesis by (simp only: nrm_A)

3780 next

3781 case False

3782 note notCondAnd = this

3783 show ?thesis

3784 proof (cases "binop=CondOr")

3785 case True

3786 note CondOr = this

3787 from BinOp.prems obtain

3788 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

3789 \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>

3790 assigns_if False (BinOp CondOr e1 e2))"

3791 by (elim da_elim_cases) (simp_all add: CondOr)

3792 from T BinOp.prems CondOr

3793 have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean"

3794 by (simp)

3795 with eval normal_s2

3796 have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2))

3797 (BinOp binop e1 e2)

3798 \<subseteq> dom (locals (store s2))"

3799 by (rule assigns_if_good_approx)

3800 have "(assigns_if True (BinOp CondOr e1 e2) \<inter>

3801 assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"

3802 proof (cases "the_Bool (eval_binop binop v1 v2)")

3803 case True

3804 with ass_if CondOr

3805 have "assigns_if True (BinOp CondOr e1 e2)

3806 \<subseteq> dom (locals (store s2))"

3807 by (simp)

3808 thus ?thesis by blast

3809 next

3810 case False

3811 with ass_if CondOr

3812 have "assigns_if False (BinOp CondOr e1 e2)

3813 \<subseteq> dom (locals (store s2))"

3814 by (simp)

3815 thus ?thesis by blast

3816 qed

3817 with s0_s2

3818 have "dom (locals (store ((Norm s0)::state)))

3819 \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>

3820 assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"

3821 by (rule Un_least)

3822 thus ?thesis by (simp only: nrm_A)

3823 next

3824 case False

3825 with notCondAnd obtain notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"

3826 by simp

3827 from BinOp.prems obtain E1

3828 where da_e1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1"

3829 and da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"

3830 by (elim da_elim_cases) (simp_all add: notAndOr)

3831 note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1\<close>

3832 with wt_e1 da_e1 G normal_s1

3833 obtain "?NormalAssigned s1 E1"

3834 by simp

3835 with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by iprover

3836 with da_e2 obtain A'

3837 where da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and

3838 nrm_A_A': "nrm A \<subseteq> nrm A'"

3839 by (rule da_weakenE) iprover

3840 from notAndOr have "need_second_arg binop v1" by simp

3841 with BinOp.hyps

3842 have "PROP ?Hyp (In1l e2) s1 s2" by simp

3843 with wt_e2 da_e2' G

3844 obtain "?NormalAssigned s2 A'"

3845 by simp

3846 with nrm_A_A' normal_s2

3847 show "nrm A \<subseteq> dom (locals (store s2))"

3848 by blast

3849 qed

3850 qed

3851 qed

3852 moreover

3853 {

3854 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3855 proof -

3856 from BinOp.prems T

3857 have "Env\<turnstile>In1l (BinOp binop e1 e2)\<Colon>Inl (PrimT (binop_type binop))"

3858 by simp

3859 from eval _ this

3860 show ?thesis

3861 by (rule eval_expression_no_jump) (simp_all add: G wf)

3862 qed

3863 }

3864 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3865 by simp_all

3866 ultimately show ?case by (intro conjI)

3867 next

3868 case (Super s Env T A)

3869 from Super.prems

3870 have "nrm A = dom (locals (store ((Norm s)::state)))"

3871 by (elim da_elim_cases) simp

3872 thus ?case by simp

3873 next

3874 case (Acc s0 v w upd s1 Env T A)

3875 show ?case

3876 proof (cases "\<exists> vn. v = LVar vn")

3877 case True

3878 then obtain vn where vn: "v=LVar vn"..

3879 from Acc.prems

3880 have "nrm A = dom (locals (store ((Norm s0)::state)))"

3881 by (simp only: vn) (elim da_elim_cases,simp_all)

3882 moreover

3883 from \<open>G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1\<close>

3884 have "s1=Norm s0"

3885 by (simp only: vn) (elim eval_elim_cases,simp)

3886 ultimately show ?thesis by simp

3887 next

3888 case False

3889 note G = \<open>prg Env = G\<close>

3890 from False Acc.prems

3891 have da_v: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>v\<rangle>\<guillemotright> A"

3892 by (elim da_elim_cases) simp_all

3893 from Acc.prems obtain vT where

3894 wt_v: "Env\<turnstile>v\<Colon>=vT"

3895 by (elim wt_elim_cases)

3896 note \<open>PROP ?Hyp (In2 v) (Norm s0) s1\<close>

3897 with wt_v da_v G obtain

3898 "?NormalAssigned s1 A" and

3899 "?BreakAssigned (Norm s0) s1 A" and

3900 "?ResAssigned (Norm s0) s1"

3901 by simp

3902 thus ?thesis by (intro conjI)

3903 qed

3904 next

3905 case (Ass s0 var w upd s1 e v s2 Env T A)

3906 note G = \<open>prg Env = G\<close>

3907 from Ass.prems obtain varT eT where

3908 wt_var: "Env\<turnstile>var\<Colon>=varT" and

3909 wt_e: "Env\<turnstile>e\<Colon>-eT"

3910 by (elim wt_elim_cases) simp

3911 have eval_var: "prg Env\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1"

3912 using Ass.hyps by (simp only: G)

3913 have "?NormalAssigned (assign upd v s2) A"

3914 proof

3915 assume normal_ass_s2: "normal (assign upd v s2)"

3916 from normal_ass_s2

3917 have normal_s2: "normal s2"

3918 by (cases s2) (simp add: assign_def Let_def)

3919 hence normal_s1: "normal s1"

3920 by - (rule eval_no_abrupt_lemma [rule_format], rule Ass.hyps)

3921 note hyp_var = \<open>PROP ?Hyp (In2 var) (Norm s0) s1\<close>

3922 note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2\<close>

3923 show "nrm A \<subseteq> dom (locals (store (assign upd v s2)))"

3924 proof (cases "\<exists> vn. var = LVar vn")

3925 case True

3926 then obtain vn where vn: "var=LVar vn"..

3927 from Ass.prems obtain E where

3928 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

3929 nrm_A: "nrm A = nrm E \<union> {vn}"

3930 by (elim da_elim_cases) (insert vn,auto)

3931 obtain E' where

3932 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" and

3933 E_E': "nrm E \<subseteq> nrm E'"

3934 proof -

3935 have "dom (locals (store ((Norm s0)::state)))

3936 \<subseteq> dom (locals (store s1))"

3937 by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)

3938 with da_e show thesis

3939 by (rule da_weakenE) (rule that)

3940 qed

3941 from G eval_var vn

3942 have eval_lvar: "G\<turnstile>Norm s0 \<midarrow>LVar vn=\<succ>(w, upd)\<rightarrow> s1"

3943 by simp

3944 then have upd: "upd = snd (lvar vn (store s1))"

3945 by cases (cases "lvar vn (store s1)",simp)

3946 have "nrm E \<subseteq> dom (locals (store (assign upd v s2)))"

3947 proof -

3948 from hyp_e wt_e da_e' G normal_s2

3949 have "nrm E' \<subseteq> dom (locals (store s2))"

3950 by simp

3951 also

3952 from upd

3953 have "dom (locals (store s2)) \<subseteq> dom (locals (store (upd v s2)))"

3954 by (simp add: lvar_def) blast

3955 hence "dom (locals (store s2))

3956 \<subseteq> dom (locals (store (assign upd v s2)))"

3957 by (rule dom_locals_assign_mono)

3958 finally

3959 show ?thesis using E_E'

3960 by blast

3961 qed

3962 moreover

3963 from upd normal_s2

3964 have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"

3965 by (auto simp add: assign_def Let_def lvar_def upd split: prod.split)

3966 ultimately

3967 show "nrm A \<subseteq> \<dots>"

3968 by (rule Un_least [elim_format]) (simp add: nrm_A)

3969 next

3970 case False

3971 from Ass.prems obtain V where

3972 da_var: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>var\<rangle>\<guillemotright> V" and

3973 da_e: "Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3974 by (elim da_elim_cases) (insert False,simp+)

3975 from hyp_var wt_var da_var G normal_s1

3976 have "nrm V \<subseteq> dom (locals (store s1))"

3977 by simp

3978 with da_e obtain A'

3979 where da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and

3980 nrm_A_A': "nrm A \<subseteq> nrm A'"

3981 by (rule da_weakenE) iprover

3982 from hyp_e wt_e da_e' G normal_s2

3983 obtain "nrm A' \<subseteq> dom (locals (store s2))"

3984 by simp

3985 with nrm_A_A' have "nrm A \<subseteq> \<dots>"

3986 by blast

3987 also have "\<dots> \<subseteq> dom (locals (store (assign upd v s2)))"

3988 proof -

3989 from eval_var normal_s1

3990 have "dom (locals (store s2)) \<subseteq> dom (locals (store (upd v s2)))"

3991 by (cases rule: dom_locals_eval_mono_elim)

3992 (cases s2, simp)

3993 thus ?thesis

3994 by (rule dom_locals_assign_mono)

3995 qed

3996 finally show ?thesis .

3997 qed

3998 qed

3999 moreover

4000 {

4001 fix j have "abrupt (assign upd v s2) \<noteq> Some (Jump j)"

4002 proof -

4003 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"

4004 by (simp only: G) (rule eval.Ass Ass.hyps)+

4005 from Ass.prems

4006 obtain T' where "T=Inl T'"

4007 by (elim wt_elim_cases) simp

4008 with Ass.prems have "Env\<turnstile>var:=e\<Colon>-T'" by simp

4009 from eval _ this

4010 show ?thesis

4011 by (rule eval_expression_no_jump) (simp_all add: G wf)

4012 qed

4013 }

4014 hence "?BreakAssigned (Norm s0) (assign upd v s2) A"

4015 and "?ResAssigned (Norm s0) (assign upd v s2)"

4016 by simp_all

4017 ultimately show ?case by (intro conjI)

4018 next

4019 case (Cond s0 e0 b s1 e1 e2 v s2 Env T A)

4020 note G = \<open>prg Env = G\<close>

4021 have "?NormalAssigned s2 A"

4022 proof

4023 assume normal_s2: "normal s2"

4024 show "nrm A \<subseteq> dom (locals (store s2))"

4025 proof (cases "Env\<turnstile>(e0 ? e1 : e2)\<Colon>-(PrimT Boolean)")

4026 case True

4027 with Cond.prems

4028 have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

4029 \<union> (assigns_if True (e0 ? e1 : e2) \<inter>

4030 assigns_if False (e0 ? e1 : e2))"

4031 by (elim da_elim_cases) simp_all

4032 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>(e0 ? e1 : e2)-\<succ>v\<rightarrow> s2"

4033 unfolding G by (rule eval.Cond Cond.hyps)+

4034 from eval

4035 have "dom (locals (store ((Norm s0)::state)))\<subseteq>dom (locals (store s2))"

4036 by (rule dom_locals_eval_mono_elim)

4037 moreover

4038 from eval normal_s2 True

4039 have ass_if: "assigns_if (the_Bool v) (e0 ? e1 : e2)

4040 \<subseteq> dom (locals (store s2))"

4041 by (rule assigns_if_good_approx)

4042 have "assigns_if True (e0 ? e1:e2) \<inter> assigns_if False (e0 ? e1:e2)

4043 \<subseteq> dom (locals (store s2))"

4044 proof (cases "the_Bool v")

4045 case True

4046 from ass_if

4047 have "assigns_if True (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"

4048 by (simp only: True)

4049 thus ?thesis by blast

4050 next

4051 case False

4052 from ass_if

4053 have "assigns_if False (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"

4054 by (simp only: False)

4055 thus ?thesis by blast

4056 qed

4057 ultimately show "nrm A \<subseteq> dom (locals (store s2))"

4058 by (simp only: nrm_A) (rule Un_least)

4059 next

4060 case False

4061 with Cond.prems obtain E1 E2 where

4062 da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

4063 \<union> assigns_if True e0) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and

4064 da_e2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

4065 \<union> assigns_if False e0) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2" and

4066 nrm_A: "nrm A = nrm E1 \<inter> nrm E2"

4067 by (elim da_elim_cases) simp_all

4068 from Cond.prems obtain e1T e2T where

4069 wt_e0: "Env\<turnstile>e0\<Colon>- PrimT Boolean" and

4070 wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and

4071 wt_e2: "Env\<turnstile>e2\<Colon>-e2T"

4072 by (elim wt_elim_cases)

4073 have s0_s1: "dom (locals (store ((Norm s0)::state)))

4074 \<subseteq> dom (locals (store s1))"

4075 by (rule dom_locals_eval_mono_elim) (rule Cond.hyps)

4076 have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"

4077 unfolding G by (rule Cond.hyps)

4078 have normal_s1: "normal s1"

4079 by (rule eval_no_abrupt_lemma [rule_format]) (rule Cond.hyps, rule normal_s2)

4080 show ?thesis

4081 proof (cases "the_Bool b")

4082 case True

4083 from True Cond.hyps have "PROP ?Hyp (In1l e1) s1 s2" by simp

4084 moreover

4085 from eval_e0 normal_s1 wt_e0

4086 have "assigns_if True e0 \<subseteq> dom (locals (store s1))"

4087 by (rule assigns_if_good_approx [elim_format]) (simp only: True)

4088 with s0_s1

4089 have "dom (locals (store ((Norm s0)::state)))

4090 \<union> assigns_if True e0 \<subseteq> \<dots>"

4091 by (rule Un_least)

4092 with da_e1 obtain E1' where

4093 da_e1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and

4094 nrm_E1_E1': "nrm E1 \<subseteq> nrm E1'"

4095 by (rule da_weakenE) iprover

4096 ultimately have "nrm E1' \<subseteq> dom (locals (store s2))"

4097 using wt_e1 G normal_s2 by simp

4098 with nrm_E1_E1' show ?thesis

4099 by (simp only: nrm_A) blast

4100 next

4101 case False

4102 from False Cond.hyps have "PROP ?Hyp (In1l e2) s1 s2" by simp

4103 moreover

4104 from eval_e0 normal_s1 wt_e0

4105 have "assigns_if False e0 \<subseteq> dom (locals (store s1))"

4106 by (rule assigns_if_good_approx [elim_format]) (simp only: False)

4107 with s0_s1

4108 have "dom (locals (store ((Norm s0)::state)))

4109 \<union> assigns_if False e0 \<subseteq> \<dots>"

4110 by (rule Un_least)

4111 with da_e2 obtain E2' where

4112 da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and

4113 nrm_E2_E2': "nrm E2 \<subseteq> nrm E2'"

4114 by (rule da_weakenE) iprover

4115 ultimately have "nrm E2' \<subseteq> dom (locals (store s2))"

4116 using wt_e2 G normal_s2 by simp

4117 with nrm_E2_E2' show ?thesis

4118 by (simp only: nrm_A) blast

4119 qed

4120 qed

4121 qed

4122 moreover

4123 {

4124 fix j have "abrupt s2 \<noteq> Some (Jump j)"

4125 proof -

4126 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"

4127 unfolding G by (rule eval.Cond Cond.hyps)+

4128 from Cond.prems

4129 obtain T' where "T=Inl T'"

4130 by (elim wt_elim_cases) simp

4131 with Cond.prems have "Env\<turnstile>e0 ? e1 : e2\<Colon>-T'" by simp

4132 from eval _ this

4133 show ?thesis

4134 by (rule eval_expression_no_jump) (simp_all add: G wf)

4135 qed

4136 }

4137 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

4138 by simp_all

4139 ultimately show ?case by (intro conjI)

4140 next

4141 case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4

4142 Env T A)

4143 note G = \<open>prg Env = G\<close>

4144 have "?NormalAssigned (restore_lvars s2 s4) A"

4145 proof

4146 assume normal_restore_lvars: "normal (restore_lvars s2 s4)"

4147 show "nrm A \<subseteq> dom (locals (store (restore_lvars s2 s4)))"

4148 proof -

4149 from Call.prems obtain E where

4150 da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

4151 da_args: "Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A"

4152 by (elim da_elim_cases)

4153 from Call.prems obtain eT argsT where

4154 wt_e: "Env\<turnstile>e\<Colon>-eT" and

4155 wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"

4156 by (elim wt_elim_cases)

4157 note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2\<close>

4158 note s3' = \<open>s3' = check_method_access G accC statT mode

4159 \<lparr>name=mn,parTs=pTs\<rparr> a s3\<close>

4160 have normal_s2: "normal s2"

4161 proof -

4162 from normal_restore_lvars have "normal s4"

4163 by simp

4164 then have "normal s3'"

4165 by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)

4166 with s3' have "normal s3"

4167 by (cases s3) (simp add: check_method_access_def Let_def)

4168 with s3 show "normal s2"

4169 by (cases s2) (simp add: init_lvars_def Let_def)

4170 qed

4171 then have normal_s1: "normal s1"

4172 by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)

4173 note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>

4174 with da_e wt_e G normal_s1

4175 have "nrm E \<subseteq> dom (locals (store s1))"

4176 by simp

4177 with da_args obtain A' where

4178 da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and

4179 nrm_A_A': "nrm A \<subseteq> nrm A'"

4180 by (rule da_weakenE) iprover

4181 note \<open>PROP ?Hyp (In3 args) s1 s2\<close>

4182 with da_args' wt_args G normal_s2

4183 have "nrm A' \<subseteq> dom (locals (store s2))"

4184 by simp

4185 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4186 by blast

4187 also have "\<dots> \<subseteq> dom (locals (store (restore_lvars s2 s4)))"

4188 by (cases s4) simp

4189 finally show ?thesis .

4190 qed

4191 qed

4192 moreover

4193 {

4194 fix j have "abrupt (restore_lvars s2 s4) \<noteq> Some (Jump j)"

4195 proof -

4196 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v

4197 \<rightarrow> (restore_lvars s2 s4)"

4198 unfolding G by (rule eval.Call Call)+

4199 from Call.prems

4200 obtain T' where "T=Inl T'"

4201 by (elim wt_elim_cases) simp

4202 with Call.prems have "Env\<turnstile>({accC,statT,mode}e\<cdot>mn( {pTs}args))\<Colon>-T'"

4203 by simp

4204 from eval _ this

4205 show ?thesis

4206 by (rule eval_expression_no_jump) (simp_all add: G wf)

4207 qed

4208 }

4209 hence "?BreakAssigned (Norm s0) (restore_lvars s2 s4) A"

4210 and "?ResAssigned (Norm s0) (restore_lvars s2 s4)"

4211 by simp_all

4212 ultimately show ?case by (intro conjI)

4213 next

4214 case (Methd s0 D sig v s1 Env T A)

4215 note G = \<open>prg Env = G\<close>

4216 from Methd.prems obtain m where

4217 m: "methd (prg Env) D sig = Some m" and

4218 da_body: "Env\<turnstile>(dom (locals (store ((Norm s0)::state))))

4219 \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A"

4220 by - (erule da_elim_cases)

4221 from Methd.prems m obtain

4222 isCls: "is_class (prg Env) D" and

4223 wt_body: "Env \<turnstile>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<Colon>T"

4224 by - (erule wt_elim_cases,simp)

4225 note \<open>PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1\<close>

4226 moreover

4227 from wt_body have "Env\<turnstile>In1l (body G D sig)\<Colon>T"

4228 using isCls m G by (simp add: body_def2)

4229 moreover

4230 from da_body have "Env\<turnstile>(dom (locals (store ((Norm s0)::state))))

4231 \<guillemotright>\<langle>body G D sig\<rangle>\<guillemotright> A"

4232 using isCls m G by (simp add: body_def2)

4233 ultimately show ?case

4234 using G by simp

4235 next

4236 case (Body s0 D s1 c s2 s3 Env T A)

4237 note G = \<open>prg Env = G\<close>

4238 from Body.prems

4239 have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"

4240 by (elim da_elim_cases) simp

4241 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)

4242 \<rightarrow>abupd (absorb Ret) s3"

4243 unfolding G by (rule eval.Body Body.hyps)+

4244 hence "nrm A \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"

4245 by (simp only: nrm_A) (rule dom_locals_eval_mono_elim)

4246 hence "?NormalAssigned (abupd (absorb Ret) s3) A"

4247 by simp

4248 moreover

4249 from eval have "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"

4250 by (rule Body_no_jump) simp

4251 hence "?BreakAssigned (Norm s0) (abupd (absorb Ret) s3) A" and

4252 "?ResAssigned (Norm s0) (abupd (absorb Ret) s3)"

4253 by simp_all

4254 ultimately show ?case by (intro conjI)

4255 next

4256 case (LVar s vn Env T A)

4257 from LVar.prems

4258 have "nrm A = dom (locals (store ((Norm s)::state)))"

4259 by (elim da_elim_cases) simp

4260 thus ?case by simp

4261 next

4262 case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC Env T A)

4263 note G = \<open>prg Env = G\<close>

4264 have "?NormalAssigned s3 A"

4265 proof

4266 assume normal_s3: "normal s3"

4267 show "nrm A \<subseteq> dom (locals (store s3))"

4268 proof -

4269 note fvar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close> and

4270 s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>

4271 from FVar.prems

4272 have da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

4273 by (elim da_elim_cases)

4274 from FVar.prems obtain eT where

4275 wt_e: "Env\<turnstile>e\<Colon>-eT"

4276 by (elim wt_elim_cases)

4277 have "(dom (locals (store ((Norm s0)::state))))

4278 \<subseteq> dom (locals (store s1))"

4279 by (rule dom_locals_eval_mono_elim) (rule FVar.hyps)

4280 with da_e obtain A' where

4281 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and

4282 nrm_A_A': "nrm A \<subseteq> nrm A'"

4283 by (rule da_weakenE) iprover

4284 have normal_s2: "normal s2"

4285 proof -

4286 from normal_s3 s3

4287 have "normal s2'"

4288 by (cases s2') (simp add: check_field_access_def Let_def)

4289 with fvar

4290 show "normal s2"

4291 by (cases s2) (simp add: fvar_def2)

4292 qed

4293 note \<open>PROP ?Hyp (In1l e) s1 s2\<close>

4294 with da_e' wt_e G normal_s2

4295 have "nrm A' \<subseteq> dom (locals (store s2))"

4296 by simp

4297 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4298 by blast

4299 also have "\<dots> \<subseteq> dom (locals (store s3))"

4300 proof -

4301 from fvar have "s2' = snd (fvar statDeclC stat fn a s2)"

4302 by (cases "fvar statDeclC stat fn a s2") simp

4303 hence "dom (locals (store s2)) \<subseteq> dom (locals (store s2'))"

4304 by (simp) (rule dom_locals_fvar_mono)

4305 also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"

4306 by (cases s2') (simp add: check_field_access_def Let_def)

4307 finally show ?thesis .

4308 qed

4309 finally show ?thesis .

4310 qed

4311 qed

4312 moreover

4313 {

4314 fix j have "abrupt s3 \<noteq> Some (Jump j)"

4315 proof -

4316 obtain w upd where v: "(w,upd)=v"

4317 by (cases v) auto

4318 have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"

4319 by (simp only: G v) (rule eval.FVar FVar.hyps)+

4320 from FVar.prems

4321 obtain T' where "T=Inl T'"

4322 by (elim wt_elim_cases) simp

4323 with FVar.prems have "Env\<turnstile>({accC,statDeclC,stat}e..fn)\<Colon>=T'"

4324 by simp

4325 from eval _ this

4326 show ?thesis

4327 by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)

4328 qed

4329 }

4330 hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"

4331 by simp_all

4332 ultimately show ?case by (intro conjI)

4333 next

4334 case (AVar s0 e1 a s1 e2 i s2 v s2' Env T A)

4335 note G = \<open>prg Env = G\<close>

4336 have "?NormalAssigned s2' A"

4337 proof

4338 assume normal_s2': "normal s2'"

4339 show "nrm A \<subseteq> dom (locals (store s2'))"

4340 proof -

4341 note avar = \<open>(v, s2') = avar G i a s2\<close>

4342 from AVar.prems obtain E1 where

4343 da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and

4344 da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"

4345 by (elim da_elim_cases)

4346 from AVar.prems obtain e1T e2T where

4347 wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and

4348 wt_e2: "Env\<turnstile>e2\<Colon>-e2T"

4349 by (elim wt_elim_cases)

4350 from avar normal_s2'

4351 have normal_s2: "normal s2"

4352 by (cases s2) (simp add: avar_def2)

4353 hence "normal s1"

4354 by - (rule eval_no_abrupt_lemma [rule_format], rule AVar, rule normal_s2)

4355 moreover note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1\<close>

4356 ultimately have "nrm E1 \<subseteq> dom (locals (store s1))"

4357 using da_e1 wt_e1 G by simp

4358 with da_e2 obtain A' where

4359 da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and

4360 nrm_A_A': "nrm A \<subseteq> nrm A'"

4361 by (rule da_weakenE) iprover

4362 note \<open>PROP ?Hyp (In1l e2) s1 s2\<close>

4363 with da_e2' wt_e2 G normal_s2

4364 have "nrm A' \<subseteq> dom (locals (store s2))"

4365 by simp

4366 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4367 by blast

4368 also have "\<dots> \<subseteq> dom (locals (store s2'))"

4369 proof -

4370 from avar have "s2' = snd (avar G i a s2)"

4371 by (cases "(avar G i a s2)") simp

4372 thus "dom (locals (store s2)) \<subseteq> dom (locals (store s2'))"

4373 by (simp) (rule dom_locals_avar_mono)

4374 qed

4375 finally show ?thesis .

4376 qed

4377 qed

4378 moreover

4379 {

4380 fix j have "abrupt s2' \<noteq> Some (Jump j)"

4381 proof -

4382 obtain w upd where v: "(w,upd)=v"

4383 by (cases v) auto

4384 have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"

4385 unfolding G v by (rule eval.AVar AVar.hyps)+

4386 from AVar.prems

4387 obtain T' where "T=Inl T'"

4388 by (elim wt_elim_cases) simp

4389 with AVar.prems have "Env\<turnstile>(e1.[e2])\<Colon>=T'"

4390 by simp

4391 from eval _ this

4392 show ?thesis

4393 by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)

4394 qed

4395 }

4396 hence "?BreakAssigned (Norm s0) s2' A" and "?ResAssigned (Norm s0) s2'"

4397 by simp_all

4398 ultimately show ?case by (intro conjI)

4399 next

4400 case (Nil s0 Env T A)

4401 from Nil.prems

4402 have "nrm A = dom (locals (store ((Norm s0)::state)))"

4403 by (elim da_elim_cases) simp

4404 thus ?case by simp

4405 next

4406 case (Cons s0 e v s1 es vs s2 Env T A)

4407 note G = \<open>prg Env = G\<close>

4408 have "?NormalAssigned s2 A"

4409 proof

4410 assume normal_s2: "normal s2"

4411 show "nrm A \<subseteq> dom (locals (store s2))"

4412 proof -

4413 from Cons.prems obtain E where

4414 da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

4415 da_es: "Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A"

4416 by (elim da_elim_cases)

4417 from Cons.prems obtain eT esT where

4418 wt_e: "Env\<turnstile>e\<Colon>-eT" and

4419 wt_es: "Env\<turnstile>es\<Colon>\<doteq>esT"

4420 by (elim wt_elim_cases)

4421 have "normal s1"

4422 by - (rule eval_no_abrupt_lemma [rule_format], rule Cons.hyps, rule normal_s2)

4423 moreover note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>

4424 ultimately have "nrm E \<subseteq> dom (locals (store s1))"

4425 using da_e wt_e G by simp

4426 with da_es obtain A' where

4427 da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and

4428 nrm_A_A': "nrm A \<subseteq> nrm A'"

4429 by (rule da_weakenE) iprover

4430 note \<open>PROP ?Hyp (In3 es) s1 s2\<close>

4431 with da_es' wt_es G normal_s2

4432 have "nrm A' \<subseteq> dom (locals (store s2))"

4433 by simp

4434 with nrm_A_A' show "nrm A \<subseteq> dom (locals (store s2))"

4435 by blast

4436 qed

4437 qed

4438 moreover

4439 {

4440 fix j have "abrupt s2 \<noteq> Some (Jump j)"

4441 proof -

4442 have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"

4443 unfolding G by (rule eval.Cons Cons.hyps)+

4444 from Cons.prems

4445 obtain T' where "T=Inr T'"

4446 by (elim wt_elim_cases) simp

4447 with Cons.prems have "Env\<turnstile>(e # es)\<Colon>\<doteq>T'"

4448 by simp

4449 from eval _ this

4450 show ?thesis

4451 by (rule eval_expression_list_no_jump) (simp_all add: G wf)

4452 qed

4453 }

4454 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

4455 by simp_all

4456 ultimately show ?case by (intro conjI)

4457 qed

4458 qed

4460 lemma da_good_approxE:

4461 assumes

4462 "prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" and "Env\<turnstile>t\<Colon>T" and

4463 "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" and "wf_prog (prg Env)"

4464 obtains

4465 "normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1))" and

4466 "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>

4467 \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and

4468 "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>\<Longrightarrow>Result \<in> dom (locals (store s1))"

4469 using assms by - (drule (3) da_good_approx, simp)

4472 (* Same as above but with explicit environment;

4473 It would be nicer to find a "normalized" way to right down those things

4474 in Bali.

4475 *)

4476 lemma da_good_approxE':

4477 assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"

4478 and wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T"

4479 and da: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"

4480 and wf: "wf_prog G"

4481 obtains "normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1))" and

4482 "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>

4483 \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and

4484 "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>

4485 \<Longrightarrow> Result \<in> dom (locals (store s1))"

4486 proof -

4487 from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" by simp

4488 moreover note wt da

4489 moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp

4490 ultimately show thesis

4491 using that by (rule da_good_approxE) iprover+

4492 qed

4494 declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]

4496 end