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

src/HOL/Bali/DefiniteAssignmentCorrect.thy

author | nipkow |

Sat Feb 08 14:46:22 2003 +0100 (2003-02-08) | |

changeset 13811 | f39f67982854 |

parent 13690 | ac335b2f4a39 |

child 14030 | cd928c0ac225 |

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

adjusted dom rules

1 header {* Correctness of Definite Assignment *}

3 theory DefiniteAssignmentCorrect = WellForm + Eval:

5 ML {*

6 Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]

7 *}

9 lemma sxalloc_no_jump:

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

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

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

13 using sxalloc no_jmp

14 by cases simp_all

16 lemma sxalloc_no_jump':

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

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

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

20 using sxalloc jump

21 by cases simp_all

23 lemma halloc_no_jump:

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

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

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

27 using halloc no_jmp

28 by cases simp_all

30 lemma halloc_no_jump':

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

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

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

34 using halloc jump

35 by cases simp_all

37 lemma Body_no_jump:

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

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

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

41 proof (cases "normal s0")

42 case True

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

44 s0: "s0 = Norm s0'"

45 by (cases s0) simp

46 from eval' obtain s2 where

47 s1: "s1 = abupd (absorb Ret)

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

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

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

51 by cases simp

52 show ?thesis

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

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

55 case True

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

57 by (cases s2) simp

58 thus ?thesis by simp

59 next

60 case False

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

62 by simp

63 with False show ?thesis

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

65 qed

66 next

67 case False

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

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

70 by (cases s0) fastsimp

71 with this jump

72 show ?thesis

73 by (cases) (simp)

74 qed

76 lemma Methd_no_jump:

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

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

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

80 proof (cases "normal s0")

81 case True

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

83 "s0 = Norm s0'"

84 by (cases s0) simp

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

86 by (cases) (simp add: body_def2)

87 from this jump

88 show ?thesis

89 by (rule Body_no_jump)

90 next

91 case False

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

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

94 by (cases s0) fastsimp

95 with this jump

96 show ?thesis

97 by (cases) (simp)

98 qed

100 lemma jumpNestingOkS_mono:

101 assumes jumpNestingOk_l': "jumpNestingOkS jmps' c"

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

103 shows "jumpNestingOkS jmps c"

104 proof -

105 have True and True and

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

107 and True

108 proof (induct rule: var_expr_stmt.induct)

109 case (Lab j c jmps' jmps)

110 have jmpOk: "jumpNestingOkS jmps' (j\<bullet> c)" .

111 have jmps: "jmps' \<subseteq> jmps" .

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

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

114 ultimately

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

116 by (rule Lab.hyps)

117 thus ?case

118 by simp

119 next

120 case (Jmp j jmps' jmps)

121 thus ?case

122 by (cases j) auto

123 next

124 case (Comp c1 c2 jmps' jmps)

125 from Comp.prems

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

127 moreover from Comp.prems

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

129 ultimately show ?case

130 by simp

131 next

132 case (If_ e c1 c2 jmps' jmps)

133 from If_.prems

134 have "jumpNestingOkS jmps c1" by - (rule If_.hyps,auto)

135 moreover from If_.prems

136 have "jumpNestingOkS jmps c2" by - (rule If_.hyps,auto)

137 ultimately show ?case

138 by simp

139 next

140 case (Loop l e c jmps' jmps)

141 have "jumpNestingOkS jmps' (l\<bullet> While(e) c)" .

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

143 moreover have "jmps' \<subseteq> jmps" .

144 hence "{Cont l} \<union> jmps' \<subseteq> {Cont l} \<union> jmps" by auto

145 ultimately

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

147 by (rule Loop.hyps)

148 thus ?case by simp

149 next

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

151 from TryC.prems

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

153 moreover from TryC.prems

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

155 ultimately show ?case

156 by simp

157 next

158 case (Fin c1 c2 jmps' jmps)

159 from Fin.prems

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

161 moreover from Fin.prems

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

163 ultimately show ?case

164 by simp

165 qed (simp_all)

166 with jumpNestingOk_l' subset

167 show ?thesis

168 by rules

169 qed

171 corollary jumpNestingOk_mono:

172 assumes jmpOk: "jumpNestingOk jmps' t"

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

174 shows "jumpNestingOk jmps t"

175 proof (cases t)

176 case (In1 expr_stmt)

177 show ?thesis

178 proof (cases expr_stmt)

179 case (Inl e)

180 with In1 show ?thesis by simp

181 next

182 case (Inr s)

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

184 qed

185 qed (simp_all)

187 lemma assign_abrupt_propagation:

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

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

190 shows "abrupt s = x"

191 proof (cases x)

192 case None

193 with ass show ?thesis

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

195 next

196 case (Some xcpt)

197 from f_ok

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

199 by (cases "f n s")

200 with Some ass f_ok show ?thesis

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

202 qed

204 lemma wt_init_comp_ty':

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

206 apply (unfold init_comp_ty_def)

207 apply (clarsimp simp add: accessible_in_RefT_simp

208 is_acc_type_def is_acc_class_def)

209 done

211 lemma fvar_upd_no_jump:

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

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

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

215 proof (cases "stat")

216 case True

217 with noJmp upd

218 show ?thesis

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

220 next

221 case False

222 with noJmp upd

223 show ?thesis

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

225 qed

228 lemma avar_state_no_jump:

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

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

231 proof (cases "normal s")

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

233 next

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

235 qed

237 lemma avar_upd_no_jump:

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

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

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

241 using upd noJmp

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

245 text {*

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

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

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

249 cant leave its enclosing method.

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

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

252 and returns) are nested

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

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

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

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

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

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

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

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

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

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

264 proof, we can't just

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

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

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

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

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

271 *}

272 theorem jumpNestingOk_eval:

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

274 and jmpOk: "jumpNestingOk jmps t"

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

276 and wf: "wf_prog G"

277 and G: "prg Env = G"

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

279 (is "?Jmp jmps s0")

280 shows "?Jmp jmps s1 \<and>

281 (normal s1 \<longrightarrow>

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

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

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

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

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

287 proof -

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

289 (\<forall> jmps T Env.

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

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

292 -- {* Variable @{text ?HypObj} is the following goal spelled in terms of

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

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

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

296 logic. See for example the case for the loop. *}

297 from eval

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

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

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

301 -- {* We need to abstract over @{term jmps} since @{term jmps} are extended

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

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

304 typing judgements. *}

305 proof (induct)

306 case Abrupt thus ?case by simp

307 next

308 case Skip thus ?case by simp

309 next

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

311 next

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

313 have jmpOK: "jumpNestingOk jmps (In1r (jmp\<bullet> c))" .

314 have G: "prg Env = G" .

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

316 using Lab.prems by (elim wt_elim_cases)

317 {

318 fix j

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

320 have "j\<in>jmps"

321 proof -

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

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

324 have hyp_c: "PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>" .

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

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

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

328 proof -

329 from jmpOK

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

331 with wt_c jmp_s1 G hyp_c

332 show ?thesis

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

334 qed

335 ultimately show ?thesis

336 by simp

337 qed

338 }

339 thus ?case by simp

340 next

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

342 have jmpOk: "jumpNestingOk jmps (In1r (c1;; c2))" .

343 have G: "prg Env = G" .

344 from Comp.prems obtain

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

346 by (elim wt_elim_cases)

347 {

348 fix j

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

350 have "j\<in>jmps"

351 proof -

352 have jmp: "?Jmp jmps s1"

353 proof -

354 have hyp_c1: "PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>" .

355 with wt_c1 jmpOk G

356 show ?thesis by simp

357 qed

358 moreover have hyp_c2: "PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)" .

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

360 moreover note wt_c2 G abr_s2

361 ultimately show "j \<in> jmps"

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

363 qed

364 } thus ?case by simp

365 next

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

367 have jmpOk: "jumpNestingOk jmps (In1r (If(e) c1 Else c2))" .

368 have G: "prg Env = G" .

369 from If.prems obtain

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

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

372 by (elim wt_elim_cases) simp

373 {

374 fix j

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

376 have "j\<in>jmps"

377 proof -

378 have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)" .

379 with wt_e G have "?Jmp jmps s1"

380 by simp

381 moreover have hyp_then_else:

382 "PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>" .

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

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

385 moreover note wt_then_else G jmp

386 ultimately show "j\<in> jmps"

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

388 qed

389 }

390 thus ?case by simp

391 next

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

393 have jmpOk: "jumpNestingOk jmps (In1r (l\<bullet> While(e) c))" .

394 have G: "prg Env = G" .

395 have wt: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .

396 then obtain

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

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

399 by (elim wt_elim_cases)

400 {

401 fix j

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

403 have "j\<in>jmps"

404 proof -

405 have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)" .

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

407 by simp

408 show ?thesis

409 proof (cases "the_Bool b")

410 case False

411 from Loop.hyps

412 have "s3=s1"

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

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

415 thus ?thesis by simp

416 next

417 case True

418 from Loop.hyps

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

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

421 leaves the hypothesis in object logic *)

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

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

424 apply (erule conjE)+

425 apply assumption

426 done

427 note hyp_c = this [rule_format (no_asm)]

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

429 by simp

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

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

432 using wt_c G by rules

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

434 proof -

435 {

436 fix j'

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

438 have "j' \<in> jmps"

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

440 case True

441 with abs show ?thesis

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

443 next

444 case False

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

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

447 with jmp_s2 False show ?thesis

448 by simp

449 qed

450 }

451 thus ?thesis by simp

452 qed

453 moreover

454 from Loop.hyps

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

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

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

458 apply (erule conjE)+

459 apply assumption

460 done

461 note hyp_w = this [rule_format (no_asm)]

462 note jmpOk wt G jmp

463 ultimately show "j\<in> jmps"

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

465 qed

466 qed

467 }

468 thus ?case by simp

469 next

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

471 next

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

473 have jmpOk: "jumpNestingOk jmps (In1r (Throw e))" .

474 have G: "prg Env = G" .

475 from Throw.prems obtain Te where

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

477 by (elim wt_elim_cases)

478 {

479 fix j

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

481 have "j\<in>jmps"

482 proof -

483 have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)" .

484 hence "?Jmp jmps s1" using wt_e G by simp

485 moreover

486 from jmp

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

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

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

490 qed

491 }

492 thus ?case by simp

493 next

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

495 have jmpOk: "jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))" .

496 have G: "prg Env = G" .

497 from Try.prems obtain

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

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

500 by (elim wt_elim_cases)

501 {

502 fix j

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

504 have "j\<in>jmps"

505 proof -

506 have "PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)" .

507 with jmpOk wt_c1 G

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

509 have s2: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .

510 show "j \<in> jmps"

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

512 case False

513 from Try.hyps have "s3=s2"

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

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

516 using sxalloc_no_jump' [OF s2] by simp

517 with jmp_s1

518 show ?thesis by simp

519 next

520 case True

521 with Try.hyps

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

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

524 apply (erule conjE)+

525 apply assumption

526 done

527 note hyp_c2 = this [rule_format (no_asm)]

528 from jmp_s1 sxalloc_no_jump' [OF s2]

529 have "?Jmp jmps s2"

530 by simp

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

532 by (cases s2) simp

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

534 moreover note wt_c2

535 moreover from G

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

537 by simp

538 moreover note jmp

539 ultimately show ?thesis

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

541 qed

542 qed

543 }

544 thus ?case by simp

545 next

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

547 have jmpOk: " jumpNestingOk jmps (In1r (c1 Finally c2))" .

548 have G: "prg Env = G" .

549 from Fin.prems obtain

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

551 by (elim wt_elim_cases)

552 {

553 fix j

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

555 have "j \<in> jmps"

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

557 case True

558 have hyp_c1: "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>" .

559 with True jmpOk wt_c1 G show ?thesis

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

561 next

562 case False

563 have hyp_c2: "PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>" .

564 have "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)

565 else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .

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

567 by (cases s2, simp add: abrupt_if_def)

568 with jmpOk wt_c2 G show ?thesis

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

570 qed

571 }

572 thus ?case by simp

573 next

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

575 have "jumpNestingOk jmps (In1r (Init C))".

576 have G: "prg Env = G" .

577 have "the (class G C) = c" .

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

579 by (elim wt_elim_cases) auto

580 {

581 fix j

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

583 have "j\<in>jmps"

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

585 case True

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

587 by simp

588 with jmp

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

590 next

591 case False

592 from wf c G

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

594 by (simp add: wf_prog_cdecl)

595 from Init.hyps

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

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

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

599 apply (erule conjE)+

600 apply assumption

601 done

602 note hyp_s1 = this [rule_format (no_asm)]

603 from wf_cdecl G have

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

605 by (cases "C=Object")

606 (auto dest: wf_cdecl_supD is_acc_classD)

607 from hyp_s1 [OF _ _ wt_super G]

608 have "?Jmp jmps s1"

609 by simp

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

611 from False Init.hyps

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

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

614 apply (erule conjE)+

615 apply assumption

616 done

617 note hyp_init_c = this [rule_format (no_asm)]

618 from wf_cdecl

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

620 by (rule wf_cdecl_wt_init)

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

622 by (cases rule: wf_cdeclE)

623 hence "jumpNestingOkS jmps (init c)"

624 by (rule jumpNestingOkS_mono) simp

625 moreover

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

627 proof -

628 from False Init.hyps

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

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

631 qed

632 ultimately show ?thesis

633 using hyp_init_c [OF jmp_s1 _ wt_init_c]

634 by simp

635 qed

636 }

637 thus ?case by simp

638 next

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

640 {

641 fix j

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

643 have "j\<in>jmps"

644 proof -

645 have "prg Env = G" .

646 moreover have hyp_init: "PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>" .

647 moreover from wf NewC.prems

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

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

650 moreover

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

652 proof -

653 have "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .

654 from this jmp show ?thesis

655 by (rule halloc_no_jump')

656 qed

657 ultimately show "j \<in> jmps"

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

659 qed

660 }

661 thus ?case by simp

662 next

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

664 {

665 fix j

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

667 have "j\<in>jmps"

668 proof -

669 have G: "prg Env = G" .

670 from NewA.prems

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

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

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

674 have "PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>" .

675 with wt_init G

676 have "?Jmp jmps s1"

677 by (simp add: init_comp_ty_def)

678 moreover

679 have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 i)" .

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

681 proof -

682 have "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".

683 moreover note jmp

684 ultimately

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

686 by (rule halloc_no_jump')

687 thus ?thesis by (cases s2) auto

688 qed

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

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

691 qed

692 }

693 thus ?case by simp

694 next

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

696 {

697 fix j

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

699 have "j\<in>jmps"

700 proof -

701 have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .

702 have "prg Env = G" .

703 moreover from Cast.prems

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

705 moreover

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

707 proof -

708 have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .

709 moreover note jmp

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

711 qed

712 ultimately show ?thesis

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

714 qed

715 }

716 thus ?case by simp

717 next

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

719 {

720 fix j

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

722 have "j\<in>jmps"

723 proof -

724 have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .

725 have "prg Env = G" .

726 moreover from Inst.prems

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

728 moreover note jmp

729 ultimately show "j\<in>jmps"

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

731 qed

732 }

733 thus ?case by simp

734 next

735 case Lit thus ?case by simp

736 next

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

738 {

739 fix j

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

741 have "j\<in>jmps"

742 proof -

743 have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .

744 have "prg Env = G" .

745 moreover from UnOp.prems

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

747 moreover note jmp

748 ultimately show "j\<in>jmps"

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

750 qed

751 }

752 thus ?case by simp

753 next

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

755 {

756 fix j

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

758 have "j\<in>jmps"

759 proof -

760 have G: "prg Env = G" .

761 from BinOp.prems

762 obtain e1T e2T where

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

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

765 by (elim wt_elim_cases)

766 have "PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)" .

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

768 have hyp_e2:

769 "PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)

770 s1 s2 (In1 v2)" .

771 show "j\<in>jmps"

772 proof (cases "need_second_arg binop v1")

773 case True with jmp_s1 wt_e2 jmp G

774 show ?thesis

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

776 next

777 case False with jmp_s1 jmp G

778 show ?thesis

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

780 qed

781 qed

782 }

783 thus ?case by simp

784 next

785 case Super thus ?case by simp

786 next

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

788 {

789 fix j

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

791 have "j\<in>jmps"

792 proof -

793 have hyp_va: "PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))" .

794 have "prg Env = G" .

795 moreover from Acc.prems

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

797 moreover note jmp

798 ultimately show "j\<in>jmps"

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

800 qed

801 }

802 thus ?case by simp

803 next

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

805 have G: "prg Env = G" .

806 from Ass.prems

807 obtain vT eT where

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

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

810 by (elim wt_elim_cases)

811 have hyp_v: "PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))" .

812 have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 v)" .

813 {

814 fix j

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

816 have "j\<in>jmps"

817 proof -

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

819 proof (cases "normal s2")

820 case True

821 have "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .

822 from this True have nrm_s1: "normal s1"

823 by (rule eval_no_abrupt_lemma [rule_format])

824 with nrm_s1 wt_va G True

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

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

827 by simp

828 from this jmp

829 show ?thesis

830 by (rule assign_abrupt_propagation)

831 next

832 case False with jmp

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

834 qed

835 moreover from wt_va G

836 have "?Jmp jmps s1"

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

838 ultimately show ?thesis using G

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

840 qed

841 }

842 thus ?case by simp

843 next

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

845 have G: "prg Env = G" .

846 have hyp_e0: "PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)" .

847 have hyp_e1_e2: "PROP ?Hyp (In1l (if the_Bool b then e1 else e2))

848 s1 s2 (In1 v)" .

849 from Cond.prems

850 obtain e1T e2T

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

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

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

854 by (elim wt_elim_cases)

855 {

856 fix j

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

858 have "j\<in>jmps"

859 proof -

860 from wt_e0 G

861 have jmp_s1: "?Jmp jmps s1"

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

863 show ?thesis

864 proof (cases "the_Bool b")

865 case True

866 with jmp_s1 wt_e1 G jmp

867 show ?thesis

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

869 next

870 case False

871 with jmp_s1 wt_e2 G jmp

872 show ?thesis

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

874 qed

875 qed

876 }

877 thus ?case by simp

878 next

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

880 jmps T Env)

881 have G: "prg Env = G" .

882 from Call.prems

883 obtain eT argsT

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

885 by (elim wt_elim_cases)

886 {

887 fix j

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

889 = Some (Jump j)"

890 have "j\<in>jmps"

891 proof -

892 have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)" .

893 from wt_e G

894 have jmp_s1: "?Jmp jmps s1"

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

896 have hyp_args: "PROP ?Hyp (In3 args) s1 s2 (In3 vs)" .

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

898 proof -

899 have "G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4" .

900 moreover

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

902 by (cases s4) simp

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

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

905 moreover have "s3' = check_method_access G accC statT mode

906 \<lparr>name = mn, parTs = pTs\<rparr> a s3" .

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

908 by (cases s3)

909 (simp add: check_method_access_def abrupt_if_def Let_def)

910 moreover

911 have "s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2" .

912 ultimately show ?thesis

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

914 qed

915 with jmp_s1 wt_args G

916 show ?thesis

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

918 qed

919 }

920 thus ?case by simp

921 next

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

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

924 by (rule eval.Methd)

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

926 by (rule Methd_no_jump) simp

927 thus ?case by simp

928 next

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

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

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

932 by (rule eval.Body)

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

934 by (rule Body_no_jump) simp

935 thus ?case by simp

936 next

937 case LVar

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

939 next

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

941 have G: "prg Env = G" .

942 from wf FVar.prems

943 obtain statC f where

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

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

946 by (elim wt_elim_cases) simp

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

948 proof -

949 from wf wt_e G

950 have "is_class (prg Env) statC"

951 by (auto dest: ty_expr_is_type type_is_class)

952 with wf accfield G

953 have "is_class (prg Env) statDeclC"

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

955 thus ?thesis

956 by simp

957 qed

958 have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .

959 {

960 fix j

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

962 have "j\<in>jmps"

963 proof -

964 have hyp_init: "PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>" .

965 from G wt_init

966 have "?Jmp jmps s1"

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

968 moreover

969 have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 a)" .

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

971 proof -

972 have "s3 = check_field_access G accC statDeclC fn stat a s2'" .

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

974 by (cases s2')

975 (simp add: check_field_access_def abrupt_if_def Let_def)

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

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

978 qed

979 ultimately show ?thesis

980 using G wt_e

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

982 qed

983 }

984 moreover

985 from fvar obtain upd w

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

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

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

989 {

990 fix j val fix s::state

991 assume "normal s3"

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

993 with upd

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

995 by (rule fvar_upd_no_jump)

996 }

997 ultimately show ?case using v by simp

998 next

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

1000 have G: "prg Env = G" .

1001 from AVar.prems

1002 obtain e1T e2T where

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

1004 by (elim wt_elim_cases) simp

1005 have avar: "(v, s2') = avar G i a s2" .

1006 {

1007 fix j

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

1009 have "j\<in>jmps"

1010 proof -

1011 have hyp_e1: "PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)" .

1012 from G wt_e1

1013 have "?Jmp jmps s1"

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

1015 moreover

1016 have hyp_e2: "PROP ?Hyp (In1l e2) s1 s2 (In1 i)" .

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

1018 proof -

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

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

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

1022 qed

1023 ultimately show ?thesis

1024 using wt_e2 G

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

1026 qed

1027 }

1028 moreover

1029 from avar obtain upd w

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

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

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

1033 {

1034 fix j val fix s::state

1035 assume "normal s2'"

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

1037 with upd

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

1039 by (rule avar_upd_no_jump)

1040 }

1041 ultimately show ?case using v by simp

1042 next

1043 case Nil thus ?case by simp

1044 next

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

1046 have G: "prg Env = G" .

1047 from Cons.prems obtain eT esT

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

1049 by (elim wt_elim_cases) simp

1050 {

1051 fix j

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

1053 have "j\<in>jmps"

1054 proof -

1055 have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .

1056 from G wt_e

1057 have "?Jmp jmps s1"

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

1059 moreover

1060 have hyp_es: "PROP ?Hyp (In3 es) s1 s2 (In3 vs)" .

1061 ultimately show ?thesis

1062 using wt_e2 G jmp

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

1064 (assumption|simp (no_asm_simp))+)

1065 qed

1066 }

1067 thus ?case by simp

1068 qed

1069 note generalized = this

1070 from no_jmp jmpOk wt G

1071 show ?thesis

1072 by (rule generalized)

1073 qed

1075 lemmas jumpNestingOk_evalE = jumpNestingOk_eval [THEN conjE,rule_format]

1078 lemma jumpNestingOk_eval_no_jump:

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

1080 jmpOk: "jumpNestingOk {} t" and

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

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

1083 wf: "wf_prog (prg Env)"

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

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

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

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

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

1089 case True

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

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

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

1093 with no_jmp jmp show ?thesis by simp

1094 next

1095 case False

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

1097 by (cases Env) simp

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

1099 moreover note jmpOk wt

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

1101 moreover note G

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

1103 by simp

1104 ultimately show ?thesis

1105 apply (rule jumpNestingOk_evalE)

1106 apply assumption

1107 apply simp

1108 apply fastsimp

1109 done

1110 qed

1112 lemmas jumpNestingOk_eval_no_jumpE

1113 = jumpNestingOk_eval_no_jump [THEN conjE,rule_format]

1115 corollary eval_expression_no_jump:

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

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

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

1119 wf: "wf_prog (prg Env)"

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

1121 using eval _ no_jmp wt wf

1122 by (rule jumpNestingOk_eval_no_jumpE, simp_all)

1124 corollary eval_var_no_jump:

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

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

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

1128 wf: "wf_prog (prg Env)"

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

1130 (normal s1 \<longrightarrow>

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

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

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

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

1135 by simp_all

1137 lemmas eval_var_no_jumpE = eval_var_no_jump [THEN conjE,rule_format]

1139 corollary eval_statement_no_jump:

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

1141 jmpOk: "jumpNestingOkS {} c" and

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

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

1144 wf: "wf_prog (prg Env)"

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

1146 using eval _ no_jmp wt wf

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

1149 corollary eval_expression_list_no_jump:

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

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

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

1153 wf: "wf_prog (prg Env)"

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

1155 using eval _ no_jmp wt wf

1156 by (rule jumpNestingOk_eval_no_jumpE, simp_all)

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

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

1160 by blast

1162 lemma dom_locals_halloc_mono:

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

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

1165 proof -

1166 from halloc show ?thesis

1167 by cases simp_all

1168 qed

1170 lemma dom_locals_sxalloc_mono:

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

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

1173 proof -

1174 from sxalloc show ?thesis

1175 proof (cases)

1176 case Norm thus ?thesis by simp

1177 next

1178 case Jmp thus ?thesis by simp

1179 next

1180 case Error thus ?thesis by simp

1181 next

1182 case XcptL thus ?thesis by simp

1183 next

1184 case SXcpt thus ?thesis

1185 by - (drule dom_locals_halloc_mono,simp)

1186 qed

1187 qed

1190 lemma dom_locals_assign_mono:

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

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

1193 proof (cases "normal s")

1194 case False thus ?thesis

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

1196 next

1197 case True

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

1199 by auto

1200 moreover

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

1202 by (cases "f n s", simp)

1203 ultimately

1204 show ?thesis

1205 using f_ok

1206 by (simp add: assign_def Let_def)

1207 qed

1209 (*

1210 lemma dom_locals_init_lvars_mono:

1211 "dom (locals (store s))

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

1213 proof (cases "mode = Static")

1214 case True

1215 thus ?thesis

1216 apply (cases s)

1217 apply (simp add: init_lvars_def Let_def)

1218 *)

1220 lemma dom_locals_lvar_mono:

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

1222 by (simp add: lvar_def) blast

1225 lemma dom_locals_fvar_vvar_mono:

1226 "dom (locals (store s))

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

1228 proof (cases stat)

1229 case True

1230 thus ?thesis

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

1232 next

1233 case False

1234 thus ?thesis

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

1236 qed

1238 lemma dom_locals_fvar_mono:

1239 "dom (locals (store s))

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

1241 proof (cases stat)

1242 case True

1243 thus ?thesis

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

1245 next

1246 case False

1247 thus ?thesis

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

1249 qed

1252 lemma dom_locals_avar_vvar_mono:

1253 "dom (locals (store s))

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

1255 by (cases s, simp add: avar_def2)

1257 lemma dom_locals_avar_mono:

1258 "dom (locals (store s))

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

1260 by (cases s, simp add: avar_def2)

1262 text {*

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

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

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

1266 complicated second part of the conjunction in the goal.

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

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

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

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

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

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

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

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

1275 two different rules to handle array reads and updates *}

1276 lemma dom_locals_eval_mono:

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

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

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

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

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

1282 proof -

1283 from eval show ?thesis

1284 proof (induct)

1285 case Abrupt thus ?case by simp

1286 next

1287 case Skip thus ?case by simp

1288 next

1289 case Expr thus ?case by simp

1290 next

1291 case Lab thus ?case by simp

1292 next

1293 case (Comp c1 c2 s0 s1 s2)

1294 from Comp.hyps

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

1296 by simp

1297 also

1298 from Comp.hyps

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

1300 by simp

1301 finally show ?case by simp

1302 next

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

1304 from If.hyps

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

1306 by simp

1307 also

1308 from If.hyps

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

1310 by simp

1311 finally show ?case by simp

1312 next

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

1314 show ?case

1315 proof (cases "the_Bool b")

1316 case True

1317 with Loop.hyps

1318 obtain

1319 s0_s1:

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

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

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

1323 by simp

1324 note s0_s1 also note s1_s2 also note s2_s3

1325 finally show ?thesis

1326 by simp

1327 next

1328 case False

1329 with Loop.hyps show ?thesis

1330 by simp

1331 qed

1332 next

1333 case Jmp thus ?case by simp

1334 next

1335 case Throw thus ?case by simp

1336 next

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

1338 then

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

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

1341 have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .

1342 hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"

1343 by (rule dom_locals_sxalloc_mono)

1344 thus ?case

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

1346 case True

1347 note s0_s1 also note s1_s2

1348 also

1349 from True Try.hyps

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

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

1352 by simp

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

1354 by (cases s2, simp )

1355 finally show ?thesis by simp

1356 next

1357 case False

1358 note s0_s1 also note s1_s2

1359 finally

1360 show ?thesis

1361 using False Try.hyps by simp

1362 qed

1363 next

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

1365 show ?case

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

1367 case True

1368 with Fin.hyps show ?thesis

1369 by simp

1370 next

1371 case False

1372 from Fin.hyps

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

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

1375 by simp

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

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

1378 by simp

1379 also

1380 from Fin.hyps

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

1382 by simp

1383 finally show ?thesis

1384 using Fin.hyps by simp

1385 qed

1386 next

1387 case (Init C c s0 s1 s2 s3)

1388 show ?case

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

1390 case True

1391 with Init.hyps show ?thesis by simp

1392 next

1393 case False

1394 with Init.hyps

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

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

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

1398 by simp

1399 from s0_s1

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

1401 by (cases s0) simp

1402 with s3

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

1404 by (cases s2) simp

1405 thus ?thesis by simp

1406 qed

1407 next

1408 case (NewC C a s0 s1 s2)

1409 have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .

1410 from NewC.hyps

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

1412 by simp

1413 also

1414 from halloc

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

1416 finally show ?case by simp

1417 next

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

1419 have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .

1420 from NewA.hyps

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

1422 by simp

1423 also

1424 from NewA.hyps

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

1426 also

1427 from halloc

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

1429 by (rule dom_locals_halloc_mono [elim_format]) simp

1430 finally show ?case by simp

1431 next

1432 case Cast thus ?case by simp

1433 next

1434 case Inst thus ?case by simp

1435 next

1436 case Lit thus ?case by simp

1437 next

1438 case UnOp thus ?case by simp

1439 next

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

1441 from BinOp.hyps

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

1443 by simp

1444 also

1445 from BinOp.hyps

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

1447 finally show ?case by simp

1448 next

1449 case Super thus ?case by simp

1450 next

1451 case Acc thus ?case by simp

1452 next

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

1454 from Ass.hyps

1455 have s0_s1:

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

1457 by simp

1458 show ?case

1459 proof (cases "normal s1")

1460 case True

1461 with Ass.hyps

1462 have ass_ok:

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

1464 by simp

1465 note s0_s1

1466 also

1467 from Ass.hyps

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

1469 by simp

1470 also

1471 from ass_ok

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

1473 by (rule dom_locals_assign_mono)

1474 finally show ?thesis by simp

1475 next

1476 case False

1477 have "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .

1478 with False

1479 have "s2=s1"

1480 by auto

1481 with s0_s1 False

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

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

1484 by simp

1485 thus ?thesis

1486 by simp

1487 qed

1488 next

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

1490 from Cond.hyps

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

1492 by simp

1493 also

1494 from Cond.hyps

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

1496 by simp

1497 finally show ?case by simp

1498 next

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

1500 have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .

1501 from Call.hyps

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

1503 by simp

1504 also

1505 from Call.hyps

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

1507 by simp

1508 also

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

1510 by (cases s4) simp

1511 finally show ?case by simp

1512 next

1513 case Methd thus ?case by simp

1514 next

1515 case (Body D c s0 s1 s2 s3)

1516 from Body.hyps

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

1518 by simp

1519 also

1520 from Body.hyps

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

1522 by simp

1523 also

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

1525 by simp

1526 also

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

1528 proof -

1529 have "s3 =

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

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

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

1533 thus ?thesis

1534 by simp

1535 qed

1536 finally show ?case by simp

1537 next

1538 case LVar

1539 thus ?case

1540 using dom_locals_lvar_mono

1541 by simp

1542 next

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

1544 from FVar.hyps

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

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

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

1548 from v

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

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

1551 by (simp add: dom_locals_fvar_vvar_mono)

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

1553 by - (intro strip, simp)

1554 have s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .

1555 from FVar.hyps

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

1557 by simp

1558 also

1559 from FVar.hyps

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

1561 by simp

1562 also

1563 from s2'

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

1565 by (simp add: dom_locals_fvar_mono)

1566 also

1567 from s3

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

1569 by (simp add: check_field_access_def Let_def)

1570 finally

1571 show ?case

1572 using v_ok

1573 by simp

1574 next

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

1576 from AVar.hyps

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

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

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

1580 from v

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

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

1583 by (simp add: dom_locals_avar_vvar_mono)

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

1585 by - (intro strip, simp)

1586 from AVar.hyps

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

1588 by simp

1589 also

1590 from AVar.hyps

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

1592 by simp

1593 also

1594 from s2'

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

1596 by (simp add: dom_locals_avar_mono)

1597 finally

1598 show ?case using v_ok by simp

1599 next

1600 case Nil thus ?case by simp

1601 next

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

1603 from Cons.hyps

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

1605 by simp

1606 also

1607 from Cons.hyps

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

1609 by simp

1610 finally show ?case by simp

1611 qed

1612 qed

1614 lemma dom_locals_eval_mono_elim [consumes 1]:

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

1616 hyps: "\<lbrakk>dom (locals (store s0)) \<subseteq> dom (locals (store s1));

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

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

1619 \<subseteq> dom (locals (store ((snd vv) val s)))\<rbrakk> \<Longrightarrow> P"

1620 shows "P"

1621 using eval

1622 proof (rule dom_locals_eval_mono [THEN conjE])

1623 qed (rule hyps,auto)

1625 lemma halloc_no_abrupt:

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

1627 normal: "normal s1"

1628 shows "normal s0"

1629 proof -

1630 from halloc normal show ?thesis

1631 by cases simp_all

1632 qed

1634 lemma sxalloc_mono_no_abrupt:

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

1636 normal: "normal s1"

1637 shows "normal s0"

1638 proof -

1639 from sxalloc normal show ?thesis

1640 by cases simp_all

1641 qed

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

1644 by blast

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

1647 by blast

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

1650 by blast

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

1653 by blast

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

1656 by blast

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

1659 by blast

1661 lemma assigns_good_approx:

1662 assumes

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

1664 normal: "normal s1"

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

1666 proof -

1667 from eval normal show ?thesis

1668 proof (induct)

1669 case Abrupt thus ?case by simp

1670 next -- {* For statements its trivial, since then @{term "assigns t = {}"} *}

1671 case Skip show ?case by simp

1672 next

1673 case Expr show ?case by simp

1674 next

1675 case Lab show ?case by simp

1676 next

1677 case Comp show ?case by simp

1678 next

1679 case If show ?case by simp

1680 next

1681 case Loop show ?case by simp

1682 next

1683 case Jmp show ?case by simp

1684 next

1685 case Throw show ?case by simp

1686 next

1687 case Try show ?case by simp

1688 next

1689 case Fin show ?case by simp

1690 next

1691 case Init show ?case by simp

1692 next

1693 case NewC show ?case by simp

1694 next

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

1696 have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .

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

1698 proof -

1699 from NewA

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

1701 by - (erule halloc_no_abrupt [rule_format])

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

1703 with NewA.hyps

1704 show ?thesis by rules

1705 qed

1706 also

1707 from halloc

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

1709 by (rule dom_locals_halloc_mono [elim_format]) simp

1710 finally show ?case by simp

1711 next

1712 case (Cast T e s0 s1 s2 v)

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

1714 with Cast.hyps

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

1716 by simp

1717 also

1718 from Cast.hyps

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

1720 by simp

1721 finally

1722 show ?case

1723 by simp

1724 next

1725 case Inst thus ?case by simp

1726 next

1727 case Lit thus ?case by simp

1728 next

1729 case UnOp thus ?case by simp

1730 next

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

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

1733 with BinOp.hyps

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

1735 by rules

1736 also

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

1738 proof -

1739 have "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2

1740 else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .

1741 thus ?thesis

1742 by (rule dom_locals_eval_mono_elim)

1743 qed

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

1745 show ?case

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

1747 case True

1748 with s2 show ?thesis by simp

1749 next

1750 case False

1751 with BinOp

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

1753 by (simp add: need_second_arg_def)

1754 with s2

1755 show ?thesis using False by (simp add: Un_subset_iff)

1756 qed

1757 next

1758 case Super thus ?case by simp

1759 next

1760 case Acc thus ?case by simp

1761 next

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

1763 have nrm_ass_s2: "normal (assign f v s2)" .

1764 hence nrm_s2: "normal s2"

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

1766 with Ass.hyps

1767 have nrm_s1: "normal s1"

1768 by - (erule eval_no_abrupt_lemma [rule_format])

1769 with Ass.hyps

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

1771 by rules

1772 also

1773 from Ass.hyps

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

1775 by - (erule dom_locals_eval_mono_elim)

1776 also

1777 from nrm_s2 Ass.hyps

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

1779 by rules

1780 ultimately

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

1782 by (rule Un_least)

1783 also

1784 from Ass.hyps nrm_s1

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

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

1787 then

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

1789 by (rule dom_locals_assign_mono)

1790 finally

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

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

1793 show ?case

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

1795 case False

1796 with va_e show ?thesis

1797 by (simp add: Un_assoc)

1798 next

1799 case True

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

1801 by blast

1802 with Ass.hyps

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

1804 by simp

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

1806 by (rule eval_elim_cases) simp

1807 with nrm_ass_s2

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

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

1810 with va_e True va

1811 show ?thesis by (simp add: Un_assoc)

1812 qed

1813 next

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

1815 hence "normal s1"

1816 by - (erule eval_no_abrupt_lemma [rule_format])

1817 with Cond.hyps

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

1819 by rules

1820 also from Cond.hyps

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

1822 by - (erule dom_locals_eval_mono_elim)

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

1824 show ?case

1825 proof (cases "the_Bool b")

1826 case True

1827 with Cond

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

1829 by simp

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

1831 by blast

1832 with e0

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

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

1835 by (rule Un_least)

1836 thus ?thesis using True by simp

1837 next

1838 case False

1839 with Cond

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

1841 by simp

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

1843 by blast

1844 with e0

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

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

1847 by (rule Un_least)

1848 thus ?thesis using False by simp

1849 qed

1850 next

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

1852 have nrm_s2: "normal s2"

1853 proof -

1854 have "normal ((set_lvars (locals (snd s2))) s4)" .

1855 hence normal_s4: "normal s4" by simp

1856 hence "normal s3'" using Call.hyps

1857 by - (erule eval_no_abrupt_lemma [rule_format])

1858 moreover have

1859 "s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3".

1860 ultimately have "normal s3"

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

1862 moreover

1863 have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .

1864 ultimately show "normal s2"

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

1866 qed

1867 hence "normal s1" using Call.hyps

1868 by - (erule eval_no_abrupt_lemma [rule_format])

1869 with Call.hyps

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

1871 by rules

1872 also from Call.hyps

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

1874 by - (erule dom_locals_eval_mono_elim)

1875 also

1876 from nrm_s2 Call.hyps

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

1878 by rules

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

1880 by (rule Un_least)

1881 also

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

1883 by (cases s4) simp

1884 finally show ?case

1885 by simp

1886 next

1887 case Methd thus ?case by simp

1888 next

1889 case Body thus ?case by simp

1890 next

1891 case LVar thus ?case by simp

1892 next

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

1894 have s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .

1895 have avar: "(v, s2') = fvar statDeclC stat fn a s2" .

1896 have nrm_s2: "normal s2"

1897 proof -

1898 have "normal s3" .

1899 with s3 have "normal s2'"

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

1901 with avar show "normal s2"

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

1903 qed

1904 with FVar.hyps

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

1906 by rules

1907 also

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

1909 proof -

1910 from avar

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

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

1913 thus ?thesis

1914 by simp (rule dom_locals_fvar_mono)

1915 qed

1916 also from s3

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

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

1919 finally show ?case

1920 by simp

1921 next

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

1923 have avar: "(v, s2') = avar G i a s2" .

1924 have nrm_s2: "normal s2"

1925 proof -

1926 have "normal s2'" .

1927 with avar

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

1929 qed

1930 with AVar.hyps

1931 have "normal s1"

1932 by - (erule eval_no_abrupt_lemma [rule_format])

1933 with AVar.hyps

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

1935 by rules

1936 also from AVar.hyps

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

1938 by - (erule dom_locals_eval_mono_elim)

1939 also

1940 from AVar.hyps nrm_s2

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

1942 by rules

1943 ultimately

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

1945 by (rule Un_least)

1946 also

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

1948 proof -

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

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

1951 thus ?thesis

1952 by simp (rule dom_locals_avar_mono)

1953 qed

1954 finally

1955 show ?case

1956 by simp

1957 next

1958 case Nil show ?case by simp

1959 next

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

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

1962 proof -

1963 from Cons

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

1965 with Cons.hyps show ?thesis by rules

1966 qed

1967 also from Cons.hyps

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

1969 by - (erule dom_locals_eval_mono_elim)

1970 also from Cons

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

1972 by rules

1973 ultimately

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

1975 by (rule Un_least)

1976 thus ?case

1977 by simp

1978 qed

1979 qed

1981 corollary assignsE_good_approx:

1982 assumes

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

1984 normal: "normal s1"

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

1986 proof -

1987 from eval normal show ?thesis

1988 by (rule assigns_good_approx [elim_format]) simp

1989 qed

1991 corollary assignsV_good_approx:

1992 assumes

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

1994 normal: "normal s1"

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

1996 proof -

1997 from eval normal show ?thesis

1998 by (rule assigns_good_approx [elim_format]) simp

1999 qed

2001 corollary assignsEs_good_approx:

2002 assumes

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

2004 normal: "normal s1"

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

2006 proof -

2007 from eval normal show ?thesis

2008 by (rule assigns_good_approx [elim_format]) simp

2009 qed

2011 lemma constVal_eval:

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

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

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

2015 proof -

2016 have True and

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

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

2019 and True and True

2020 proof (induct rule: var_expr_stmt.induct)

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

2022 next

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

2024 next

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

2026 next

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

2028 next

2029 case (Lit val c v s0 s)

2030 have "constVal (Lit val) = Some c" .

2031 moreover

2032 have "G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s" .

2033 then obtain "v=val" and "normal s"

2034 by cases simp

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

2036 next

2037 case (UnOp unop e c v s0 s)

2038 have const: "constVal (UnOp unop e) = Some c" .

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

2040 have "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s" .

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

2042 v: "v = eval_unop unop ve"

2043 by cases simp

2044 from ce ve

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

2046 by (rule UnOp.hyps [elim_format]) rules

2047 from eq_ve_ce const ce v

2048 have "v=c"

2049 by simp

2050 from this nrm_s

2051 show ?case ..

2052 next

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

2054 have const: "constVal (BinOp binop e1 e2) = Some c" .

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

2056 c2: "constVal e2 = Some c2" and

2057 c: "c = eval_binop binop c1 c2"

2058 by simp

2059 have "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s" .

2060 then obtain v1 s1 v2

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

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

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

2064 v: "v = eval_binop binop v1 v2"

2065 by cases simp

2066 from c1 v1

2067 obtain eq_v1_c1: "v1 = c1" and

2068 nrm_s1: "normal s1"

2069 by (rule BinOp.hyps [elim_format]) rules

2070 show ?case

2071 proof (cases "need_second_arg binop v1")

2072 case True

2073 with v2 nrm_s1 obtain s1'

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

2075 by (cases s1) simp

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

2077 by (rule BinOp.hyps [elim_format]) rules

2078 with c c1 c2 eq_v1_c1 v

2079 show ?thesis by simp

2080 next

2081 case False

2082 with nrm_s1 v2

2083 have "s=s1"

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

2085 moreover

2086 from False c v eq_v1_c1

2087 have "v = c"

2088 by (simp add: eval_binop_arg2_indep)

2089 ultimately

2090 show ?thesis

2091 using nrm_s1 by simp

2092 qed (* hallo ehco *)

2093 next

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

2095 next

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

2097 next

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

2099 next

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

2101 have c: "constVal (b ? e1 : e2) = Some c" .

2102 then obtain cb c1 c2 where

2103 cb: "constVal b = Some cb" and

2104 c1: "constVal e1 = Some c1" and

2105 c2: "constVal e2 = Some c2"

2106 by (auto split: bool.splits)

2107 have "G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s" .

2108 then obtain vb s1

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

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

2111 by cases simp

2112 from cb vb

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

2114 by (rule Cond.hyps [elim_format]) rules

2115 show ?case

2116 proof (cases "the_Bool vb")

2117 case True

2118 with c cb c1 eq_vb_cb

2119 have "c = c1"

2120 by simp

2121 moreover

2122 from True eval_v nrm_s1 obtain s1'

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

2124 by (cases s1) simp

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

2126 by (rule Cond.hyps [elim_format]) rules

2127 ultimately show ?thesis by simp

2128 next

2129 case False

2130 with c cb c2 eq_vb_cb

2131 have "c = c2"

2132 by simp

2133 moreover

2134 from False eval_v nrm_s1 obtain s1'

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

2136 by (cases s1) simp

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

2138 by (rule Cond.hyps [elim_format]) rules

2139 ultimately show ?thesis by simp

2140 qed

2141 next

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

2143 qed simp_all

2144 with const eval

2145 show ?thesis

2146 by rules

2147 qed

2149 lemmas constVal_eval_elim = constVal_eval [THEN conjE]

2151 lemma eval_unop_type:

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

2153 by (cases unop) simp_all

2155 lemma eval_binop_type:

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

2157 by (cases binop) simp_all

2159 lemma constVal_Boolean:

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

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

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

2163 proof -

2164 have True and

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

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

2167 and True and True

2168 proof (induct rule: var_expr_stmt.induct)

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

2170 next

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

2172 next

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

2174 next

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

2176 next

2177 case (Lit v c)

2178 have "constVal (Lit v) = Some c" .

2179 hence "c=v" by simp

2180 moreover have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .

2181 hence "typeof empty_dt v = Some (PrimT Boolean)"

2182 by cases simp

2183 ultimately show ?case by simp

2184 next

2185 case (UnOp unop e c)

2186 have "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .

2187 hence "Boolean = unop_type unop" by cases simp

2188 moreover have "constVal (UnOp unop e) = Some c" .

2189 then obtain ce where "c = eval_unop unop ce" by auto

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

2191 next

2192 case (BinOp binop e1 e2 c)

2193 have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .

2194 hence "Boolean = binop_type binop" by cases simp

2195 moreover have "constVal (BinOp binop e1 e2) = Some c" .

2196 then obtain c1 c2 where "c = eval_binop binop c1 c2" by auto

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

2198 next

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

2200 next

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

2202 next

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

2204 next

2205 case (Cond b e1 e2 c)

2206 have c: "constVal (b ? e1 : e2) = Some c" .

2207 then obtain cb c1 c2 where

2208 cb: "constVal b = Some cb" and

2209 c1: "constVal e1 = Some c1" and

2210 c2: "constVal e2 = Some c2"

2211 by (auto split: bool.splits)

2212 have wt: "Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean" .

2213 then

2214 obtain T1 T2

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

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

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

2218 by cases (auto dest: widen_Boolean2)

2219 show ?case

2220 proof (cases "the_Bool cb")

2221 case True

2222 from c1 wt_e1

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

2224 by (rule Cond.hyps)

2225 with True c cb c1 show ?thesis by simp

2226 next

2227 case False

2228 from c2 wt_e2

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

2230 by (rule Cond.hyps)

2231 with False c cb c2 show ?thesis by simp

2232 qed

2233 next

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

2235 qed simp_all

2236 with const wt

2237 show ?thesis

2238 by rules

2239 qed

2241 lemma assigns_if_good_approx:

2242 assumes

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

2244 normal: "normal s1" and

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

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

2247 proof -

2248 -- {* To properly perform induction on the evaluation relation we have to

2249 generalize the lemma to terms not only expressions. *}

2250 { fix t val

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

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

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

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

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

2256 using eval' normal bool' expr

2257 proof (induct)

2258 case Abrupt thus ?case by simp

2259 next

2260 case (NewC C a s0 s1 s2)

2261 have "Env\<turnstile>NewC C\<Colon>-PrimT Boolean" .

2262 hence False

2263 by cases simp

2264 thus ?case ..

2265 next

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

2267 have "Env\<turnstile>New T[e]\<Colon>-PrimT Boolean" .

2268 hence False

2269 by cases simp

2270 thus ?case ..

2271 next

2272 case (Cast T e s0 s1 s2 b)

2273 have s2: "s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1".

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

2275 proof -

2276 have "normal s2" .

2277 with s2 have "normal s1"

2278 by (cases s1) simp

2279 moreover

2280 have "Env\<turnstile>Cast T e\<Colon>-PrimT Boolean" .

2281 hence "Env\<turnstile>e\<Colon>- PrimT Boolean"

2282 by (cases) (auto dest: cast_Boolean2)

2283 ultimately show ?thesis

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

2285 qed

2286 also from s2

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

2288 by simp

2289 finally show ?case by simp

2290 next

2291 case (Inst T b e s0 s1 v)

2292 have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and "normal s1" .

2293 hence "assignsE e \<subseteq> dom (locals (store s1))"

2294 by (rule assignsE_good_approx)

2295 thus ?case

2296 by simp

2297 next

2298 case (Lit s v)

2299 have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .

2300 hence "typeof empty_dt v = Some (PrimT Boolean)"

2301 by cases simp

2302 then obtain b where "v=Bool b"

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

2304 thus ?case

2305 by simp

2306 next

2307 case (UnOp e s0 s1 unop v)

2308 have bool: "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .

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

2310 by cases (cases unop,simp_all)

2311 show ?case

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

2313 case None

2314 have "normal s1" .

2315 moreover note bool_e

2316 ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"

2317 by (rule UnOp.hyps [elim_format]) auto

2318 moreover

2319 from bool have "unop = UNot"

2320 by cases (cases unop, simp_all)

2321 moreover note None

2322 ultimately

2323 have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e)

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

2325 by simp

2326 thus ?thesis by simp

2327 next

2328 case (Some c)

2329 moreover

2330 have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .

2331 hence "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1"

2332 by (rule eval.UnOp)

2333 with Some

2334 have "eval_unop unop v=c"

2335 by (rule constVal_eval_elim) simp

2336 moreover

2337 from Some bool

2338 obtain b where "c=Bool b"

2339 by (rule constVal_Boolean [elim_format])

2340 (cases c, simp_all add: empty_dt_def)

2341 ultimately

2342 have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) = {}"

2343 by simp

2344 thus ?thesis by simp

2345 qed

2346 next

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

2348 have bool: "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .

2349 show ?case

2350 proof (cases "constVal (BinOp binop e1 e2)")

2351 case (Some c)

2352 moreover

2353 from BinOp.hyps

2354 have

2355 "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"

2356 by - (rule eval.BinOp)

2357 with Some

2358 have "eval_binop binop v1 v2=c"

2359 by (rule constVal_eval_elim) simp

2360 moreover

2361 from Some bool

2362 obtain b where "c = Bool b"

2363 by (rule constVal_Boolean [elim_format])

2364 (cases c, simp_all add: empty_dt_def)

2365 ultimately

2366 have "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2)

2367 = {}"

2368 by simp

2369 thus ?thesis by simp

2370 next

2371 case None

2372 show ?thesis

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

2374 case True

2375 from bool obtain bool_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and

2376 bool_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"

2377 using True by cases auto

2378 have "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s1))"

2379 proof -

2380 from BinOp have "normal s1"

2381 by - (erule eval_no_abrupt_lemma [rule_format])

2382 from this bool_e1

2383 show ?thesis

2384 by (rule BinOp.hyps [elim_format]) auto

2385 qed

2386 also

2387 from BinOp.hyps

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

2389 by - (erule dom_locals_eval_mono_elim,simp)

2390 finally

2391 have e1_s2: "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s2))".

2392 from True show ?thesis

2393 proof

2394 assume condAnd: "binop = CondAnd"

2395 show ?thesis

2396 proof (cases "the_Bool (eval_binop binop v1 v2)")

2397 case True

2398 with condAnd

2399 have need_second: "need_second_arg binop v1"

2400 by (simp add: need_second_arg_def)

2401 have "normal s2" .

2402 hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2403 by (rule BinOp.hyps [elim_format])

2404 (simp add: need_second bool_e2)+

2405 with e1_s2

2406 have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2

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

2408 by (rule Un_least)

2409 with True condAnd None show ?thesis

2410 by simp

2411 next

2412 case False

2413 note binop_False = this

2414 show ?thesis

2415 proof (cases "need_second_arg binop v1")

2416 case True

2417 with binop_False condAnd

2418 obtain "the_Bool v1=True" and "the_Bool v2 = False"

2419 by (simp add: need_second_arg_def)

2420 moreover

2421 have "normal s2" .

2422 hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2423 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+

2424 with e1_s2

2425 have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2

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

2427 by (rule Un_least)

2428 moreover note binop_False condAnd None

2429 ultimately show ?thesis

2430 by auto

2431 next

2432 case False

2433 with binop_False condAnd

2434 have "the_Bool v1=False"

2435 by (simp add: need_second_arg_def)

2436 with e1_s2

2437 show ?thesis

2438 using binop_False condAnd None by auto

2439 qed

2440 qed

2441 next

2442 assume condOr: "binop = CondOr"

2443 show ?thesis

2444 proof (cases "the_Bool (eval_binop binop v1 v2)")

2445 case False

2446 with condOr

2447 have need_second: "need_second_arg binop v1"

2448 by (simp add: need_second_arg_def)

2449 have "normal s2" .

2450 hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2451 by (rule BinOp.hyps [elim_format])

2452 (simp add: need_second bool_e2)+

2453 with e1_s2

2454 have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2

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

2456 by (rule Un_least)

2457 with False condOr None show ?thesis

2458 by simp

2459 next

2460 case True

2461 note binop_True = this

2462 show ?thesis

2463 proof (cases "need_second_arg binop v1")

2464 case True

2465 with binop_True condOr

2466 obtain "the_Bool v1=False" and "the_Bool v2 = True"

2467 by (simp add: need_second_arg_def)

2468 moreover

2469 have "normal s2" .

2470 hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2471 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+

2472 with e1_s2

2473 have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2

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

2475 by (rule Un_least)

2476 moreover note binop_True condOr None

2477 ultimately show ?thesis

2478 by auto

2479 next

2480 case False

2481 with binop_True condOr

2482 have "the_Bool v1=True"

2483 by (simp add: need_second_arg_def)

2484 with e1_s2

2485 show ?thesis

2486 using binop_True condOr None by auto

2487 qed

2488 qed

2489 qed

2490 next

2491 case False

2492 have "\<not> (binop = CondAnd \<or> binop = CondOr)" .

2493 from BinOp.hyps

2494 have

2495 "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"

2496 by - (rule eval.BinOp)

2497 moreover have "normal s2" .

2498 ultimately

2499 have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"

2500 by (rule assignsE_good_approx)

2501 with False None

2502 show ?thesis

2503 by simp

2504 qed

2505 qed

2506 next

2507 case Super

2508 have "Env\<turnstile>Super\<Colon>-PrimT Boolean" .

2509 hence False

2510 by cases simp

2511 thus ?case ..

2512 next

2513 case (Acc f s0 s1 v va)

2514 have "prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1" and "normal s1".

2515 hence "assignsV va \<subseteq> dom (locals (store s1))"

2516 by (rule assignsV_good_approx)

2517 thus ?case by simp

2518 next

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

2520 hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"

2521 by - (rule eval.Ass)

2522 moreover have "normal (assign f v s2)" .

2523 ultimately

2524 have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"

2525 by (rule assignsE_good_approx)

2526 thus ?case by simp

2527 next

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

2529 have "Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean" .

2530 then obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and

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

2532 by cases (auto dest: widen_Boolean2)

2533 have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .

2534 have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"

2535 proof -

2536 note eval_e0

2537 moreover

2538 have "normal s2" .

2539 with Cond.hyps have "normal s1"

2540 by - (erule eval_no_abrupt_lemma [rule_format],simp)

2541 ultimately

2542 have "assignsE e0 \<subseteq> dom (locals (store s1))"

2543 by (rule assignsE_good_approx)

2544 also

2545 from Cond

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

2547 by - (erule dom_locals_eval_mono [elim_format],simp)

2548 finally show ?thesis .

2549 qed

2550 show ?case

2551 proof (cases "constVal e0")

2552 case None

2553 have "assigns_if (the_Bool v) e1 \<inter> assigns_if (the_Bool v) e2

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

2555 proof (cases "the_Bool b")

2556 case True

2557 have "normal s2" .

2558 hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"

2559 by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)

2560 thus ?thesis

2561 by blast

2562 next

2563 case False

2564 have "normal s2" .

2565 hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"

2566 by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)

2567 thus ?thesis

2568 by blast

2569 qed

2570 with e0_s2

2571 have "assignsE e0 \<union>

2572 (assigns_if (the_Bool v) e1 \<inter> assigns_if (the_Bool v) e2)

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

2574 by (rule Un_least)

2575 with None show ?thesis

2576 by simp

2577 next

2578 case (Some c)

2579 from this eval_e0 have eq_b_c: "b=c"

2580 by (rule constVal_eval_elim)

2581 show ?thesis

2582 proof (cases "the_Bool c")

2583 case True

2584 have "normal s2" .

2585 hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"

2586 by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True)

2587 with e0_s2

2588 have "assignsE e0 \<union> assigns_if (the_Bool v) e1 \<subseteq> \<dots>"

2589 by (rule Un_least)

2590 with Some True show ?thesis

2591 by simp

2592 next

2593 case False

2594 have "normal s2" .

2595 hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"

2596 by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False)

2597 with e0_s2

2598 have "assignsE e0 \<union> assigns_if (the_Bool v) e2 \<subseteq> \<dots>"

2599 by (rule Un_least)

2600 with Some False show ?thesis

2601 by simp

2602 qed

2603 qed

2604 next

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

2606 hence

2607 "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v\<rightarrow>

2608 (set_lvars (locals (store s2)) s4)"

2609 by - (rule eval.Call)

2610 hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args))

2611 \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"

2612 by (rule assignsE_good_approx)

2613 thus ?case by simp

2614 next

2615 case Methd show ?case by simp

2616 next

2617 case Body show ?case by simp

2618 qed simp+ -- {* all the statements and variables *}

2619 }

2620 note generalized = this

2621 from eval bool show ?thesis

2622 by (rule generalized [elim_format]) simp+

2623 qed

2625 lemma assigns_if_good_approx':

2626 assumes eval: "G\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1"

2627 and normal: "normal s1"

2628 and bool: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>- (PrimT Boolean)"

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

2630 proof -

2631 from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp

2632 from this normal bool show ?thesis

2633 by (rule assigns_if_good_approx)

2634 qed

2637 lemma subset_Intl: "A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"

2638 by blast

2640 lemma subset_Intr: "B \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"

2641 by blast

2643 lemma da_good_approx:

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

2645 wt: "Env\<turnstile>t\<Colon>T" (is "?Wt Env t T") and

2646 da: "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" (is "?Da Env s0 t A") and

2647 wf: "wf_prog (prg Env)"

2648 shows "(normal s1 \<longrightarrow> (nrm A \<subseteq> dom (locals (store s1)))) \<and>

2649 (\<forall> l. abrupt s1 = Some (Jump (Break l)) \<and> normal s0

2650 \<longrightarrow> (brk A l \<subseteq> dom (locals (store s1)))) \<and>

2651 (abrupt s1 = Some (Jump Ret) \<and> normal s0

2652 \<longrightarrow> Result \<in> dom (locals (store s1)))"

2653 (is "?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1")

2654 proof -

2655 note inj_term_simps [simp]

2656 obtain G where G: "prg Env = G" by (cases Env) simp

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

2658 from G wf have wf: "wf_prog G" by simp

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

2660 \<forall> Env T A. ?Wt Env t T \<longrightarrow> ?Da Env s0 t A \<longrightarrow> prg Env = G

2661 \<longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1"

2662 -- {* Goal in object logic variant *}

2663 from eval

2664 show "\<And> Env T A. \<lbrakk>?Wt Env t T; ?Da Env s0 t A; prg Env = G\<rbrakk>

2665 \<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1"

2666 (is "PROP ?Hyp t s0 s1")

2667 proof (induct)

2668 case (Abrupt s t xc Env T A)

2669 have da: "Env\<turnstile> dom (locals s) \<guillemotright>t\<guillemotright> A" using Abrupt.prems by simp

2670 have "?NormalAssigned (Some xc,s) A"

2671 by simp

2672 moreover

2673 have "?BreakAssigned (Some xc,s) (Some xc,s) A"

2674 by simp

2675 moreover have "?ResAssigned (Some xc,s) (Some xc,s)"

2676 by simp

2677 ultimately show ?case by (intro conjI)

2678 next

2679 case (Skip s Env T A)

2680 have da: "Env\<turnstile> dom (locals (store (Norm s))) \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"

2681 using Skip.prems by simp

2682 hence "nrm A = dom (locals (store (Norm s)))"

2683 by (rule da_elim_cases) simp

2684 hence "?NormalAssigned (Norm s) A"

2685 by auto

2686 moreover

2687 have "?BreakAssigned (Norm s) (Norm s) A"

2688 by simp

2689 moreover have "?ResAssigned (Norm s) (Norm s)"

2690 by simp

2691 ultimately show ?case by (intro conjI)

2692 next

2693 case (Expr e s0 s1 v Env T A)

2694 from Expr.prems

2695 show "?NormalAssigned s1 A \<and> ?BreakAssigned (Norm s0) s1 A

2696 \<and> ?ResAssigned (Norm s0) s1"

2697 by (elim wt_elim_cases da_elim_cases)

2698 (rule Expr.hyps, auto)

2699 next

2700 case (Lab c j s0 s1 Env T A)

2701 have G: "prg Env = G" .

2702 from Lab.prems

2703 obtain C l where

2704 da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and

2705 A: "nrm A = nrm C \<inter> (brk C) l" "brk A = rmlab l (brk C)" and

2706 j: "j = Break l"

2707 by - (erule da_elim_cases, simp)

2708 from Lab.prems

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

2710 by - (erule wt_elim_cases, simp)

2711 from wt_c da_c G and Lab.hyps

2712 have norm_c: "?NormalAssigned s1 C" and

2713 brk_c: "?BreakAssigned (Norm s0) s1 C" and

2714 res_c: "?ResAssigned (Norm s0) s1"

2715 by simp_all

2716 have "?NormalAssigned (abupd (absorb j) s1) A"

2717 proof

2718 assume normal: "normal (abupd (absorb j) s1)"

2719 show "nrm A \<subseteq> dom (locals (store (abupd (absorb j) s1)))"

2720 proof (cases "abrupt s1")

2721 case None

2722 with norm_c A

2723 show ?thesis

2724 by auto

2725 next

2726 case Some

2727 with normal j

2728 have "abrupt s1 = Some (Jump (Break l))"

2729 by (auto dest: absorb_Some_NoneD)

2730 with brk_c A

2731 show ?thesis

2732 by auto

2733 qed

2734 qed

2735 moreover

2736 have "?BreakAssigned (Norm s0) (abupd (absorb j) s1) A"

2737 proof -

2738 {

2739 fix l'

2740 assume break: "abrupt (abupd (absorb j) s1) = Some (Jump (Break l'))"

2741 with j

2742 have "l\<noteq>l'"

2743 by (cases s1) (auto dest!: absorb_Some_JumpD)

2744 hence "(rmlab l (brk C)) l'= (brk C) l'"

2745 by (simp)

2746 with break brk_c A

2747 have

2748 "(brk A l' \<subseteq> dom (locals (store (abupd (absorb j) s1))))"

2749 by (cases s1) auto

2750 }

2751 then show ?thesis

2752 by simp

2753 qed

2754 moreover

2755 from res_c have "?ResAssigned (Norm s0) (abupd (absorb j) s1)"

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

2757 ultimately show ?case by (intro conjI)

2758 next

2759 case (Comp c1 c2 s0 s1 s2 Env T A)

2760 have G: "prg Env = G" .

2761 from Comp.prems

2762 obtain C1 C2

2763 where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

2764 da_c2: "Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

2765 A: "nrm A = nrm C2" "brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)"

2766 by (elim da_elim_cases) simp

2767 from Comp.prems

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

2769 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

2770 by (elim wt_elim_cases) simp

2771 have "PROP ?Hyp (In1r c1) (Norm s0) s1" .

2772 with wt_c1 da_c1 G

2773 obtain nrm_c1: "?NormalAssigned s1 C1" and

2774 brk_c1: "?BreakAssigned (Norm s0) s1 C1" and

2775 res_c1: "?ResAssigned (Norm s0) s1"

2776 by simp

2777 show ?case

2778 proof (cases "normal s1")

2779 case True

2780 with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by rules

2781 with da_c2 obtain C2'

2782 where da_c2': "Env\<turnstile> dom (locals (snd s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

2783 nrm_c2: "nrm C2 \<subseteq> nrm C2'" and

2784 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"

2785 by (rule da_weakenE) rules

2786 have "PROP ?Hyp (In1r c2) s1 s2" .

2787 with wt_c2 da_c2' G

2788 obtain nrm_c2': "?NormalAssigned s2 C2'" and

2789 brk_c2': "?BreakAssigned s1 s2 C2'" and

2790 res_c2 : "?ResAssigned s1 s2"

2791 by simp

2792 from nrm_c2' nrm_c2 A

2793 have "?NormalAssigned s2 A"

2794 by blast

2795 moreover from brk_c2' brk_c2 A

2796 have "?BreakAssigned s1 s2 A"

2797 by fastsimp

2798 with True

2799 have "?BreakAssigned (Norm s0) s2 A" by simp

2800 moreover from res_c2 True

2801 have "?ResAssigned (Norm s0) s2"

2802 by simp

2803 ultimately show ?thesis by (intro conjI)

2804 next

2805 case False

2806 have "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .

2807 with False have eq_s1_s2: "s2=s1" by auto

2808 with False have "?NormalAssigned s2 A" by blast

2809 moreover

2810 have "?BreakAssigned (Norm s0) s2 A"

2811 proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")

2812 case True

2813 then obtain l where l: "abrupt s1 = Some (Jump (Break l))" ..

2814 with brk_c1

2815 have "brk C1 l \<subseteq> dom (locals (store s1))"

2816 by simp

2817 with A eq_s1_s2

2818 have "brk A l \<subseteq> dom (locals (store s2))"

2819 by auto

2820 with l eq_s1_s2

2821 show ?thesis by simp

2822 next

2823 case False

2824 with eq_s1_s2 show ?thesis by simp

2825 qed

2826 moreover from False res_c1 eq_s1_s2

2827 have "?ResAssigned (Norm s0) s2"

2828 by simp

2829 ultimately show ?thesis by (intro conjI)

2830 qed

2831 next

2832 -- {*

2833 \par

2834 *} (* dummy text command to break paragraph for latex;

2835 large paragraphs exhaust memory of debian pdflatex *)

2836 case (If b c1 c2 e s0 s1 s2 Env T A)

2837 have G: "prg Env = G" .

2838 with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp

2839 from If.prems

2840 obtain E C1 C2 where

2841 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

2842 da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2843 \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

2844 da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2845 \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

2846 A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"

2847 by (elim da_elim_cases)

2848 from If.prems

2849 obtain

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

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

2852 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

2853 by (elim wt_elim_cases)

2854 from wt_e da_e G

2855 obtain nrm_s1: "?NormalAssigned s1 E" and

2856 brk_s1: "?BreakAssigned (Norm s0) s1 E" and

2857 res_s1: "?ResAssigned (Norm s0) s1"

2858 by (elim If.hyps [elim_format]) simp+

2859 from If.hyps have

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

2861 by (elim dom_locals_eval_mono_elim)

2862 show ?case

2863 proof (cases "normal s1")

2864 case True

2865 note normal_s1 = this

2866 show ?thesis

2867 proof (cases "the_Bool b")

2868 case True

2869 from eval_e normal_s1 wt_e

2870 have "assigns_if True e \<subseteq> dom (locals (store s1))"

2871 by (rule assigns_if_good_approx [elim_format]) (simp add: True)

2872 with s0_s1

2873 have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"

2874 by (rule Un_least)

2875 with da_c1 obtain C1'

2876 where da_c1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and

2877 nrm_c1: "nrm C1 \<subseteq> nrm C1'" and

2878 brk_c1: "\<forall> l. brk C1 l \<subseteq> brk C1' l"

2879 by (rule da_weakenE) rules

2880 from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp

2881 with wt_c1 da_c1'

2882 obtain nrm_c1': "?NormalAssigned s2 C1'" and

2883 brk_c1': "?BreakAssigned s1 s2 C1'" and

2884 res_c1: "?ResAssigned s1 s2"

2885 using G by simp

2886 from nrm_c1' nrm_c1 A

2887 have "?NormalAssigned s2 A"

2888 by blast

2889 moreover from brk_c1' brk_c1 A

2890 have "?BreakAssigned s1 s2 A"

2891 by fastsimp

2892 with normal_s1

2893 have "?BreakAssigned (Norm s0) s2 A" by simp

2894 moreover from res_c1 normal_s1 have "?ResAssigned (Norm s0) s2"

2895 by simp

2896 ultimately show ?thesis by (intro conjI)

2897 next

2898 case False

2899 from eval_e normal_s1 wt_e

2900 have "assigns_if False e \<subseteq> dom (locals (store s1))"

2901 by (rule assigns_if_good_approx [elim_format]) (simp add: False)

2902 with s0_s1

2903 have "dom (locals (store ((Norm s0)::state)))\<union> assigns_if False e \<subseteq> \<dots>"

2904 by (rule Un_least)

2905 with da_c2 obtain C2'

2906 where da_c2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

2907 nrm_c2: "nrm C2 \<subseteq> nrm C2'" and

2908 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"

2909 by (rule da_weakenE) rules

2910 from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp

2911 with wt_c2 da_c2'

2912 obtain nrm_c2': "?NormalAssigned s2 C2'" and

2913 brk_c2': "?BreakAssigned s1 s2 C2'" and

2914 res_c2: "?ResAssigned s1 s2"

2915 using G by simp

2916 from nrm_c2' nrm_c2 A

2917 have "?NormalAssigned s2 A"

2918 by blast

2919 moreover from brk_c2' brk_c2 A

2920 have "?BreakAssigned s1 s2 A"

2921 by fastsimp

2922 with normal_s1

2923 have "?BreakAssigned (Norm s0) s2 A" by simp

2924 moreover from res_c2 normal_s1 have "?ResAssigned (Norm s0) s2"

2925 by simp

2926 ultimately show ?thesis by (intro conjI)

2927 qed

2928 next

2929 case False

2930 then obtain abr where abr: "abrupt s1 = Some abr"

2931 by (cases s1) auto

2932 moreover

2933 from eval_e _ wt_e have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"

2934 by (rule eval_expression_no_jump) (simp_all add: G wf)

2935 moreover

2936 have "s2 = s1"

2937 proof -

2938 have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .

2939 with abr show ?thesis

2940 by (cases s1) simp

2941 qed

2942 ultimately show ?thesis using res_s1 by simp

2943 qed

2944 next

2945 -- {*

2946 \par

2947 *} (* dummy text command to break paragraph for latex;

2948 large paragraphs exhaust memory of debian pdflatex *)

2949 case (Loop b c e l s0 s1 s2 s3 Env T A)

2950 have G: "prg Env = G" .

2951 with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"

2952 by (simp (no_asm_simp))

2953 from Loop.prems

2954 obtain E C where

2955 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

2956 da_c: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2957 \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and

2958 A: "nrm A = nrm C \<inter>

2959 (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)"

2960 "brk A = brk C"

2961 by (elim da_elim_cases)

2962 from Loop.prems

2963 obtain

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

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

2966 by (elim wt_elim_cases)

2967 from wt_e da_e G

2968 obtain res_s1: "?ResAssigned (Norm s0) s1"

2969 by (elim Loop.hyps [elim_format]) simp+

2970 from Loop.hyps have

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

2972 by (elim dom_locals_eval_mono_elim)

2973 show ?case

2974 proof (cases "normal s1")

2975 case True

2976 note normal_s1 = this

2977 show ?thesis

2978 proof (cases "the_Bool b")

2979 case True

2980 with Loop.hyps obtain

2981 eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and

2982 eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"

2983 by simp

2984 from Loop.hyps True

2985 have "?HypObj (In1r c) s1 s2" by simp

2986 note hyp_c = this [rule_format]

2987 from Loop.hyps True

2988 have "?HypObj (In1r (l\<bullet> While(e) c)) (abupd (absorb (Cont l)) s2) s3"

2989 by simp

2990 note hyp_while = this [rule_format]

2991 from eval_e normal_s1 wt_e

2992 have "assigns_if True e \<subseteq> dom (locals (store s1))"

2993 by (rule assigns_if_good_approx [elim_format]) (simp add: True)

2994 with s0_s1

2995 have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"

2996 by (rule Un_least)

2997 with da_c obtain C'

2998 where da_c': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and

2999 nrm_C_C': "nrm C \<subseteq> nrm C'" and

3000 brk_C_C': "\<forall> l. brk C l \<subseteq> brk C' l"

3001 by (rule da_weakenE) rules

3002 from hyp_c wt_c da_c'

3003 obtain nrm_C': "?NormalAssigned s2 C'" and

3004 brk_C': "?BreakAssigned s1 s2 C'" and

3005 res_s2: "?ResAssigned s1 s2"

3006 using G by simp

3007 show ?thesis

3008 proof (cases "normal s2 \<or> abrupt s2 = Some (Jump (Cont l))")

3009 case True

3010 from Loop.prems obtain

3011 wt_while: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" and

3012 da_while: "Env\<turnstile> dom (locals (store ((Norm s0)::state)))

3013 \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"

3014 by simp

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

3016 \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"

3017 proof -

3018 note s0_s1

3019 also from eval_c

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

3021 by (rule dom_locals_eval_mono_elim)

3022 also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"

3023 by simp

3024 finally show ?thesis .

3025 qed

3026 with da_while obtain A'

3027 where

3028 da_while': "Env\<turnstile> dom (locals (store (abupd (absorb (Cont l)) s2)))

3029 \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"

3030 and nrm_A_A': "nrm A \<subseteq> nrm A'"

3031 and brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"

3032 by (rule da_weakenE) simp

3033 with wt_while hyp_while

3034 obtain nrm_A': "?NormalAssigned s3 A'" and

3035 brk_A': "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A'" and

3036 res_s3: "?ResAssigned (abupd (absorb (Cont l)) s2) s3"

3037 using G by simp

3038 from nrm_A_A' nrm_A'

3039 have "?NormalAssigned s3 A"

3040 by blast

3041 moreover

3042 have "?BreakAssigned (Norm s0) s3 A"

3043 proof -

3044 from brk_A_A' brk_A'

3045 have "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A"

3046 by fastsimp

3047 moreover

3048 from True have "normal (abupd (absorb (Cont l)) s2)"

3049 by (cases s2) auto

3050 ultimately show ?thesis

3051 by simp

3052 qed

3053 moreover from res_s3 True have "?ResAssigned (Norm s0) s3"

3054 by auto

3055 ultimately show ?thesis by (intro conjI)

3056 next

3057 case False

3058 then obtain abr where

3059 "abrupt s2 = Some abr" and

3060 "abrupt (abupd (absorb (Cont l)) s2) = Some abr"

3061 by auto

3062 with eval_while

3063 have eq_s3_s2: "s3=s2"

3064 by auto

3065 with nrm_C_C' nrm_C' A

3066 have "?NormalAssigned s3 A"

3067 by fastsimp

3068 moreover

3069 from eq_s3_s2 brk_C_C' brk_C' normal_s1 A

3070 have "?BreakAssigned (Norm s0) s3 A"

3071 by fastsimp

3072 moreover

3073 from eq_s3_s2 res_s2 normal_s1 have "?ResAssigned (Norm s0) s3"

3074 by simp

3075 ultimately show ?thesis by (intro conjI)

3076 qed

3077 next

3078 case False

3079 with Loop.hyps have eq_s3_s1: "s3=s1"

3080 by simp

3081 from eq_s3_s1 res_s1

3082 have res_s3: "?ResAssigned (Norm s0) s3"

3083 by simp

3084 from eval_e True wt_e

3085 have "assigns_if False e \<subseteq> dom (locals (store s1))"

3086 by (rule assigns_if_good_approx [elim_format]) (simp add: False)

3087 with s0_s1

3088 have "dom (locals (store ((Norm s0)::state)))\<union>assigns_if False e \<subseteq> \<dots>"

3089 by (rule Un_least)

3090 hence "nrm C \<inter>

3091 (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)

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

3093 by (rule subset_Intr)

3094 with normal_s1 A eq_s3_s1

3095 have "?NormalAssigned s3 A"

3096 by simp

3097 moreover

3098 from normal_s1 eq_s3_s1

3099 have "?BreakAssigned (Norm s0) s3 A"

3100 by simp

3101 moreover note res_s3

3102 ultimately show ?thesis by (intro conjI)

3103 qed

3104 next

3105 case False

3106 then obtain abr where abr: "abrupt s1 = Some abr"

3107 by (cases s1) auto

3108 moreover

3109 from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"

3110 by (rule eval_expression_no_jump) (simp_all add: wf G)

3111 moreover

3112 have eq_s3_s1: "s3=s1"

3113 proof (cases "the_Bool b")

3114 case True

3115 with Loop.hyps obtain

3116 eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and

3117 eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"

3118 by simp

3119 from eval_c abr have "s2=s1" by auto

3120 moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"

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

3122 ultimately show ?thesis

3123 using eval_while abr

3124 by auto

3125 next

3126 case False

3127 with Loop.hyps show ?thesis by simp

3128 qed

3129 moreover

3130 from eq_s3_s1 res_s1

3131 have res_s3: "?ResAssigned (Norm s0) s3"

3132 by simp

3133 ultimately show ?thesis

3134 by simp

3135 qed

3136 next

3137 case (Jmp j s Env T A)

3138 have "?NormalAssigned (Some (Jump j),s) A" by simp

3139 moreover

3140 from Jmp.prems

3141 obtain ret: "j = Ret \<longrightarrow> Result \<in> dom (locals (store (Norm s)))" and

3142 brk: "brk A = (case j of

3143 Break l \<Rightarrow> \<lambda> k. if k=l

3144 then dom (locals (store ((Norm s)::state)))

3145 else UNIV

3146 | Cont l \<Rightarrow> \<lambda> k. UNIV

3147 | Ret \<Rightarrow> \<lambda> k. UNIV)"

3148 by (elim da_elim_cases) simp

3149 from brk have "?BreakAssigned (Norm s) (Some (Jump j),s) A"

3150 by simp

3151 moreover from ret have "?ResAssigned (Norm s) (Some (Jump j),s)"

3152 by simp

3153 ultimately show ?case by (intro conjI)

3154 next

3155 case (Throw a e s0 s1 Env T A)

3156 have G: "prg Env = G" .

3157 from Throw.prems obtain E where

3158 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"

3159 by (elim da_elim_cases)

3160 from Throw.prems

3161 obtain eT where wt_e: "Env\<turnstile>e\<Colon>-eT"

3162 by (elim wt_elim_cases)

3163 have "?NormalAssigned (abupd (throw a) s1) A"

3164 by (cases s1) (simp add: throw_def)

3165 moreover

3166 have "?BreakAssigned (Norm s0) (abupd (throw a) s1) A"

3167 proof -

3168 from G Throw.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"

3169 by (simp (no_asm_simp))

3170 from eval_e _ wt_e

3171 have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"

3172 by (rule eval_expression_no_jump) (simp_all add: wf G)

3173 hence "\<And> l. abrupt (abupd (throw a) s1) \<noteq> Some (Jump (Break l))"

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

3175 thus ?thesis

3176 by simp

3177 qed

3178 moreover

3179 from wt_e da_e G have "?ResAssigned (Norm s0) s1"

3180 by (elim Throw.hyps [elim_format]) simp+

3181 hence "?ResAssigned (Norm s0) (abupd (throw a) s1)"

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

3183 ultimately show ?case by (intro conjI)

3184 next

3185 case (Try C c1 c2 s0 s1 s2 s3 vn Env T A)

3186 have G: "prg Env = G" .

3187 from Try.prems obtain C1 C2 where

3188 da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

3189 da_c2:

3190 "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>

3191 \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

3192 A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"

3193 by (elim da_elim_cases) simp

3194 from Try.prems obtain

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

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

3197 by (elim wt_elim_cases)

3198 have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G

3199 by (simp (no_asm_simp))

3200 have "PROP ?Hyp (In1r c1) (Norm s0) s1" .

3201 with wt_c1 da_c1 G

3202 obtain nrm_C1: "?NormalAssigned s1 C1" and

3203 brk_C1: "?BreakAssigned (Norm s0) s1 C1" and

3204 res_s1: "?ResAssigned (Norm s0) s1"

3205 by simp

3206 show ?case

3207 proof (cases "normal s1")

3208 case True

3209 with nrm_C1 have "nrm C1 \<inter> nrm C2 \<subseteq> dom (locals (store s1))"

3210 by auto

3211 moreover

3212 have "s3=s1"

3213 proof -

3214 from sxalloc True have eq_s2_s1: "s2=s1"

3215 by (cases s1) (auto elim: sxalloc_elim_cases)

3216 with True have "\<not> G,s2\<turnstile>catch C"

3217 by (simp add: catch_def)

3218 with Try.hyps have "s3=s2"

3219 by simp

3220 with eq_s2_s1 show ?thesis by simp

3221 qed

3222 ultimately show ?thesis

3223 using True A res_s1 by simp

3224 next

3225 case False

3226 note not_normal_s1 = this

3227 show ?thesis

3228 proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")

3229 case True

3230 then obtain l where l: "abrupt s1 = Some (Jump (Break l))"

3231 by auto

3232 with brk_C1 have "(brk C1 \<Rightarrow>\<inter> brk C2) l \<subseteq> dom (locals (store s1))"

3233 by auto

3234 moreover have "s3=s1"

3235 proof -

3236 from sxalloc l have eq_s2_s1: "s2=s1"

3237 by (cases s1) (auto elim: sxalloc_elim_cases)

3238 with l have "\<not> G,s2\<turnstile>catch C"

3239 by (simp add: catch_def)

3240 with Try.hyps have "s3=s2"

3241 by simp

3242 with eq_s2_s1 show ?thesis by simp

3243 qed

3244 ultimately show ?thesis

3245 using l A res_s1 by simp

3246 next

3247 case False

3248 note abrupt_no_break = this

3249 show ?thesis

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

3251 case True

3252 with Try.hyps have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3"

3253 by simp

3254 note hyp_c2 = this [rule_format]

3255 have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn})

3256 \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"

3257 proof -

3258 have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .

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

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

3261 by (rule dom_locals_eval_mono_elim)

3262 also

3263 from sxalloc

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

3265 by (rule dom_locals_sxalloc_mono)

3266 also

3267 have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"

3268 by (cases s2) (simp add: new_xcpt_var_def, blast)

3269 also

3270 have "{VName vn} \<subseteq> \<dots>"

3271 by (cases s2) simp

3272 ultimately show ?thesis

3273 by (rule Un_least)

3274 qed

3275 with da_c2

3276 obtain C2' where

3277 da_C2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>

3278 \<turnstile> dom (locals (store (new_xcpt_var vn s2))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"

3279 and nrm_C2': "nrm C2 \<subseteq> nrm C2'"

3280 and brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"

3281 by (rule da_weakenE) simp

3282 from wt_c2 da_C2' G and hyp_c2

3283 obtain nrmAss_C2: "?NormalAssigned s3 C2'" and

3284 brkAss_C2: "?BreakAssigned (new_xcpt_var vn s2) s3 C2'" and

3285 resAss_s3: "?ResAssigned (new_xcpt_var vn s2) s3"

3286 by simp

3287 from nrmAss_C2 nrm_C2' A

3288 have "?NormalAssigned s3 A"

3289 by auto

3290 moreover

3291 have "?BreakAssigned (Norm s0) s3 A"

3292 proof -

3293 from brkAss_C2 have "?BreakAssigned (Norm s0) s3 C2'"

3294 by (cases s2) (auto simp add: new_xcpt_var_def)

3295 with brk_C2' A show ?thesis

3296 by fastsimp

3297 qed

3298 moreover

3299 from resAss_s3 have "?ResAssigned (Norm s0) s3"

3300 by (cases s2) ( simp add: new_xcpt_var_def)

3301 ultimately show ?thesis by (intro conjI)

3302 next

3303 case False

3304 with Try.hyps

3305 have eq_s3_s2: "s3=s2" by simp

3306 moreover from sxalloc not_normal_s1 abrupt_no_break

3307 obtain "\<not> normal s2"

3308 "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l))"

3309 by - (rule sxalloc_cases,auto)

3310 ultimately obtain

3311 "?NormalAssigned s3 A" and "?BreakAssigned (Norm s0) s3 A"

3312 by (cases s2) auto

3313 moreover have "?ResAssigned (Norm s0) s3"

3314 proof (cases "abrupt s1 = Some (Jump Ret)")

3315 case True

3316 with sxalloc have "s2=s1"

3317 by (elim sxalloc_cases) auto

3318 with res_s1 eq_s3_s2 show ?thesis by simp

3319 next

3320 case False

3321 with sxalloc

3322 have "abrupt s2 \<noteq> Some (Jump Ret)"

3323 by (rule sxalloc_no_jump)

3324 with eq_s3_s2 show ?thesis

3325 by simp

3326 qed

3327 ultimately show ?thesis by (intro conjI)

3328 qed

3329 qed

3330 qed

3331 next

3332 -- {*

3333 \par

3334 *} (* dummy text command to break paragraph for latex;

3335 large paragraphs exhaust memory of debian pdflatex *)

3336 case (Fin c1 c2 s0 s1 s2 s3 x1 Env T A)

3337 have G: "prg Env = G" .

3338 from Fin.prems obtain C1 C2 where

3339 da_C1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

3340 da_C2: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

3341 nrm_A: "nrm A = nrm C1 \<union> nrm C2" and

3342 brk_A: "brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)"

3343 by (elim da_elim_cases) simp

3344 from Fin.prems obtain

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

3346 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

3347 by (elim wt_elim_cases)

3348 have "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)" .

3349 with wt_c1 da_C1 G

3350 obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and

3351 brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and

3352 resAss_s1: "?ResAssigned (Norm s0) (x1,s1)"

3353 by simp

3354 obtain nrmAss_C2: "?NormalAssigned s2 C2" and

3355 brkAss_C2: "?BreakAssigned (Norm s1) s2 C2" and

3356 resAss_s2: "?ResAssigned (Norm s1) s2"

3357 proof -

3358 from Fin.hyps

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

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

3361 by - (rule dom_locals_eval_mono_elim)

3362 with da_C2 obtain C2'

3363 where

3364 da_C2': "Env\<turnstile> dom (locals (store (x1,s1))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

3365 nrm_C2': "nrm C2 \<subseteq> nrm C2'" and

3366 brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"

3367 by (rule da_weakenE) simp

3368 have "PROP ?Hyp (In1r c2) (Norm s1) s2" .

3369 with wt_c2 da_C2' G

3370 obtain nrmAss_C2': "?NormalAssigned s2 C2'" and

3371 brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and

3372 resAss_s2': "?ResAssigned (Norm s1) s2"

3373 by simp

3374 from nrmAss_C2' nrm_C2' have "?NormalAssigned s2 C2"

3375 by blast

3376 moreover

3377 from brkAss_C2' brk_C2' have "?BreakAssigned (Norm s1) s2 C2"

3378 by fastsimp

3379 ultimately

3380 show ?thesis

3381 using that resAss_s2' by simp

3382 qed

3383 have s3: "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)

3384 else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .

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

3386 proof -

3387 have "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .

3388 thus ?thesis

3389 by (rule dom_locals_eval_mono_elim) simp

3390 qed

3392 have "?NormalAssigned s3 A"

3393 proof

3394 assume normal_s3: "normal s3"

3395 show "nrm A \<subseteq> dom (locals (snd s3))"

3396 proof -

3397 have "nrm C1 \<subseteq> dom (locals (snd s3))"

3398 proof -

3399 from normal_s3 s3

3400 have "normal (x1,s1)"

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

3402 with normal_s3 nrmAss_C1 s3 s1_s2

3403 show ?thesis

3404 by fastsimp

3405 qed

3406 moreover

3407 have "nrm C2 \<subseteq> dom (locals (snd s3))"

3408 proof -

3409 from normal_s3 s3

3410 have "normal s2"

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

3412 with normal_s3 nrmAss_C2 s3 s1_s2

3413 show ?thesis

3414 by fastsimp

3415 qed

3416 ultimately have "nrm C1 \<union> nrm C2 \<subseteq> \<dots>"

3417 by (rule Un_least)

3418 with nrm_A show ?thesis

3419 by simp

3420 qed

3421 qed

3422 moreover

3423 {

3424 fix l assume brk_s3: "abrupt s3 = Some (Jump (Break l))"

3425 have "brk A l \<subseteq> dom (locals (store s3))"

3426 proof (cases "normal s2")

3427 case True

3428 with brk_s3 s3

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

3430 by simp

3431 have "brk C1 l \<subseteq> dom (locals (store s3))"

3432 proof -

3433 from True brk_s3 s3 have "x1=Some (Jump (Break l))"

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

3435 with brkAss_C1 s1_s2 s2_s3

3436 show ?thesis

3437 by simp (blast intro: subset_trans)

3438 qed

3439 moreover from True nrmAss_C2 s2_s3

3440 have "nrm C2 \<subseteq> dom (locals (store s3))"

3441 by - (rule subset_trans, simp_all)

3442 ultimately

3443 have "((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) l \<subseteq> \<dots>"

3444 by blast

3445 with brk_A show ?thesis

3446 by simp blast

3447 next

3448 case False

3449 note not_normal_s2 = this

3450 have "s3=s2"

3451 proof (cases "normal (x1,s1)")

3452 case True with not_normal_s2 s3 show ?thesis

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

3454 next

3455 case False with not_normal_s2 s3 brk_s3 show ?thesis

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

3457 qed

3458 with brkAss_C2 brk_s3

3459 have "brk C2 l \<subseteq> dom (locals (store s3))"

3460 by simp

3461 with brk_A show ?thesis

3462 by simp blast

3463 qed

3464 }

3465 hence "?BreakAssigned (Norm s0) s3 A"

3466 by simp

3467 moreover

3468 {

3469 assume abr_s3: "abrupt s3 = Some (Jump Ret)"

3470 have "Result \<in> dom (locals (store s3))"

3471 proof (cases "x1 = Some (Jump Ret)")

3472 case True

3473 note ret_x1 = this

3474 with resAss_s1 have res_s1: "Result \<in> dom (locals s1)"

3475 by simp

3476 moreover have "dom (locals (store ((Norm s1)::state)))

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

3478 by (rule dom_locals_eval_mono_elim)

3479 ultimately have "Result \<in> dom (locals (store s2))"

3480 by - (rule subsetD,auto)

3481 with res_s1 s3 show ?thesis

3482 by simp

3483 next

3484 case False

3485 with s3 abr_s3 obtain "abrupt s2 = Some (Jump Ret)" and "s3=s2"

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

3487 with resAss_s2 show ?thesis

3488 by simp

3489 qed

3490 }

3491 hence "?ResAssigned (Norm s0) s3"

3492 by simp

3493 ultimately show ?case by (intro conjI)

3494 next

3495 case (Init C c s0 s1 s2 s3 Env T A)

3496 have G: "prg Env = G" .

3497 from Init.hyps

3498 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Init C\<rightarrow> s3"

3499 apply (simp only: G)

3500 apply (rule eval.Init, assumption)

3501 apply (cases "inited C (globs s0) ")

3502 apply simp

3503 apply (simp only: if_False )

3504 apply (elim conjE,intro conjI,assumption+,simp)

3505 done (* auto or simp alone always do too much *)

3506 have "the (class G C) = c" .

3507 with Init.prems

3508 have c: "class G C = Some c"

3509 by (elim wt_elim_cases) auto

3510 from Init.prems obtain

3511 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"

3512 by (elim da_elim_cases) simp

3513 show ?case

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

3515 case True

3516 with Init.hyps have "s3=Norm s0" by simp

3517 thus ?thesis

3518 using nrm_A by simp

3519 next

3520 case False

3521 from Init.hyps False G

3522 obtain eval_initC:

3523 "prg Env\<turnstile>Norm ((init_class_obj G C) s0)

3524 \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and

3525 eval_init: "prg Env\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and

3526 s3: "s3=(set_lvars (locals (store s1))) s2"

3527 by simp

3528 have "?NormalAssigned s3 A"

3529 proof

3530 show "nrm A \<subseteq> dom (locals (store s3))"

3531 proof -

3532 from nrm_A have "nrm A \<subseteq> dom (locals (init_class_obj G C s0))"

3533 by simp

3534 also from eval_initC have "\<dots> \<subseteq> dom (locals (store s1))"

3535 by (rule dom_locals_eval_mono_elim) simp

3536 also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"

3537 by (cases s1) (cases s2, simp add: init_lvars_def2)

3538 finally show ?thesis .

3539 qed

3540 qed

3541 moreover

3542 from eval

3543 have "\<And> j. abrupt s3 \<noteq> Some (Jump j)"

3544 by (rule eval_statement_no_jump) (auto simp add: wf c G)

3545 then obtain "?BreakAssigned (Norm s0) s3 A"

3546 and "?ResAssigned (Norm s0) s3"

3547 by simp

3548 ultimately show ?thesis by (intro conjI)

3549 qed

3550 next

3551 case (NewC C a s0 s1 s2 Env T A)

3552 have G: "prg Env = G" .

3553 from NewC.prems

3554 obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))"

3555 "brk A = (\<lambda> l. UNIV)"

3556 by (elim da_elim_cases) simp

3557 from wf NewC.prems

3558 have wt_init: "Env\<turnstile>(Init C)\<Colon>\<surd>"

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

3560 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s2))"

3561 proof -

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

3563 by (rule dom_locals_eval_mono_elim)

3564 also

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

3566 by (rule dom_locals_halloc_mono)

3567 finally show ?thesis .

3568 qed

3569 with A have "?NormalAssigned s2 A"

3570 by simp

3571 moreover

3572 {

3573 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3574 proof -

3575 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"

3576 by (simp only: G) (rule eval.NewC)

3577 from NewC.prems

3578 obtain T' where "T=Inl T'"

3579 by (elim wt_elim_cases) simp

3580 with NewC.prems have "Env\<turnstile>NewC C\<Colon>-T'"

3581 by simp

3582 from eval _ this

3583 show ?thesis

3584 by (rule eval_expression_no_jump) (simp_all add: G wf)

3585 qed

3586 }

3587 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3588 by simp_all

3589 ultimately show ?case by (intro conjI)

3590 next

3591 -- {*

3592 \par

3593 *} (* dummy text command to break paragraph for latex;

3594 large paragraphs exhaust memory of debian pdflatex *)

3595 case (NewA elT a e i s0 s1 s2 s3 Env T A)

3596 have G: "prg Env = G" .

3597 from NewA.prems obtain

3598 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3599 by (elim da_elim_cases)

3600 from NewA.prems obtain

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

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

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

3604 have halloc:"G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3".

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

3606 by (rule dom_locals_eval_mono_elim)

3607 with da_e obtain A' where

3608 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"

3609 and nrm_A_A': "nrm A \<subseteq> nrm A'"

3610 and brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"

3611 by (rule da_weakenE) simp

3612 have "PROP ?Hyp (In1l e) s1 s2" .

3613 with wt_size da_e' G obtain

3614 nrmAss_A': "?NormalAssigned s2 A'" and

3615 brkAss_A': "?BreakAssigned s1 s2 A'"

3616 by simp

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

3618 proof -

3619 have "dom (locals (store s2))

3620 \<subseteq> dom (locals (store (abupd (check_neg i) s2)))"

3621 by (simp)

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

3623 by (rule dom_locals_halloc_mono)

3624 finally show ?thesis .

3625 qed

3626 have "?NormalAssigned s3 A"

3627 proof

3628 assume normal_s3: "normal s3"

3629 show "nrm A \<subseteq> dom (locals (store s3))"

3630 proof -

3631 from halloc normal_s3

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

3633 by cases simp_all

3634 hence "normal s2"

3635 by (cases s2) simp

3636 with nrmAss_A' nrm_A_A' s2_s3 show ?thesis

3637 by blast

3638 qed

3639 qed

3640 moreover

3641 {

3642 fix j have "abrupt s3 \<noteq> Some (Jump j)"

3643 proof -

3644 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"

3645 by (simp only: G) (rule eval.NewA)

3646 from NewA.prems

3647 obtain T' where "T=Inl T'"

3648 by (elim wt_elim_cases) simp

3649 with NewA.prems have "Env\<turnstile>New elT[e]\<Colon>-T'"

3650 by simp

3651 from eval _ this

3652 show ?thesis

3653 by (rule eval_expression_no_jump) (simp_all add: G wf)

3654 qed

3655 }

3656 hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"

3657 by simp_all

3658 ultimately show ?case by (intro conjI)

3659 next

3660 case (Cast cT e s0 s1 s2 v Env T A)

3661 have G: "prg Env = G" .

3662 from Cast.prems obtain

3663 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3664 by (elim da_elim_cases)

3665 from Cast.prems obtain eT where

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

3667 by (elim wt_elim_cases)

3668 have "PROP ?Hyp (In1l e) (Norm s0) s1" .

3669 with wt_e da_e G obtain

3670 nrmAss_A: "?NormalAssigned s1 A" and

3671 brkAss_A: "?BreakAssigned (Norm s0) s1 A"

3672 by simp

3673 have s2: "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .

3674 hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"

3675 by simp

3676 have "?NormalAssigned s2 A"

3677 proof

3678 assume "normal s2"

3679 with s2 have "normal s1"

3680 by (cases s1) simp

3681 with nrmAss_A s1_s2

3682 show "nrm A \<subseteq> dom (locals (store s2))"

3683 by blast

3684 qed

3685 moreover

3686 {

3687 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3688 proof -

3689 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"

3690 by (simp only: G) (rule eval.Cast)

3691 from Cast.prems

3692 obtain T' where "T=Inl T'"

3693 by (elim wt_elim_cases) simp

3694 with Cast.prems have "Env\<turnstile>Cast cT e\<Colon>-T'"

3695 by simp

3696 from eval _ this

3697 show ?thesis

3698 by (rule eval_expression_no_jump) (simp_all add: G wf)

3699 qed

3700 }

3701 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3702 by simp_all

3703 ultimately show ?case by (intro conjI)

3704 next

3705 case (Inst iT b e s0 s1 v Env T A)

3706 have G: "prg Env = G" .

3707 from Inst.prems obtain

3708 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3709 by (elim da_elim_cases)

3710 from Inst.prems obtain eT where

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

3712 by (elim wt_elim_cases)

3713 have "PROP ?Hyp (In1l e) (Norm s0) s1" .

3714 with wt_e da_e G obtain

3715 "?NormalAssigned s1 A" and

3716 "?BreakAssigned (Norm s0) s1 A" and

3717 "?ResAssigned (Norm s0) s1"

3718 by simp

3719 thus ?case by (intro conjI)

3720 next

3721 case (Lit s v Env T A)

3722 from Lit.prems

3723 have "nrm A = dom (locals (store ((Norm s)::state)))"

3724 by (elim da_elim_cases) simp

3725 thus ?case by simp

3726 next

3727 case (UnOp e s0 s1 unop v Env T A)

3728 have G: "prg Env = G" .

3729 from UnOp.prems obtain

3730 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3731 by (elim da_elim_cases)

3732 from UnOp.prems obtain eT where

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

3734 by (elim wt_elim_cases)

3735 have "PROP ?Hyp (In1l e) (Norm s0) s1" .

3736 with wt_e da_e G obtain

3737 "?NormalAssigned s1 A" and

3738 "?BreakAssigned (Norm s0) s1 A" and

3739 "?ResAssigned (Norm s0) s1"

3740 by simp

3741 thus ?case by (intro conjI)

3742 next

3743 case (BinOp binop e1 e2 s0 s1 s2 v1 v2 Env T A)

3744 have G: "prg Env = G".

3745 from BinOp.hyps

3746 have

3747 eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"

3748 by (simp only: G) (rule eval.BinOp)

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

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

3751 by (rule dom_locals_eval_mono_elim)

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

3753 by (rule dom_locals_eval_mono_elim)

3754 finally

3755 have s0_s2: "dom (locals (store ((Norm s0)::state)))

3756 \<subseteq> dom (locals (store s2))" .

3757 from BinOp.prems obtain e1T e2T

3758 where wt_e1: "Env\<turnstile>e1\<Colon>-e1T"

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

3760 and wt_binop: "wt_binop (prg Env) binop e1T e2T"

3761 and T: "T=Inl (PrimT (binop_type binop))"

3762 by (elim wt_elim_cases) simp

3763 have "?NormalAssigned s2 A"

3764 proof

3765 assume normal_s2: "normal s2"

3766 have normal_s1: "normal s1"

3767 by (rule eval_no_abrupt_lemma [rule_format])

3768 show "nrm A \<subseteq> dom (locals (store s2))"

3769 proof (cases "binop=CondAnd")

3770 case True

3771 note CondAnd = this

3772 from BinOp.prems obtain

3773 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

3774 \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>

3775 assigns_if False (BinOp CondAnd e1 e2))"

3776 by (elim da_elim_cases) (simp_all add: CondAnd)

3777 from T BinOp.prems CondAnd

3778 have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean"

3779 by (simp)

3780 with eval normal_s2

3781 have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2))

3782 (BinOp binop e1 e2)

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

3784 by (rule assigns_if_good_approx)

3785 have "(assigns_if True (BinOp CondAnd e1 e2) \<inter>

3786 assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"

3787 proof (cases "the_Bool (eval_binop binop v1 v2)")

3788 case True

3789 with ass_if CondAnd

3790 have "assigns_if True (BinOp CondAnd e1 e2)

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

3792 by simp

3793 thus ?thesis by blast

3794 next

3795 case False

3796 with ass_if CondAnd

3797 have "assigns_if False (BinOp CondAnd e1 e2)

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

3799 by (simp only: False)

3800 thus ?thesis by blast

3801 qed

3802 with s0_s2

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

3804 \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>

3805 assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"

3806 by (rule Un_least)

3807 thus ?thesis by (simp only: nrm_A)

3808 next

3809 case False

3810 note notCondAnd = this

3811 show ?thesis

3812 proof (cases "binop=CondOr")

3813 case True

3814 note CondOr = this

3815 from BinOp.prems obtain

3816 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

3817 \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>

3818 assigns_if False (BinOp CondOr e1 e2))"

3819 by (elim da_elim_cases) (simp_all add: CondOr)

3820 from T BinOp.prems CondOr

3821 have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean"

3822 by (simp)

3823 with eval normal_s2

3824 have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2))

3825 (BinOp binop e1 e2)

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

3827 by (rule assigns_if_good_approx)

3828 have "(assigns_if True (BinOp CondOr e1 e2) \<inter>

3829 assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"

3830 proof (cases "the_Bool (eval_binop binop v1 v2)")

3831 case True

3832 with ass_if CondOr

3833 have "assigns_if True (BinOp CondOr e1 e2)

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

3835 by (simp)

3836 thus ?thesis by blast

3837 next

3838 case False

3839 with ass_if CondOr

3840 have "assigns_if False (BinOp CondOr e1 e2)

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

3842 by (simp)

3843 thus ?thesis by blast

3844 qed

3845 with s0_s2

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

3847 \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>

3848 assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"

3849 by (rule Un_least)

3850 thus ?thesis by (simp only: nrm_A)

3851 next

3852 case False

3853 with notCondAnd obtain notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"

3854 by simp

3855 from BinOp.prems obtain E1

3856 where da_e1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1"

3857 and da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"

3858 by (elim da_elim_cases) (simp_all add: notAndOr)

3859 have "PROP ?Hyp (In1l e1) (Norm s0) s1" .

3860 with wt_e1 da_e1 G normal_s1

3861 obtain "?NormalAssigned s1 E1"

3862 by simp

3863 with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by rules

3864 with da_e2 obtain A'

3865 where da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and

3866 nrm_A_A': "nrm A \<subseteq> nrm A'"

3867 by (rule da_weakenE) rules

3868 from notAndOr have "need_second_arg binop v1" by simp

3869 with BinOp.hyps

3870 have "PROP ?Hyp (In1l e2) s1 s2" by simp

3871 with wt_e2 da_e2' G

3872 obtain "?NormalAssigned s2 A'"

3873 by simp

3874 with nrm_A_A' normal_s2

3875 show "nrm A \<subseteq> dom (locals (store s2))"

3876 by blast

3877 qed

3878 qed

3879 qed

3880 moreover

3881 {

3882 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3883 proof -

3884 from BinOp.prems T

3885 have "Env\<turnstile>In1l (BinOp binop e1 e2)\<Colon>Inl (PrimT (binop_type binop))"

3886 by simp

3887 from eval _ this

3888 show ?thesis

3889 by (rule eval_expression_no_jump) (simp_all add: G wf)

3890 qed

3891 }

3892 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3893 by simp_all

3894 ultimately show ?case by (intro conjI)

3895 next

3896 -- {*

3897 \par

3898 *} (* dummy text command to break paragraph for latex;

3899 large paragraphs exhaust memory of debian pdflatex *)

3900 case (Super s Env T A)

3901 from Super.prems

3902 have "nrm A = dom (locals (store ((Norm s)::state)))"

3903 by (elim da_elim_cases) simp

3904 thus ?case by simp

3905 next

3906 case (Acc upd s0 s1 w v Env T A)

3907 show ?case

3908 proof (cases "\<exists> vn. v = LVar vn")

3909 case True

3910 then obtain vn where vn: "v=LVar vn"..

3911 from Acc.prems

3912 have "nrm A = dom (locals (store ((Norm s0)::state)))"

3913 by (simp only: vn) (elim da_elim_cases,simp_all)

3914 moreover have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .

3915 hence "s1=Norm s0"

3916 by (simp only: vn) (elim eval_elim_cases,simp)

3917 ultimately show ?thesis by simp

3918 next

3919 case False

3920 have G: "prg Env = G" .

3921 from False Acc.prems

3922 have da_v: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>v\<rangle>\<guillemotright> A"

3923 by (elim da_elim_cases) simp_all

3924 from Acc.prems obtain vT where

3925 wt_v: "Env\<turnstile>v\<Colon>=vT"

3926 by (elim wt_elim_cases)

3927 have "PROP ?Hyp (In2 v) (Norm s0) s1" .

3928 with wt_v da_v G obtain

3929 "?NormalAssigned s1 A" and

3930 "?BreakAssigned (Norm s0) s1 A" and

3931 "?ResAssigned (Norm s0) s1"

3932 by simp

3933 thus ?thesis by (intro conjI)

3934 qed

3935 next

3936 case (Ass e upd s0 s1 s2 v var w Env T A)

3937 have G: "prg Env = G" .

3938 from Ass.prems obtain varT eT where

3939 wt_var: "Env\<turnstile>var\<Colon>=varT" and

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

3941 by (elim wt_elim_cases) simp

3942 have eval_var: "prg Env\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1"

3943 using Ass.hyps by (simp only: G)

3944 have "?NormalAssigned (assign upd v s2) A"

3945 proof

3946 assume normal_ass_s2: "normal (assign upd v s2)"

3947 from normal_ass_s2

3948 have normal_s2: "normal s2"

3949 by (cases s2) (simp add: assign_def Let_def)

3950 hence normal_s1: "normal s1"

3951 by - (rule eval_no_abrupt_lemma [rule_format])

3952 have hyp_var: "PROP ?Hyp (In2 var) (Norm s0) s1" .

3953 have hyp_e: "PROP ?Hyp (In1l e) s1 s2" .

3954 show "nrm A \<subseteq> dom (locals (store (assign upd v s2)))"

3955 proof (cases "\<exists> vn. var = LVar vn")

3956 case True

3957 then obtain vn where vn: "var=LVar vn"..

3958 from Ass.prems obtain E where

3959 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

3960 nrm_A: "nrm A = nrm E \<union> {vn}"

3961 by (elim da_elim_cases) (insert vn,auto)

3962 obtain E' where

3963 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" and

3964 E_E': "nrm E \<subseteq> nrm E'"

3965 proof -

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

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

3968 by (rule dom_locals_eval_mono_elim)

3969 with da_e show ?thesis

3970 by (rule da_weakenE)

3971 qed

3972 from G eval_var vn

3973 have eval_lvar: "G\<turnstile>Norm s0 \<midarrow>LVar vn=\<succ>(w, upd)\<rightarrow> s1"

3974 by simp

3975 then have upd: "upd = snd (lvar vn (store s1))"

3976 by cases (cases "lvar vn (store s1)",simp)

3977 have "nrm E \<subseteq> dom (locals (store (assign upd v s2)))"

3978 proof -

3979 from hyp_e wt_e da_e' G normal_s2

3980 have "nrm E' \<subseteq> dom (locals (store s2))"

3981 by simp

3982 also

3983 from upd

3984 have "dom (locals (store s2)) \<subseteq> dom (locals (store (upd v s2)))"

3985 by (simp add: lvar_def) blast

3986 hence "dom (locals (store s2))

3987 \<subseteq> dom (locals (store (assign upd v s2)))"

3988 by (rule dom_locals_assign_mono)

3989 finally

3990 show ?thesis using E_E'

3991 by blast

3992 qed

3993 moreover

3994 from upd normal_s2

3995 have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"

3996 by (auto simp add: assign_def Let_def lvar_def upd split: split_split)

3997 ultimately

3998 show "nrm A \<subseteq> \<dots>"

3999 by (rule Un_least [elim_format]) (simp add: nrm_A)

4000 next

4001 case False

4002 from Ass.prems obtain V where

4003 da_var: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>var\<rangle>\<guillemotright> V" and

4004 da_e: "Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

4005 by (elim da_elim_cases) (insert False,simp+)

4006 from hyp_var wt_var da_var G normal_s1

4007 have "nrm V \<subseteq> dom (locals (store s1))"

4008 by simp

4009 with da_e obtain A'

4010 where da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and

4011 nrm_A_A': "nrm A \<subseteq> nrm A'"

4012 by (rule da_weakenE) rules

4013 from hyp_e wt_e da_e' G normal_s2

4014 obtain "nrm A' \<subseteq> dom (locals (store s2))"

4015 by simp

4016 with nrm_A_A' have "nrm A \<subseteq> \<dots>"

4017 by blast

4018 also have "\<dots> \<subseteq> dom (locals (store (assign upd v s2)))"

4019 proof -

4020 from eval_var normal_s1

4021 have "dom (locals (store s2)) \<subseteq> dom (locals (store (upd v s2)))"

4022 by (cases rule: dom_locals_eval_mono_elim)

4023 (cases s2, simp)

4024 thus ?thesis

4025 by (rule dom_locals_assign_mono)

4026 qed

4027 finally show ?thesis .

4028 qed

4029 qed

4030 moreover

4031 {

4032 fix j have "abrupt (assign upd v s2) \<noteq> Some (Jump j)"

4033 proof -

4034 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"

4035 by (simp only: G) (rule eval.Ass)

4036 from Ass.prems

4037 obtain T' where "T=Inl T'"

4038 by (elim wt_elim_cases) simp

4039 with Ass.prems have "Env\<turnstile>var:=e\<Colon>-T'" by simp

4040 from eval _ this

4041 show ?thesis

4042 by (rule eval_expression_no_jump) (simp_all add: G wf)

4043 qed

4044 }

4045 hence "?BreakAssigned (Norm s0) (assign upd v s2) A"

4046 and "?ResAssigned (Norm s0) (assign upd v s2)"

4047 by simp_all

4048 ultimately show ?case by (intro conjI)

4049 next

4050 -- {*

4051 \par

4052 *} (* dummy text command to break paragraph for latex;

4053 large paragraphs exhaust memory of debian pdflatex *)

4054 case (Cond b e0 e1 e2 s0 s1 s2 v Env T A)

4055 have G: "prg Env = G" .

4056 have "?NormalAssigned s2 A"

4057 proof

4058 assume normal_s2: "normal s2"

4059 show "nrm A \<subseteq> dom (locals (store s2))"

4060 proof (cases "Env\<turnstile>(e0 ? e1 : e2)\<Colon>-(PrimT Boolean)")

4061 case True

4062 with Cond.prems

4063 have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

4064 \<union> (assigns_if True (e0 ? e1 : e2) \<inter>

4065 assigns_if False (e0 ? e1 : e2))"

4066 by (elim da_elim_cases) simp_all

4067 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>(e0 ? e1 : e2)-\<succ>v\<rightarrow> s2"

4068 by (simp only: G) (rule eval.Cond)

4069 from eval

4070 have "dom (locals (store ((Norm s0)::state)))\<subseteq>dom (locals (store s2))"

4071 by (rule dom_locals_eval_mono_elim)

4072 moreover

4073 from eval normal_s2 True

4074 have ass_if: "assigns_if (the_Bool v) (e0 ? e1 : e2)

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

4076 by (rule assigns_if_good_approx)

4077 have "assigns_if True (e0 ? e1:e2) \<inter> assigns_if False (e0 ? e1:e2)

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

4079 proof (cases "the_Bool v")

4080 case True

4081 from ass_if

4082 have "assigns_if True (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"

4083 by (simp only: True)

4084 thus ?thesis by blast

4085 next

4086 case False

4087 from ass_if

4088 have "assigns_if False (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"

4089 by (simp only: False)

4090 thus ?thesis by blast

4091 qed

4092 ultimately show "nrm A \<subseteq> dom (locals (store s2))"

4093 by (simp only: nrm_A) (rule Un_least)

4094 next

4095 case False

4096 with Cond.prems obtain E1 E2 where

4097 da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

4098 \<union> assigns_if True e0) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and

4099 da_e2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

4100 \<union> assigns_if False e0) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2" and

4101 nrm_A: "nrm A = nrm E1 \<inter> nrm E2"

4102 by (elim da_elim_cases) simp_all

4103 from Cond.prems obtain e1T e2T where

4104 wt_e0: "Env\<turnstile>e0\<Colon>- PrimT Boolean" and

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

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

4107 by (elim wt_elim_cases)

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

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

4110 by (rule dom_locals_eval_mono_elim)

4111 have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" by (simp only: G)

4112 have normal_s1: "normal s1"

4113 by (rule eval_no_abrupt_lemma [rule_format])

4114 show ?thesis

4115 proof (cases "the_Bool b")

4116 case True

4117 from True Cond.hyps have "PROP ?Hyp (In1l e1) s1 s2" by simp

4118 moreover

4119 from eval_e0 normal_s1 wt_e0

4120 have "assigns_if True e0 \<subseteq> dom (locals (store s1))"

4121 by (rule assigns_if_good_approx [elim_format]) (simp only: True)

4122 with s0_s1

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

4124 \<union> assigns_if True e0 \<subseteq> \<dots>"

4125 by (rule Un_least)

4126 with da_e1 obtain E1' where

4127 da_e1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and

4128 nrm_E1_E1': "nrm E1 \<subseteq> nrm E1'"

4129 by (rule da_weakenE) rules

4130 ultimately have "nrm E1' \<subseteq> dom (locals (store s2))"

4131 using wt_e1 G normal_s2 by simp

4132 with nrm_E1_E1' show ?thesis

4133 by (simp only: nrm_A) blast

4134 next

4135 case False

4136 from False Cond.hyps have "PROP ?Hyp (In1l e2) s1 s2" by simp

4137 moreover

4138 from eval_e0 normal_s1 wt_e0

4139 have "assigns_if False e0 \<subseteq> dom (locals (store s1))"

4140 by (rule assigns_if_good_approx [elim_format]) (simp only: False)

4141 with s0_s1

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

4143 \<union> assigns_if False e0 \<subseteq> \<dots>"

4144 by (rule Un_least)

4145 with da_e2 obtain E2' where

4146 da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and

4147 nrm_E2_E2': "nrm E2 \<subseteq> nrm E2'"

4148 by (rule da_weakenE) rules

4149 ultimately have "nrm E2' \<subseteq> dom (locals (store s2))"

4150 using wt_e2 G normal_s2 by simp

4151 with nrm_E2_E2' show ?thesis

4152 by (simp only: nrm_A) blast

4153 qed

4154 qed

4155 qed

4156 moreover

4157 {

4158 fix j have "abrupt s2 \<noteq> Some (Jump j)"

4159 proof -

4160 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"

4161 by (simp only: G) (rule eval.Cond)

4162 from Cond.prems

4163 obtain T' where "T=Inl T'"

4164 by (elim wt_elim_cases) simp

4165 with Cond.prems have "Env\<turnstile>e0 ? e1 : e2\<Colon>-T'" by simp

4166 from eval _ this

4167 show ?thesis

4168 by (rule eval_expression_no_jump) (simp_all add: G wf)

4169 qed

4170 }

4171 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

4172 by simp_all

4173 ultimately show ?case by (intro conjI)

4174 next

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

4176 Env T A)

4177 have G: "prg Env = G" .

4178 have "?NormalAssigned (restore_lvars s2 s4) A"

4179 proof

4180 assume normal_restore_lvars: "normal (restore_lvars s2 s4)"

4181 show "nrm A \<subseteq> dom (locals (store (restore_lvars s2 s4)))"

4182 proof -

4183 from Call.prems obtain E where

4184 da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

4185 da_args: "Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A"

4186 by (elim da_elim_cases)

4187 from Call.prems obtain eT argsT where

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

4189 wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"

4190 by (elim wt_elim_cases)

4191 have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2" .

4192 have s3': "s3' = check_method_access G accC statT mode

4193 \<lparr>name=mn,parTs=pTs\<rparr> a s3" .

4194 have normal_s2: "normal s2"

4195 proof -

4196 from normal_restore_lvars have "normal s4"

4197 by simp

4198 then have "normal s3'"

4199 by - (rule eval_no_abrupt_lemma [rule_format])

4200 with s3' have "normal s3"

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

4202 with s3 show "normal s2"

4203 by (cases s2) (simp add: init_lvars_def Let_def)

4204 qed

4205 then have normal_s1: "normal s1"

4206 by - (rule eval_no_abrupt_lemma [rule_format])

4207 have "PROP ?Hyp (In1l e) (Norm s0) s1" .

4208 with da_e wt_e G normal_s1

4209 have "nrm E \<subseteq> dom (locals (store s1))"

4210 by simp

4211 with da_args obtain A' where

4212 da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and

4213 nrm_A_A': "nrm A \<subseteq> nrm A'"

4214 by (rule da_weakenE) rules

4215 have "PROP ?Hyp (In3 args) s1 s2" .

4216 with da_args' wt_args G normal_s2

4217 have "nrm A' \<subseteq> dom (locals (store s2))"

4218 by simp

4219 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4220 by blast

4221 also have "\<dots> \<subseteq> dom (locals (store (restore_lvars s2 s4)))"

4222 by (cases s4) simp

4223 finally show ?thesis .

4224 qed

4225 qed

4226 moreover

4227 {

4228 fix j have "abrupt (restore_lvars s2 s4) \<noteq> Some (Jump j)"

4229 proof -

4230 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v

4231 \<rightarrow> (restore_lvars s2 s4)"

4232 by (simp only: G) (rule eval.Call)

4233 from Call.prems

4234 obtain T' where "T=Inl T'"

4235 by (elim wt_elim_cases) simp

4236 with Call.prems have "Env\<turnstile>({accC,statT,mode}e\<cdot>mn( {pTs}args))\<Colon>-T'"

4237 by simp

4238 from eval _ this

4239 show ?thesis

4240 by (rule eval_expression_no_jump) (simp_all add: G wf)

4241 qed

4242 }

4243 hence "?BreakAssigned (Norm s0) (restore_lvars s2 s4) A"

4244 and "?ResAssigned (Norm s0) (restore_lvars s2 s4)"

4245 by simp_all

4246 ultimately show ?case by (intro conjI)

4247 next

4248 case (Methd D s0 s1 sig v Env T A)

4249 have G: "prg Env = G".

4250 from Methd.prems obtain m where

4251 m: "methd (prg Env) D sig = Some m" and

4252 da_body: "Env\<turnstile>(dom (locals (store ((Norm s0)::state))))

4253 \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A"

4254 by - (erule da_elim_cases)

4255 from Methd.prems m obtain

4256 isCls: "is_class (prg Env) D" and

4257 wt_body: "Env \<turnstile>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<Colon>T"

4258 by - (erule wt_elim_cases,simp)

4259 have "PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1" .

4260 moreover

4261 from wt_body have "Env\<turnstile>In1l (body G D sig)\<Colon>T"

4262 using isCls m G by (simp add: body_def2)

4263 moreover

4264 from da_body have "Env\<turnstile>(dom (locals (store ((Norm s0)::state))))

4265 \<guillemotright>\<langle>body G D sig\<rangle>\<guillemotright> A"

4266 using isCls m G by (simp add: body_def2)

4267 ultimately show ?case

4268 using G by simp

4269 next

4270 case (Body D c s0 s1 s2 s3 Env T A)

4271 have G: "prg Env = G" .

4272 from Body.prems

4273 have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"

4274 by (elim da_elim_cases) simp

4275 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)

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

4277 by (simp only: G) (rule eval.Body)

4278 hence "nrm A \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"

4279 by (simp only: nrm_A) (rule dom_locals_eval_mono_elim)

4280 hence "?NormalAssigned (abupd (absorb Ret) s3) A"

4281 by simp

4282 moreover

4283 from eval have "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"

4284 by (rule Body_no_jump) simp

4285 hence "?BreakAssigned (Norm s0) (abupd (absorb Ret) s3) A" and

4286 "?ResAssigned (Norm s0) (abupd (absorb Ret) s3)"

4287 by simp_all

4288 ultimately show ?case by (intro conjI)

4289 next

4290 -- {*

4291 \par

4292 *} (* dummy text command to break paragraph for latex;

4293 large paragraphs exhaust memory of debian pdflatex *)

4294 case (LVar s vn Env T A)

4295 from LVar.prems

4296 have "nrm A = dom (locals (store ((Norm s)::state)))"

4297 by (elim da_elim_cases) simp

4298 thus ?case by simp

4299 next

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

4301 have G: "prg Env = G" .

4302 have "?NormalAssigned s3 A"

4303 proof

4304 assume normal_s3: "normal s3"

4305 show "nrm A \<subseteq> dom (locals (store s3))"

4306 proof -

4307 have fvar: "(v, s2') = fvar statDeclC stat fn a s2" and

4308 s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .

4309 from FVar.prems

4310 have da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

4311 by (elim da_elim_cases)

4312 from FVar.prems obtain eT where

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

4314 by (elim wt_elim_cases)

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

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

4317 by (rule dom_locals_eval_mono_elim)

4318 with da_e obtain A' where

4319 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and

4320 nrm_A_A': "nrm A \<subseteq> nrm A'"

4321 by (rule da_weakenE) rules

4322 have normal_s2: "normal s2"

4323 proof -

4324 from normal_s3 s3

4325 have "normal s2'"

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

4327 with fvar

4328 show "normal s2"

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

4330 qed

4331 have "PROP ?Hyp (In1l e) s1 s2" .

4332 with da_e' wt_e G normal_s2

4333 have "nrm A' \<subseteq> dom (locals (store s2))"

4334 by simp

4335 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4336 by blast

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

4338 proof -

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

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

4341 hence "dom (locals (store s2)) \<subseteq> dom (locals (store s2'))"

4342 by (simp) (rule dom_locals_fvar_mono)

4343 also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"

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

4345 finally show ?thesis .

4346 qed

4347 finally show ?thesis .

4348 qed

4349 qed

4350 moreover

4351 {

4352 fix j have "abrupt s3 \<noteq> Some (Jump j)"

4353 proof -

4354 obtain w upd where v: "(w,upd)=v"

4355 by (cases v) auto

4356 have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"

4357 by (simp only: G v) (rule eval.FVar)

4358 from FVar.prems

4359 obtain T' where "T=Inl T'"

4360 by (elim wt_elim_cases) simp

4361 with FVar.prems have "Env\<turnstile>({accC,statDeclC,stat}e..fn)\<Colon>=T'"

4362 by simp

4363 from eval _ this

4364 show ?thesis

4365 by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)

4366 qed

4367 }

4368 hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"

4369 by simp_all

4370 ultimately show ?case by (intro conjI)

4371 next

4372 case (AVar a e1 e2 i s0 s1 s2 s2' v Env T A)

4373 have G: "prg Env = G" .

4374 have "?NormalAssigned s2' A"

4375 proof

4376 assume normal_s2': "normal s2'"

4377 show "nrm A \<subseteq> dom (locals (store s2'))"

4378 proof -

4379 have avar: "(v, s2') = avar G i a s2" .

4380 from AVar.prems obtain E1 where

4381 da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and

4382 da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"

4383 by (elim da_elim_cases)

4384 from AVar.prems obtain e1T e2T where

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

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

4387 by (elim wt_elim_cases)

4388 from avar normal_s2'

4389 have normal_s2: "normal s2"

4390 by (cases s2) (simp add: avar_def2)

4391 hence "normal s1"

4392 by - (rule eval_no_abrupt_lemma [rule_format])

4393 moreover have "PROP ?Hyp (In1l e1) (Norm s0) s1" .

4394 ultimately have "nrm E1 \<subseteq> dom (locals (store s1))"

4395 using da_e1 wt_e1 G by simp

4396 with da_e2 obtain A' where

4397 da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and

4398 nrm_A_A': "nrm A \<subseteq> nrm A'"

4399 by (rule da_weakenE) rules

4400 have "PROP ?Hyp (In1l e2) s1 s2" .

4401 with da_e2' wt_e2 G normal_s2

4402 have "nrm A' \<subseteq> dom (locals (store s2))"

4403 by simp

4404 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4405 by blast

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

4407 proof -

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

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

4410 thus "dom (locals (store s2)) \<subseteq> dom (locals (store s2'))"

4411 by (simp) (rule dom_locals_avar_mono)

4412 qed

4413 finally show ?thesis .

4414 qed

4415 qed

4416 moreover

4417 {

4418 fix j have "abrupt s2' \<noteq> Some (Jump j)"

4419 proof -

4420 obtain w upd where v: "(w,upd)=v"

4421 by (cases v) auto

4422 have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"

4423 by (simp only: G v) (rule eval.AVar)

4424 from AVar.prems

4425 obtain T' where "T=Inl T'"

4426 by (elim wt_elim_cases) simp

4427 with AVar.prems have "Env\<turnstile>(e1.[e2])\<Colon>=T'"

4428 by simp

4429 from eval _ this

4430 show ?thesis

4431 by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)

4432 qed

4433 }

4434 hence "?BreakAssigned (Norm s0) s2' A" and "?ResAssigned (Norm s0) s2'"

4435 by simp_all

4436 ultimately show ?case by (intro conjI)

4437 next

4438 case (Nil s0 Env T A)

4439 from Nil.prems

4440 have "nrm A = dom (locals (store ((Norm s0)::state)))"

4441 by (elim da_elim_cases) simp

4442 thus ?case by simp

4443 next

4444 case (Cons e es s0 s1 s2 v vs Env T A)

4445 have G: "prg Env = G" .

4446 have "?NormalAssigned s2 A"

4447 proof

4448 assume normal_s2: "normal s2"

4449 show "nrm A \<subseteq> dom (locals (store s2))"

4450 proof -

4451 from Cons.prems obtain E where

4452 da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

4453 da_es: "Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A"

4454 by (elim da_elim_cases)

4455 from Cons.prems obtain eT esT where

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

4457 wt_es: "Env\<turnstile>es\<Colon>\<doteq>esT"

4458 by (elim wt_elim_cases)

4459 have "normal s1"

4460 by - (rule eval_no_abrupt_lemma [rule_format])

4461 moreover have "PROP ?Hyp (In1l e) (Norm s0) s1" .

4462 ultimately have "nrm E \<subseteq> dom (locals (store s1))"

4463 using da_e wt_e G by simp

4464 with da_es obtain A' where

4465 da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and

4466 nrm_A_A': "nrm A \<subseteq> nrm A'"

4467 by (rule da_weakenE) rules

4468 have "PROP ?Hyp (In3 es) s1 s2" .

4469 with da_es' wt_es G normal_s2

4470 have "nrm A' \<subseteq> dom (locals (store s2))"

4471 by simp

4472 with nrm_A_A' show "nrm A \<subseteq> dom (locals (store s2))"

4473 by blast

4474 qed

4475 qed

4476 moreover

4477 {

4478 fix j have "abrupt s2 \<noteq> Some (Jump j)"

4479 proof -

4480 have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"

4481 by (simp only: G) (rule eval.Cons)

4482 from Cons.prems

4483 obtain T' where "T=Inr T'"

4484 by (elim wt_elim_cases) simp

4485 with Cons.prems have "Env\<turnstile>(e # es)\<Colon>\<doteq>T'"

4486 by simp

4487 from eval _ this

4488 show ?thesis

4489 by (rule eval_expression_list_no_jump) (simp_all add: G wf)

4490 qed

4491 }

4492 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

4493 by simp_all

4494 ultimately show ?case by (intro conjI)

4495 qed

4496 qed

4498 lemma da_good_approxE [consumes 4]:

4499 "\<lbrakk>prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1); Env\<turnstile>t\<Colon>T; Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A;

4500 wf_prog (prg Env);

4501 \<lbrakk>normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1));

4502 \<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>

4503 \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1));

4504 \<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>\<Longrightarrow>Result \<in> dom (locals (store s1))

4505 \<rbrakk> \<Longrightarrow> P

4506 \<rbrakk> \<Longrightarrow> P"

4507 by (drule (3) da_good_approx) simp

4510 (* Same as above but with explicit environment;

4511 It would be nicer to find a "normalized" way to right down those things

4512 in Bali.

4513 *)

4514 lemma da_good_approxE' [consumes 4]:

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

4516 and wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T"

4517 and da: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"

4518 and wf: "wf_prog G"

4519 and elim: "\<lbrakk>normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1));

4520 \<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>

4521 \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1));

4522 \<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>

4523 \<Longrightarrow>Result \<in> dom (locals (store s1))

4524 \<rbrakk> \<Longrightarrow> P"

4525 shows "P"

4526 proof -

4527 from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" by simp

4528 moreover note wt da

4529 moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp

4530 ultimately show ?thesis

4531 using elim by (rule da_good_approxE) rules+

4532 qed

4534 ML {*

4535 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]

4536 *}

4537 end