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

src/HOL/Bali/DefiniteAssignmentCorrect.thy

author | kuncar |

Fri Dec 09 18:07:04 2011 +0100 (2011-12-09) | |

changeset 45802 | b16f976db515 |

parent 44890 | 22f665a2e91c |

child 50710 | 32007a8db6bb |

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

Quotient_Info stores only relation maps

1 header {* Correctness of Definite Assignment *}

3 theory DefiniteAssignmentCorrect imports WellForm Eval begin

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

7 lemma sxalloc_no_jump:

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

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

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

11 using sxalloc no_jmp

12 by cases simp_all

14 lemma sxalloc_no_jump':

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

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

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

18 using sxalloc jump

19 by cases simp_all

21 lemma halloc_no_jump:

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

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

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

25 using halloc no_jmp

26 by cases simp_all

28 lemma halloc_no_jump':

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

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

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

32 using halloc jump

33 by cases simp_all

35 lemma Body_no_jump:

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

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

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

39 proof (cases "normal s0")

40 case True

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

42 s0: "s0 = Norm s0'"

43 by (cases s0) simp

44 from eval' obtain s2 where

45 s1: "s1 = abupd (absorb Ret)

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

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

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

49 by cases simp

50 show ?thesis

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

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

53 case True

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

55 by (cases s2) simp

56 thus ?thesis by simp

57 next

58 case False

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

60 by simp

61 with False show ?thesis

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

63 qed

64 next

65 case False

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

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

68 by (cases s0) fastforce

69 with this jump

70 show ?thesis

71 by (cases) (simp)

72 qed

74 lemma Methd_no_jump:

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

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

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

78 proof (cases "normal s0")

79 case True

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

81 "s0 = Norm s0'"

82 by (cases s0) simp

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

84 by (cases) (simp add: body_def2)

85 from this jump

86 show ?thesis

87 by (rule Body_no_jump)

88 next

89 case False

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

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

92 by (cases s0) fastforce

93 with this jump

94 show ?thesis

95 by (cases) (simp)

96 qed

98 lemma jumpNestingOkS_mono:

99 assumes jumpNestingOk_l': "jumpNestingOkS jmps' c"

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

101 shows "jumpNestingOkS jmps c"

102 proof -

103 have True and True and

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

105 and True

106 proof (induct rule: var_expr_stmt.inducts)

107 case (Lab j c jmps' jmps)

108 note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`

109 note jmps = `jmps' \<subseteq> jmps`

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

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

112 ultimately

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

114 by (rule Lab.hyps)

115 thus ?case

116 by simp

117 next

118 case (Jmp j jmps' jmps)

119 thus ?case

120 by (cases j) auto

121 next

122 case (Comp c1 c2 jmps' jmps)

123 from Comp.prems

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

125 moreover from Comp.prems

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

127 ultimately show ?case

128 by simp

129 next

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

131 from If'.prems

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

133 moreover from If'.prems

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

135 ultimately show ?case

136 by simp

137 next

138 case (Loop l e c jmps' jmps)

139 from `jumpNestingOkS jmps' (l\<bullet> While(e) c)`

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

141 moreover

142 from `jmps' \<subseteq> jmps`

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

144 ultimately

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

146 by (rule Loop.hyps)

147 thus ?case by simp

148 next

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

150 from TryC.prems

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

152 moreover from TryC.prems

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

154 ultimately show ?case

155 by simp

156 next

157 case (Fin c1 c2 jmps' jmps)

158 from Fin.prems

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

160 moreover from Fin.prems

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

162 ultimately show ?case

163 by simp

164 qed (simp_all)

165 with jumpNestingOk_l' subset

166 show ?thesis

167 by iprover

168 qed

170 corollary jumpNestingOk_mono:

171 assumes jmpOk: "jumpNestingOk jmps' t"

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

173 shows "jumpNestingOk jmps t"

174 proof (cases t)

175 case (In1 expr_stmt)

176 show ?thesis

177 proof (cases expr_stmt)

178 case (Inl e)

179 with In1 show ?thesis by simp

180 next

181 case (Inr s)

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

183 qed

184 qed (simp_all)

186 lemma assign_abrupt_propagation:

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

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

189 shows "abrupt s = x"

190 proof (cases x)

191 case None

192 with ass show ?thesis

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

194 next

195 case (Some xcpt)

196 from f_ok

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

198 by (cases "f n s")

199 with Some ass f_ok show ?thesis

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

201 qed

203 lemma wt_init_comp_ty':

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

205 apply (unfold init_comp_ty_def)

206 apply (clarsimp simp add: accessible_in_RefT_simp

207 is_acc_type_def is_acc_class_def)

208 done

210 lemma fvar_upd_no_jump:

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

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

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

214 proof (cases "stat")

215 case True

216 with noJmp upd

217 show ?thesis

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

219 next

220 case False

221 with noJmp upd

222 show ?thesis

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

224 qed

227 lemma avar_state_no_jump:

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

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

230 proof (cases "normal s")

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

232 next

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

234 qed

236 lemma avar_upd_no_jump:

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

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

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

240 using upd noJmp

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

244 text {*

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

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

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

248 cant leave its enclosing method.

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

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

251 and returns) are nested

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

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

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

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

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

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

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

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

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

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

263 proof, we can't just

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

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

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

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

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

270 *}

271 theorem jumpNestingOk_eval:

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

273 and jmpOk: "jumpNestingOk jmps t"

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

275 and wf: "wf_prog G"

276 and G: "prg Env = G"

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

278 (is "?Jmp jmps s0")

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

280 (normal s1 \<longrightarrow>

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

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

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

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

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

286 proof -

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

288 (\<forall> jmps T Env.

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

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

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

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

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

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

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

296 from eval

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

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

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

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

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

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

303 typing judgements. *}

304 proof (induct)

305 case Abrupt thus ?case by simp

306 next

307 case Skip thus ?case by simp

308 next

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

310 next

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

312 note jmpOK = `jumpNestingOk jmps (In1r (jmp\<bullet> c))`

313 note G = `prg Env = G`

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

315 using Lab.prems by (elim wt_elim_cases)

316 {

317 fix j

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

319 have "j\<in>jmps"

320 proof -

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

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

323 note hyp_c = `PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>`

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

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

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

327 proof -

328 from jmpOK

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

330 with wt_c jmp_s1 G hyp_c

331 show ?thesis

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

333 qed

334 ultimately show ?thesis

335 by simp

336 qed

337 }

338 thus ?case by simp

339 next

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

341 note jmpOk = `jumpNestingOk jmps (In1r (c1;; c2))`

342 note G = `prg Env = G`

343 from Comp.prems obtain

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

345 by (elim wt_elim_cases)

346 {

347 fix j

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

349 have "j\<in>jmps"

350 proof -

351 have jmp: "?Jmp jmps s1"

352 proof -

353 note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>`

354 with wt_c1 jmpOk G

355 show ?thesis by simp

356 qed

357 moreover note hyp_c2 = `PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)`

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

359 moreover note wt_c2 G abr_s2

360 ultimately show "j \<in> jmps"

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

362 qed

363 } thus ?case by simp

364 next

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

366 note jmpOk = `jumpNestingOk jmps (In1r (If(e) c1 Else c2))`

367 note G = `prg Env = G`

368 from If.prems obtain

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

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

371 by (elim wt_elim_cases) simp

372 {

373 fix j

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

375 have "j\<in>jmps"

376 proof -

377 note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`

378 with wt_e G have "?Jmp jmps s1"

379 by simp

380 moreover note hyp_then_else =

381 `PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>`

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

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

384 moreover note wt_then_else G jmp

385 ultimately show "j\<in> jmps"

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

387 qed

388 }

389 thus ?case by simp

390 next

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

392 note jmpOk = `jumpNestingOk jmps (In1r (l\<bullet> While(e) c))`

393 note G = `prg Env = G`

394 note wt = `Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`

395 then obtain

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

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

398 by (elim wt_elim_cases)

399 {

400 fix j

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

402 have "j\<in>jmps"

403 proof -

404 note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`

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

406 by simp

407 show ?thesis

408 proof (cases "the_Bool b")

409 case False

410 from Loop.hyps

411 have "s3=s1"

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

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

414 thus ?thesis by simp

415 next

416 case True

417 from Loop.hyps

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

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

420 leaves the hypothesis in object logic *)

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

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

423 apply (erule conjE)+

424 apply assumption

425 done

426 note hyp_c = this [rule_format (no_asm)]

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

428 by simp

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

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

431 using wt_c G by iprover

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

433 proof -

434 {

435 fix j'

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

437 have "j' \<in> jmps"

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

439 case True

440 with abs show ?thesis

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

442 next

443 case False

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

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

446 with jmp_s2 False show ?thesis

447 by simp

448 qed

449 }

450 thus ?thesis by simp

451 qed

452 moreover

453 from Loop.hyps

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

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

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

457 apply (erule conjE)+

458 apply assumption

459 done

460 note hyp_w = this [rule_format (no_asm)]

461 note jmpOk wt G jmp

462 ultimately show "j\<in> jmps"

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

464 qed

465 qed

466 }

467 thus ?case by simp

468 next

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

470 next

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

472 note jmpOk = `jumpNestingOk jmps (In1r (Throw e))`

473 note G = `prg Env = G`

474 from Throw.prems obtain Te where

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

476 by (elim wt_elim_cases)

477 {

478 fix j

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

480 have "j\<in>jmps"

481 proof -

482 from `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`

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

484 moreover

485 from jmp

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

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

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

489 qed

490 }

491 thus ?case by simp

492 next

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

494 note jmpOk = `jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))`

495 note G = `prg Env = G`

496 from Try.prems obtain

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

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

499 by (elim wt_elim_cases)

500 {

501 fix j

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

503 have "j\<in>jmps"

504 proof -

505 note `PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)`

506 with jmpOk wt_c1 G

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

508 note s2 = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`

509 show "j \<in> jmps"

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

511 case False

512 from Try.hyps have "s3=s2"

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

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

515 using sxalloc_no_jump' [OF s2] by simp

516 with jmp_s1

517 show ?thesis by simp

518 next

519 case True

520 with Try.hyps

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

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

523 apply (erule conjE)+

524 apply assumption

525 done

526 note hyp_c2 = this [rule_format (no_asm)]

527 from jmp_s1 sxalloc_no_jump' [OF s2]

528 have "?Jmp jmps s2"

529 by simp

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

531 by (cases s2) simp

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

533 moreover note wt_c2

534 moreover from G

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

536 by simp

537 moreover note jmp

538 ultimately show ?thesis

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

540 qed

541 qed

542 }

543 thus ?case by simp

544 next

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

546 note jmpOk = `jumpNestingOk jmps (In1r (c1 Finally c2))`

547 note G = `prg Env = G`

548 from Fin.prems obtain

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

550 by (elim wt_elim_cases)

551 {

552 fix j

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

554 have "j \<in> jmps"

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

556 case True

557 note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>`

558 with True jmpOk wt_c1 G show ?thesis

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

560 next

561 case False

562 note hyp_c2 = `PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>`

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

564 else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`

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

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

567 with jmpOk wt_c2 G show ?thesis

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

569 qed

570 }

571 thus ?case by simp

572 next

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

574 note `jumpNestingOk jmps (In1r (Init C))`

575 note G = `prg Env = G`

576 note `the (class G C) = c`

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

578 by (elim wt_elim_cases) auto

579 {

580 fix j

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

582 have "j\<in>jmps"

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

584 case True

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

586 by simp

587 with jmp

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

589 next

590 case False

591 from wf c G

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

593 by (simp add: wf_prog_cdecl)

594 from Init.hyps

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

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

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

598 apply (erule conjE)+

599 apply assumption

600 done

601 note hyp_s1 = this [rule_format (no_asm)]

602 from wf_cdecl G have

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

604 by (cases "C=Object")

605 (auto dest: wf_cdecl_supD is_acc_classD)

606 from hyp_s1 [OF _ _ wt_super G]

607 have "?Jmp jmps s1"

608 by simp

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

610 from False Init.hyps

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

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

613 apply (erule conjE)+

614 apply assumption

615 done

616 note hyp_init_c = this [rule_format (no_asm)]

617 from wf_cdecl

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

619 by (rule wf_cdecl_wt_init)

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

621 by (cases rule: wf_cdeclE)

622 hence "jumpNestingOkS jmps (init c)"

623 by (rule jumpNestingOkS_mono) simp

624 moreover

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

626 proof -

627 from False Init.hyps

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

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

630 qed

631 ultimately show ?thesis

632 using hyp_init_c [OF jmp_s1 _ wt_init_c]

633 by simp

634 qed

635 }

636 thus ?case by simp

637 next

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

639 {

640 fix j

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

642 have "j\<in>jmps"

643 proof -

644 note `prg Env = G`

645 moreover note hyp_init = `PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>`

646 moreover from wf NewC.prems

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

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

649 moreover

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

651 proof -

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

653 by (rule halloc_no_jump')

654 qed

655 ultimately show "j \<in> jmps"

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

657 qed

658 }

659 thus ?case by simp

660 next

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

662 {

663 fix j

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

665 have "j\<in>jmps"

666 proof -

667 note G = `prg Env = G`

668 from NewA.prems

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

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

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

672 note `PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>`

673 with wt_init G

674 have "?Jmp jmps s1"

675 by (simp add: init_comp_ty_def)

676 moreover

677 note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 i)`

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

679 proof -

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

681 moreover note jmp

682 ultimately

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

684 by (rule halloc_no_jump')

685 thus ?thesis by (cases s2) auto

686 qed

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

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

689 qed

690 }

691 thus ?case by simp

692 next

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

694 {

695 fix j

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

697 have "j\<in>jmps"

698 proof -

699 note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`

700 note `prg Env = G`

701 moreover from Cast.prems

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

703 moreover

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

705 proof -

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

707 moreover note jmp

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

709 qed

710 ultimately show ?thesis

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

712 qed

713 }

714 thus ?case by simp

715 next

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

717 {

718 fix j

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

720 have "j\<in>jmps"

721 proof -

722 note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`

723 note `prg Env = G`

724 moreover from Inst.prems

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

726 moreover note jmp

727 ultimately show "j\<in>jmps"

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

729 qed

730 }

731 thus ?case by simp

732 next

733 case Lit thus ?case by simp

734 next

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

736 {

737 fix j

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

739 have "j\<in>jmps"

740 proof -

741 note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`

742 note `prg Env = G`

743 moreover from UnOp.prems

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

745 moreover note jmp

746 ultimately show "j\<in>jmps"

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

748 qed

749 }

750 thus ?case by simp

751 next

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

753 {

754 fix j

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

756 have "j\<in>jmps"

757 proof -

758 note G = `prg Env = G`

759 from BinOp.prems

760 obtain e1T e2T where

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

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

763 by (elim wt_elim_cases)

764 note `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)`

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

766 note hyp_e2 =

767 `PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)

768 s1 s2 (In1 v2)`

769 show "j\<in>jmps"

770 proof (cases "need_second_arg binop v1")

771 case True with jmp_s1 wt_e2 jmp G

772 show ?thesis

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

774 next

775 case False with jmp_s1 jmp G

776 show ?thesis

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

778 qed

779 qed

780 }

781 thus ?case by simp

782 next

783 case Super thus ?case by simp

784 next

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

786 {

787 fix j

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

789 have "j\<in>jmps"

790 proof -

791 note hyp_va = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))`

792 note `prg Env = G`

793 moreover from Acc.prems

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

795 moreover note jmp

796 ultimately show "j\<in>jmps"

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

798 qed

799 }

800 thus ?case by simp

801 next

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

803 note G = `prg Env = G`

804 from Ass.prems

805 obtain vT eT where

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

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

808 by (elim wt_elim_cases)

809 note hyp_v = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))`

810 note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 v)`

811 {

812 fix j

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

814 have "j\<in>jmps"

815 proof -

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

817 proof (cases "normal s2")

818 case True

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

820 by (rule eval_no_abrupt_lemma [rule_format])

821 with nrm_s1 wt_va G True

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

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

824 by simp

825 from this jmp

826 show ?thesis

827 by (rule assign_abrupt_propagation)

828 next

829 case False with jmp

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

831 qed

832 moreover from wt_va G

833 have "?Jmp jmps s1"

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

835 ultimately show ?thesis using G

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

837 qed

838 }

839 thus ?case by simp

840 next

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

842 note G = `prg Env = G`

843 note hyp_e0 = `PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)`

844 note hyp_e1_e2 = `PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)`

845 from Cond.prems

846 obtain e1T e2T

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

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

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

850 by (elim wt_elim_cases)

851 {

852 fix j

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

854 have "j\<in>jmps"

855 proof -

856 from wt_e0 G

857 have jmp_s1: "?Jmp jmps s1"

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

859 show ?thesis

860 proof (cases "the_Bool b")

861 case True

862 with jmp_s1 wt_e1 G jmp

863 show ?thesis

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

865 next

866 case False

867 with jmp_s1 wt_e2 G jmp

868 show ?thesis

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

870 qed

871 qed

872 }

873 thus ?case by simp

874 next

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

876 jmps T Env)

877 note G = `prg Env = G`

878 from Call.prems

879 obtain eT argsT

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

881 by (elim wt_elim_cases)

882 {

883 fix j

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

885 = Some (Jump j)"

886 have "j\<in>jmps"

887 proof -

888 note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`

889 from wt_e G

890 have jmp_s1: "?Jmp jmps s1"

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

892 note hyp_args = `PROP ?Hyp (In3 args) s1 s2 (In3 vs)`

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

894 proof -

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

896 moreover

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

898 by (cases s4) simp

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

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

901 moreover note `s3' = check_method_access G accC statT mode

902 \<lparr>name = mn, parTs = pTs\<rparr> a s3`

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

904 by (cases s3)

905 (simp add: check_method_access_def abrupt_if_def Let_def)

906 moreover

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

908 ultimately show ?thesis

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

910 qed

911 with jmp_s1 wt_args G

912 show ?thesis

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

914 qed

915 }

916 thus ?case by simp

917 next

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

919 from `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`

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

921 by (rule eval.Methd)

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

923 by (rule Methd_no_jump) simp

924 thus ?case by simp

925 next

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

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

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

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

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

931 by (rule Body_no_jump) simp

932 thus ?case by simp

933 next

934 case LVar

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

936 next

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

938 note G = `prg Env = G`

939 from wf FVar.prems

940 obtain statC f where

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

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

943 by (elim wt_elim_cases) simp

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

945 proof -

946 from wf wt_e G

947 have "is_class (prg Env) statC"

948 by (auto dest: ty_expr_is_type type_is_class)

949 with wf accfield G

950 have "is_class (prg Env) statDeclC"

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

952 thus ?thesis

953 by simp

954 qed

955 note fvar = `(v, s2') = fvar statDeclC stat fn a s2`

956 {

957 fix j

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

959 have "j\<in>jmps"

960 proof -

961 note hyp_init = `PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>`

962 from G wt_init

963 have "?Jmp jmps s1"

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

965 moreover

966 note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 a)`

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

968 proof -

969 note `s3 = check_field_access G accC statDeclC fn stat a s2'`

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

971 by (cases s2')

972 (simp add: check_field_access_def abrupt_if_def Let_def)

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

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

975 qed

976 ultimately show ?thesis

977 using G wt_e

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

979 qed

980 }

981 moreover

982 from fvar obtain upd w

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

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

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

986 {

987 fix j val fix s::state

988 assume "normal s3"

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

990 with upd

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

992 by (rule fvar_upd_no_jump)

993 }

994 ultimately show ?case using v by simp

995 next

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

997 note G = `prg Env = G`

998 from AVar.prems

999 obtain e1T e2T where

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

1001 by (elim wt_elim_cases) simp

1002 note avar = `(v, s2') = avar G i a s2`

1003 {

1004 fix j

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

1006 have "j\<in>jmps"

1007 proof -

1008 note hyp_e1 = `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)`

1009 from G wt_e1

1010 have "?Jmp jmps s1"

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

1012 moreover

1013 note hyp_e2 = `PROP ?Hyp (In1l e2) s1 s2 (In1 i)`

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

1015 proof -

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

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

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

1019 qed

1020 ultimately show ?thesis

1021 using wt_e2 G

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

1023 qed

1024 }

1025 moreover

1026 from avar obtain upd w

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

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

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

1030 {

1031 fix j val fix s::state

1032 assume "normal s2'"

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

1034 with upd

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

1036 by (rule avar_upd_no_jump)

1037 }

1038 ultimately show ?case using v by simp

1039 next

1040 case Nil thus ?case by simp

1041 next

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

1043 note G = `prg Env = G`

1044 from Cons.prems obtain eT esT

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

1046 by (elim wt_elim_cases) simp

1047 {

1048 fix j

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

1050 have "j\<in>jmps"

1051 proof -

1052 note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`

1053 from G wt_e

1054 have "?Jmp jmps s1"

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

1056 moreover

1057 note hyp_es = `PROP ?Hyp (In3 es) s1 s2 (In3 vs)`

1058 ultimately show ?thesis

1059 using wt_e2 G jmp

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

1061 (assumption|simp (no_asm_simp))+)

1062 qed

1063 }

1064 thus ?case by simp

1065 qed

1066 note generalized = this

1067 from no_jmp jmpOk wt G

1068 show ?thesis

1069 by (rule generalized)

1070 qed

1072 lemmas jumpNestingOk_evalE = jumpNestingOk_eval [THEN conjE,rule_format]

1075 lemma jumpNestingOk_eval_no_jump:

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

1077 jmpOk: "jumpNestingOk {} t" and

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

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

1080 wf: "wf_prog (prg Env)"

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

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

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

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

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

1086 case True

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

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

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

1090 with no_jmp jmp show ?thesis by simp

1091 next

1092 case False

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

1094 by (cases Env) simp

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

1096 moreover note jmpOk wt

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

1098 moreover note G

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

1100 by simp

1101 ultimately show ?thesis

1102 apply (rule jumpNestingOk_evalE)

1103 apply assumption

1104 apply simp

1105 apply fastforce

1106 done

1107 qed

1109 lemmas jumpNestingOk_eval_no_jumpE

1110 = jumpNestingOk_eval_no_jump [THEN conjE,rule_format]

1112 corollary eval_expression_no_jump:

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

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

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

1116 wf: "wf_prog (prg Env)"

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

1118 using eval _ no_jmp wt wf

1119 by (rule jumpNestingOk_eval_no_jumpE, simp_all)

1121 corollary eval_var_no_jump:

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

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

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

1125 wf: "wf_prog (prg Env)"

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

1127 (normal s1 \<longrightarrow>

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

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

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

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

1132 by simp_all

1134 lemmas eval_var_no_jumpE = eval_var_no_jump [THEN conjE,rule_format]

1136 corollary eval_statement_no_jump:

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

1138 jmpOk: "jumpNestingOkS {} c" and

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

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

1141 wf: "wf_prog (prg Env)"

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

1143 using eval _ no_jmp wt wf

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

1146 corollary eval_expression_list_no_jump:

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

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

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

1150 wf: "wf_prog (prg Env)"

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

1152 using eval _ no_jmp wt wf

1153 by (rule jumpNestingOk_eval_no_jumpE, simp_all)

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

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

1157 by blast

1159 lemma dom_locals_halloc_mono:

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

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

1162 proof -

1163 from halloc show ?thesis

1164 by cases simp_all

1165 qed

1167 lemma dom_locals_sxalloc_mono:

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

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

1170 proof -

1171 from sxalloc show ?thesis

1172 proof (cases)

1173 case Norm thus ?thesis by simp

1174 next

1175 case Jmp thus ?thesis by simp

1176 next

1177 case Error thus ?thesis by simp

1178 next

1179 case XcptL thus ?thesis by simp

1180 next

1181 case SXcpt thus ?thesis

1182 by - (drule dom_locals_halloc_mono,simp)

1183 qed

1184 qed

1187 lemma dom_locals_assign_mono:

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

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

1190 proof (cases "normal s")

1191 case False thus ?thesis

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

1193 next

1194 case True

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

1196 by auto

1197 moreover

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

1199 by (cases "f n s")

1200 ultimately

1201 show ?thesis

1202 using f_ok

1203 by (simp add: assign_def Let_def)

1204 qed

1206 (*

1207 lemma dom_locals_init_lvars_mono:

1208 "dom (locals (store s))

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

1210 proof (cases "mode = Static")

1211 case True

1212 thus ?thesis

1213 apply (cases s)

1214 apply (simp add: init_lvars_def Let_def)

1215 *)

1217 lemma dom_locals_lvar_mono:

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

1219 by (simp add: lvar_def) blast

1222 lemma dom_locals_fvar_vvar_mono:

1223 "dom (locals (store s))

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

1225 proof (cases stat)

1226 case True

1227 thus ?thesis

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

1229 next

1230 case False

1231 thus ?thesis

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

1233 qed

1235 lemma dom_locals_fvar_mono:

1236 "dom (locals (store s))

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

1238 proof (cases stat)

1239 case True

1240 thus ?thesis

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

1242 next

1243 case False

1244 thus ?thesis

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

1246 qed

1249 lemma dom_locals_avar_vvar_mono:

1250 "dom (locals (store s))

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

1252 by (cases s, simp add: avar_def2)

1254 lemma dom_locals_avar_mono:

1255 "dom (locals (store s))

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

1257 by (cases s, simp add: avar_def2)

1259 text {*

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

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

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

1263 complicated second part of the conjunction in the goal.

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

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

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

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

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

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

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

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

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

1273 lemma dom_locals_eval_mono:

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

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

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

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

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

1279 proof -

1280 from eval show ?thesis

1281 proof (induct)

1282 case Abrupt thus ?case by simp

1283 next

1284 case Skip thus ?case by simp

1285 next

1286 case Expr thus ?case by simp

1287 next

1288 case Lab thus ?case by simp

1289 next

1290 case (Comp s0 c1 s1 c2 s2)

1291 from Comp.hyps

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

1293 by simp

1294 also

1295 from Comp.hyps

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

1297 by simp

1298 finally show ?case by simp

1299 next

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

1301 from If.hyps

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

1303 by simp

1304 also

1305 from If.hyps

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

1307 by simp

1308 finally show ?case by simp

1309 next

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

1311 show ?case

1312 proof (cases "the_Bool b")

1313 case True

1314 with Loop.hyps

1315 obtain

1316 s0_s1:

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

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

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

1320 by simp

1321 note s0_s1 also note s1_s2 also note s2_s3

1322 finally show ?thesis

1323 by simp

1324 next

1325 case False

1326 with Loop.hyps show ?thesis

1327 by simp

1328 qed

1329 next

1330 case Jmp thus ?case by simp

1331 next

1332 case Throw thus ?case by simp

1333 next

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

1335 then

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

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

1338 from `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`

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

1340 by (rule dom_locals_sxalloc_mono)

1341 thus ?case

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

1343 case True

1344 note s0_s1 also note s1_s2

1345 also

1346 from True Try.hyps

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

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

1349 by simp

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

1351 by (cases s2, simp )

1352 finally show ?thesis by simp

1353 next

1354 case False

1355 note s0_s1 also note s1_s2

1356 finally

1357 show ?thesis

1358 using False Try.hyps by simp

1359 qed

1360 next

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

1362 show ?case

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

1364 case True

1365 with Fin.hyps show ?thesis

1366 by simp

1367 next

1368 case False

1369 from Fin.hyps

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

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

1372 by simp

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

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

1375 by simp

1376 also

1377 from Fin.hyps

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

1379 by simp

1380 finally show ?thesis

1381 using Fin.hyps by simp

1382 qed

1383 next

1384 case (Init C c s0 s3 s1 s2)

1385 show ?case

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

1387 case True

1388 with Init.hyps show ?thesis by simp

1389 next

1390 case False

1391 with Init.hyps

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

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

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

1395 by simp

1396 from s0_s1

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

1398 by (cases s0) simp

1399 with s3

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

1401 by (cases s2) simp

1402 thus ?thesis by simp

1403 qed

1404 next

1405 case (NewC s0 C s1 a s2)

1406 note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`

1407 from NewC.hyps

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

1409 by simp

1410 also

1411 from halloc

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

1413 finally show ?case by simp

1414 next

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

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

1417 from NewA.hyps

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

1419 by simp

1420 also

1421 from NewA.hyps

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

1423 also

1424 from halloc

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

1426 by (rule dom_locals_halloc_mono [elim_format]) simp

1427 finally show ?case by simp

1428 next

1429 case Cast thus ?case by simp

1430 next

1431 case Inst thus ?case by simp

1432 next

1433 case Lit thus ?case by simp

1434 next

1435 case UnOp thus ?case by simp

1436 next

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

1438 from BinOp.hyps

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

1440 by simp

1441 also

1442 from BinOp.hyps

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

1444 finally show ?case by simp

1445 next

1446 case Super thus ?case by simp

1447 next

1448 case Acc thus ?case by simp

1449 next

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

1451 from Ass.hyps

1452 have s0_s1:

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

1454 by simp

1455 show ?case

1456 proof (cases "normal s1")

1457 case True

1458 with Ass.hyps

1459 have ass_ok:

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

1461 by simp

1462 note s0_s1

1463 also

1464 from Ass.hyps

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

1466 by simp

1467 also

1468 from ass_ok

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

1470 by (rule dom_locals_assign_mono)

1471 finally show ?thesis by simp

1472 next

1473 case False

1474 with `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`

1475 have "s2=s1"

1476 by auto

1477 with s0_s1 False

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

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

1480 by simp

1481 thus ?thesis

1482 by simp

1483 qed

1484 next

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

1486 from Cond.hyps

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

1488 by simp

1489 also

1490 from Cond.hyps

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

1492 by simp

1493 finally show ?case by simp

1494 next

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

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

1497 from Call.hyps

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

1499 by simp

1500 also

1501 from Call.hyps

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

1503 by simp

1504 also

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

1506 by (cases s4) simp

1507 finally show ?case by simp

1508 next

1509 case Methd thus ?case by simp

1510 next

1511 case (Body s0 D s1 c s2 s3)

1512 from Body.hyps

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

1514 by simp

1515 also

1516 from Body.hyps

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

1518 by simp

1519 also

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

1521 by simp

1522 also

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

1524 proof -

1525 from `s3 =

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

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

1528 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`

1529 show ?thesis

1530 by simp

1531 qed

1532 finally show ?case by simp

1533 next

1534 case LVar

1535 thus ?case

1536 using dom_locals_lvar_mono

1537 by simp

1538 next

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

1540 from FVar.hyps

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

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

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

1544 from v

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

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

1547 by (simp add: dom_locals_fvar_vvar_mono)

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

1549 by - (intro strip, simp)

1550 note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`

1551 from FVar.hyps

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

1553 by simp

1554 also

1555 from FVar.hyps

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

1557 by simp

1558 also

1559 from s2'

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

1561 by (simp add: dom_locals_fvar_mono)

1562 also

1563 from s3

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

1565 by (simp add: check_field_access_def Let_def)

1566 finally

1567 show ?case

1568 using v_ok

1569 by simp

1570 next

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

1572 from AVar.hyps

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

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

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

1576 from v

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

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

1579 by (simp add: dom_locals_avar_vvar_mono)

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

1581 by - (intro strip, simp)

1582 from AVar.hyps

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

1584 by simp

1585 also

1586 from AVar.hyps

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

1588 by simp

1589 also

1590 from s2'

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

1592 by (simp add: dom_locals_avar_mono)

1593 finally

1594 show ?case using v_ok by simp

1595 next

1596 case Nil thus ?case by simp

1597 next

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

1599 from Cons.hyps

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

1601 by simp

1602 also

1603 from Cons.hyps

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

1605 by simp

1606 finally show ?case by simp

1607 qed

1608 qed

1610 lemma dom_locals_eval_mono_elim:

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

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

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

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

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

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

1618 lemma halloc_no_abrupt:

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

1620 normal: "normal s1"

1621 shows "normal s0"

1622 proof -

1623 from halloc normal show ?thesis

1624 by cases simp_all

1625 qed

1627 lemma sxalloc_mono_no_abrupt:

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

1629 normal: "normal s1"

1630 shows "normal s0"

1631 proof -

1632 from sxalloc normal show ?thesis

1633 by cases simp_all

1634 qed

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

1637 by blast

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

1640 by blast

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

1643 by blast

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

1646 by blast

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

1649 by blast

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

1652 by blast

1654 lemma assigns_good_approx:

1655 assumes

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

1657 normal: "normal s1"

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

1659 proof -

1660 from eval normal show ?thesis

1661 proof (induct)

1662 case Abrupt thus ?case by simp

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

1664 case Skip show ?case by simp

1665 next

1666 case Expr show ?case by simp

1667 next

1668 case Lab show ?case by simp

1669 next

1670 case Comp show ?case by simp

1671 next

1672 case If show ?case by simp

1673 next

1674 case Loop show ?case by simp

1675 next

1676 case Jmp show ?case by simp

1677 next

1678 case Throw show ?case by simp

1679 next

1680 case Try show ?case by simp

1681 next

1682 case Fin show ?case by simp

1683 next

1684 case Init show ?case by simp

1685 next

1686 case NewC show ?case by simp

1687 next

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

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

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

1691 proof -

1692 from NewA

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

1694 by - (erule halloc_no_abrupt [rule_format])

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

1696 with NewA.hyps

1697 show ?thesis by iprover

1698 qed

1699 also

1700 from halloc

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

1702 by (rule dom_locals_halloc_mono [elim_format]) simp

1703 finally show ?case by simp

1704 next

1705 case (Cast s0 e v s1 s2 T)

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

1707 with Cast.hyps

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

1709 by simp

1710 also

1711 from Cast.hyps

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

1713 by simp

1714 finally

1715 show ?case

1716 by simp

1717 next

1718 case Inst thus ?case by simp

1719 next

1720 case Lit thus ?case by simp

1721 next

1722 case UnOp thus ?case by simp

1723 next

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

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

1726 with BinOp.hyps

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

1728 by iprover

1729 also

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

1731 proof -

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

1733 else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`

1734 thus ?thesis

1735 by (rule dom_locals_eval_mono_elim)

1736 qed

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

1738 show ?case

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

1740 case True

1741 with s2 show ?thesis by simp

1742 next

1743 case False

1744 with BinOp

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

1746 by (simp add: need_second_arg_def)

1747 with s2

1748 show ?thesis using False by simp

1749 qed

1750 next

1751 case Super thus ?case by simp

1752 next

1753 case Acc thus ?case by simp

1754 next

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

1756 note nrm_ass_s2 = `normal (assign f v s2)`

1757 hence nrm_s2: "normal s2"

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

1759 with Ass.hyps

1760 have nrm_s1: "normal s1"

1761 by - (erule eval_no_abrupt_lemma [rule_format])

1762 with Ass.hyps

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

1764 by iprover

1765 also

1766 from Ass.hyps

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

1768 by - (erule dom_locals_eval_mono_elim)

1769 also

1770 from nrm_s2 Ass.hyps

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

1772 by iprover

1773 ultimately

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

1775 by (rule Un_least)

1776 also

1777 from Ass.hyps nrm_s1

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

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

1780 then

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

1782 by (rule dom_locals_assign_mono)

1783 finally

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

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

1786 show ?case

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

1788 case False

1789 with va_e show ?thesis

1790 by (simp add: Un_assoc)

1791 next

1792 case True

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

1794 by blast

1795 with Ass.hyps

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

1797 by simp

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

1799 by (rule eval_elim_cases) simp

1800 with nrm_ass_s2

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

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

1803 with va_e True va

1804 show ?thesis by (simp add: Un_assoc)

1805 qed

1806 next

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

1808 hence "normal s1"

1809 by - (erule eval_no_abrupt_lemma [rule_format])

1810 with Cond.hyps

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

1812 by iprover

1813 also from Cond.hyps

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

1815 by - (erule dom_locals_eval_mono_elim)

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

1817 show ?case

1818 proof (cases "the_Bool b")

1819 case True

1820 with Cond

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

1822 by simp

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

1824 by blast

1825 with e0

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

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

1828 by (rule Un_least)

1829 thus ?thesis using True by simp

1830 next

1831 case False

1832 with Cond

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

1834 by simp

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

1836 by blast

1837 with e0

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

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

1840 by (rule Un_least)

1841 thus ?thesis using False by simp

1842 qed

1843 next

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

1845 have nrm_s2: "normal s2"

1846 proof -

1847 from `normal ((set_lvars (locals (snd s2))) s4)`

1848 have normal_s4: "normal s4" by simp

1849 hence "normal s3'" using Call.hyps

1850 by - (erule eval_no_abrupt_lemma [rule_format])

1851 moreover note

1852 `s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3`

1853 ultimately have "normal s3"

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

1855 moreover

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

1857 ultimately show "normal s2"

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

1859 qed

1860 hence "normal s1" using Call.hyps

1861 by - (erule eval_no_abrupt_lemma [rule_format])

1862 with Call.hyps

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

1864 by iprover

1865 also from Call.hyps

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

1867 by - (erule dom_locals_eval_mono_elim)

1868 also

1869 from nrm_s2 Call.hyps

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

1871 by iprover

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

1873 by (rule Un_least)

1874 also

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

1876 by (cases s4) simp

1877 finally show ?case

1878 by simp

1879 next

1880 case Methd thus ?case by simp

1881 next

1882 case Body thus ?case by simp

1883 next

1884 case LVar thus ?case by simp

1885 next

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

1887 note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`

1888 note avar = `(v, s2') = fvar statDeclC stat fn a s2`

1889 have nrm_s2: "normal s2"

1890 proof -

1891 note `normal s3`

1892 with s3 have "normal s2'"

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

1894 with avar show "normal s2"

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

1896 qed

1897 with FVar.hyps

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

1899 by iprover

1900 also

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

1902 proof -

1903 from avar

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

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

1906 thus ?thesis

1907 by simp (rule dom_locals_fvar_mono)

1908 qed

1909 also from s3

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

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

1912 finally show ?case

1913 by simp

1914 next

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

1916 note avar = `(v, s2') = avar G i a s2`

1917 have nrm_s2: "normal s2"

1918 proof -

1919 from avar and `normal s2'`

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

1921 qed

1922 with AVar.hyps

1923 have "normal s1"

1924 by - (erule eval_no_abrupt_lemma [rule_format])

1925 with AVar.hyps

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

1927 by iprover

1928 also from AVar.hyps

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

1930 by - (erule dom_locals_eval_mono_elim)

1931 also

1932 from AVar.hyps nrm_s2

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

1934 by iprover

1935 ultimately

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

1937 by (rule Un_least)

1938 also

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

1940 proof -

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

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

1943 thus ?thesis

1944 by simp (rule dom_locals_avar_mono)

1945 qed

1946 finally

1947 show ?case

1948 by simp

1949 next

1950 case Nil show ?case by simp

1951 next

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

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

1954 proof -

1955 from Cons

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

1957 with Cons.hyps show ?thesis by iprover

1958 qed

1959 also from Cons.hyps

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

1961 by - (erule dom_locals_eval_mono_elim)

1962 also from Cons

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

1964 by iprover

1965 ultimately

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

1967 by (rule Un_least)

1968 thus ?case

1969 by simp

1970 qed

1971 qed

1973 corollary assignsE_good_approx:

1974 assumes

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

1976 normal: "normal s1"

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

1978 proof -

1979 from eval normal show ?thesis

1980 by (rule assigns_good_approx [elim_format]) simp

1981 qed

1983 corollary assignsV_good_approx:

1984 assumes

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

1986 normal: "normal s1"

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

1988 proof -

1989 from eval normal show ?thesis

1990 by (rule assigns_good_approx [elim_format]) simp

1991 qed

1993 corollary assignsEs_good_approx:

1994 assumes

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

1996 normal: "normal s1"

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

1998 proof -

1999 from eval normal show ?thesis

2000 by (rule assigns_good_approx [elim_format]) simp

2001 qed

2003 lemma constVal_eval:

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

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

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

2007 proof -

2008 have True and

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

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

2011 and True and True

2012 proof (induct rule: var_expr_stmt.inducts)

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

2014 next

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

2016 next

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

2018 next

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

2020 next

2021 case (Lit val c v s0 s)

2022 note `constVal (Lit val) = Some c`

2023 moreover

2024 from `G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s`

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

2026 by cases simp

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

2028 next

2029 case (UnOp unop e c v s0 s)

2030 note const = `constVal (UnOp unop e) = Some c`

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

2032 from `G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s`

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

2034 v: "v = eval_unop unop ve"

2035 by cases simp

2036 from ce ve

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

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

2039 from eq_ve_ce const ce v

2040 have "v=c"

2041 by simp

2042 from this nrm_s

2043 show ?case ..

2044 next

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

2046 note const = `constVal (BinOp binop e1 e2) = Some c`

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

2048 c2: "constVal e2 = Some c2" and

2049 c: "c = eval_binop binop c1 c2"

2050 by simp

2051 from `G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s`

2052 obtain v1 s1 v2

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

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

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

2056 v: "v = eval_binop binop v1 v2"

2057 by cases simp

2058 from c1 v1

2059 obtain eq_v1_c1: "v1 = c1" and

2060 nrm_s1: "normal s1"

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

2062 show ?case

2063 proof (cases "need_second_arg binop v1")

2064 case True

2065 with v2 nrm_s1 obtain s1'

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

2067 by (cases s1) simp

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

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

2070 with c c1 c2 eq_v1_c1 v

2071 show ?thesis by simp

2072 next

2073 case False

2074 with nrm_s1 v2

2075 have "s=s1"

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

2077 moreover

2078 from False c v eq_v1_c1

2079 have "v = c"

2080 by (simp add: eval_binop_arg2_indep)

2081 ultimately

2082 show ?thesis

2083 using nrm_s1 by simp

2084 qed (* hallo ehco *)

2085 next

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

2087 next

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

2089 next

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

2091 next

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

2093 note c = `constVal (b ? e1 : e2) = Some c`

2094 then obtain cb c1 c2 where

2095 cb: "constVal b = Some cb" and

2096 c1: "constVal e1 = Some c1" and

2097 c2: "constVal e2 = Some c2"

2098 by (auto split: bool.splits)

2099 from `G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s`

2100 obtain vb s1

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

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

2103 by cases simp

2104 from cb vb

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

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

2107 show ?case

2108 proof (cases "the_Bool vb")

2109 case True

2110 with c cb c1 eq_vb_cb

2111 have "c = c1"

2112 by simp

2113 moreover

2114 from True eval_v nrm_s1 obtain s1'

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

2116 by (cases s1) simp

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

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

2119 ultimately show ?thesis by simp

2120 next

2121 case False

2122 with c cb c2 eq_vb_cb

2123 have "c = c2"

2124 by simp

2125 moreover

2126 from False eval_v nrm_s1 obtain s1'

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

2128 by (cases s1) simp

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

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

2131 ultimately show ?thesis by simp

2132 qed

2133 next

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

2135 qed simp_all

2136 with const eval

2137 show ?thesis

2138 by iprover

2139 qed

2141 lemmas constVal_eval_elim = constVal_eval [THEN conjE]

2143 lemma eval_unop_type:

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

2145 by (cases unop) simp_all

2147 lemma eval_binop_type:

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

2149 by (cases binop) simp_all

2151 lemma constVal_Boolean:

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

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

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

2155 proof -

2156 have True and

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

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

2159 and True and True

2160 proof (induct rule: var_expr_stmt.inducts)

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

2162 next

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

2164 next

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

2166 next

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

2168 next

2169 case (Lit v c)

2170 from `constVal (Lit v) = Some c`

2171 have "c=v" by simp

2172 moreover

2173 from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`

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

2175 by cases simp

2176 ultimately show ?case by simp

2177 next

2178 case (UnOp unop e c)

2179 from `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`

2180 have "Boolean = unop_type unop" by cases simp

2181 moreover

2182 from `constVal (UnOp unop e) = Some c`

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

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

2185 next

2186 case (BinOp binop e1 e2 c)

2187 from `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`

2188 have "Boolean = binop_type binop" by cases simp

2189 moreover

2190 from `constVal (BinOp binop e1 e2) = Some c`

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

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

2193 next

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

2195 next

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

2197 next

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

2199 next

2200 case (Cond b e1 e2 c)

2201 note c = `constVal (b ? e1 : e2) = Some c`

2202 then obtain cb c1 c2 where

2203 cb: "constVal b = Some cb" and

2204 c1: "constVal e1 = Some c1" and

2205 c2: "constVal e2 = Some c2"

2206 by (auto split: bool.splits)

2207 note wt = `Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean`

2208 then

2209 obtain T1 T2

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

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

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

2213 by cases (auto dest: widen_Boolean2)

2214 show ?case

2215 proof (cases "the_Bool cb")

2216 case True

2217 from c1 wt_e1

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

2219 by (rule Cond.hyps)

2220 with True c cb c1 show ?thesis by simp

2221 next

2222 case False

2223 from c2 wt_e2

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

2225 by (rule Cond.hyps)

2226 with False c cb c2 show ?thesis by simp

2227 qed

2228 next

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

2230 qed simp_all

2231 with const wt

2232 show ?thesis

2233 by iprover

2234 qed

2236 lemma assigns_if_good_approx:

2237 assumes

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

2239 normal: "normal s1" and

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

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

2242 proof -

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

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

2245 { fix t val

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

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

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

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

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

2251 using eval' normal bool' expr

2252 proof (induct)

2253 case Abrupt thus ?case by simp

2254 next

2255 case (NewC s0 C s1 a s2)

2256 from `Env\<turnstile>NewC C\<Colon>-PrimT Boolean`

2257 have False

2258 by cases simp

2259 thus ?case ..

2260 next

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

2262 from `Env\<turnstile>New T[e]\<Colon>-PrimT Boolean`

2263 have False

2264 by cases simp

2265 thus ?case ..

2266 next

2267 case (Cast s0 e b s1 s2 T)

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

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

2270 proof -

2271 from s2 and `normal s2`

2272 have "normal s1"

2273 by (cases s1) simp

2274 moreover

2275 from `Env\<turnstile>Cast T e\<Colon>-PrimT Boolean`

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

2277 by cases (auto dest: cast_Boolean2)

2278 ultimately show ?thesis

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

2280 qed

2281 also from s2

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

2283 by simp

2284 finally show ?case by simp

2285 next

2286 case (Inst s0 e v s1 b T)

2287 from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1` and `normal s1`

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

2289 by (rule assignsE_good_approx)

2290 thus ?case

2291 by simp

2292 next

2293 case (Lit s v)

2294 from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`

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

2296 by cases simp

2297 then obtain b where "v=Bool b"

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

2299 thus ?case

2300 by simp

2301 next

2302 case (UnOp s0 e v s1 unop)

2303 note bool = `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`

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

2305 by cases (cases unop,simp_all)

2306 show ?case

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

2308 case None

2309 note `normal s1`

2310 moreover note bool_e

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

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

2313 moreover

2314 from bool have "unop = UNot"

2315 by cases (cases unop, simp_all)

2316 moreover note None

2317 ultimately

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

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

2320 by simp

2321 thus ?thesis by simp

2322 next

2323 case (Some c)

2324 moreover

2325 from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`

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

2327 by (rule eval.UnOp)

2328 with Some

2329 have "eval_unop unop v=c"

2330 by (rule constVal_eval_elim) simp

2331 moreover

2332 from Some bool

2333 obtain b where "c=Bool b"

2334 by (rule constVal_Boolean [elim_format])

2335 (cases c, simp_all add: empty_dt_def)

2336 ultimately

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

2338 by simp

2339 thus ?thesis by simp

2340 qed

2341 next

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

2343 note bool = `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`

2344 show ?case

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

2346 case (Some c)

2347 moreover

2348 from BinOp.hyps

2349 have

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

2351 by - (rule eval.BinOp)

2352 with Some

2353 have "eval_binop binop v1 v2=c"

2354 by (rule constVal_eval_elim) simp

2355 moreover

2356 from Some bool

2357 obtain b where "c = Bool b"

2358 by (rule constVal_Boolean [elim_format])

2359 (cases c, simp_all add: empty_dt_def)

2360 ultimately

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

2362 = {}"

2363 by simp

2364 thus ?thesis by simp

2365 next

2366 case None

2367 show ?thesis

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

2369 case True

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

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

2372 using True by cases auto

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

2374 proof -

2375 from BinOp have "normal s1"

2376 by - (erule eval_no_abrupt_lemma [rule_format])

2377 from this bool_e1

2378 show ?thesis

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

2380 qed

2381 also

2382 from BinOp.hyps

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

2384 by - (erule dom_locals_eval_mono_elim,simp)

2385 finally

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

2387 from True show ?thesis

2388 proof

2389 assume condAnd: "binop = CondAnd"

2390 show ?thesis

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

2392 case True

2393 with condAnd

2394 have need_second: "need_second_arg binop v1"

2395 by (simp add: need_second_arg_def)

2396 from `normal s2`

2397 have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2398 by (rule BinOp.hyps [elim_format])

2399 (simp add: need_second bool_e2)+

2400 with e1_s2

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

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

2403 by (rule Un_least)

2404 with True condAnd None show ?thesis

2405 by simp

2406 next

2407 case False

2408 note binop_False = this

2409 show ?thesis

2410 proof (cases "need_second_arg binop v1")

2411 case True

2412 with binop_False condAnd

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

2414 by (simp add: need_second_arg_def)

2415 moreover

2416 from `normal s2`

2417 have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

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

2419 with e1_s2

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

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

2422 by (rule Un_least)

2423 moreover note binop_False condAnd None

2424 ultimately show ?thesis

2425 by auto

2426 next

2427 case False

2428 with binop_False condAnd

2429 have "the_Bool v1=False"

2430 by (simp add: need_second_arg_def)

2431 with e1_s2

2432 show ?thesis

2433 using binop_False condAnd None by auto

2434 qed

2435 qed

2436 next

2437 assume condOr: "binop = CondOr"

2438 show ?thesis

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

2440 case False

2441 with condOr

2442 have need_second: "need_second_arg binop v1"

2443 by (simp add: need_second_arg_def)

2444 from `normal s2`

2445 have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

2446 by (rule BinOp.hyps [elim_format])

2447 (simp add: need_second bool_e2)+

2448 with e1_s2

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

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

2451 by (rule Un_least)

2452 with False condOr None show ?thesis

2453 by simp

2454 next

2455 case True

2456 note binop_True = this

2457 show ?thesis

2458 proof (cases "need_second_arg binop v1")

2459 case True

2460 with binop_True condOr

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

2462 by (simp add: need_second_arg_def)

2463 moreover

2464 from `normal s2`

2465 have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"

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

2467 with e1_s2

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

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

2470 by (rule Un_least)

2471 moreover note binop_True condOr None

2472 ultimately show ?thesis

2473 by auto

2474 next

2475 case False

2476 with binop_True condOr

2477 have "the_Bool v1=True"

2478 by (simp add: need_second_arg_def)

2479 with e1_s2

2480 show ?thesis

2481 using binop_True condOr None by auto

2482 qed

2483 qed

2484 qed

2485 next

2486 case False

2487 note `\<not> (binop = CondAnd \<or> binop = CondOr)`

2488 from BinOp.hyps

2489 have

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

2491 by - (rule eval.BinOp)

2492 moreover note `normal s2`

2493 ultimately

2494 have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"

2495 by (rule assignsE_good_approx)

2496 with False None

2497 show ?thesis

2498 by simp

2499 qed

2500 qed

2501 next

2502 case Super

2503 note `Env\<turnstile>Super\<Colon>-PrimT Boolean`

2504 hence False

2505 by cases simp

2506 thus ?case ..

2507 next

2508 case (Acc s0 va v f s1)

2509 from `prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1` and `normal s1`

2510 have "assignsV va \<subseteq> dom (locals (store s1))"

2511 by (rule assignsV_good_approx)

2512 thus ?case by simp

2513 next

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

2515 hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"

2516 by - (rule eval.Ass)

2517 moreover note `normal (assign f v s2)`

2518 ultimately

2519 have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"

2520 by (rule assignsE_good_approx)

2521 thus ?case by simp

2522 next

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

2524 from `Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean`

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

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

2527 by cases (auto dest: widen_Boolean2)

2528 note eval_e0 = `prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`

2529 have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"

2530 proof -

2531 note eval_e0

2532 moreover

2533 from Cond.hyps and `normal s2` have "normal s1"

2534 by - (erule eval_no_abrupt_lemma [rule_format],simp)

2535 ultimately

2536 have "assignsE e0 \<subseteq> dom (locals (store s1))"

2537 by (rule assignsE_good_approx)

2538 also

2539 from Cond

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

2541 by - (erule dom_locals_eval_mono [elim_format],simp)

2542 finally show ?thesis .

2543 qed

2544 show ?case

2545 proof (cases "constVal e0")

2546 case None

2547 have "assigns_if (the_Bool v) e1 \<inter> assigns_if (the_Bool v) e2

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

2549 proof (cases "the_Bool b")

2550 case True

2551 from `normal s2`

2552 have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"

2553 by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)

2554 thus ?thesis

2555 by blast

2556 next

2557 case False

2558 from `normal s2`

2559 have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"

2560 by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)

2561 thus ?thesis

2562 by blast

2563 qed

2564 with e0_s2

2565 have "assignsE e0 \<union>

2566 (assigns_if (the_Bool v) e1 \<inter> assigns_if (the_Bool v) e2)

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

2568 by (rule Un_least)

2569 with None show ?thesis

2570 by simp

2571 next

2572 case (Some c)

2573 from this eval_e0 have eq_b_c: "b=c"

2574 by (rule constVal_eval_elim)

2575 show ?thesis

2576 proof (cases "the_Bool c")

2577 case True

2578 from `normal s2`

2579 have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"

2580 by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1)

2581 with e0_s2

2582 have "assignsE e0 \<union> assigns_if (the_Bool v) e1 \<subseteq> \<dots>"

2583 by (rule Un_least)

2584 with Some True show ?thesis

2585 by simp

2586 next

2587 case False

2588 from `normal s2`

2589 have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"

2590 by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2)

2591 with e0_s2

2592 have "assignsE e0 \<union> assigns_if (the_Bool v) e2 \<subseteq> \<dots>"

2593 by (rule Un_least)

2594 with Some False show ?thesis

2595 by simp

2596 qed

2597 qed

2598 next

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

2600 hence

2601 "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v\<rightarrow>

2602 (set_lvars (locals (store s2)) s4)"

2603 by - (rule eval.Call)

2604 hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args))

2605 \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"

2606 using `normal ((set_lvars (locals (snd s2))) s4)`

2607 by (rule assignsE_good_approx)

2608 thus ?case by simp

2609 next

2610 case Methd show ?case by simp

2611 next

2612 case Body show ?case by simp

2613 qed simp+ -- {* all the statements and variables *}

2614 }

2615 note generalized = this

2616 from eval bool show ?thesis

2617 by (rule generalized [elim_format]) simp+

2618 qed

2620 lemma assigns_if_good_approx':

2621 assumes eval: "G\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1"

2622 and normal: "normal s1"

2623 and bool: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>- (PrimT Boolean)"

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

2625 proof -

2626 from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp

2627 from this normal bool show ?thesis

2628 by (rule assigns_if_good_approx)

2629 qed

2632 lemma subset_Intl: "A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"

2633 by blast

2635 lemma subset_Intr: "B \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C"

2636 by blast

2638 lemma da_good_approx:

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

2640 wt: "Env\<turnstile>t\<Colon>T" (is "?Wt Env t T") and

2641 da: "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" (is "?Da Env s0 t A") and

2642 wf: "wf_prog (prg Env)"

2643 shows "(normal s1 \<longrightarrow> (nrm A \<subseteq> dom (locals (store s1)))) \<and>

2644 (\<forall> l. abrupt s1 = Some (Jump (Break l)) \<and> normal s0

2645 \<longrightarrow> (brk A l \<subseteq> dom (locals (store s1)))) \<and>

2646 (abrupt s1 = Some (Jump Ret) \<and> normal s0

2647 \<longrightarrow> Result \<in> dom (locals (store s1)))"

2648 (is "?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1")

2649 proof -

2650 note inj_term_simps [simp]

2651 obtain G where G: "prg Env = G" by (cases Env) simp

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

2653 from G wf have wf: "wf_prog G" by simp

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

2655 \<forall> Env T A. ?Wt Env t T \<longrightarrow> ?Da Env s0 t A \<longrightarrow> prg Env = G

2656 \<longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1"

2657 -- {* Goal in object logic variant *}

2658 let ?Hyp = "\<lambda>t s0 s1. (\<And> Env T A. \<lbrakk>?Wt Env t T; ?Da Env s0 t A; prg Env = G\<rbrakk>

2659 \<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1)"

2660 from eval and wt da G

2661 show ?thesis

2662 proof (induct arbitrary: Env T A)

2663 case (Abrupt xc s t Env T A)

2664 have da: "Env\<turnstile> dom (locals s) \<guillemotright>t\<guillemotright> A" using Abrupt.prems by simp

2665 have "?NormalAssigned (Some xc,s) A"

2666 by simp

2667 moreover

2668 have "?BreakAssigned (Some xc,s) (Some xc,s) A"

2669 by simp

2670 moreover have "?ResAssigned (Some xc,s) (Some xc,s)"

2671 by simp

2672 ultimately show ?case by (intro conjI)

2673 next

2674 case (Skip s Env T A)

2675 have da: "Env\<turnstile> dom (locals (store (Norm s))) \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"

2676 using Skip.prems by simp

2677 hence "nrm A = dom (locals (store (Norm s)))"

2678 by (rule da_elim_cases) simp

2679 hence "?NormalAssigned (Norm s) A"

2680 by auto

2681 moreover

2682 have "?BreakAssigned (Norm s) (Norm s) A"

2683 by simp

2684 moreover have "?ResAssigned (Norm s) (Norm s)"

2685 by simp

2686 ultimately show ?case by (intro conjI)

2687 next

2688 case (Expr s0 e v s1 Env T A)

2689 from Expr.prems

2690 show "?NormalAssigned s1 A \<and> ?BreakAssigned (Norm s0) s1 A

2691 \<and> ?ResAssigned (Norm s0) s1"

2692 by (elim wt_elim_cases da_elim_cases)

2693 (rule Expr.hyps, auto)

2694 next

2695 case (Lab s0 c s1 j Env T A)

2696 note G = `prg Env = G`

2697 from Lab.prems

2698 obtain C l where

2699 da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and

2700 A: "nrm A = nrm C \<inter> (brk C) l" "brk A = rmlab l (brk C)" and

2701 j: "j = Break l"

2702 by - (erule da_elim_cases, simp)

2703 from Lab.prems

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

2705 by - (erule wt_elim_cases, simp)

2706 from wt_c da_c G and Lab.hyps

2707 have norm_c: "?NormalAssigned s1 C" and

2708 brk_c: "?BreakAssigned (Norm s0) s1 C" and

2709 res_c: "?ResAssigned (Norm s0) s1"

2710 by simp_all

2711 have "?NormalAssigned (abupd (absorb j) s1) A"

2712 proof

2713 assume normal: "normal (abupd (absorb j) s1)"

2714 show "nrm A \<subseteq> dom (locals (store (abupd (absorb j) s1)))"

2715 proof (cases "abrupt s1")

2716 case None

2717 with norm_c A

2718 show ?thesis

2719 by auto

2720 next

2721 case Some

2722 with normal j

2723 have "abrupt s1 = Some (Jump (Break l))"

2724 by (auto dest: absorb_Some_NoneD)

2725 with brk_c A

2726 show ?thesis

2727 by auto

2728 qed

2729 qed

2730 moreover

2731 have "?BreakAssigned (Norm s0) (abupd (absorb j) s1) A"

2732 proof -

2733 {

2734 fix l'

2735 assume break: "abrupt (abupd (absorb j) s1) = Some (Jump (Break l'))"

2736 with j

2737 have "l\<noteq>l'"

2738 by (cases s1) (auto dest!: absorb_Some_JumpD)

2739 hence "(rmlab l (brk C)) l'= (brk C) l'"

2740 by (simp)

2741 with break brk_c A

2742 have

2743 "(brk A l' \<subseteq> dom (locals (store (abupd (absorb j) s1))))"

2744 by (cases s1) auto

2745 }

2746 then show ?thesis

2747 by simp

2748 qed

2749 moreover

2750 from res_c have "?ResAssigned (Norm s0) (abupd (absorb j) s1)"

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

2752 ultimately show ?case by (intro conjI)

2753 next

2754 case (Comp s0 c1 s1 c2 s2 Env T A)

2755 note G = `prg Env = G`

2756 from Comp.prems

2757 obtain C1 C2

2758 where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

2759 da_c2: "Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

2760 A: "nrm A = nrm C2" "brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)"

2761 by (elim da_elim_cases) simp

2762 from Comp.prems

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

2764 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

2765 by (elim wt_elim_cases) simp

2766 note `PROP ?Hyp (In1r c1) (Norm s0) s1`

2767 with wt_c1 da_c1 G

2768 obtain nrm_c1: "?NormalAssigned s1 C1" and

2769 brk_c1: "?BreakAssigned (Norm s0) s1 C1" and

2770 res_c1: "?ResAssigned (Norm s0) s1"

2771 by simp

2772 show ?case

2773 proof (cases "normal s1")

2774 case True

2775 with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by iprover

2776 with da_c2 obtain C2'

2777 where da_c2': "Env\<turnstile> dom (locals (snd s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

2778 nrm_c2: "nrm C2 \<subseteq> nrm C2'" and

2779 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"

2780 by (rule da_weakenE) iprover

2781 note `PROP ?Hyp (In1r c2) s1 s2`

2782 with wt_c2 da_c2' G

2783 obtain nrm_c2': "?NormalAssigned s2 C2'" and

2784 brk_c2': "?BreakAssigned s1 s2 C2'" and

2785 res_c2 : "?ResAssigned s1 s2"

2786 by simp

2787 from nrm_c2' nrm_c2 A

2788 have "?NormalAssigned s2 A"

2789 by blast

2790 moreover from brk_c2' brk_c2 A

2791 have "?BreakAssigned s1 s2 A"

2792 by fastforce

2793 with True

2794 have "?BreakAssigned (Norm s0) s2 A" by simp

2795 moreover from res_c2 True

2796 have "?ResAssigned (Norm s0) s2"

2797 by simp

2798 ultimately show ?thesis by (intro conjI)

2799 next

2800 case False

2801 with `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`

2802 have eq_s1_s2: "s2=s1" by auto

2803 with False have "?NormalAssigned s2 A" by blast

2804 moreover

2805 have "?BreakAssigned (Norm s0) s2 A"

2806 proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")

2807 case True

2808 then obtain l where l: "abrupt s1 = Some (Jump (Break l))" ..

2809 with brk_c1

2810 have "brk C1 l \<subseteq> dom (locals (store s1))"

2811 by simp

2812 with A eq_s1_s2

2813 have "brk A l \<subseteq> dom (locals (store s2))"

2814 by auto

2815 with l eq_s1_s2

2816 show ?thesis by simp

2817 next

2818 case False

2819 with eq_s1_s2 show ?thesis by simp

2820 qed

2821 moreover from False res_c1 eq_s1_s2

2822 have "?ResAssigned (Norm s0) s2"

2823 by simp

2824 ultimately show ?thesis by (intro conjI)

2825 qed

2826 next

2827 case (If s0 e b s1 c1 c2 s2 Env T A)

2828 note G = `prg Env = G`

2829 with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp

2830 from If.prems

2831 obtain E C1 C2 where

2832 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

2833 da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2834 \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

2835 da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2836 \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

2837 A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"

2838 by (elim da_elim_cases)

2839 from If.prems

2840 obtain

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

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

2843 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

2844 by (elim wt_elim_cases)

2845 from If.hyps have

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

2847 by (elim dom_locals_eval_mono_elim)

2848 show ?case

2849 proof (cases "normal s1")

2850 case True

2851 note normal_s1 = this

2852 show ?thesis

2853 proof (cases "the_Bool b")

2854 case True

2855 from eval_e normal_s1 wt_e

2856 have "assigns_if True e \<subseteq> dom (locals (store s1))"

2857 by (rule assigns_if_good_approx [elim_format]) (simp add: True)

2858 with s0_s1

2859 have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"

2860 by (rule Un_least)

2861 with da_c1 obtain C1'

2862 where da_c1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and

2863 nrm_c1: "nrm C1 \<subseteq> nrm C1'" and

2864 brk_c1: "\<forall> l. brk C1 l \<subseteq> brk C1' l"

2865 by (rule da_weakenE) iprover

2866 from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp

2867 with wt_c1 da_c1'

2868 obtain nrm_c1': "?NormalAssigned s2 C1'" and

2869 brk_c1': "?BreakAssigned s1 s2 C1'" and

2870 res_c1: "?ResAssigned s1 s2"

2871 using G by simp

2872 from nrm_c1' nrm_c1 A

2873 have "?NormalAssigned s2 A"

2874 by blast

2875 moreover from brk_c1' brk_c1 A

2876 have "?BreakAssigned s1 s2 A"

2877 by fastforce

2878 with normal_s1

2879 have "?BreakAssigned (Norm s0) s2 A" by simp

2880 moreover from res_c1 normal_s1 have "?ResAssigned (Norm s0) s2"

2881 by simp

2882 ultimately show ?thesis by (intro conjI)

2883 next

2884 case False

2885 from eval_e normal_s1 wt_e

2886 have "assigns_if False e \<subseteq> dom (locals (store s1))"

2887 by (rule assigns_if_good_approx [elim_format]) (simp add: False)

2888 with s0_s1

2889 have "dom (locals (store ((Norm s0)::state)))\<union> assigns_if False e \<subseteq> \<dots>"

2890 by (rule Un_least)

2891 with da_c2 obtain C2'

2892 where da_c2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

2893 nrm_c2: "nrm C2 \<subseteq> nrm C2'" and

2894 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"

2895 by (rule da_weakenE) iprover

2896 from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp

2897 with wt_c2 da_c2'

2898 obtain nrm_c2': "?NormalAssigned s2 C2'" and

2899 brk_c2': "?BreakAssigned s1 s2 C2'" and

2900 res_c2: "?ResAssigned s1 s2"

2901 using G by simp

2902 from nrm_c2' nrm_c2 A

2903 have "?NormalAssigned s2 A"

2904 by blast

2905 moreover from brk_c2' brk_c2 A

2906 have "?BreakAssigned s1 s2 A"

2907 by fastforce

2908 with normal_s1

2909 have "?BreakAssigned (Norm s0) s2 A" by simp

2910 moreover from res_c2 normal_s1 have "?ResAssigned (Norm s0) s2"

2911 by simp

2912 ultimately show ?thesis by (intro conjI)

2913 qed

2914 next

2915 case False

2916 then obtain abr where abr: "abrupt s1 = Some abr"

2917 by (cases s1) auto

2918 moreover

2919 from eval_e _ wt_e have "\<And> j. abrupt s1 \<noteq> Some (Jump j)"

2920 by (rule eval_expression_no_jump) (simp_all add: G wf)

2921 moreover

2922 have "s2 = s1"

2923 proof -

2924 from abr and `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`

2925 show ?thesis

2926 by (cases s1) simp

2927 qed

2928 ultimately show ?thesis by simp

2929 qed

2930 next

2931 case (Loop s0 e b s1 c s2 l s3 Env T A)

2932 note G = `prg Env = G`

2933 with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"

2934 by (simp (no_asm_simp))

2935 from Loop.prems

2936 obtain E C where

2937 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

2938 da_c: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

2939 \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and

2940 A: "nrm A = nrm C \<inter>

2941 (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)"

2942 "brk A = brk C"

2943 by (elim da_elim_cases)

2944 from Loop.prems

2945 obtain

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

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

2948 by (elim wt_elim_cases)

2949 from wt_e da_e G

2950 obtain res_s1: "?ResAssigned (Norm s0) s1"

2951 by (elim Loop.hyps [elim_format]) simp+

2952 from Loop.hyps have

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

2954 by (elim dom_locals_eval_mono_elim)

2955 show ?case

2956 proof (cases "normal s1")

2957 case True

2958 note normal_s1 = this

2959 show ?thesis

2960 proof (cases "the_Bool b")

2961 case True

2962 with Loop.hyps obtain

2963 eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and

2964 eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"

2965 by simp

2966 from Loop.hyps True

2967 have "?HypObj (In1r c) s1 s2" by simp

2968 note hyp_c = this [rule_format]

2969 from Loop.hyps True

2970 have "?HypObj (In1r (l\<bullet> While(e) c)) (abupd (absorb (Cont l)) s2) s3"

2971 by simp

2972 note hyp_while = this [rule_format]

2973 from eval_e normal_s1 wt_e

2974 have "assigns_if True e \<subseteq> dom (locals (store s1))"

2975 by (rule assigns_if_good_approx [elim_format]) (simp add: True)

2976 with s0_s1

2977 have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"

2978 by (rule Un_least)

2979 with da_c obtain C'

2980 where da_c': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and

2981 nrm_C_C': "nrm C \<subseteq> nrm C'" and

2982 brk_C_C': "\<forall> l. brk C l \<subseteq> brk C' l"

2983 by (rule da_weakenE) iprover

2984 from hyp_c wt_c da_c'

2985 obtain nrm_C': "?NormalAssigned s2 C'" and

2986 brk_C': "?BreakAssigned s1 s2 C'" and

2987 res_s2: "?ResAssigned s1 s2"

2988 using G by simp

2989 show ?thesis

2990 proof (cases "normal s2 \<or> abrupt s2 = Some (Jump (Cont l))")

2991 case True

2992 from Loop.prems obtain

2993 wt_while: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" and

2994 da_while: "Env\<turnstile> dom (locals (store ((Norm s0)::state)))

2995 \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"

2996 by simp

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

2998 \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"

2999 proof -

3000 note s0_s1

3001 also from eval_c

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

3003 by (rule dom_locals_eval_mono_elim)

3004 also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"

3005 by simp

3006 finally show ?thesis .

3007 qed

3008 with da_while obtain A'

3009 where

3010 da_while': "Env\<turnstile> dom (locals (store (abupd (absorb (Cont l)) s2)))

3011 \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"

3012 and nrm_A_A': "nrm A \<subseteq> nrm A'"

3013 and brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"

3014 by (rule da_weakenE) simp

3015 with wt_while hyp_while

3016 obtain nrm_A': "?NormalAssigned s3 A'" and

3017 brk_A': "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A'" and

3018 res_s3: "?ResAssigned (abupd (absorb (Cont l)) s2) s3"

3019 using G by simp

3020 from nrm_A_A' nrm_A'

3021 have "?NormalAssigned s3 A"

3022 by blast

3023 moreover

3024 have "?BreakAssigned (Norm s0) s3 A"

3025 proof -

3026 from brk_A_A' brk_A'

3027 have "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A"

3028 by fastforce

3029 moreover

3030 from True have "normal (abupd (absorb (Cont l)) s2)"

3031 by (cases s2) auto

3032 ultimately show ?thesis

3033 by simp

3034 qed

3035 moreover from res_s3 True have "?ResAssigned (Norm s0) s3"

3036 by auto

3037 ultimately show ?thesis by (intro conjI)

3038 next

3039 case False

3040 then obtain abr where

3041 "abrupt s2 = Some abr" and

3042 "abrupt (abupd (absorb (Cont l)) s2) = Some abr"

3043 by auto

3044 with eval_while

3045 have eq_s3_s2: "s3=s2"

3046 by auto

3047 with nrm_C_C' nrm_C' A

3048 have "?NormalAssigned s3 A"

3049 by fastforce

3050 moreover

3051 from eq_s3_s2 brk_C_C' brk_C' normal_s1 A

3052 have "?BreakAssigned (Norm s0) s3 A"

3053 by fastforce

3054 moreover

3055 from eq_s3_s2 res_s2 normal_s1 have "?ResAssigned (Norm s0) s3"

3056 by simp

3057 ultimately show ?thesis by (intro conjI)

3058 qed

3059 next

3060 case False

3061 with Loop.hyps have eq_s3_s1: "s3=s1"

3062 by simp

3063 from eq_s3_s1 res_s1

3064 have res_s3: "?ResAssigned (Norm s0) s3"

3065 by simp

3066 from eval_e True wt_e

3067 have "assigns_if False e \<subseteq> dom (locals (store s1))"

3068 by (rule assigns_if_good_approx [elim_format]) (simp add: False)

3069 with s0_s1

3070 have "dom (locals (store ((Norm s0)::state)))\<union>assigns_if False e \<subseteq> \<dots>"

3071 by (rule Un_least)

3072 hence "nrm C \<inter>

3073 (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)

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

3075 by (rule subset_Intr)

3076 with normal_s1 A eq_s3_s1

3077 have "?NormalAssigned s3 A"

3078 by simp

3079 moreover

3080 from normal_s1 eq_s3_s1

3081 have "?BreakAssigned (Norm s0) s3 A"

3082 by simp

3083 moreover note res_s3

3084 ultimately show ?thesis by (intro conjI)

3085 qed

3086 next

3087 case False

3088 then obtain abr where abr: "abrupt s1 = Some abr"

3089 by (cases s1) auto

3090 moreover

3091 from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"

3092 by (rule eval_expression_no_jump) (simp_all add: wf G)

3093 moreover

3094 have eq_s3_s1: "s3=s1"

3095 proof (cases "the_Bool b")

3096 case True

3097 with Loop.hyps obtain

3098 eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and

3099 eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"

3100 by simp

3101 from eval_c abr have "s2=s1" by auto

3102 moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"

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

3104 ultimately show ?thesis

3105 using eval_while abr

3106 by auto

3107 next

3108 case False

3109 with Loop.hyps show ?thesis by simp

3110 qed

3111 moreover

3112 from eq_s3_s1 res_s1

3113 have res_s3: "?ResAssigned (Norm s0) s3"

3114 by simp

3115 ultimately show ?thesis

3116 by simp

3117 qed

3118 next

3119 case (Jmp s j Env T A)

3120 have "?NormalAssigned (Some (Jump j),s) A" by simp

3121 moreover

3122 from Jmp.prems

3123 obtain ret: "j = Ret \<longrightarrow> Result \<in> dom (locals (store (Norm s)))" and

3124 brk: "brk A = (case j of

3125 Break l \<Rightarrow> \<lambda> k. if k=l

3126 then dom (locals (store ((Norm s)::state)))

3127 else UNIV

3128 | Cont l \<Rightarrow> \<lambda> k. UNIV

3129 | Ret \<Rightarrow> \<lambda> k. UNIV)"

3130 by (elim da_elim_cases) simp

3131 from brk have "?BreakAssigned (Norm s) (Some (Jump j),s) A"

3132 by simp

3133 moreover from ret have "?ResAssigned (Norm s) (Some (Jump j),s)"

3134 by simp

3135 ultimately show ?case by (intro conjI)

3136 next

3137 case (Throw s0 e a s1 Env T A)

3138 note G = `prg Env = G`

3139 from Throw.prems obtain E where

3140 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"

3141 by (elim da_elim_cases)

3142 from Throw.prems

3143 obtain eT where wt_e: "Env\<turnstile>e\<Colon>-eT"

3144 by (elim wt_elim_cases)

3145 have "?NormalAssigned (abupd (throw a) s1) A"

3146 by (cases s1) (simp add: throw_def)

3147 moreover

3148 have "?BreakAssigned (Norm s0) (abupd (throw a) s1) A"

3149 proof -

3150 from G Throw.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"

3151 by (simp (no_asm_simp))

3152 from eval_e _ wt_e

3153 have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"

3154 by (rule eval_expression_no_jump) (simp_all add: wf G)

3155 hence "\<And> l. abrupt (abupd (throw a) s1) \<noteq> Some (Jump (Break l))"

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

3157 thus ?thesis

3158 by simp

3159 qed

3160 moreover

3161 from wt_e da_e G have "?ResAssigned (Norm s0) s1"

3162 by (elim Throw.hyps [elim_format]) simp+

3163 hence "?ResAssigned (Norm s0) (abupd (throw a) s1)"

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

3165 ultimately show ?case by (intro conjI)

3166 next

3167 case (Try s0 c1 s1 s2 C vn c2 s3 Env T A)

3168 note G = `prg Env = G`

3169 from Try.prems obtain C1 C2 where

3170 da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

3171 da_c2:

3172 "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>

3173 \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

3174 A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"

3175 by (elim da_elim_cases) simp

3176 from Try.prems obtain

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

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

3179 by (elim wt_elim_cases)

3180 have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G

3181 by (simp (no_asm_simp))

3182 note `PROP ?Hyp (In1r c1) (Norm s0) s1`

3183 with wt_c1 da_c1 G

3184 obtain nrm_C1: "?NormalAssigned s1 C1" and

3185 brk_C1: "?BreakAssigned (Norm s0) s1 C1" and

3186 res_s1: "?ResAssigned (Norm s0) s1"

3187 by simp

3188 show ?case

3189 proof (cases "normal s1")

3190 case True

3191 with nrm_C1 have "nrm C1 \<inter> nrm C2 \<subseteq> dom (locals (store s1))"

3192 by auto

3193 moreover

3194 have "s3=s1"

3195 proof -

3196 from sxalloc True have eq_s2_s1: "s2=s1"

3197 by (cases s1) (auto elim: sxalloc_elim_cases)

3198 with True have "\<not> G,s2\<turnstile>catch C"

3199 by (simp add: catch_def)

3200 with Try.hyps have "s3=s2"

3201 by simp

3202 with eq_s2_s1 show ?thesis by simp

3203 qed

3204 ultimately show ?thesis

3205 using True A res_s1 by simp

3206 next

3207 case False

3208 note not_normal_s1 = this

3209 show ?thesis

3210 proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")

3211 case True

3212 then obtain l where l: "abrupt s1 = Some (Jump (Break l))"

3213 by auto

3214 with brk_C1 have "(brk C1 \<Rightarrow>\<inter> brk C2) l \<subseteq> dom (locals (store s1))"

3215 by auto

3216 moreover have "s3=s1"

3217 proof -

3218 from sxalloc l have eq_s2_s1: "s2=s1"

3219 by (cases s1) (auto elim: sxalloc_elim_cases)

3220 with l have "\<not> G,s2\<turnstile>catch C"

3221 by (simp add: catch_def)

3222 with Try.hyps have "s3=s2"

3223 by simp

3224 with eq_s2_s1 show ?thesis by simp

3225 qed

3226 ultimately show ?thesis

3227 using l A res_s1 by simp

3228 next

3229 case False

3230 note abrupt_no_break = this

3231 show ?thesis

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

3233 case True

3234 with Try.hyps have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3"

3235 by simp

3236 note hyp_c2 = this [rule_format]

3237 have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn})

3238 \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"

3239 proof -

3240 from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`

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

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

3243 by (rule dom_locals_eval_mono_elim)

3244 also

3245 from sxalloc

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

3247 by (rule dom_locals_sxalloc_mono)

3248 also

3249 have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"

3250 by (cases s2) (simp add: new_xcpt_var_def, blast)

3251 also

3252 have "{VName vn} \<subseteq> \<dots>"

3253 by (cases s2) simp

3254 ultimately show ?thesis

3255 by (rule Un_least)

3256 qed

3257 with da_c2

3258 obtain C2' where

3259 da_C2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>

3260 \<turnstile> dom (locals (store (new_xcpt_var vn s2))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"

3261 and nrm_C2': "nrm C2 \<subseteq> nrm C2'"

3262 and brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"

3263 by (rule da_weakenE) simp

3264 from wt_c2 da_C2' G and hyp_c2

3265 obtain nrmAss_C2: "?NormalAssigned s3 C2'" and

3266 brkAss_C2: "?BreakAssigned (new_xcpt_var vn s2) s3 C2'" and

3267 resAss_s3: "?ResAssigned (new_xcpt_var vn s2) s3"

3268 by simp

3269 from nrmAss_C2 nrm_C2' A

3270 have "?NormalAssigned s3 A"

3271 by auto

3272 moreover

3273 have "?BreakAssigned (Norm s0) s3 A"

3274 proof -

3275 from brkAss_C2 have "?BreakAssigned (Norm s0) s3 C2'"

3276 by (cases s2) (auto simp add: new_xcpt_var_def)

3277 with brk_C2' A show ?thesis

3278 by fastforce

3279 qed

3280 moreover

3281 from resAss_s3 have "?ResAssigned (Norm s0) s3"

3282 by (cases s2) ( simp add: new_xcpt_var_def)

3283 ultimately show ?thesis by (intro conjI)

3284 next

3285 case False

3286 with Try.hyps

3287 have eq_s3_s2: "s3=s2" by simp

3288 moreover from sxalloc not_normal_s1 abrupt_no_break

3289 obtain "\<not> normal s2"

3290 "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l))"

3291 by - (rule sxalloc_cases,auto)

3292 ultimately obtain

3293 "?NormalAssigned s3 A" and "?BreakAssigned (Norm s0) s3 A"

3294 by (cases s2) auto

3295 moreover have "?ResAssigned (Norm s0) s3"

3296 proof (cases "abrupt s1 = Some (Jump Ret)")

3297 case True

3298 with sxalloc have "s2=s1"

3299 by (elim sxalloc_cases) auto

3300 with res_s1 eq_s3_s2 show ?thesis by simp

3301 next

3302 case False

3303 with sxalloc

3304 have "abrupt s2 \<noteq> Some (Jump Ret)"

3305 by (rule sxalloc_no_jump)

3306 with eq_s3_s2 show ?thesis

3307 by simp

3308 qed

3309 ultimately show ?thesis by (intro conjI)

3310 qed

3311 qed

3312 qed

3313 next

3314 case (Fin s0 c1 x1 s1 c2 s2 s3 Env T A)

3315 note G = `prg Env = G`

3316 from Fin.prems obtain C1 C2 where

3317 da_C1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and

3318 da_C2: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and

3319 nrm_A: "nrm A = nrm C1 \<union> nrm C2" and

3320 brk_A: "brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)"

3321 by (elim da_elim_cases) simp

3322 from Fin.prems obtain

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

3324 wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"

3325 by (elim wt_elim_cases)

3326 note `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)`

3327 with wt_c1 da_C1 G

3328 obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and

3329 brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and

3330 resAss_s1: "?ResAssigned (Norm s0) (x1,s1)"

3331 by simp

3332 obtain nrmAss_C2: "?NormalAssigned s2 C2" and

3333 brkAss_C2: "?BreakAssigned (Norm s1) s2 C2" and

3334 resAss_s2: "?ResAssigned (Norm s1) s2"

3335 proof -

3336 from Fin.hyps

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

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

3339 by - (rule dom_locals_eval_mono_elim)

3340 with da_C2 obtain C2'

3341 where

3342 da_C2': "Env\<turnstile> dom (locals (store (x1,s1))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

3343 nrm_C2': "nrm C2 \<subseteq> nrm C2'" and

3344 brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"

3345 by (rule da_weakenE) simp

3346 note `PROP ?Hyp (In1r c2) (Norm s1) s2`

3347 with wt_c2 da_C2' G

3348 obtain nrmAss_C2': "?NormalAssigned s2 C2'" and

3349 brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and

3350 resAss_s2': "?ResAssigned (Norm s1) s2"

3351 by simp

3352 from nrmAss_C2' nrm_C2' have "?NormalAssigned s2 C2"

3353 by blast

3354 moreover

3355 from brkAss_C2' brk_C2' have "?BreakAssigned (Norm s1) s2 C2"

3356 by fastforce

3357 ultimately

3358 show ?thesis

3359 using that resAss_s2' by simp

3360 qed

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

3362 else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`

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

3364 proof -

3365 from `G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2`

3366 show ?thesis

3367 by (rule dom_locals_eval_mono_elim) simp

3368 qed

3370 have "?NormalAssigned s3 A"

3371 proof

3372 assume normal_s3: "normal s3"

3373 show "nrm A \<subseteq> dom (locals (snd s3))"

3374 proof -

3375 have "nrm C1 \<subseteq> dom (locals (snd s3))"

3376 proof -

3377 from normal_s3 s3

3378 have "normal (x1,s1)"

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

3380 with normal_s3 nrmAss_C1 s3 s1_s2

3381 show ?thesis

3382 by fastforce

3383 qed

3384 moreover

3385 have "nrm C2 \<subseteq> dom (locals (snd s3))"

3386 proof -

3387 from normal_s3 s3

3388 have "normal s2"

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

3390 with normal_s3 nrmAss_C2 s3 s1_s2

3391 show ?thesis

3392 by fastforce

3393 qed

3394 ultimately have "nrm C1 \<union> nrm C2 \<subseteq> \<dots>"

3395 by (rule Un_least)

3396 with nrm_A show ?thesis

3397 by simp

3398 qed

3399 qed

3400 moreover

3401 {

3402 fix l assume brk_s3: "abrupt s3 = Some (Jump (Break l))"

3403 have "brk A l \<subseteq> dom (locals (store s3))"

3404 proof (cases "normal s2")

3405 case True

3406 with brk_s3 s3

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

3408 by simp

3409 have "brk C1 l \<subseteq> dom (locals (store s3))"

3410 proof -

3411 from True brk_s3 s3 have "x1=Some (Jump (Break l))"

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

3413 with brkAss_C1 s1_s2 s2_s3

3414 show ?thesis

3415 by simp

3416 qed

3417 moreover from True nrmAss_C2 s2_s3

3418 have "nrm C2 \<subseteq> dom (locals (store s3))"

3419 by - (rule subset_trans, simp_all)

3420 ultimately

3421 have "((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) l \<subseteq> \<dots>"

3422 by blast

3423 with brk_A show ?thesis

3424 by simp blast

3425 next

3426 case False

3427 note not_normal_s2 = this

3428 have "s3=s2"

3429 proof (cases "normal (x1,s1)")

3430 case True with not_normal_s2 s3 show ?thesis

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

3432 next

3433 case False with not_normal_s2 s3 brk_s3 show ?thesis

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

3435 qed

3436 with brkAss_C2 brk_s3

3437 have "brk C2 l \<subseteq> dom (locals (store s3))"

3438 by simp

3439 with brk_A show ?thesis

3440 by simp blast

3441 qed

3442 }

3443 hence "?BreakAssigned (Norm s0) s3 A"

3444 by simp

3445 moreover

3446 {

3447 assume abr_s3: "abrupt s3 = Some (Jump Ret)"

3448 have "Result \<in> dom (locals (store s3))"

3449 proof (cases "x1 = Some (Jump Ret)")

3450 case True

3451 note ret_x1 = this

3452 with resAss_s1 have res_s1: "Result \<in> dom (locals s1)"

3453 by simp

3454 moreover have "dom (locals (store ((Norm s1)::state)))

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

3456 by (rule dom_locals_eval_mono_elim) (rule Fin.hyps)

3457 ultimately have "Result \<in> dom (locals (store s2))"

3458 by - (rule subsetD,auto)

3459 with res_s1 s3 show ?thesis

3460 by simp

3461 next

3462 case False

3463 with s3 abr_s3 obtain "abrupt s2 = Some (Jump Ret)" and "s3=s2"

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

3465 with resAss_s2 show ?thesis

3466 by simp

3467 qed

3468 }

3469 hence "?ResAssigned (Norm s0) s3"

3470 by simp

3471 ultimately show ?case by (intro conjI)

3472 next

3473 case (Init C c s0 s3 s1 s2 Env T A)

3474 note G = `prg Env = G`

3475 from Init.hyps

3476 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Init C\<rightarrow> s3"

3477 apply (simp only: G)

3478 apply (rule eval.Init, assumption)

3479 apply (cases "inited C (globs s0) ")

3480 apply simp

3481 apply (simp only: if_False )

3482 apply (elim conjE,intro conjI,assumption+,simp)

3483 done (* auto or simp alone always do too much *)

3484 from Init.prems and `the (class G C) = c`

3485 have c: "class G C = Some c"

3486 by (elim wt_elim_cases) auto

3487 from Init.prems obtain

3488 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"

3489 by (elim da_elim_cases) simp

3490 show ?case

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

3492 case True

3493 with Init.hyps have "s3=Norm s0" by simp

3494 thus ?thesis

3495 using nrm_A by simp

3496 next

3497 case False

3498 from Init.hyps False G

3499 obtain eval_initC:

3500 "prg Env\<turnstile>Norm ((init_class_obj G C) s0)

3501 \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and

3502 eval_init: "prg Env\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and

3503 s3: "s3=(set_lvars (locals (store s1))) s2"

3504 by simp

3505 have "?NormalAssigned s3 A"

3506 proof

3507 show "nrm A \<subseteq> dom (locals (store s3))"

3508 proof -

3509 from nrm_A have "nrm A \<subseteq> dom (locals (init_class_obj G C s0))"

3510 by simp

3511 also from eval_initC have "\<dots> \<subseteq> dom (locals (store s1))"

3512 by (rule dom_locals_eval_mono_elim) simp

3513 also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"

3514 by (cases s1) (cases s2, simp add: init_lvars_def2)

3515 finally show ?thesis .

3516 qed

3517 qed

3518 moreover

3519 from eval

3520 have "\<And> j. abrupt s3 \<noteq> Some (Jump j)"

3521 by (rule eval_statement_no_jump) (auto simp add: wf c G)

3522 then obtain "?BreakAssigned (Norm s0) s3 A"

3523 and "?ResAssigned (Norm s0) s3"

3524 by simp

3525 ultimately show ?thesis by (intro conjI)

3526 qed

3527 next

3528 case (NewC s0 C s1 a s2 Env T A)

3529 note G = `prg Env = G`

3530 from NewC.prems

3531 obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))"

3532 "brk A = (\<lambda> l. UNIV)"

3533 by (elim da_elim_cases) simp

3534 from wf NewC.prems

3535 have wt_init: "Env\<turnstile>(Init C)\<Colon>\<surd>"

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

3537 have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s2))"

3538 proof -

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

3540 by (rule dom_locals_eval_mono_elim) (rule NewC.hyps)

3541 also

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

3543 by (rule dom_locals_halloc_mono) (rule NewC.hyps)

3544 finally show ?thesis .

3545 qed

3546 with A have "?NormalAssigned s2 A"

3547 by simp

3548 moreover

3549 {

3550 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3551 proof -

3552 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"

3553 unfolding G by (rule eval.NewC NewC.hyps)+

3554 from NewC.prems

3555 obtain T' where "T=Inl T'"

3556 by (elim wt_elim_cases) simp

3557 with NewC.prems have "Env\<turnstile>NewC C\<Colon>-T'"

3558 by simp

3559 from eval _ this

3560 show ?thesis

3561 by (rule eval_expression_no_jump) (simp_all add: G wf)

3562 qed

3563 }

3564 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3565 by simp_all

3566 ultimately show ?case by (intro conjI)

3567 next

3568 case (NewA s0 elT s1 e i s2 a s3 Env T A)

3569 note G = `prg Env = G`

3570 from NewA.prems obtain

3571 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3572 by (elim da_elim_cases)

3573 from NewA.prems obtain

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

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

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

3577 note halloc = `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3`

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

3579 by (rule dom_locals_eval_mono_elim) (rule NewA.hyps)

3580 with da_e obtain A' where

3581 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"

3582 and nrm_A_A': "nrm A \<subseteq> nrm A'"

3583 and brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"

3584 by (rule da_weakenE) simp

3585 note `PROP ?Hyp (In1l e) s1 s2`

3586 with wt_size da_e' G obtain

3587 nrmAss_A': "?NormalAssigned s2 A'" and

3588 brkAss_A': "?BreakAssigned s1 s2 A'"

3589 by simp

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

3591 proof -

3592 have "dom (locals (store s2))

3593 \<subseteq> dom (locals (store (abupd (check_neg i) s2)))"

3594 by (simp)

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

3596 by (rule dom_locals_halloc_mono) (rule NewA.hyps)

3597 finally show ?thesis .

3598 qed

3599 have "?NormalAssigned s3 A"

3600 proof

3601 assume normal_s3: "normal s3"

3602 show "nrm A \<subseteq> dom (locals (store s3))"

3603 proof -

3604 from halloc normal_s3

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

3606 by cases simp_all

3607 hence "normal s2"

3608 by (cases s2) simp

3609 with nrmAss_A' nrm_A_A' s2_s3 show ?thesis

3610 by blast

3611 qed

3612 qed

3613 moreover

3614 {

3615 fix j have "abrupt s3 \<noteq> Some (Jump j)"

3616 proof -

3617 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"

3618 unfolding G by (rule eval.NewA NewA.hyps)+

3619 from NewA.prems

3620 obtain T' where "T=Inl T'"

3621 by (elim wt_elim_cases) simp

3622 with NewA.prems have "Env\<turnstile>New elT[e]\<Colon>-T'"

3623 by simp

3624 from eval _ this

3625 show ?thesis

3626 by (rule eval_expression_no_jump) (simp_all add: G wf)

3627 qed

3628 }

3629 hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"

3630 by simp_all

3631 ultimately show ?case by (intro conjI)

3632 next

3633 case (Cast s0 e v s1 s2 cT Env T A)

3634 note G = `prg Env = G`

3635 from Cast.prems obtain

3636 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3637 by (elim da_elim_cases)

3638 from Cast.prems obtain eT where

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

3640 by (elim wt_elim_cases)

3641 note `PROP ?Hyp (In1l e) (Norm s0) s1`

3642 with wt_e da_e G obtain

3643 nrmAss_A: "?NormalAssigned s1 A" and

3644 brkAss_A: "?BreakAssigned (Norm s0) s1 A"

3645 by simp

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

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

3648 by simp

3649 have "?NormalAssigned s2 A"

3650 proof

3651 assume "normal s2"

3652 with s2 have "normal s1"

3653 by (cases s1) simp

3654 with nrmAss_A s1_s2

3655 show "nrm A \<subseteq> dom (locals (store s2))"

3656 by blast

3657 qed

3658 moreover

3659 {

3660 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3661 proof -

3662 have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"

3663 unfolding G by (rule eval.Cast Cast.hyps)+

3664 from Cast.prems

3665 obtain T' where "T=Inl T'"

3666 by (elim wt_elim_cases) simp

3667 with Cast.prems have "Env\<turnstile>Cast cT e\<Colon>-T'"

3668 by simp

3669 from eval _ this

3670 show ?thesis

3671 by (rule eval_expression_no_jump) (simp_all add: G wf)

3672 qed

3673 }

3674 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3675 by simp_all

3676 ultimately show ?case by (intro conjI)

3677 next

3678 case (Inst s0 e v s1 b iT Env T A)

3679 note G = `prg Env = G`

3680 from Inst.prems obtain

3681 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3682 by (elim da_elim_cases)

3683 from Inst.prems obtain eT where

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

3685 by (elim wt_elim_cases)

3686 note `PROP ?Hyp (In1l e) (Norm s0) s1`

3687 with wt_e da_e G obtain

3688 "?NormalAssigned s1 A" and

3689 "?BreakAssigned (Norm s0) s1 A" and

3690 "?ResAssigned (Norm s0) s1"

3691 by simp

3692 thus ?case by (intro conjI)

3693 next

3694 case (Lit s v Env T A)

3695 from Lit.prems

3696 have "nrm A = dom (locals (store ((Norm s)::state)))"

3697 by (elim da_elim_cases) simp

3698 thus ?case by simp

3699 next

3700 case (UnOp s0 e v s1 unop Env T A)

3701 note G = `prg Env = G`

3702 from UnOp.prems obtain

3703 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3704 by (elim da_elim_cases)

3705 from UnOp.prems obtain eT where

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

3707 by (elim wt_elim_cases)

3708 note `PROP ?Hyp (In1l e) (Norm s0) s1`

3709 with wt_e da_e G obtain

3710 "?NormalAssigned s1 A" and

3711 "?BreakAssigned (Norm s0) s1 A" and

3712 "?ResAssigned (Norm s0) s1"

3713 by simp

3714 thus ?case by (intro conjI)

3715 next

3716 case (BinOp s0 e1 v1 s1 binop e2 v2 s2 Env T A)

3717 note G = `prg Env = G`

3718 from BinOp.hyps

3719 have

3720 eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"

3721 by (simp only: G) (rule eval.BinOp)

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

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

3724 by (rule dom_locals_eval_mono_elim) (rule BinOp)

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

3726 by (rule dom_locals_eval_mono_elim) (rule BinOp)

3727 finally

3728 have s0_s2: "dom (locals (store ((Norm s0)::state)))

3729 \<subseteq> dom (locals (store s2))" .

3730 from BinOp.prems obtain e1T e2T

3731 where wt_e1: "Env\<turnstile>e1\<Colon>-e1T"

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

3733 and wt_binop: "wt_binop (prg Env) binop e1T e2T"

3734 and T: "T=Inl (PrimT (binop_type binop))"

3735 by (elim wt_elim_cases) simp

3736 have "?NormalAssigned s2 A"

3737 proof

3738 assume normal_s2: "normal s2"

3739 have normal_s1: "normal s1"

3740 by (rule eval_no_abrupt_lemma [rule_format]) (rule BinOp.hyps, rule normal_s2)

3741 show "nrm A \<subseteq> dom (locals (store s2))"

3742 proof (cases "binop=CondAnd")

3743 case True

3744 note CondAnd = this

3745 from BinOp.prems obtain

3746 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

3747 \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>

3748 assigns_if False (BinOp CondAnd e1 e2))"

3749 by (elim da_elim_cases) (simp_all add: CondAnd)

3750 from T BinOp.prems CondAnd

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

3752 by (simp)

3753 with eval normal_s2

3754 have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2))

3755 (BinOp binop e1 e2)

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

3757 by (rule assigns_if_good_approx)

3758 have "(assigns_if True (BinOp CondAnd e1 e2) \<inter>

3759 assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"

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

3761 case True

3762 with ass_if CondAnd

3763 have "assigns_if True (BinOp CondAnd e1 e2)

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

3765 by simp

3766 thus ?thesis by blast

3767 next

3768 case False

3769 with ass_if CondAnd

3770 have "assigns_if False (BinOp CondAnd e1 e2)

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

3772 by (simp only: False)

3773 thus ?thesis by blast

3774 qed

3775 with s0_s2

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

3777 \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>

3778 assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"

3779 by (rule Un_least)

3780 thus ?thesis by (simp only: nrm_A)

3781 next

3782 case False

3783 note notCondAnd = this

3784 show ?thesis

3785 proof (cases "binop=CondOr")

3786 case True

3787 note CondOr = this

3788 from BinOp.prems obtain

3789 nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

3790 \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>

3791 assigns_if False (BinOp CondOr e1 e2))"

3792 by (elim da_elim_cases) (simp_all add: CondOr)

3793 from T BinOp.prems CondOr

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

3795 by (simp)

3796 with eval normal_s2

3797 have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2))

3798 (BinOp binop e1 e2)

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

3800 by (rule assigns_if_good_approx)

3801 have "(assigns_if True (BinOp CondOr e1 e2) \<inter>

3802 assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"

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

3804 case True

3805 with ass_if CondOr

3806 have "assigns_if True (BinOp CondOr e1 e2)

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

3808 by (simp)

3809 thus ?thesis by blast

3810 next

3811 case False

3812 with ass_if CondOr

3813 have "assigns_if False (BinOp CondOr e1 e2)

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

3815 by (simp)

3816 thus ?thesis by blast

3817 qed

3818 with s0_s2

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

3820 \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>

3821 assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"

3822 by (rule Un_least)

3823 thus ?thesis by (simp only: nrm_A)

3824 next

3825 case False

3826 with notCondAnd obtain notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"

3827 by simp

3828 from BinOp.prems obtain E1

3829 where da_e1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1"

3830 and da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"

3831 by (elim da_elim_cases) (simp_all add: notAndOr)

3832 note `PROP ?Hyp (In1l e1) (Norm s0) s1`

3833 with wt_e1 da_e1 G normal_s1

3834 obtain "?NormalAssigned s1 E1"

3835 by simp

3836 with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by iprover

3837 with da_e2 obtain A'

3838 where da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and

3839 nrm_A_A': "nrm A \<subseteq> nrm A'"

3840 by (rule da_weakenE) iprover

3841 from notAndOr have "need_second_arg binop v1" by simp

3842 with BinOp.hyps

3843 have "PROP ?Hyp (In1l e2) s1 s2" by simp

3844 with wt_e2 da_e2' G

3845 obtain "?NormalAssigned s2 A'"

3846 by simp

3847 with nrm_A_A' normal_s2

3848 show "nrm A \<subseteq> dom (locals (store s2))"

3849 by blast

3850 qed

3851 qed

3852 qed

3853 moreover

3854 {

3855 fix j have "abrupt s2 \<noteq> Some (Jump j)"

3856 proof -

3857 from BinOp.prems T

3858 have "Env\<turnstile>In1l (BinOp binop e1 e2)\<Colon>Inl (PrimT (binop_type binop))"

3859 by simp

3860 from eval _ this

3861 show ?thesis

3862 by (rule eval_expression_no_jump) (simp_all add: G wf)

3863 qed

3864 }

3865 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

3866 by simp_all

3867 ultimately show ?case by (intro conjI)

3868 next

3869 case (Super s Env T A)

3870 from Super.prems

3871 have "nrm A = dom (locals (store ((Norm s)::state)))"

3872 by (elim da_elim_cases) simp

3873 thus ?case by simp

3874 next

3875 case (Acc s0 v w upd s1 Env T A)

3876 show ?case

3877 proof (cases "\<exists> vn. v = LVar vn")

3878 case True

3879 then obtain vn where vn: "v=LVar vn"..

3880 from Acc.prems

3881 have "nrm A = dom (locals (store ((Norm s0)::state)))"

3882 by (simp only: vn) (elim da_elim_cases,simp_all)

3883 moreover

3884 from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`

3885 have "s1=Norm s0"

3886 by (simp only: vn) (elim eval_elim_cases,simp)

3887 ultimately show ?thesis by simp

3888 next

3889 case False

3890 note G = `prg Env = G`

3891 from False Acc.prems

3892 have da_v: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>v\<rangle>\<guillemotright> A"

3893 by (elim da_elim_cases) simp_all

3894 from Acc.prems obtain vT where

3895 wt_v: "Env\<turnstile>v\<Colon>=vT"

3896 by (elim wt_elim_cases)

3897 note `PROP ?Hyp (In2 v) (Norm s0) s1`

3898 with wt_v da_v G obtain

3899 "?NormalAssigned s1 A" and

3900 "?BreakAssigned (Norm s0) s1 A" and

3901 "?ResAssigned (Norm s0) s1"

3902 by simp

3903 thus ?thesis by (intro conjI)

3904 qed

3905 next

3906 case (Ass s0 var w upd s1 e v s2 Env T A)

3907 note G = `prg Env = G`

3908 from Ass.prems obtain varT eT where

3909 wt_var: "Env\<turnstile>var\<Colon>=varT" and

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

3911 by (elim wt_elim_cases) simp

3912 have eval_var: "prg Env\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1"

3913 using Ass.hyps by (simp only: G)

3914 have "?NormalAssigned (assign upd v s2) A"

3915 proof

3916 assume normal_ass_s2: "normal (assign upd v s2)"

3917 from normal_ass_s2

3918 have normal_s2: "normal s2"

3919 by (cases s2) (simp add: assign_def Let_def)

3920 hence normal_s1: "normal s1"

3921 by - (rule eval_no_abrupt_lemma [rule_format], rule Ass.hyps)

3922 note hyp_var = `PROP ?Hyp (In2 var) (Norm s0) s1`

3923 note hyp_e = `PROP ?Hyp (In1l e) s1 s2`

3924 show "nrm A \<subseteq> dom (locals (store (assign upd v s2)))"

3925 proof (cases "\<exists> vn. var = LVar vn")

3926 case True

3927 then obtain vn where vn: "var=LVar vn"..

3928 from Ass.prems obtain E where

3929 da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

3930 nrm_A: "nrm A = nrm E \<union> {vn}"

3931 by (elim da_elim_cases) (insert vn,auto)

3932 obtain E' where

3933 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" and

3934 E_E': "nrm E \<subseteq> nrm E'"

3935 proof -

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

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

3938 by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)

3939 with da_e show thesis

3940 by (rule da_weakenE) (rule that)

3941 qed

3942 from G eval_var vn

3943 have eval_lvar: "G\<turnstile>Norm s0 \<midarrow>LVar vn=\<succ>(w, upd)\<rightarrow> s1"

3944 by simp

3945 then have upd: "upd = snd (lvar vn (store s1))"

3946 by cases (cases "lvar vn (store s1)",simp)

3947 have "nrm E \<subseteq> dom (locals (store (assign upd v s2)))"

3948 proof -

3949 from hyp_e wt_e da_e' G normal_s2

3950 have "nrm E' \<subseteq> dom (locals (store s2))"

3951 by simp

3952 also

3953 from upd

3954 have "dom (locals (store s2)) \<subseteq> dom (locals (store (upd v s2)))"

3955 by (simp add: lvar_def) blast

3956 hence "dom (locals (store s2))

3957 \<subseteq> dom (locals (store (assign upd v s2)))"

3958 by (rule dom_locals_assign_mono)

3959 finally

3960 show ?thesis using E_E'

3961 by blast

3962 qed

3963 moreover

3964 from upd normal_s2

3965 have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"

3966 by (auto simp add: assign_def Let_def lvar_def upd split: split_split)

3967 ultimately

3968 show "nrm A \<subseteq> \<dots>"

3969 by (rule Un_least [elim_format]) (simp add: nrm_A)

3970 next

3971 case False

3972 from Ass.prems obtain V where

3973 da_var: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>var\<rangle>\<guillemotright> V" and

3974 da_e: "Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

3975 by (elim da_elim_cases) (insert False,simp+)

3976 from hyp_var wt_var da_var G normal_s1

3977 have "nrm V \<subseteq> dom (locals (store s1))"

3978 by simp

3979 with da_e obtain A'

3980 where da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and

3981 nrm_A_A': "nrm A \<subseteq> nrm A'"

3982 by (rule da_weakenE) iprover

3983 from hyp_e wt_e da_e' G normal_s2

3984 obtain "nrm A' \<subseteq> dom (locals (store s2))"

3985 by simp

3986 with nrm_A_A' have "nrm A \<subseteq> \<dots>"

3987 by blast

3988 also have "\<dots> \<subseteq> dom (locals (store (assign upd v s2)))"

3989 proof -

3990 from eval_var normal_s1

3991 have "dom (locals (store s2)) \<subseteq> dom (locals (store (upd v s2)))"

3992 by (cases rule: dom_locals_eval_mono_elim)

3993 (cases s2, simp)

3994 thus ?thesis

3995 by (rule dom_locals_assign_mono)

3996 qed

3997 finally show ?thesis .

3998 qed

3999 qed

4000 moreover

4001 {

4002 fix j have "abrupt (assign upd v s2) \<noteq> Some (Jump j)"

4003 proof -

4004 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"

4005 by (simp only: G) (rule eval.Ass Ass.hyps)+

4006 from Ass.prems

4007 obtain T' where "T=Inl T'"

4008 by (elim wt_elim_cases) simp

4009 with Ass.prems have "Env\<turnstile>var:=e\<Colon>-T'" by simp

4010 from eval _ this

4011 show ?thesis

4012 by (rule eval_expression_no_jump) (simp_all add: G wf)

4013 qed

4014 }

4015 hence "?BreakAssigned (Norm s0) (assign upd v s2) A"

4016 and "?ResAssigned (Norm s0) (assign upd v s2)"

4017 by simp_all

4018 ultimately show ?case by (intro conjI)

4019 next

4020 case (Cond s0 e0 b s1 e1 e2 v s2 Env T A)

4021 note G = `prg Env = G`

4022 have "?NormalAssigned s2 A"

4023 proof

4024 assume normal_s2: "normal s2"

4025 show "nrm A \<subseteq> dom (locals (store s2))"

4026 proof (cases "Env\<turnstile>(e0 ? e1 : e2)\<Colon>-(PrimT Boolean)")

4027 case True

4028 with Cond.prems

4029 have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))

4030 \<union> (assigns_if True (e0 ? e1 : e2) \<inter>

4031 assigns_if False (e0 ? e1 : e2))"

4032 by (elim da_elim_cases) simp_all

4033 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>(e0 ? e1 : e2)-\<succ>v\<rightarrow> s2"

4034 unfolding G by (rule eval.Cond Cond.hyps)+

4035 from eval

4036 have "dom (locals (store ((Norm s0)::state)))\<subseteq>dom (locals (store s2))"

4037 by (rule dom_locals_eval_mono_elim)

4038 moreover

4039 from eval normal_s2 True

4040 have ass_if: "assigns_if (the_Bool v) (e0 ? e1 : e2)

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

4042 by (rule assigns_if_good_approx)

4043 have "assigns_if True (e0 ? e1:e2) \<inter> assigns_if False (e0 ? e1:e2)

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

4045 proof (cases "the_Bool v")

4046 case True

4047 from ass_if

4048 have "assigns_if True (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"

4049 by (simp only: True)

4050 thus ?thesis by blast

4051 next

4052 case False

4053 from ass_if

4054 have "assigns_if False (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"

4055 by (simp only: False)

4056 thus ?thesis by blast

4057 qed

4058 ultimately show "nrm A \<subseteq> dom (locals (store s2))"

4059 by (simp only: nrm_A) (rule Un_least)

4060 next

4061 case False

4062 with Cond.prems obtain E1 E2 where

4063 da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

4064 \<union> assigns_if True e0) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and

4065 da_e2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))

4066 \<union> assigns_if False e0) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2" and

4067 nrm_A: "nrm A = nrm E1 \<inter> nrm E2"

4068 by (elim da_elim_cases) simp_all

4069 from Cond.prems obtain e1T e2T where

4070 wt_e0: "Env\<turnstile>e0\<Colon>- PrimT Boolean" and

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

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

4073 by (elim wt_elim_cases)

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

4075 \<subseteq> dom (locals (store s1))"

4076 by (rule dom_locals_eval_mono_elim) (rule Cond.hyps)

4077 have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"

4078 unfolding G by (rule Cond.hyps)

4079 have normal_s1: "normal s1"

4080 by (rule eval_no_abrupt_lemma [rule_format]) (rule Cond.hyps, rule normal_s2)

4081 show ?thesis

4082 proof (cases "the_Bool b")

4083 case True

4084 from True Cond.hyps have "PROP ?Hyp (In1l e1) s1 s2" by simp

4085 moreover

4086 from eval_e0 normal_s1 wt_e0

4087 have "assigns_if True e0 \<subseteq> dom (locals (store s1))"

4088 by (rule assigns_if_good_approx [elim_format]) (simp only: True)

4089 with s0_s1

4090 have "dom (locals (store ((Norm s0)::state)))

4091 \<union> assigns_if True e0 \<subseteq> \<dots>"

4092 by (rule Un_least)

4093 with da_e1 obtain E1' where

4094 da_e1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and

4095 nrm_E1_E1': "nrm E1 \<subseteq> nrm E1'"

4096 by (rule da_weakenE) iprover

4097 ultimately have "nrm E1' \<subseteq> dom (locals (store s2))"

4098 using wt_e1 G normal_s2 by simp

4099 with nrm_E1_E1' show ?thesis

4100 by (simp only: nrm_A) blast

4101 next

4102 case False

4103 from False Cond.hyps have "PROP ?Hyp (In1l e2) s1 s2" by simp

4104 moreover

4105 from eval_e0 normal_s1 wt_e0

4106 have "assigns_if False e0 \<subseteq> dom (locals (store s1))"

4107 by (rule assigns_if_good_approx [elim_format]) (simp only: False)

4108 with s0_s1

4109 have "dom (locals (store ((Norm s0)::state)))

4110 \<union> assigns_if False e0 \<subseteq> \<dots>"

4111 by (rule Un_least)

4112 with da_e2 obtain E2' where

4113 da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and

4114 nrm_E2_E2': "nrm E2 \<subseteq> nrm E2'"

4115 by (rule da_weakenE) iprover

4116 ultimately have "nrm E2' \<subseteq> dom (locals (store s2))"

4117 using wt_e2 G normal_s2 by simp

4118 with nrm_E2_E2' show ?thesis

4119 by (simp only: nrm_A) blast

4120 qed

4121 qed

4122 qed

4123 moreover

4124 {

4125 fix j have "abrupt s2 \<noteq> Some (Jump j)"

4126 proof -

4127 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"

4128 unfolding G by (rule eval.Cond Cond.hyps)+

4129 from Cond.prems

4130 obtain T' where "T=Inl T'"

4131 by (elim wt_elim_cases) simp

4132 with Cond.prems have "Env\<turnstile>e0 ? e1 : e2\<Colon>-T'" by simp

4133 from eval _ this

4134 show ?thesis

4135 by (rule eval_expression_no_jump) (simp_all add: G wf)

4136 qed

4137 }

4138 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

4139 by simp_all

4140 ultimately show ?case by (intro conjI)

4141 next

4142 case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4

4143 Env T A)

4144 note G = `prg Env = G`

4145 have "?NormalAssigned (restore_lvars s2 s4) A"

4146 proof

4147 assume normal_restore_lvars: "normal (restore_lvars s2 s4)"

4148 show "nrm A \<subseteq> dom (locals (store (restore_lvars s2 s4)))"

4149 proof -

4150 from Call.prems obtain E where

4151 da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

4152 da_args: "Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A"

4153 by (elim da_elim_cases)

4154 from Call.prems obtain eT argsT where

4155 wt_e: "Env\<turnstile>e\<Colon>-eT" and

4156 wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"

4157 by (elim wt_elim_cases)

4158 note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2`

4159 note s3' = `s3' = check_method_access G accC statT mode

4160 \<lparr>name=mn,parTs=pTs\<rparr> a s3`

4161 have normal_s2: "normal s2"

4162 proof -

4163 from normal_restore_lvars have "normal s4"

4164 by simp

4165 then have "normal s3'"

4166 by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)

4167 with s3' have "normal s3"

4168 by (cases s3) (simp add: check_method_access_def Let_def)

4169 with s3 show "normal s2"

4170 by (cases s2) (simp add: init_lvars_def Let_def)

4171 qed

4172 then have normal_s1: "normal s1"

4173 by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)

4174 note `PROP ?Hyp (In1l e) (Norm s0) s1`

4175 with da_e wt_e G normal_s1

4176 have "nrm E \<subseteq> dom (locals (store s1))"

4177 by simp

4178 with da_args obtain A' where

4179 da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and

4180 nrm_A_A': "nrm A \<subseteq> nrm A'"

4181 by (rule da_weakenE) iprover

4182 note `PROP ?Hyp (In3 args) s1 s2`

4183 with da_args' wt_args G normal_s2

4184 have "nrm A' \<subseteq> dom (locals (store s2))"

4185 by simp

4186 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4187 by blast

4188 also have "\<dots> \<subseteq> dom (locals (store (restore_lvars s2 s4)))"

4189 by (cases s4) simp

4190 finally show ?thesis .

4191 qed

4192 qed

4193 moreover

4194 {

4195 fix j have "abrupt (restore_lvars s2 s4) \<noteq> Some (Jump j)"

4196 proof -

4197 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v

4198 \<rightarrow> (restore_lvars s2 s4)"

4199 unfolding G by (rule eval.Call Call)+

4200 from Call.prems

4201 obtain T' where "T=Inl T'"

4202 by (elim wt_elim_cases) simp

4203 with Call.prems have "Env\<turnstile>({accC,statT,mode}e\<cdot>mn( {pTs}args))\<Colon>-T'"

4204 by simp

4205 from eval _ this

4206 show ?thesis

4207 by (rule eval_expression_no_jump) (simp_all add: G wf)

4208 qed

4209 }

4210 hence "?BreakAssigned (Norm s0) (restore_lvars s2 s4) A"

4211 and "?ResAssigned (Norm s0) (restore_lvars s2 s4)"

4212 by simp_all

4213 ultimately show ?case by (intro conjI)

4214 next

4215 case (Methd s0 D sig v s1 Env T A)

4216 note G = `prg Env = G`

4217 from Methd.prems obtain m where

4218 m: "methd (prg Env) D sig = Some m" and

4219 da_body: "Env\<turnstile>(dom (locals (store ((Norm s0)::state))))

4220 \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A"

4221 by - (erule da_elim_cases)

4222 from Methd.prems m obtain

4223 isCls: "is_class (prg Env) D" and

4224 wt_body: "Env \<turnstile>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<Colon>T"

4225 by - (erule wt_elim_cases,simp)

4226 note `PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1`

4227 moreover

4228 from wt_body have "Env\<turnstile>In1l (body G D sig)\<Colon>T"

4229 using isCls m G by (simp add: body_def2)

4230 moreover

4231 from da_body have "Env\<turnstile>(dom (locals (store ((Norm s0)::state))))

4232 \<guillemotright>\<langle>body G D sig\<rangle>\<guillemotright> A"

4233 using isCls m G by (simp add: body_def2)

4234 ultimately show ?case

4235 using G by simp

4236 next

4237 case (Body s0 D s1 c s2 s3 Env T A)

4238 note G = `prg Env = G`

4239 from Body.prems

4240 have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"

4241 by (elim da_elim_cases) simp

4242 have eval: "prg Env\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)

4243 \<rightarrow>abupd (absorb Ret) s3"

4244 unfolding G by (rule eval.Body Body.hyps)+

4245 hence "nrm A \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"

4246 by (simp only: nrm_A) (rule dom_locals_eval_mono_elim)

4247 hence "?NormalAssigned (abupd (absorb Ret) s3) A"

4248 by simp

4249 moreover

4250 from eval have "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"

4251 by (rule Body_no_jump) simp

4252 hence "?BreakAssigned (Norm s0) (abupd (absorb Ret) s3) A" and

4253 "?ResAssigned (Norm s0) (abupd (absorb Ret) s3)"

4254 by simp_all

4255 ultimately show ?case by (intro conjI)

4256 next

4257 case (LVar s vn Env T A)

4258 from LVar.prems

4259 have "nrm A = dom (locals (store ((Norm s)::state)))"

4260 by (elim da_elim_cases) simp

4261 thus ?case by simp

4262 next

4263 case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC Env T A)

4264 note G = `prg Env = G`

4265 have "?NormalAssigned s3 A"

4266 proof

4267 assume normal_s3: "normal s3"

4268 show "nrm A \<subseteq> dom (locals (store s3))"

4269 proof -

4270 note fvar = `(v, s2') = fvar statDeclC stat fn a s2` and

4271 s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`

4272 from FVar.prems

4273 have da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> A"

4274 by (elim da_elim_cases)

4275 from FVar.prems obtain eT where

4276 wt_e: "Env\<turnstile>e\<Colon>-eT"

4277 by (elim wt_elim_cases)

4278 have "(dom (locals (store ((Norm s0)::state))))

4279 \<subseteq> dom (locals (store s1))"

4280 by (rule dom_locals_eval_mono_elim) (rule FVar.hyps)

4281 with da_e obtain A' where

4282 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and

4283 nrm_A_A': "nrm A \<subseteq> nrm A'"

4284 by (rule da_weakenE) iprover

4285 have normal_s2: "normal s2"

4286 proof -

4287 from normal_s3 s3

4288 have "normal s2'"

4289 by (cases s2') (simp add: check_field_access_def Let_def)

4290 with fvar

4291 show "normal s2"

4292 by (cases s2) (simp add: fvar_def2)

4293 qed

4294 note `PROP ?Hyp (In1l e) s1 s2`

4295 with da_e' wt_e G normal_s2

4296 have "nrm A' \<subseteq> dom (locals (store s2))"

4297 by simp

4298 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4299 by blast

4300 also have "\<dots> \<subseteq> dom (locals (store s3))"

4301 proof -

4302 from fvar have "s2' = snd (fvar statDeclC stat fn a s2)"

4303 by (cases "fvar statDeclC stat fn a s2") simp

4304 hence "dom (locals (store s2)) \<subseteq> dom (locals (store s2'))"

4305 by (simp) (rule dom_locals_fvar_mono)

4306 also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"

4307 by (cases s2') (simp add: check_field_access_def Let_def)

4308 finally show ?thesis .

4309 qed

4310 finally show ?thesis .

4311 qed

4312 qed

4313 moreover

4314 {

4315 fix j have "abrupt s3 \<noteq> Some (Jump j)"

4316 proof -

4317 obtain w upd where v: "(w,upd)=v"

4318 by (cases v) auto

4319 have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"

4320 by (simp only: G v) (rule eval.FVar FVar.hyps)+

4321 from FVar.prems

4322 obtain T' where "T=Inl T'"

4323 by (elim wt_elim_cases) simp

4324 with FVar.prems have "Env\<turnstile>({accC,statDeclC,stat}e..fn)\<Colon>=T'"

4325 by simp

4326 from eval _ this

4327 show ?thesis

4328 by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)

4329 qed

4330 }

4331 hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"

4332 by simp_all

4333 ultimately show ?case by (intro conjI)

4334 next

4335 case (AVar s0 e1 a s1 e2 i s2 v s2' Env T A)

4336 note G = `prg Env = G`

4337 have "?NormalAssigned s2' A"

4338 proof

4339 assume normal_s2': "normal s2'"

4340 show "nrm A \<subseteq> dom (locals (store s2'))"

4341 proof -

4342 note avar = `(v, s2') = avar G i a s2`

4343 from AVar.prems obtain E1 where

4344 da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and

4345 da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"

4346 by (elim da_elim_cases)

4347 from AVar.prems obtain e1T e2T where

4348 wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and

4349 wt_e2: "Env\<turnstile>e2\<Colon>-e2T"

4350 by (elim wt_elim_cases)

4351 from avar normal_s2'

4352 have normal_s2: "normal s2"

4353 by (cases s2) (simp add: avar_def2)

4354 hence "normal s1"

4355 by - (rule eval_no_abrupt_lemma [rule_format], rule AVar, rule normal_s2)

4356 moreover note `PROP ?Hyp (In1l e1) (Norm s0) s1`

4357 ultimately have "nrm E1 \<subseteq> dom (locals (store s1))"

4358 using da_e1 wt_e1 G by simp

4359 with da_e2 obtain A' where

4360 da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and

4361 nrm_A_A': "nrm A \<subseteq> nrm A'"

4362 by (rule da_weakenE) iprover

4363 note `PROP ?Hyp (In1l e2) s1 s2`

4364 with da_e2' wt_e2 G normal_s2

4365 have "nrm A' \<subseteq> dom (locals (store s2))"

4366 by simp

4367 with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"

4368 by blast

4369 also have "\<dots> \<subseteq> dom (locals (store s2'))"

4370 proof -

4371 from avar have "s2' = snd (avar G i a s2)"

4372 by (cases "(avar G i a s2)") simp

4373 thus "dom (locals (store s2)) \<subseteq> dom (locals (store s2'))"

4374 by (simp) (rule dom_locals_avar_mono)

4375 qed

4376 finally show ?thesis .

4377 qed

4378 qed

4379 moreover

4380 {

4381 fix j have "abrupt s2' \<noteq> Some (Jump j)"

4382 proof -

4383 obtain w upd where v: "(w,upd)=v"

4384 by (cases v) auto

4385 have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"

4386 unfolding G v by (rule eval.AVar AVar.hyps)+

4387 from AVar.prems

4388 obtain T' where "T=Inl T'"

4389 by (elim wt_elim_cases) simp

4390 with AVar.prems have "Env\<turnstile>(e1.[e2])\<Colon>=T'"

4391 by simp

4392 from eval _ this

4393 show ?thesis

4394 by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)

4395 qed

4396 }

4397 hence "?BreakAssigned (Norm s0) s2' A" and "?ResAssigned (Norm s0) s2'"

4398 by simp_all

4399 ultimately show ?case by (intro conjI)

4400 next

4401 case (Nil s0 Env T A)

4402 from Nil.prems

4403 have "nrm A = dom (locals (store ((Norm s0)::state)))"

4404 by (elim da_elim_cases) simp

4405 thus ?case by simp

4406 next

4407 case (Cons s0 e v s1 es vs s2 Env T A)

4408 note G = `prg Env = G`

4409 have "?NormalAssigned s2 A"

4410 proof

4411 assume normal_s2: "normal s2"

4412 show "nrm A \<subseteq> dom (locals (store s2))"

4413 proof -

4414 from Cons.prems obtain E where

4415 da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and

4416 da_es: "Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A"

4417 by (elim da_elim_cases)

4418 from Cons.prems obtain eT esT where

4419 wt_e: "Env\<turnstile>e\<Colon>-eT" and

4420 wt_es: "Env\<turnstile>es\<Colon>\<doteq>esT"

4421 by (elim wt_elim_cases)

4422 have "normal s1"

4423 by - (rule eval_no_abrupt_lemma [rule_format], rule Cons.hyps, rule normal_s2)

4424 moreover note `PROP ?Hyp (In1l e) (Norm s0) s1`

4425 ultimately have "nrm E \<subseteq> dom (locals (store s1))"

4426 using da_e wt_e G by simp

4427 with da_es obtain A' where

4428 da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and

4429 nrm_A_A': "nrm A \<subseteq> nrm A'"

4430 by (rule da_weakenE) iprover

4431 note `PROP ?Hyp (In3 es) s1 s2`

4432 with da_es' wt_es G normal_s2

4433 have "nrm A' \<subseteq> dom (locals (store s2))"

4434 by simp

4435 with nrm_A_A' show "nrm A \<subseteq> dom (locals (store s2))"

4436 by blast

4437 qed

4438 qed

4439 moreover

4440 {

4441 fix j have "abrupt s2 \<noteq> Some (Jump j)"

4442 proof -

4443 have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"

4444 unfolding G by (rule eval.Cons Cons.hyps)+

4445 from Cons.prems

4446 obtain T' where "T=Inr T'"

4447 by (elim wt_elim_cases) simp

4448 with Cons.prems have "Env\<turnstile>(e # es)\<Colon>\<doteq>T'"

4449 by simp

4450 from eval _ this

4451 show ?thesis

4452 by (rule eval_expression_list_no_jump) (simp_all add: G wf)

4453 qed

4454 }

4455 hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"

4456 by simp_all

4457 ultimately show ?case by (intro conjI)

4458 qed

4459 qed

4461 lemma da_good_approxE:

4462 assumes

4463 "prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" and "Env\<turnstile>t\<Colon>T" and

4464 "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" and "wf_prog (prg Env)"

4465 obtains

4466 "normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1))" and

4467 "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>

4468 \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and

4469 "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>\<Longrightarrow>Result \<in> dom (locals (store s1))"

4470 using assms by - (drule (3) da_good_approx, simp)

4473 (* Same as above but with explicit environment;

4474 It would be nicer to find a "normalized" way to right down those things

4475 in Bali.

4476 *)

4477 lemma da_good_approxE':

4478 assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"

4479 and wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T"

4480 and da: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"

4481 and wf: "wf_prog G"

4482 obtains "normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1))" and

4483 "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>

4484 \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and

4485 "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>

4486 \<Longrightarrow> Result \<in> dom (locals (store s1))"

4487 proof -

4488 from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" by simp

4489 moreover note wt da

4490 moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp

4491 ultimately show thesis

4492 using that by (rule da_good_approxE) iprover+

4493 qed

4495 declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]

4497 end