subsection ‹Correctness of Definite Assignment› theory DefiniteAssignmentCorrect imports WellForm Eval begin declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]] lemma sxalloc_no_jump: assumes sxalloc: "G⊢s0 ─sxalloc→ s1" and no_jmp: "abrupt s0 ≠ Some (Jump j)" shows "abrupt s1 ≠ Some (Jump j)" using sxalloc no_jmp by cases simp_all lemma sxalloc_no_jump': assumes sxalloc: "G⊢s0 ─sxalloc→ s1" and jump: "abrupt s1 = Some (Jump j)" shows "abrupt s0 = Some (Jump j)" using sxalloc jump by cases simp_all lemma halloc_no_jump: assumes halloc: "G⊢s0 ─halloc oi≻a→ s1" and no_jmp: "abrupt s0 ≠ Some (Jump j)" shows "abrupt s1 ≠ Some (Jump j)" using halloc no_jmp by cases simp_all lemma halloc_no_jump': assumes halloc: "G⊢s0 ─halloc oi≻a→ s1" and jump: "abrupt s1 = Some (Jump j)" shows "abrupt s0 = Some (Jump j)" using halloc jump by cases simp_all lemma Body_no_jump: assumes eval: "G⊢s0 ─Body D c-≻v→s1" and jump: "abrupt s0 ≠ Some (Jump j)" shows "abrupt s1 ≠ Some (Jump j)" proof (cases "normal s0") case True with eval obtain s0' where eval': "G⊢Norm s0' ─Body D c-≻v→s1" and s0: "s0 = Norm s0'" by (cases s0) simp from eval' obtain s2 where s1: "s1 = abupd (absorb Ret) (if ∃l. abrupt s2 = Some (Jump (Break l)) ∨ abrupt s2 = Some (Jump (Cont l)) then abupd (λx. Some (Error CrossMethodJump)) s2 else s2)" by cases simp show ?thesis proof (cases "∃l. abrupt s2 = Some (Jump (Break l)) ∨ abrupt s2 = Some (Jump (Cont l))") case True with s1 have "abrupt s1 = Some (Error CrossMethodJump)" by (cases s2) simp thus ?thesis by simp next case False with s1 have "s1=abupd (absorb Ret) s2" by simp with False show ?thesis by (cases s2,cases j) (auto simp add: absorb_def) qed next case False with eval obtain s0' abr where "G⊢(Some abr,s0') ─Body D c-≻v→s1" "s0 = (Some abr, s0')" by (cases s0) fastforce with this jump show ?thesis by (cases) (simp) qed lemma Methd_no_jump: assumes eval: "G⊢s0 ─Methd D sig-≻v→ s1" and jump: "abrupt s0 ≠ Some (Jump j)" shows "abrupt s1 ≠ Some (Jump j)" proof (cases "normal s0") case True with eval obtain s0' where "G⊢Norm s0' ─Methd D sig-≻v→s1" "s0 = Norm s0'" by (cases s0) simp then obtain D' body where "G⊢s0 ─Body D' body-≻v→s1" by (cases) (simp add: body_def2) from this jump show ?thesis by (rule Body_no_jump) next case False with eval obtain s0' abr where "G⊢(Some abr,s0') ─Methd D sig-≻v→s1" "s0 = (Some abr, s0')" by (cases s0) fastforce with this jump show ?thesis by (cases) (simp) qed lemma jumpNestingOkS_mono: assumes jumpNestingOk_l': "jumpNestingOkS jmps' c" and subset: "jmps' ⊆ jmps" shows "jumpNestingOkS jmps c" proof - have True and True and "⋀ jmps' jmps. ⟦jumpNestingOkS jmps' c; jmps' ⊆ jmps⟧ ⟹ jumpNestingOkS jmps c" proof (induct rule: var.induct expr.induct stmt.induct) case (Lab j c jmps' jmps) note jmpOk = ‹jumpNestingOkS jmps' (j∙ c)› note jmps = ‹jmps' ⊆ jmps› with jmpOk have "jumpNestingOkS ({j} ∪ jmps') c" by simp moreover from jmps have "({j} ∪ jmps') ⊆ ({j} ∪ jmps)" by auto ultimately have "jumpNestingOkS ({j} ∪ jmps) c" by (rule Lab.hyps) thus ?case by simp next case (Jmp j jmps' jmps) thus ?case by (cases j) auto next case (Comp c1 c2 jmps' jmps) from Comp.prems have "jumpNestingOkS jmps c1" by - (rule Comp.hyps,auto) moreover from Comp.prems have "jumpNestingOkS jmps c2" by - (rule Comp.hyps,auto) ultimately show ?case by simp next case (If' e c1 c2 jmps' jmps) from If'.prems have "jumpNestingOkS jmps c1" by - (rule If'.hyps,auto) moreover from If'.prems have "jumpNestingOkS jmps c2" by - (rule If'.hyps,auto) ultimately show ?case by simp next case (Loop l e c jmps' jmps) from ‹jumpNestingOkS jmps' (l∙ While(e) c)› have "jumpNestingOkS ({Cont l} ∪ jmps') c" by simp moreover from ‹jmps' ⊆ jmps› have "{Cont l} ∪ jmps' ⊆ {Cont l} ∪ jmps" by auto ultimately have "jumpNestingOkS ({Cont l} ∪ jmps) c" by (rule Loop.hyps) thus ?case by simp next case (TryC c1 C vn c2 jmps' jmps) from TryC.prems have "jumpNestingOkS jmps c1" by - (rule TryC.hyps,auto) moreover from TryC.prems have "jumpNestingOkS jmps c2" by - (rule TryC.hyps,auto) ultimately show ?case by simp next case (Fin c1 c2 jmps' jmps) from Fin.prems have "jumpNestingOkS jmps c1" by - (rule Fin.hyps,auto) moreover from Fin.prems have "jumpNestingOkS jmps c2" by - (rule Fin.hyps,auto) ultimately show ?case by simp qed (simp_all) with jumpNestingOk_l' subset show ?thesis by iprover qed corollary jumpNestingOk_mono: assumes jmpOk: "jumpNestingOk jmps' t" and subset: "jmps' ⊆ jmps" shows "jumpNestingOk jmps t" proof (cases t) case (In1 expr_stmt) show ?thesis proof (cases expr_stmt) case (Inl e) with In1 show ?thesis by simp next case (Inr s) with In1 jmpOk subset show ?thesis by (auto intro: jumpNestingOkS_mono) qed qed (simp_all) lemma assign_abrupt_propagation: assumes f_ok: "abrupt (f n s) ≠ x" and ass: "abrupt (assign f n s) = x" shows "abrupt s = x" proof (cases x) case None with ass show ?thesis by (cases s) (simp add: assign_def Let_def) next case (Some xcpt) from f_ok obtain xf sf where "f n s = (xf,sf)" by (cases "f n s") with Some ass f_ok show ?thesis by (cases s) (simp add: assign_def Let_def) qed lemma wt_init_comp_ty': "is_acc_type (prg Env) (pid (cls Env)) T ⟹ Env⊢init_comp_ty T∷√" apply (unfold init_comp_ty_def) apply (clarsimp simp add: accessible_in_RefT_simp is_acc_type_def is_acc_class_def) done lemma fvar_upd_no_jump: assumes upd: "upd = snd (fst (fvar statDeclC stat fn a s'))" and noJmp: "abrupt s ≠ Some (Jump j)" shows "abrupt (upd val s) ≠ Some (Jump j)" proof (cases "stat") case True with noJmp upd show ?thesis by (cases s) (simp add: fvar_def2) next case False with noJmp upd show ?thesis by (cases s) (simp add: fvar_def2) qed lemma avar_state_no_jump: assumes jmp: "abrupt (snd (avar G i a s)) = Some (Jump j)" shows "abrupt s = Some (Jump j)" proof (cases "normal s") case True with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def) next case False with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def) qed lemma avar_upd_no_jump: assumes upd: "upd = snd (fst (avar G i a s'))" and noJmp: "abrupt s ≠ Some (Jump j)" shows "abrupt (upd val s) ≠ Some (Jump j)" using upd noJmp by (cases s) (simp add: avar_def2 abrupt_if_def) text ‹ The next theorem expresses: If jumps (breaks, continues, returns) are nested correctly, we won't find an unexpected jump in the result state of the evaluation. For exeample, a break can't leave its enclosing loop, an return cant leave its enclosing method. To proove this, the method call is critical. Allthough the wellformedness of the whole program guarantees that the jumps (breaks,continues and returns) are nested correctly in all method bodies, the call rule alone does not guarantee that I will call a method or even a class that is part of the program due to dynamic binding! To be able to enshure this we need a kind of conformance of the state, like in the typesafety proof. But then we will redo the typesafty proof here. It would be nice if we could find an easy precondition that will guarantee that all calls will actually call classes and methods of the current program, which can be instantiated in the typesafty proof later on. To fix this problem, I have instrumented the semantic definition of a call to filter out any breaks in the state and to throw an error instead. To get an induction hypothesis which is strong enough to perform the proof, we can't just assume \<^term>‹jumpNestingOk› for the empty set and conlcude, that no jump at all will be in the resulting state, because the set is altered by the statements \<^term>‹Lab› and \<^term>‹While›. The wellformedness of the program is used to enshure that for all classinitialisations and methods the nesting of jumps is wellformed, too. › theorem jumpNestingOk_eval: assumes eval: "G⊢ s0 ─t≻→ (v,s1)" and jmpOk: "jumpNestingOk jmps t" and wt: "Env⊢t∷T" and wf: "wf_prog G" and G: "prg Env = G" and no_jmp: "∀j. abrupt s0 = Some (Jump j) ⟶ j ∈ jmps" (is "?Jmp jmps s0") shows "(∀j. fst s1 = Some (Jump j) ⟶ j ∈ jmps) ∧ (normal s1 ⟶ (∀ w upd. v=In2 (w,upd) ⟶ (∀ s j val. abrupt s ≠ Some (Jump j) ⟶ abrupt (upd val s) ≠ Some (Jump j))))" (is "?Jmp jmps s1 ∧ ?Upd v s1") proof - let ?HypObj = "λ t s0 s1 v. (∀ jmps T Env. ?Jmp jmps s0 ⟶ jumpNestingOk jmps t ⟶ Env⊢t∷T ⟶ prg Env=G⟶ ?Jmp jmps s1 ∧ ?Upd v s1)" ― ‹Variable ‹?HypObj› is the following goal spelled in terms of the object logic, instead of the meta logic. It is needed in some cases of the induction were, the atomize-rulify process of induct does not work fine, because the eval rules mix up object and meta logic. See for example the case for the loop.› from eval have "⋀ jmps T Env. ⟦?Jmp jmps s0; jumpNestingOk jmps t; Env⊢t∷T;prg Env=G⟧ ⟹ ?Jmp jmps s1 ∧ ?Upd v s1" (is "PROP ?Hyp t s0 s1 v") ― ‹We need to abstract over \<^term>‹jmps› since \<^term>‹jmps› are extended during analysis of \<^term>‹Lab›. Also we need to abstract over \<^term>‹T› and \<^term>‹Env› since they are altered in various typing judgements.› proof (induct) case Abrupt thus ?case by simp next case Skip thus ?case by simp next case Expr thus ?case by (elim wt_elim_cases) simp next case (Lab s0 c s1 jmp jmps T Env) note jmpOK = ‹jumpNestingOk jmps (In1r (jmp∙ c))› note G = ‹prg Env = G› have wt_c: "Env⊢c∷√" using Lab.prems by (elim wt_elim_cases) { fix j assume ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)" have "j∈jmps" proof - from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)" by (cases s1) (simp add: absorb_def) note hyp_c = ‹PROP ?Hyp (In1r c) (Norm s0) s1 ♢› from ab_s1 have "j ≠ jmp" by (cases s1) (simp add: absorb_def) moreover have "j ∈ {jmp} ∪ jmps" proof - from jmpOK have "jumpNestingOk ({jmp} ∪ jmps) (In1r c)" by simp with wt_c jmp_s1 G hyp_c show ?thesis by - (rule hyp_c [THEN conjunct1,rule_format],simp) qed ultimately show ?thesis by simp qed } thus ?case by simp next case (Comp s0 c1 s1 c2 s2 jmps T Env) note jmpOk = ‹jumpNestingOk jmps (In1r (c1;; c2))› note G = ‹prg Env = G› from Comp.prems obtain wt_c1: "Env⊢c1∷√" and wt_c2: "Env⊢c2∷√" by (elim wt_elim_cases) { fix j assume abr_s2: "abrupt s2 = Some (Jump j)" have "j∈jmps" proof - have jmp: "?Jmp jmps s1" proof - note hyp_c1 = ‹PROP ?Hyp (In1r c1) (Norm s0) s1 ♢› with wt_c1 jmpOk G show ?thesis by simp qed moreover note hyp_c2 = ‹PROP ?Hyp (In1r c2) s1 s2 (♢::vals)› have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp moreover note wt_c2 G abr_s2 ultimately show "j ∈ jmps" by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)]) qed } thus ?case by simp next case (If s0 e b s1 c1 c2 s2 jmps T Env) note jmpOk = ‹jumpNestingOk jmps (In1r (If(e) c1 Else c2))› note G = ‹prg Env = G› from If.prems obtain wt_e: "Env⊢e∷-PrimT Boolean" and wt_then_else: "Env⊢(if the_Bool b then c1 else c2)∷√" by (elim wt_elim_cases) simp { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j∈jmps" proof - note ‹PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)› with wt_e G have "?Jmp jmps s1" by simp moreover note hyp_then_else = ‹PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 ♢› have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))" using jmpOk by (cases "the_Bool b") simp_all moreover note wt_then_else G jmp ultimately show "j∈ jmps" by (rule hyp_then_else [THEN conjunct1,rule_format (no_asm)]) qed } thus ?case by simp next case (Loop s0 e b s1 c s2 l s3 jmps T Env) note jmpOk = ‹jumpNestingOk jmps (In1r (l∙ While(e) c))› note G = ‹prg Env = G› note wt = ‹Env⊢In1r (l∙ While(e) c)∷T› then obtain wt_e: "Env⊢e∷-PrimT Boolean" and wt_c: "Env⊢c∷√" by (elim wt_elim_cases) { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j∈jmps" proof - note ‹PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)› with wt_e G have jmp_s1: "?Jmp jmps s1" by simp show ?thesis proof (cases "the_Bool b") case False from Loop.hyps have "s3=s1" by (simp (no_asm_use) only: if_False False) with jmp_s1 jmp have "j ∈ jmps" by simp thus ?thesis by simp next case True from Loop.hyps (* Because of the mixture of object and pure logic in the rule eval.If the atomization-rulification of the induct method leaves the hypothesis in object logic *) have "?HypObj (In1r c) s1 s2 (♢::vals)" apply (simp (no_asm_use) only: True if_True ) apply (erule conjE)+ apply assumption done note hyp_c = this [rule_format (no_asm)] moreover from jmpOk have "jumpNestingOk ({Cont l} ∪ jmps) (In1r c)" by simp moreover from jmp_s1 have "?Jmp ({Cont l} ∪ jmps) s1" by simp ultimately have jmp_s2: "?Jmp ({Cont l} ∪ jmps) s2" using wt_c G by iprover have "?Jmp jmps (abupd (absorb (Cont l)) s2)" proof - { fix j' assume abs: "abrupt (abupd (absorb (Cont l)) s2)=Some (Jump j')" have "j' ∈ jmps" proof (cases "j' = Cont l") case True with abs show ?thesis by (cases s2) (simp add: absorb_def) next case False with abs have "abrupt s2 = Some (Jump j')" by (cases s2) (simp add: absorb_def) with jmp_s2 False show ?thesis by simp qed } thus ?thesis by simp qed moreover from Loop.hyps have "?HypObj (In1r (l∙ While(e) c)) (abupd (absorb (Cont l)) s2) s3 (♢::vals)" apply (simp (no_asm_use) only: True if_True) apply (erule conjE)+ apply assumption done note hyp_w = this [rule_format (no_asm)] note jmpOk wt G jmp ultimately show "j∈ jmps" by (rule hyp_w [THEN conjunct1,rule_format (no_asm)]) qed qed } thus ?case by simp next case (Jmp s j jmps T Env) thus ?case by simp next case (Throw s0 e a s1 jmps T Env) note jmpOk = ‹jumpNestingOk jmps (In1r (Throw e))› note G = ‹prg Env = G› from Throw.prems obtain Te where wt_e: "Env⊢e∷-Te" by (elim wt_elim_cases) { fix j assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)" have "j∈jmps" proof - from ‹PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)› have "?Jmp jmps s1" using wt_e G by simp moreover from jmp have "abrupt s1 = Some (Jump j)" by (cases s1) (simp add: throw_def abrupt_if_def) ultimately show "j ∈ jmps" by simp qed } thus ?case by simp next case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env) note jmpOk = ‹jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))› note G = ‹prg Env = G› from Try.prems obtain wt_c1: "Env⊢c1∷√" and wt_c2: "Env⦇lcl := lcl Env(VName vn↦Class C)⦈⊢c2∷√" by (elim wt_elim_cases) { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j∈jmps" proof - note ‹PROP ?Hyp (In1r c1) (Norm s0) s1 (♢::vals)› with jmpOk wt_c1 G have jmp_s1: "?Jmp jmps s1" by simp note s2 = ‹G⊢s1 ─sxalloc→ s2› show "j ∈ jmps" proof (cases "G,s2⊢catch C") case False from Try.hyps have "s3=s2" by (simp (no_asm_use) only: False if_False) with jmp have "abrupt s1 = Some (Jump j)" using sxalloc_no_jump' [OF s2] by simp with jmp_s1 show ?thesis by simp next case True with Try.hyps have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3 (♢::vals)" apply (simp (no_asm_use) only: True if_True simp_thms) apply (erule conjE)+ apply assumption done note hyp_c2 = this [rule_format (no_asm)] from jmp_s1 sxalloc_no_jump' [OF s2] have "?Jmp jmps s2" by simp hence "?Jmp jmps (new_xcpt_var vn s2)" by (cases s2) simp moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp moreover note wt_c2 moreover from G have "prg (Env⦇lcl := lcl Env(VName vn↦Class C)⦈) = G" by simp moreover note jmp ultimately show ?thesis by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)]) qed qed } thus ?case by simp next case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env) note jmpOk = ‹jumpNestingOk jmps (In1r (c1 Finally c2))› note G = ‹prg Env = G› from Fin.prems obtain wt_c1: "Env⊢c1∷√" and wt_c2: "Env⊢c2∷√" by (elim wt_elim_cases) { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j ∈ jmps" proof (cases "x1=Some (Jump j)") case True note hyp_c1 = ‹PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) ♢› with True jmpOk wt_c1 G show ?thesis by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all) next case False note hyp_c2 = ‹PROP ?Hyp (In1r c2) (Norm s1) s2 ♢› note ‹s3 = (if ∃err. x1 = Some (Error err) then (x1, s1) else abupd (abrupt_if (x1 ≠ None) x1) s2)› with False jmp have "abrupt s2 = Some (Jump j)" by (cases s2) (simp add: abrupt_if_def) with jmpOk wt_c2 G show ?thesis by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all) qed } thus ?case by simp next case (Init C c s0 s3 s1 s2 jmps T Env) note ‹jumpNestingOk jmps (In1r (Init C))› note G = ‹prg Env = G› note ‹the (class G C) = c› with Init.prems have c: "class G C = Some c" by (elim wt_elim_cases) auto { fix j assume jmp: "abrupt s3 = (Some (Jump j))" have "j∈jmps" proof (cases "inited C (globs s0)") case True with Init.hyps have "s3=Norm s0" by simp with jmp have "False" by simp thus ?thesis .. next case False from wf c G have wf_cdecl: "wf_cdecl G (C,c)" by (simp add: wf_prog_cdecl) from Init.hyps have "?HypObj (In1r (if C = Object then Skip else Init (super c))) (Norm ((init_class_obj G C) s0)) s1 (♢::vals)" apply (simp (no_asm_use) only: False if_False simp_thms) apply (erule conjE)+ apply assumption done note hyp_s1 = this [rule_format (no_asm)] from wf_cdecl G have wt_super: "Env⊢(if C = Object then Skip else Init (super c))∷√" by (cases "C=Object") (auto dest: wf_cdecl_supD is_acc_classD) from hyp_s1 [OF _ _ wt_super G] have "?Jmp jmps s1" by simp hence jmp_s1: "?Jmp jmps ((set_lvars Map.empty) s1)" by (cases s1) simp from False Init.hyps have "?HypObj (In1r (init c)) ((set_lvars Map.empty) s1) s2 (♢::vals)" apply (simp (no_asm_use) only: False if_False simp_thms) apply (erule conjE)+ apply assumption done note hyp_init_c = this [rule_format (no_asm)] from wf_cdecl have wt_init_c: "⦇prg = G, cls = C, lcl = Map.empty⦈⊢init c∷√" by (rule wf_cdecl_wt_init) from wf_cdecl have "jumpNestingOkS {} (init c)" by (cases rule: wf_cdeclE) hence "jumpNestingOkS jmps (init c)" by (rule jumpNestingOkS_mono) simp moreover have "abrupt s2 = Some (Jump j)" proof - from False Init.hyps have "s3 = (set_lvars (locals (store s1))) s2" by simp with jmp show ?thesis by (cases s2) simp qed ultimately show ?thesis using hyp_init_c [OF jmp_s1 _ wt_init_c] by simp qed } thus ?case by simp next case (NewC s0 C s1 a s2 jmps T Env) { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j∈jmps" proof - note ‹prg Env = G› moreover note hyp_init = ‹PROP ?Hyp (In1r (Init C)) (Norm s0) s1 ♢› moreover from wf NewC.prems have "Env⊢(Init C)∷√" by (elim wt_elim_cases) (drule is_acc_classD,simp) moreover have "abrupt s1 = Some (Jump j)" proof - from ‹G⊢s1 ─halloc CInst C≻a→ s2› and jmp show ?thesis by (rule halloc_no_jump') qed ultimately show "j ∈ jmps" by - (rule hyp_init [THEN conjunct1,rule_format (no_asm)],auto) qed } thus ?case by simp next case (NewA s0 elT s1 e i s2 a s3 jmps T Env) { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j∈jmps" proof - note G = ‹prg Env = G› from NewA.prems obtain wt_init: "Env⊢init_comp_ty elT∷√" and wt_size: "Env⊢e∷-PrimT Integer" by (elim wt_elim_cases) (auto dest: wt_init_comp_ty') note ‹PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 ♢› with wt_init G have "?Jmp jmps s1" by (simp add: init_comp_ty_def) moreover note hyp_e = ‹PROP ?Hyp (In1l e) s1 s2 (In1 i)› have "abrupt s2 = Some (Jump j)" proof - note ‹G⊢abupd (check_neg i) s2─halloc Arr elT (the_Intg i)≻a→ s3› moreover note jmp ultimately have "abrupt (abupd (check_neg i) s2) = Some (Jump j)" by (rule halloc_no_jump') thus ?thesis by (cases s2) auto qed ultimately show "j∈jmps" using wt_size G by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all) qed } thus ?case by simp next case (Cast s0 e v s1 s2 cT jmps T Env) { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j∈jmps" proof - note hyp_e = ‹PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)› note ‹prg Env = G› moreover from Cast.prems obtain eT where "Env⊢e∷-eT" by (elim wt_elim_cases) moreover have "abrupt s1 = Some (Jump j)" proof - note ‹s2 = abupd (raise_if (¬ G,snd s1⊢v fits cT) ClassCast) s1› moreover note jmp ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def) qed ultimately show ?thesis by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all) qed } thus ?case by simp next case (Inst s0 e v s1 b eT jmps T Env) { fix j assume jmp: "abrupt s1 = Some (Jump j)" have "j∈jmps" proof - note hyp_e = ‹PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)› note ‹prg Env = G› moreover from Inst.prems obtain eT where "Env⊢e∷-eT" by (elim wt_elim_cases) moreover note jmp ultimately show "j∈jmps" by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all) qed } thus ?case by simp next case Lit thus ?case by simp next case (UnOp s0 e v s1 unop jmps T Env) { fix j assume jmp: "abrupt s1 = Some (Jump j)" have "j∈jmps" proof - note hyp_e = ‹PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)› note ‹prg Env = G› moreover from UnOp.prems obtain eT where "Env⊢e∷-eT" by (elim wt_elim_cases) moreover note jmp ultimately show "j∈jmps" by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all) qed } thus ?case by simp next case (BinOp s0 e1 v1 s1 binop e2 v2 s2 jmps T Env) { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j∈jmps" proof - note G = ‹prg Env = G› from BinOp.prems obtain e1T e2T where wt_e1: "Env⊢e1∷-e1T" and wt_e2: "Env⊢e2∷-e2T" by (elim wt_elim_cases) note ‹PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)› with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp note hyp_e2 = ‹PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip) s1 s2 (In1 v2)› show "j∈jmps" proof (cases "need_second_arg binop v1") case True with jmp_s1 wt_e2 jmp G show ?thesis by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],simp_all) next case False with jmp_s1 jmp G show ?thesis by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],auto) qed qed } thus ?case by simp next case Super thus ?case by simp next case (Acc s0 va v f s1 jmps T Env) { fix j assume jmp: "abrupt s1 = Some (Jump j)" have "j∈jmps" proof - note hyp_va = ‹PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))› note ‹prg Env = G› moreover from Acc.prems obtain vT where "Env⊢va∷=vT" by (elim wt_elim_cases) moreover note jmp ultimately show "j∈jmps" by - (rule hyp_va [THEN conjunct1,rule_format (no_asm)], simp_all) qed } thus ?case by simp next case (Ass s0 va w f s1 e v s2 jmps T Env) note G = ‹prg Env = G› from Ass.prems obtain vT eT where wt_va: "Env⊢va∷=vT" and wt_e: "Env⊢e∷-eT" by (elim wt_elim_cases) note hyp_v = ‹PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))› note hyp_e = ‹PROP ?Hyp (In1l e) s1 s2 (In1 v)› { fix j assume jmp: "abrupt (assign f v s2) = Some (Jump j)" have "j∈jmps" proof - have "abrupt s2 = Some (Jump j)" proof (cases "normal s2") case True from ‹G⊢s1 ─e-≻v→ s2› and True have nrm_s1: "normal s1" by (rule eval_no_abrupt_lemma [rule_format]) with nrm_s1 wt_va G True have "abrupt (f v s2) ≠ Some (Jump j)" using hyp_v [THEN conjunct2,rule_format (no_asm)] by simp from this jmp show ?thesis by (rule assign_abrupt_propagation) next case False with jmp show ?thesis by (cases s2) (simp add: assign_def Let_def) qed moreover from wt_va G have "?Jmp jmps s1" by - (rule hyp_v [THEN conjunct1],simp_all) ultimately show ?thesis using G by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e) qed } thus ?case by simp next case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env) note G = ‹prg Env = G› note hyp_e0 = ‹PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)› note hyp_e1_e2 = ‹PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)› from Cond.prems obtain e1T e2T where wt_e0: "Env⊢e0∷-PrimT Boolean" and wt_e1: "Env⊢e1∷-e1T" and wt_e2: "Env⊢e2∷-e2T" by (elim wt_elim_cases) { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j∈jmps" proof - from wt_e0 G have jmp_s1: "?Jmp jmps s1" by - (rule hyp_e0 [THEN conjunct1],simp_all) show ?thesis proof (cases "the_Bool b") case True with jmp_s1 wt_e1 G jmp show ?thesis by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all) next case False with jmp_s1 wt_e2 G jmp show ?thesis by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all) qed qed } thus ?case by simp next case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4 jmps T Env) note G = ‹prg Env = G› from Call.prems obtain eT argsT where wt_e: "Env⊢e∷-eT" and wt_args: "Env⊢args∷≐argsT" by (elim wt_elim_cases) { fix j assume jmp: "abrupt ((set_lvars (locals (store s2))) s4) = Some (Jump j)" have "j∈jmps" proof - note hyp_e = ‹PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)› from wt_e G have jmp_s1: "?Jmp jmps s1" by - (rule hyp_e [THEN conjunct1],simp_all) note hyp_args = ‹PROP ?Hyp (In3 args) s1 s2 (In3 vs)› have "abrupt s2 = Some (Jump j)" proof - note ‹G⊢s3' ─Methd D ⦇name = mn, parTs = pTs⦈-≻v→ s4› moreover from jmp have "abrupt s4 = Some (Jump j)" by (cases s4) simp ultimately have "abrupt s3' = Some (Jump j)" by - (rule ccontr,drule (1) Methd_no_jump,simp) moreover note ‹s3' = check_method_access G accC statT mode ⦇name = mn, parTs = pTs⦈ a s3› ultimately have "abrupt s3 = Some (Jump j)" by (cases s3) (simp add: check_method_access_def abrupt_if_def Let_def) moreover note ‹s3 = init_lvars G D ⦇name=mn, parTs=pTs⦈ mode a vs s2› ultimately show ?thesis by (cases s2) (auto simp add: init_lvars_def2) qed with jmp_s1 wt_args G show ?thesis by - (rule hyp_args [THEN conjunct1,rule_format (no_asm)], simp_all) qed } thus ?case by simp next case (Methd s0 D sig v s1 jmps T Env) from ‹G⊢Norm s0 ─body G D sig-≻v→ s1› have "G⊢Norm s0 ─Methd D sig-≻v→ s1" by (rule eval.Methd) hence "⋀ j. abrupt s1 ≠ Some (Jump j)" by (rule Methd_no_jump) simp thus ?case by simp next case (Body s0 D s1 c s2 s3 jmps T Env) have "G⊢Norm s0 ─Body D c-≻the (locals (store s2) Result) → abupd (absorb Ret) s3" by (rule eval.Body) (rule Body)+ hence "⋀ j. abrupt (abupd (absorb Ret) s3) ≠ Some (Jump j)" by (rule Body_no_jump) simp thus ?case by simp next case LVar thus ?case by (simp add: lvar_def Let_def) next case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env) note G = ‹prg Env = G› from wf FVar.prems obtain statC f where wt_e: "Env⊢e∷-Class statC" and accfield: "accfield (prg Env) accC statC fn = Some (statDeclC,f)" by (elim wt_elim_cases) simp have wt_init: "Env⊢Init statDeclC∷√" proof - from wf wt_e G have "is_class (prg Env) statC" by (auto dest: ty_expr_is_type type_is_class) with wf accfield G have "is_class (prg Env) statDeclC" by (auto dest!: accfield_fields dest: fields_declC) thus ?thesis by simp qed note fvar = ‹(v, s2') = fvar statDeclC stat fn a s2› { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j∈jmps" proof - note hyp_init = ‹PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 ♢› from G wt_init have "?Jmp jmps s1" by - (rule hyp_init [THEN conjunct1],auto) moreover note hyp_e = ‹PROP ?Hyp (In1l e) s1 s2 (In1 a)› have "abrupt s2 = Some (Jump j)" proof - note ‹s3 = check_field_access G accC statDeclC fn stat a s2'› with jmp have "abrupt s2' = Some (Jump j)" by (cases s2') (simp add: check_field_access_def abrupt_if_def Let_def) with fvar show "abrupt s2 = Some (Jump j)" by (cases s2) (simp add: fvar_def2 abrupt_if_def) qed ultimately show ?thesis using G wt_e by - (rule hyp_e [THEN conjunct1, rule_format (no_asm)],simp_all) qed } moreover from fvar obtain upd w where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and v: "v=(w,upd)" by (cases "fvar statDeclC stat fn a s2") simp { fix j val fix s::state assume "normal s3" assume no_jmp: "abrupt s ≠ Some (Jump j)" with upd have "abrupt (upd val s) ≠ Some (Jump j)" by (rule fvar_upd_no_jump) } ultimately show ?case using v by simp next case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env) note G = ‹prg Env = G› from AVar.prems obtain e1T e2T where wt_e1: "Env⊢e1∷-e1T" and wt_e2: "Env⊢e2∷-e2T" by (elim wt_elim_cases) simp note avar = ‹(v, s2') = avar G i a s2› { fix j assume jmp: "abrupt s2' = Some (Jump j)" have "j∈jmps" proof - note hyp_e1 = ‹PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)› from G wt_e1 have "?Jmp jmps s1" by - (rule hyp_e1 [THEN conjunct1], auto) moreover note hyp_e2 = ‹PROP ?Hyp (In1l e2) s1 s2 (In1 i)› have "abrupt s2 = Some (Jump j)" proof - from avar have "s2' = snd (avar G i a s2)" by (cases "avar G i a s2") simp with jmp show ?thesis by - (rule avar_state_no_jump,simp) qed ultimately show ?thesis using wt_e2 G by - (rule hyp_e2 [THEN conjunct1, rule_format (no_asm)],simp_all) qed } moreover from avar obtain upd w where upd: "upd = snd (fst (avar G i a s2))" and v: "v=(w,upd)" by (cases "avar G i a s2") simp { fix j val fix s::state assume "normal s2'" assume no_jmp: "abrupt s ≠ Some (Jump j)" with upd have "abrupt (upd val s) ≠ Some (Jump j)" by (rule avar_upd_no_jump) } ultimately show ?case using v by simp next case Nil thus ?case by simp next case (Cons s0 e v s1 es vs s2 jmps T Env) note G = ‹prg Env = G› from Cons.prems obtain eT esT where wt_e: "Env⊢e∷-eT" and wt_e2: "Env⊢es∷≐esT" by (elim wt_elim_cases) simp { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j∈jmps" proof - note hyp_e = ‹PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)› from G wt_e have "?Jmp jmps s1" by - (rule hyp_e [THEN conjunct1],simp_all) moreover note hyp_es = ‹PROP ?Hyp (In3 es) s1 s2 (In3 vs)› ultimately show ?thesis using wt_e2 G jmp by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)], (assumption|simp (no_asm_simp))+) qed } thus ?case by simp qed note generalized = this from no_jmp jmpOk wt G show ?thesis by (rule generalized) qed lemmas jumpNestingOk_evalE = jumpNestingOk_eval [THEN conjE,rule_format] lemma jumpNestingOk_eval_no_jump: assumes eval: "prg Env⊢ s0 ─t≻→ (v,s1)" and jmpOk: "jumpNestingOk {} t" and no_jmp: "abrupt s0 ≠ Some (Jump j)" and wt: "Env⊢t∷T" and wf: "wf_prog (prg Env)" shows "abrupt s1 ≠ Some (Jump j) ∧ (normal s1 ⟶ v=In2 (w,upd) ⟶ abrupt s ≠ Some (Jump j') ⟶ abrupt (upd val s) ≠ Some (Jump j'))" proof (cases "∃ j'. abrupt s0 = Some (Jump j')") case True then obtain j' where jmp: "abrupt s0 = Some (Jump j')" .. with no_jmp have "j'≠j" by simp with eval jmp have "s1=s0" by auto with no_jmp jmp show ?thesis by simp next case False obtain G where G: "prg Env = G" by (cases Env) simp from G eval have "G⊢ s0 ─t≻→ (v,s1)" by simp moreover note jmpOk wt moreover from G wf have "wf_prog G" by simp moreover note G moreover from False have "⋀ j. abrupt s0 = Some (Jump j) ⟹ j ∈ {}" by simp ultimately show ?thesis apply (rule jumpNestingOk_evalE) apply assumption apply simp apply fastforce done qed lemmas jumpNestingOk_eval_no_jumpE = jumpNestingOk_eval_no_jump [THEN conjE,rule_format] corollary eval_expression_no_jump: assumes eval: "prg Env⊢s0 ─e-≻v→ s1" and no_jmp: "abrupt s0 ≠ Some (Jump j)" and wt: "Env⊢e∷-T" and wf: "wf_prog (prg Env)" shows "abrupt s1 ≠ Some (Jump j)" using eval _ no_jmp wt wf by (rule jumpNestingOk_eval_no_jumpE, simp_all) corollary eval_var_no_jump: assumes eval: "prg Env⊢s0 ─var=≻(w,upd)→ s1" and no_jmp: "abrupt s0 ≠ Some (Jump j)" and wt: "Env⊢var∷=T" and wf: "wf_prog (prg Env)" shows "abrupt s1 ≠ Some (Jump j) ∧ (normal s1 ⟶ (abrupt s ≠ Some (Jump j') ⟶ abrupt (upd val s) ≠ Some (Jump j')))" apply (rule_tac upd="upd" and val="val" and s="s" and w="w" and j'=j' in jumpNestingOk_eval_no_jumpE [OF eval _ no_jmp wt wf]) by simp_all lemmas eval_var_no_jumpE = eval_var_no_jump [THEN conjE,rule_format] corollary eval_statement_no_jump: assumes eval: "prg Env⊢s0 ─c→ s1" and jmpOk: "jumpNestingOkS {} c" and no_jmp: "abrupt s0 ≠ Some (Jump j)" and wt: "Env⊢c∷√" and wf: "wf_prog (prg Env)" shows "abrupt s1 ≠ Some (Jump j)" using eval _ no_jmp wt wf by (rule jumpNestingOk_eval_no_jumpE) (simp_all add: jmpOk) corollary eval_expression_list_no_jump: assumes eval: "prg Env⊢s0 ─es≐≻v→ s1" and no_jmp: "abrupt s0 ≠ Some (Jump j)" and wt: "Env⊢es∷≐T" and wf: "wf_prog (prg Env)" shows "abrupt s1 ≠ Some (Jump j)" using eval _ no_jmp wt wf by (rule jumpNestingOk_eval_no_jumpE, simp_all) (* ### FIXME: Do i need this *) lemma union_subseteq_elim [elim]: "⟦A ∪ B ⊆ C; ⟦A ⊆ C; B ⊆ C⟧ ⟹ P⟧ ⟹ P" by blast lemma dom_locals_halloc_mono: assumes halloc: "G⊢s0─halloc oi≻a→s1" shows "dom (locals (store s0)) ⊆ dom (locals (store s1))" proof - from halloc show ?thesis by cases simp_all qed lemma dom_locals_sxalloc_mono: assumes sxalloc: "G⊢s0─sxalloc→s1" shows "dom (locals (store s0)) ⊆ dom (locals (store s1))" proof - from sxalloc show ?thesis proof (cases) case Norm thus ?thesis by simp next case Jmp thus ?thesis by simp next case Error thus ?thesis by simp next case XcptL thus ?thesis by simp next case SXcpt thus ?thesis by - (drule dom_locals_halloc_mono,simp) qed qed lemma dom_locals_assign_mono: assumes f_ok: "dom (locals (store s)) ⊆ dom (locals (store (f n s)))" shows "dom (locals (store s)) ⊆ dom (locals (store (assign f n s)))" proof (cases "normal s") case False thus ?thesis by (cases s) (auto simp add: assign_def Let_def) next case True then obtain s' where s': "s = (None,s')" by auto moreover obtain x1 s1 where "f n s = (x1,s1)" by (cases "f n s") ultimately show ?thesis using f_ok by (simp add: assign_def Let_def) qed (* lemma dom_locals_init_lvars_mono: "dom (locals (store s)) ⊆ dom (locals (store (init_lvars G D sig mode a vs s)))" proof (cases "mode = Static") case True thus ?thesis apply (cases s) apply (simp add: init_lvars_def Let_def) *) lemma dom_locals_lvar_mono: "dom (locals (store s)) ⊆ dom (locals (store (snd (lvar vn s') val s)))" by (simp add: lvar_def) blast lemma dom_locals_fvar_vvar_mono: "dom (locals (store s)) ⊆ dom (locals (store (snd (fst (fvar statDeclC stat fn a s')) val s)))" proof (cases stat) case True thus ?thesis by (cases s) (simp add: fvar_def2) next case False thus ?thesis by (cases s) (simp add: fvar_def2) qed lemma dom_locals_fvar_mono: "dom (locals (store s)) ⊆ dom (locals (store (snd (fvar statDeclC stat fn a s))))" proof (cases stat) case True thus ?thesis by (cases s) (simp add: fvar_def2) next case False thus ?thesis by (cases s) (simp add: fvar_def2) qed lemma dom_locals_avar_vvar_mono: "dom (locals (store s)) ⊆ dom (locals (store (snd (fst (avar G i a s')) val s)))" by (cases s, simp add: avar_def2) lemma dom_locals_avar_mono: "dom (locals (store s)) ⊆ dom (locals (store (snd (avar G i a s))))" by (cases s, simp add: avar_def2) text ‹ Since assignments are modelled as functions from states to states, we must take into account these functions. They appear only in the assignment rule and as result from evaluating a variable. Thats why we need the complicated second part of the conjunction in the goal. The reason for the very generic way to treat assignments was the aim to omit redundancy. There is only one evaluation rule for each kind of variable (locals, fields, arrays). These rules are used for both accessing variables and updating variables. Thats why the evaluation rules for variables result in a pair consisting of a value and an update function. Of course we could also think of a pair of a value and a reference in the store, instead of the generic update function. But as only array updates can cause a special exception (if the types mismatch) and not array reads we then have to introduce two different rules to handle array reads and updates› lemma dom_locals_eval_mono: assumes eval: "G⊢ s0 ─t≻→ (v,s1)" shows "dom (locals (store s0)) ⊆ dom (locals (store s1)) ∧ (∀ vv. v=In2 vv ∧ normal s1 ⟶ (∀ s val. dom (locals (store s)) ⊆ dom (locals (store ((snd vv) val s)))))" proof - from eval show ?thesis proof (induct) case Abrupt thus ?case by simp next case Skip thus ?case by simp next case Expr thus ?case by simp next case Lab thus ?case by simp next case (Comp s0 c1 s1 c2 s2) from Comp.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from Comp.hyps have "… ⊆ dom (locals (store s2))" by simp finally show ?case by simp next case (If s0 e b s1 c1 c2 s2) from If.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from If.hyps have "… ⊆ dom (locals (store s2))" by simp finally show ?case by simp next case (Loop s0 e b s1 c s2 l s3) show ?case proof (cases "the_Bool b") case True with Loop.hyps obtain s0_s1: "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" and s1_s2: "dom (locals (store s1)) ⊆ dom (locals (store s2))" and s2_s3: "dom (locals (store s2)) ⊆ dom (locals (store s3))" by simp note s0_s1 also note s1_s2 also note s2_s3 finally show ?thesis by simp next case False with Loop.hyps show ?thesis by simp qed next case Jmp thus ?case by simp next case Throw thus ?case by simp next case (Try s0 c1 s1 s2 C vn c2 s3) then have s0_s1: "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp from ‹G⊢s1 ─sxalloc→ s2› have s1_s2: "dom (locals (store s1)) ⊆ dom (locals (store s2))" by (rule dom_locals_sxalloc_mono) thus ?case proof (cases "G,s2⊢catch C") case True note s0_s1 also note s1_s2 also from True Try.hyps have "dom (locals (store (new_xcpt_var vn s2))) ⊆ dom (locals (store s3))" by simp hence "dom (locals (store s2)) ⊆ dom (locals (store s3))" by (cases s2, simp ) finally show ?thesis by simp next case False note s0_s1 also note s1_s2 finally show ?thesis using False Try.hyps by simp qed next case (Fin s0 c1 x1 s1 c2 s2 s3) show ?case proof (cases "∃err. x1 = Some (Error err)") case True with Fin.hyps show ?thesis by simp next case False from Fin.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store (x1, s1)))" by simp hence "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store ((Norm s1)::state)))" by simp also from Fin.hyps have "… ⊆ dom (locals (store s2))" by simp finally show ?thesis using Fin.hyps by simp qed next case (Init C c s0 s3 s1 s2) show ?case proof (cases "inited C (globs s0)") case True with Init.hyps show ?thesis by simp next case False with Init.hyps obtain s0_s1: "dom (locals (store (Norm ((init_class_obj G C) s0)))) ⊆ dom (locals (store s1))" and s3: "s3 = (set_lvars (locals (snd s1))) s2" by simp from s0_s1 have "dom (locals (store (Norm s0))) ⊆ dom (locals (store s1))" by (cases s0) simp with s3 have "dom (locals (store (Norm s0))) ⊆ dom (locals (store s3))" by (cases s2) simp thus ?thesis by simp qed next case (NewC s0 C s1 a s2) note halloc = ‹G⊢s1 ─halloc CInst C≻a→ s2› from NewC.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from halloc have "… ⊆ dom (locals (store s2))" by (rule dom_locals_halloc_mono) finally show ?case by simp next case (NewA s0 T s1 e i s2 a s3) note halloc = ‹G⊢abupd (check_neg i) s2 ─halloc Arr T (the_Intg i)≻a→ s3› from NewA.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from NewA.hyps have "… ⊆ dom (locals (store s2))" by simp also from halloc have "… ⊆ dom (locals (store s3))" by (rule dom_locals_halloc_mono [elim_format]) simp finally show ?case by simp next case Cast thus ?case by simp next case Inst thus ?case by simp next case Lit thus ?case by simp next case UnOp thus ?case by simp next case (BinOp s0 e1 v1 s1 binop e2 v2 s2) from BinOp.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from BinOp.hyps have "… ⊆ dom (locals (store s2))" by simp finally show ?case by simp next case Super thus ?case by simp next case Acc thus ?case by simp next case (Ass s0 va w f s1 e v s2) from Ass.hyps have s0_s1: "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp show ?case proof (cases "normal s1") case True with Ass.hyps have ass_ok: "⋀ s val. dom (locals (store s)) ⊆ dom (locals (store (f val s)))" by simp note s0_s1 also from Ass.hyps have "dom (locals (store s1)) ⊆ dom (locals (store s2))" by simp also from ass_ok have "… ⊆ dom (locals (store (assign f v s2)))" by (rule dom_locals_assign_mono [where f = f]) finally show ?thesis by simp next case False with ‹G⊢s1 ─e-≻v→ s2› have "s2=s1" by auto with s0_s1 False have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store (assign f v s2)))" by simp thus ?thesis by simp qed next case (Cond s0 e0 b s1 e1 e2 v s2) from Cond.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from Cond.hyps have "… ⊆ dom (locals (store s2))" by simp finally show ?case by simp next case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4) note s3 = ‹s3 = init_lvars G D ⦇name = mn, parTs = pTs⦈ mode a' vs s2› from Call.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from Call.hyps have "… ⊆ dom (locals (store s2))" by simp also have "… ⊆ dom (locals (store ((set_lvars (locals (store s2))) s4)))" by (cases s4) simp finally show ?case by simp next case Methd thus ?case by simp next case (Body s0 D s1 c s2 s3) from Body.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from Body.hyps have "… ⊆ dom (locals (store s2))" by simp also have "… ⊆ dom (locals (store (abupd (absorb Ret) s2)))" by simp also have "… ⊆ dom (locals (store (abupd (absorb Ret) s3)))" proof - from ‹s3 = (if ∃l. abrupt s2 = Some (Jump (Break l)) ∨ abrupt s2 = Some (Jump (Cont l)) then abupd (λx. Some (Error CrossMethodJump)) s2 else s2)› show ?thesis by simp qed finally show ?case by simp next case LVar thus ?case using dom_locals_lvar_mono by simp next case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC) from FVar.hyps obtain s2': "s2' = snd (fvar statDeclC stat fn a s2)" and v: "v = fst (fvar statDeclC stat fn a s2)" by (cases "fvar statDeclC stat fn a s2" ) simp from v have "∀s val. dom (locals (store s)) ⊆ dom (locals (store (snd v val s)))" (is "?V_ok") by (simp add: dom_locals_fvar_vvar_mono) hence v_ok: "(∀vv. In2 v = In2 vv ∧ normal s3 ⟶ ?V_ok)" by - (intro strip, simp) note s3 = ‹s3 = check_field_access G accC statDeclC fn stat a s2'› from FVar.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from FVar.hyps have "… ⊆ dom (locals (store s2))" by simp also from s2' have "… ⊆ dom (locals (store s2'))" by (simp add: dom_locals_fvar_mono) also from s3 have "… ⊆ dom (locals (store s3))" by (simp add: check_field_access_def Let_def) finally show ?case using v_ok by simp next case (AVar s0 e1 a s1 e2 i s2 v s2') from AVar.hyps obtain s2': "s2' = snd (avar G i a s2)" and v: "v = fst (avar G i a s2)" by (cases "avar G i a s2") simp from v have "∀s val. dom (locals (store s)) ⊆ dom (locals (store (snd v val s)))" (is "?V_ok") by (simp add: dom_locals_avar_vvar_mono) hence v_ok: "(∀vv. In2 v = In2 vv ∧ normal s2' ⟶ ?V_ok)" by - (intro strip, simp) from AVar.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from AVar.hyps have "… ⊆ dom (locals (store s2))" by simp also from s2' have "… ⊆ dom (locals (store s2'))" by (simp add: dom_locals_avar_mono) finally show ?case using v_ok by simp next case Nil thus ?case by simp next case (Cons s0 e v s1 es vs s2) from Cons.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by simp also from Cons.hyps have "… ⊆ dom (locals (store s2))" by simp finally show ?case by simp qed qed lemma dom_locals_eval_mono_elim: assumes eval: "G⊢ s0 ─t≻→ (v,s1)" obtains "dom (locals (store s0)) ⊆ dom (locals (store s1))" and "⋀ vv s val. ⟦v=In2 vv; normal s1⟧ ⟹ dom (locals (store s)) ⊆ dom (locals (store ((snd vv) val s)))" using eval by (rule dom_locals_eval_mono [THEN conjE]) (rule that, auto) lemma halloc_no_abrupt: assumes halloc: "G⊢s0─halloc oi≻a→s1" and normal: "normal s1" shows "normal s0" proof - from halloc normal show ?thesis by cases simp_all qed lemma sxalloc_mono_no_abrupt: assumes sxalloc: "G⊢s0─sxalloc→s1" and normal: "normal s1" shows "normal s0" proof - from sxalloc normal show ?thesis by cases simp_all qed lemma union_subseteqI: "⟦A ∪ B ⊆ C; A' ⊆ A; B' ⊆ B⟧ ⟹ A' ∪ B' ⊆ C" by blast lemma union_subseteqIl: "⟦A ∪ B ⊆ C; A' ⊆ A⟧ ⟹ A' ∪ B ⊆ C" by blast lemma union_subseteqIr: "⟦A ∪ B ⊆ C; B' ⊆ B⟧ ⟹ A ∪ B' ⊆ C" by blast lemma subseteq_union_transl [trans]: "⟦A ⊆ B; B ∪ C ⊆ D⟧ ⟹ A ∪ C ⊆ D" by blast lemma subseteq_union_transr [trans]: "⟦A ⊆ B; C ∪ B ⊆ D⟧ ⟹ A ∪ C ⊆ D" by blast lemma union_subseteq_weaken: "⟦A ∪ B ⊆ C; ⟦A ⊆ C; B ⊆ C⟧ ⟹ P ⟧ ⟹ P" by blast lemma assigns_good_approx: assumes eval: "G⊢ s0 ─t≻→ (v,s1)" and normal: "normal s1" shows "assigns t ⊆ dom (locals (store s1))" proof - from eval normal show ?thesis proof (induct) case Abrupt thus ?case by simp next ― ‹For statements its trivial, since then \<^term>‹assigns t = {}›› case Skip show ?case by simp next case Expr show ?case by simp next case Lab show ?case by simp next case Comp show ?case by simp next case If show ?case by simp next case Loop show ?case by simp next case Jmp show ?case by simp next case Throw show ?case by simp next case Try show ?case by simp next case Fin show ?case by simp next case Init show ?case by simp next case NewC show ?case by simp next case (NewA s0 T s1 e i s2 a s3) note halloc = ‹G⊢abupd (check_neg i) s2 ─halloc Arr T (the_Intg i)≻a→ s3› have "assigns (In1l e) ⊆ dom (locals (store s2))" proof - from NewA have "normal (abupd (check_neg i) s2)" by - (erule halloc_no_abrupt [rule_format]) hence "normal s2" by (cases s2) simp with NewA.hyps show ?thesis by iprover qed also from halloc have "… ⊆ dom (locals (store s3))" by (rule dom_locals_halloc_mono [elim_format]) simp finally show ?case by simp next case (Cast s0 e v s1 s2 T) hence "normal s1" by (cases s1,simp) with Cast.hyps have "assigns (In1l e) ⊆ dom (locals (store s1))" by simp also from Cast.hyps have "… ⊆ dom (locals (store s2))" by simp finally show ?case by simp next case Inst thus ?case by simp next case Lit thus ?case by simp next case UnOp thus ?case by simp next case (BinOp s0 e1 v1 s1 binop e2 v2 s2) hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) with BinOp.hyps have "assigns (In1l e1) ⊆ dom (locals (store s1))" by iprover also have "… ⊆ dom (locals (store s2))" proof - note ‹G⊢s1 ─(if need_second_arg binop v1 then In1l e2 else In1r Skip)≻→ (In1 v2, s2)› thus ?thesis by (rule dom_locals_eval_mono_elim) qed finally have s2: "assigns (In1l e1) ⊆ dom (locals (store s2))" . show ?case proof (cases "binop=CondAnd ∨ binop=CondOr") case True with s2 show ?thesis by simp next case False with BinOp have "assigns (In1l e2) ⊆ dom (locals (store s2))" by (simp add: need_second_arg_def) with s2 show ?thesis using False by simp qed next case Super thus ?case by simp next case Acc thus ?case by simp next case (Ass s0 va w f s1 e v s2) note nrm_ass_s2 = ‹normal (assign f v s2)› hence nrm_s2: "normal s2" by (cases s2, simp add: assign_def Let_def) with Ass.hyps have nrm_s1: "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) with Ass.hyps have "assigns (In2 va) ⊆ dom (locals (store s1))" by iprover also from Ass.hyps have "… ⊆ dom (locals (store s2))" by - (erule dom_locals_eval_mono_elim) also from nrm_s2 Ass.hyps have "assigns (In1l e) ⊆ dom (locals (store s2))" by iprover ultimately have "assigns (In2 va) ∪ assigns (In1l e) ⊆ dom (locals (store s2))" by (rule Un_least) also from Ass.hyps nrm_s1 have "… ⊆ dom (locals (store (f v s2)))" by - (erule dom_locals_eval_mono_elim, cases s2,simp) then have "dom (locals (store s2)) ⊆ dom (locals (store (assign f v s2)))" by (rule dom_locals_assign_mono) finally have va_e: " assigns (In2 va) ∪ assigns (In1l e) ⊆ dom (locals (snd (assign f v s2)))" . show ?case proof (cases "∃ n. va = LVar n") case False with va_e show ?thesis by (simp add: Un_assoc) next case True then obtain n where va: "va = LVar n" by blast with Ass.hyps have "G⊢Norm s0 ─LVar n=≻(w,f)→ s1" by simp hence "(w,f) = lvar n s0" by (rule eval_elim_cases) simp with nrm_ass_s2 have "n ∈ dom (locals (store (assign f v s2)))" by (cases s2) (simp add: assign_def Let_def lvar_def) with va_e True va show ?thesis by (simp add: Un_assoc) qed next case (Cond s0 e0 b s1 e1 e2 v s2) hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) with Cond.hyps have "assigns (In1l e0) ⊆ dom (locals (store s1))" by iprover also from Cond.hyps have "… ⊆ dom (locals (store s2))" by - (erule dom_locals_eval_mono_elim) finally have e0: "assigns (In1l e0) ⊆ dom (locals (store s2))" . show ?case proof (cases "the_Bool b") case True with Cond have "assigns (In1l e1) ⊆ dom (locals (store s2))" by simp hence "assigns (In1l e1) ∩ assigns (In1l e2) ⊆ …" by blast with e0 have "assigns (In1l e0) ∪ assigns (In1l e1) ∩ assigns (In1l e2) ⊆ dom (locals (store s2))" by (rule Un_least) thus ?thesis using True by simp next case False with Cond have " assigns (In1l e2) ⊆ dom (locals (store s2))" by simp hence "assigns (In1l e1) ∩ assigns (In1l e2) ⊆ …" by blast with e0 have "assigns (In1l e0) ∪ assigns (In1l e1) ∩ assigns (In1l e2) ⊆ dom (locals (store s2))" by (rule Un_least) thus ?thesis using False by simp qed next case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4) have nrm_s2: "normal s2" proof - from ‹normal ((set_lvars (locals (snd s2))) s4)› have normal_s4: "normal s4" by simp hence "normal s3'" using Call.hyps by - (erule eval_no_abrupt_lemma [rule_format]) moreover note ‹s3' = check_method_access G accC statT mode ⦇name=mn, parTs=pTs⦈ a' s3› ultimately have "normal s3" by (cases s3) (simp add: check_method_access_def Let_def) moreover note s3 = ‹s3 = init_lvars G D ⦇name = mn, parTs = pTs⦈ mode a' vs s2› ultimately show "normal s2" by (cases s2) (simp add: init_lvars_def2) qed hence "normal s1" using Call.hyps by - (erule eval_no_abrupt_lemma [rule_format]) with Call.hyps have "assigns (In1l e) ⊆ dom (locals (store s1))" by iprover also from Call.hyps have "… ⊆ dom (locals (store s2))" by - (erule dom_locals_eval_mono_elim) also from nrm_s2 Call.hyps have "assigns (In3 args) ⊆ dom (locals (store s2))" by iprover ultimately have "assigns (In1l e) ∪ assigns (In3 args) ⊆ …" by (rule Un_least) also have "… ⊆ dom (locals (store ((set_lvars (locals (store s2))) s4)))" by (cases s4) simp finally show ?case by simp next case Methd thus ?case by simp next case Body thus ?case by simp next case LVar thus ?case by simp next case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC) note s3 = ‹s3 = check_field_access G accC statDeclC fn stat a s2'› note avar = ‹(v, s2') = fvar statDeclC stat fn a s2› have nrm_s2: "normal s2" proof - note ‹normal s3› with s3 have "normal s2'" by (cases s2') (simp add: check_field_access_def Let_def) with avar show "normal s2" by (cases s2) (simp add: fvar_def2) qed with FVar.hyps have "assigns (In1l e) ⊆ dom (locals (store s2))" by iprover also have "… ⊆ dom (locals (store s2'))" proof - from avar have "s2' = snd (fvar statDeclC stat fn a s2)" by (cases "fvar statDeclC stat fn a s2") simp thus ?thesis by simp (rule dom_locals_fvar_mono) qed also from s3 have "… ⊆ dom (locals (store s3))" by (cases s2') (simp add: check_field_access_def Let_def) finally show ?case by simp next case (AVar s0 e1 a s1 e2 i s2 v s2') note avar = ‹(v, s2') = avar G i a s2› have nrm_s2: "normal s2" proof - from avar and ‹normal s2'› show ?thesis by (cases s2) (simp add: avar_def2) qed with AVar.hyps have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) with AVar.hyps have "assigns (In1l e1) ⊆ dom (locals (store s1))" by iprover also from AVar.hyps have "… ⊆ dom (locals (store s2))" by - (erule dom_locals_eval_mono_elim) also from AVar.hyps nrm_s2 have "assigns (In1l e2) ⊆ dom (locals (store s2))" by iprover ultimately have "assigns (In1l e1) ∪ assigns (In1l e2) ⊆ …" by (rule Un_least) also have "dom (locals (store s2)) ⊆ dom (locals (store s2'))" proof - from avar have "s2' = snd (avar G i a s2)" by (cases "avar G i a s2") simp thus ?thesis by simp (rule dom_locals_avar_mono) qed finally show ?case by simp next case Nil show ?case by simp next case (Cons s0 e v s1 es vs s2) have "assigns (In1l e) ⊆ dom (locals (store s1))" proof - from Cons have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) with Cons.hyps show ?thesis by iprover qed also from Cons.hyps have "… ⊆ dom (locals (store s2))" by - (erule dom_locals_eval_mono_elim) also from Cons have "assigns (In3 es) ⊆ dom (locals (store s2))" by iprover ultimately have "assigns (In1l e) ∪ assigns (In3 es) ⊆ dom (locals (store s2))" by (rule Un_least) thus ?case by simp qed qed corollary assignsE_good_approx: assumes eval: "prg Env⊢ s0 ─e-≻v→ s1" and normal: "normal s1" shows "assignsE e ⊆ dom (locals (store s1))" proof - from eval normal show ?thesis by (rule assigns_good_approx [elim_format]) simp qed corollary assignsV_good_approx: assumes eval: "prg Env⊢ s0 ─v=≻vf→ s1" and normal: "normal s1" shows "assignsV v ⊆ dom (locals (store s1))" proof - from eval normal show ?thesis by (rule assigns_good_approx [elim_format]) simp qed corollary assignsEs_good_approx: assumes eval: "prg Env⊢ s0 ─es≐≻vs→ s1" and normal: "normal s1" shows "assignsEs es ⊆ dom (locals (store s1))" proof - from eval normal show ?thesis by (rule assigns_good_approx [elim_format]) simp qed lemma constVal_eval: assumes const: "constVal e = Some c" and eval: "G⊢Norm s0 ─e-≻v→ s" shows "v = c ∧ normal s" proof - have True and "⋀ c v s0 s. ⟦ constVal e = Some c; G⊢Norm s0 ─e-≻v→ s⟧ ⟹ v = c ∧ normal s" and True proof (induct rule: var.induct expr.induct stmt.induct) case NewC hence False by simp thus ?case .. next case NewA hence False by simp thus ?case .. next case Cast hence False by simp thus ?case .. next case Inst hence False by simp thus ?case .. next case (Lit val c v s0 s) note ‹constVal (Lit val) = Some c› moreover from ‹G⊢Norm s0 ─Lit val-≻v→ s› obtain "v=val" and "normal s" by cases simp ultimately show "v=c ∧ normal s" by simp next case (UnOp unop e c v s0 s) note const = ‹constVal (UnOp unop e) = Some c› then obtain ce where ce: "constVal e = Some ce" by simp from ‹G⊢Norm s0 ─UnOp unop e-≻v→ s› obtain ve where ve: "G⊢Norm s0 ─e-≻ve→ s" and v: "v = eval_unop unop ve" by cases simp from ce ve obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s" by (rule UnOp.hyps [elim_format]) iprover from eq_ve_ce const ce v have "v=c" by simp from this nrm_s show ?case .. next case (BinOp binop e1 e2 c v s0 s) note const = ‹constVal (BinOp binop e1 e2) = Some c› then obtain c1 c2 where c1: "constVal e1 = Some c1" and c2: "constVal e2 = Some c2" and c: "c = eval_binop binop c1 c2" by simp from ‹G⊢Norm s0 ─BinOp binop e1 e2-≻v→ s› obtain v1 s1 v2 where v1: "G⊢Norm s0 ─e1-≻v1→ s1" and v2: "G⊢s1 ─(if need_second_arg binop v1 then In1l e2 else In1r Skip)≻→ (In1 v2, s)" and v: "v = eval_binop binop v1 v2" by cases simp from c1 v1 obtain eq_v1_c1: "v1 = c1" and nrm_s1: "normal s1" by (rule BinOp.hyps [elim_format]) iprover show ?case proof (cases "need_second_arg binop v1") case True with v2 nrm_s1 obtain s1' where "G⊢Norm s1' ─e2-≻v2→ s" by (cases s1) simp with c2 obtain "v2 = c2" "normal s" by (rule BinOp.hyps [elim_format]) iprover with c c1 c2 eq_v1_c1 v show ?thesis by simp next case False with nrm_s1 v2 have "s=s1" by (cases s1) (auto elim!: eval_elim_cases) moreover from False c v eq_v1_c1 have "v = c" by (simp add: eval_binop_arg2_indep) ultimately show ?thesis using nrm_s1 by simp qed (* hallo ehco *) next case Super hence False by simp thus ?case .. next case Acc hence False by simp thus ?case .. next case Ass hence False by simp thus ?case .. next case (Cond b e1 e2 c v s0 s) note c = ‹constVal (b ? e1 : e2) = Some c› then obtain cb c1 c2 where cb: "constVal b = Some cb" and c1: "constVal e1 = Some c1" and c2: "constVal e2 = Some c2" by (auto split: bool.splits) from ‹G⊢Norm s0 ─b ? e1 : e2-≻v→ s› obtain vb s1 where vb: "G⊢Norm s0 ─b-≻vb→ s1" and eval_v: "G⊢s1 ─(if the_Bool vb then e1 else e2)-≻v→ s" by cases simp from cb vb obtain eq_vb_cb: "vb = cb" and nrm_s1: "normal s1" by (rule Cond.hyps [elim_format]) iprover show ?case proof (cases "the_Bool vb") case True with c cb c1 eq_vb_cb have "c = c1" by simp moreover from True eval_v nrm_s1 obtain s1' where "G⊢Norm s1' ─e1-≻v→ s" by (cases s1) simp with c1 obtain "c1 = v" "normal s" by (rule Cond.hyps [elim_format]) iprover ultimately show ?thesis by simp next case False with c cb c2 eq_vb_cb have "c = c2" by simp moreover from False eval_v nrm_s1 obtain s1' where "G⊢Norm s1' ─e2-≻v→ s" by (cases s1) simp with c2 obtain "c2 = v" "normal s" by (rule Cond.hyps [elim_format]) iprover ultimately show ?thesis by simp qed next case Call hence False by simp thus ?case .. qed simp_all with const eval show ?thesis by iprover qed lemmas constVal_eval_elim = constVal_eval [THEN conjE] lemma eval_unop_type: "typeof dt (eval_unop unop v) = Some (PrimT (unop_type unop))" by (cases unop) simp_all lemma eval_binop_type: "typeof dt (eval_binop binop v1 v2) = Some (PrimT (binop_type binop))" by (cases binop) simp_all lemma constVal_Boolean: assumes const: "constVal e = Some c" and wt: "Env⊢e∷-PrimT Boolean" shows "typeof empty_dt c = Some (PrimT Boolean)" proof - have True and "⋀ c. ⟦constVal e = Some c;Env⊢e∷-PrimT Boolean⟧ ⟹ typeof empty_dt c = Some (PrimT Boolean)" and True proof (induct rule: var.induct expr.induct stmt.induct) case NewC hence False by simp thus ?case .. next case NewA hence False by simp thus ?case .. next case Cast hence False by simp thus ?case .. next case Inst hence False by simp thus ?case .. next case (Lit v c) from ‹constVal (Lit v) = Some c› have "c=v" by simp moreover from ‹Env⊢Lit v∷-PrimT Boolean› have "typeof empty_dt v = Some (PrimT Boolean)" by cases simp ultimately show ?case by simp next case (UnOp unop e c) from ‹Env⊢UnOp unop e∷-PrimT Boolean› have "Boolean = unop_type unop" by cases simp moreover from ‹constVal (UnOp unop e) = Some c› obtain ce where "c = eval_unop unop ce" by auto ultimately show ?case by (simp add: eval_unop_type) next case (BinOp binop e1 e2 c) from ‹Env⊢BinOp binop e1 e2∷-PrimT Boolean› have "Boolean = binop_type binop" by cases simp moreover from ‹constVal (BinOp binop e1 e2) = Some c› obtain c1 c2 where "c = eval_binop binop c1 c2" by auto ultimately show ?case by (simp add: eval_binop_type) next case Super hence False by simp thus ?case .. next case Acc hence False by simp thus ?case .. next case Ass hence False by simp thus ?case .. next case (Cond b e1 e2 c) note c = ‹constVal (b ? e1 : e2) = Some c› then obtain cb c1 c2 where cb: "constVal b = Some cb" and c1: "constVal e1 = Some c1" and c2: "constVal e2 = Some c2" by (auto split: bool.splits) note wt = ‹Env⊢b ? e1 : e2∷-PrimT Boolean› then obtain T1 T2 where "Env⊢b∷-PrimT Boolean" and wt_e1: "Env⊢e1∷-PrimT Boolean" and wt_e2: "Env⊢e2∷-PrimT Boolean" by cases (auto dest: widen_Boolean2) show ?case proof (cases "the_Bool cb") case True from c1 wt_e1 have "typeof empty_dt c1 = Some (PrimT Boolean)" by (rule Cond.hyps) with True c cb c1 show ?thesis by simp next case False from c2 wt_e2 have "typeof empty_dt c2 = Some (PrimT Boolean)" by (rule Cond.hyps) with False c cb c2 show ?thesis by simp qed next case Call hence False by simp thus ?case .. qed simp_all with const wt show ?thesis by iprover qed lemma assigns_if_good_approx: assumes eval: "prg Env⊢ s0 ─e-≻b→ s1" and normal: "normal s1" and bool: "Env⊢ e∷-PrimT Boolean" shows "assigns_if (the_Bool b) e ⊆ dom (locals (store s1))" proof - ― ‹To properly perform induction on the evaluation relation we have to generalize the lemma to terms not only expressions.› { fix t val assume eval': "prg Env⊢ s0 ─t≻→ (val,s1)" assume bool': "Env⊢ t∷Inl (PrimT Boolean)" assume expr: "∃ expr. t=In1l expr" have "assigns_if (the_Bool (the_In1 val)) (the_In1l t) ⊆ dom (locals (store s1))" using eval' normal bool' expr proof (induct) case Abrupt thus ?case by simp next case (NewC s0 C s1 a s2) from ‹Env⊢NewC C∷-PrimT Boolean› have False by cases simp thus ?case .. next case (NewA s0 T s1 e i s2 a s3) from ‹Env⊢New T[e]∷-PrimT Boolean› have False by cases simp thus ?case .. next case (Cast s0 e b s1 s2 T) note s2 = ‹s2 = abupd (raise_if (¬ prg Env,snd s1⊢b fits T) ClassCast) s1› have "assigns_if (the_Bool b) e ⊆ dom (locals (store s1))" proof - from s2 and ‹normal s2› have "normal s1" by (cases s1) simp moreover from ‹Env⊢Cast T e∷-PrimT Boolean› have "Env⊢e∷- PrimT Boolean" by cases (auto dest: cast_Boolean2) ultimately show ?thesis by (rule Cast.hyps [elim_format]) auto qed also from s2 have "… ⊆ dom (locals (store s2))" by simp finally show ?case by simp next case (Inst s0 e v s1 b T) from ‹prg Env⊢Norm s0 ─e-≻v→ s1› and ‹normal s1› have "assignsE e ⊆ dom (locals (store s1))" by (rule assignsE_good_approx) thus ?case by simp next case (Lit s v) from ‹Env⊢Lit v∷-PrimT Boolean› have "typeof empty_dt v = Some (PrimT Boolean)" by cases simp then obtain b where "v=Bool b" by (cases v) (simp_all add: empty_dt_def) thus ?case by simp next case (UnOp s0 e v s1 unop) note bool = ‹Env⊢UnOp unop e∷-PrimT Boolean› hence bool_e: "Env⊢e∷-PrimT Boolean" by cases (cases unop,simp_all) show ?case proof (cases "constVal (UnOp unop e)") case None note ‹normal s1› moreover note bool_e ultimately have "assigns_if (the_Bool v) e ⊆ dom (locals (store s1))" by (rule UnOp.hyps [elim_format]) auto moreover from bool have "unop = UNot" by cases (cases unop, simp_all) moreover note None ultimately have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) ⊆ dom (locals (store s1))" by simp thus ?thesis by simp next case (Some c) moreover from ‹prg Env⊢Norm s0 ─e-≻v→ s1› have "prg Env⊢Norm s0 ─UnOp unop e-≻eval_unop unop v→ s1" by (rule eval.UnOp) with Some have "eval_unop unop v=c" by (rule constVal_eval_elim) simp moreover from Some bool obtain b where "c=Bool b" by (rule constVal_Boolean [elim_format]) (cases c, simp_all add: empty_dt_def) ultimately have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) = {}" by simp thus ?thesis by simp qed next case (BinOp s0 e1 v1 s1 binop e2 v2 s2) note bool = ‹Env⊢BinOp binop e1 e2∷-PrimT Boolean› show ?case proof (cases "constVal (BinOp binop e1 e2)") case (Some c) moreover from BinOp.hyps have "prg Env⊢Norm s0 ─BinOp binop e1 e2-≻eval_binop binop v1 v2→ s2" by - (rule eval.BinOp) with Some have "eval_binop binop v1 v2=c" by (rule constVal_eval_elim) simp moreover from Some bool obtain b where "c = Bool b" by (rule constVal_Boolean [elim_format]) (cases c, simp_all add: empty_dt_def) ultimately have "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2) = {}" by simp thus ?thesis by simp next case None show ?thesis proof (cases "binop=CondAnd ∨ binop=CondOr") case True from bool obtain bool_e1: "Env⊢e1∷-PrimT Boolean" and bool_e2: "Env⊢e2∷-PrimT Boolean" using True by cases auto have "assigns_if (the_Bool v1) e1 ⊆ dom (locals (store s1))" proof - from BinOp have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) from this bool_e1 show ?thesis by (rule BinOp.hyps [elim_format]) auto qed also from BinOp.hyps have "… ⊆ dom (locals (store s2))" by - (erule dom_locals_eval_mono_elim,simp) finally have e1_s2: "assigns_if (the_Bool v1) e1 ⊆ dom (locals (store s2))". from True show ?thesis proof assume condAnd: "binop = CondAnd" show ?thesis proof (cases "the_Bool (eval_binop binop v1 v2)") case True with condAnd have need_second: "need_second_arg binop v1" by (simp add: need_second_arg_def) from ‹normal s2› have "assigns_if (the_Bool v2) e2 ⊆ dom (locals (store s2))" by (rule BinOp.hyps [elim_format]) (simp add: need_second bool_e2)+ with e1_s2 have "assigns_if (the_Bool v1) e1 ∪ assigns_if (the_Bool v2) e2 ⊆ dom (locals (store s2))" by (rule Un_least) with True condAnd None show ?thesis by simp next case False note binop_False = this show ?thesis proof (cases "need_second_arg binop v1") case True with binop_False condAnd obtain "the_Bool v1=True" and "the_Bool v2 = False" by (simp add: need_second_arg_def) moreover from ‹normal s2› have "assigns_if (the_Bool v2) e2 ⊆ dom (locals (store s2))" by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+ with e1_s2 have "assigns_if (the_Bool v1) e1 ∪ assigns_if (the_Bool v2) e2 ⊆ dom (locals (store s2))" by (rule Un_least) moreover note binop_False condAnd None ultimately show ?thesis by auto next case False with binop_False condAnd have "the_Bool v1=False" by (simp add: need_second_arg_def) with e1_s2 show ?thesis using binop_False condAnd None by auto qed qed next assume condOr: "binop = CondOr" show ?thesis proof (cases "the_Bool (eval_binop binop v1 v2)") case False with condOr have need_second: "need_second_arg binop v1" by (simp add: need_second_arg_def) from ‹normal s2› have "assigns_if (the_Bool v2) e2 ⊆ dom (locals (store s2))" by (rule BinOp.hyps [elim_format]) (simp add: need_second bool_e2)+ with e1_s2 have "assigns_if (the_Bool v1) e1 ∪ assigns_if (the_Bool v2) e2 ⊆ dom (locals (store s2))" by (rule Un_least) with False condOr None show ?thesis by simp next case True note binop_True = this show ?thesis proof (cases "need_second_arg binop v1") case True with binop_True condOr obtain "the_Bool v1=False" and "the_Bool v2 = True" by (simp add: need_second_arg_def) moreover from ‹normal s2› have "assigns_if (the_Bool v2) e2 ⊆ dom (locals (store s2))" by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+ with e1_s2 have "assigns_if (the_Bool v1) e1 ∪ assigns_if (the_Bool v2) e2 ⊆ dom (locals (store s2))" by (rule Un_least) moreover note binop_True condOr None ultimately show ?thesis by auto next case False with binop_True condOr have "the_Bool v1=True" by (simp add: need_second_arg_def) with e1_s2 show ?thesis using binop_True condOr None by auto qed qed qed next case False note ‹¬ (binop = CondAnd ∨ binop = CondOr)› from BinOp.hyps have "prg Env⊢Norm s0 ─BinOp binop e1 e2-≻eval_binop binop v1 v2→ s2" by - (rule eval.BinOp) moreover note ‹normal s2› ultimately have "assignsE (BinOp binop e1 e2) ⊆ dom (locals (store s2))" by (rule assignsE_good_approx) with False None show ?thesis by simp qed qed next case Super note ‹Env⊢Super∷-PrimT Boolean› hence False by cases simp thus ?case .. next case (Acc s0 va v f s1) from ‹prg Env⊢Norm s0 ─va=≻(v, f)→ s1› and ‹normal s1› have "assignsV va ⊆ dom (locals (store s1))" by (rule assignsV_good_approx) thus ?case by simp next case (Ass s0 va w f s1 e v s2) hence "prg Env⊢Norm s0 ─va := e-≻v→ assign f v s2" by - (rule eval.Ass) moreover note ‹normal (assign f v s2)› ultimately have "assignsE (va := e) ⊆ dom (locals (store (assign f v s2)))" by (rule assignsE_good_approx) thus ?case by simp next case (Cond s0 e0 b s1 e1 e2 v s2) from ‹Env⊢e0 ? e1 : e2∷-PrimT Boolean› obtain wt_e1: "Env⊢e1∷-PrimT Boolean" and wt_e2: "Env⊢e2∷-PrimT Boolean" by cases (auto dest: widen_Boolean2) note eval_e0 = ‹prg Env⊢Norm s0 ─e0-≻b→ s1› have e0_s2: "assignsE e0 ⊆ dom (locals (store s2))" proof - note eval_e0 moreover from Cond.hyps and ‹normal s2› have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format],simp) ultimately have "assignsE e0 ⊆ dom (locals (store s1))" by (rule assignsE_good_approx) also from Cond have "… ⊆ dom (locals (store s2))" by - (erule dom_locals_eval_mono [elim_format],simp) finally show ?thesis . qed show ?case proof (cases "constVal e0") case None have "assigns_if (the_Bool v) e1 ∩ assigns_if (the_Bool v) e2 ⊆ dom (locals (store s2))" proof (cases "the_Bool b") case True from ‹normal s2› have "assigns_if (the_Bool v) e1 ⊆ dom (locals (store s2))" by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True) thus ?thesis by blast next case False from ‹normal s2› have "assigns_if (the_Bool v) e2 ⊆ dom (locals (store s2))" by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False) thus ?thesis by blast qed with e0_s2 have "assignsE e0 ∪ (assigns_if (the_Bool v) e1 ∩ assigns_if (the_Bool v) e2) ⊆ dom (locals (store s2))" by (rule Un_least) with None show ?thesis by simp next case (Some c) from this eval_e0 have eq_b_c: "b=c" by (rule constVal_eval_elim) show ?thesis proof (cases "the_Bool c") case True from ‹normal s2› have "assigns_if (the_Bool v) e1 ⊆ dom (locals (store s2))" by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1) with e0_s2 have "assignsE e0 ∪ assigns_if (the_Bool v) e1 ⊆ …" by (rule Un_least) with Some True show ?thesis by simp next case False from ‹normal s2› have "assigns_if (the_Bool v) e2 ⊆ dom (locals (store s2))" by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2) with e0_s2 have "assignsE e0 ∪ assigns_if (the_Bool v) e2 ⊆ …" by (rule Un_least) with Some False show ?thesis by simp qed qed next case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4) hence "prg Env⊢Norm s0 ─({accC,statT,mode}e⋅mn( {pTs}args))-≻v→ (set_lvars (locals (store s2)) s4)" by - (rule eval.Call) hence "assignsE ({accC,statT,mode}e⋅mn( {pTs}args)) ⊆ dom (locals (store ((set_lvars (locals (store s2))) s4)))" using ‹normal ((set_lvars (locals (snd s2))) s4)› by (rule assignsE_good_approx) thus ?case by simp next case Methd show ?case by simp next case Body show ?case by simp qed simp+ ― ‹all the statements and variables› } note generalized = this from eval bool show ?thesis by (rule generalized [elim_format]) simp+ qed lemma assigns_if_good_approx': assumes eval: "G⊢s0 ─e-≻b→ s1" and normal: "normal s1" and bool: "⦇prg=G,cls=C,lcl=L⦈⊢e∷- (PrimT Boolean)" shows "assigns_if (the_Bool b) e ⊆ dom (locals (store s1))" proof - from eval have "prg ⦇prg=G,cls=C,lcl=L⦈⊢s0 ─e-≻b→ s1" by simp from this normal bool show ?thesis by (rule assigns_if_good_approx) qed lemma subset_Intl: "A ⊆ C ⟹ A ∩ B ⊆ C" by blast lemma subset_Intr: "B ⊆ C ⟹ A ∩ B ⊆ C" by blast lemma da_good_approx: assumes eval: "prg Env⊢s0 ─t≻→ (v,s1)" and wt: "Env⊢t∷T" (is "?Wt Env t T") and da: "Env⊢ dom (locals (store s0)) »t» A" (is "?Da Env s0 t A") and wf: "wf_prog (prg Env)" shows "(normal s1 ⟶ (nrm A ⊆ dom (locals (store s1)))) ∧ (∀ l. abrupt s1 = Some (Jump (Break l)) ∧ normal s0 ⟶ (brk A l ⊆ dom (locals (store s1)))) ∧ (abrupt s1 = Some (Jump Ret) ∧ normal s0 ⟶ Result ∈ dom (locals (store s1)))" (is "?NormalAssigned s1 A ∧ ?BreakAssigned s0 s1 A ∧ ?ResAssigned s0 s1") proof - note inj_term_simps [simp] obtain G where G: "prg Env = G" by (cases Env) simp with eval have eval: "G⊢s0 ─t≻→ (v,s1)" by simp from G wf have wf: "wf_prog G" by simp let ?HypObj = "λ t s0 s1. ∀ Env T A. ?Wt Env t T ⟶ ?Da Env s0 t A ⟶ prg Env = G ⟶ ?NormalAssigned s1 A ∧ ?BreakAssigned s0 s1 A ∧ ?ResAssigned s0 s1" ― ‹Goal in object logic variant› let ?Hyp = "λt s0 s1. (⋀ Env T A. ⟦?Wt Env t T; ?Da Env s0 t A; prg Env = G⟧ ⟹ ?NormalAssigned s1 A ∧ ?BreakAssigned s0 s1 A ∧ ?ResAssigned s0 s1)" from eval and wt da G show ?thesis proof (induct arbitrary: Env T A) case (Abrupt xc s t Env T A) have da: "Env⊢ dom (locals s) »t» A" using Abrupt.prems by simp have "?NormalAssigned (Some xc,s) A" by simp moreover have "?BreakAssigned (Some xc,s) (Some xc,s) A" by simp moreover have "?ResAssigned (Some xc,s) (Some xc,s)" by simp ultimately show ?case by (intro conjI) next case (Skip s Env T A) have da: "Env⊢ dom (locals (store (Norm s))) »⟨Skip⟩» A" using Skip.prems by simp hence "nrm A = dom (locals (store (Norm s)))" by (rule da_elim_cases) simp hence "?NormalAssigned (Norm s) A" by auto moreover have "?BreakAssigned (Norm s) (Norm s) A" by simp moreover have "?ResAssigned (Norm s) (Norm s)" by simp ultimately show ?case by (intro conjI) next case (Expr s0 e v s1 Env T A) from Expr.prems show "?NormalAssigned s1 A ∧ ?BreakAssigned (Norm s0) s1 A ∧ ?ResAssigned (Norm s0) s1" by (elim wt_elim_cases da_elim_cases) (rule Expr.hyps, auto) next case (Lab s0 c s1 j Env T A) note G = ‹prg Env = G› from Lab.prems obtain C l where da_c: "Env⊢ dom (locals (snd (Norm s0))) »⟨c⟩» C" and A: "nrm A = nrm C ∩ (brk C) l" "brk A = rmlab l (brk C)" and j: "j = Break l" by - (erule da_elim_cases, simp) from Lab.prems have wt_c: "Env⊢c∷√" by - (erule wt_elim_cases, simp) from wt_c da_c G and Lab.hyps have norm_c: "?NormalAssigned s1 C" and brk_c: "?BreakAssigned (Norm s0) s1 C" and res_c: "?ResAssigned (Norm s0) s1" by simp_all have "?NormalAssigned (abupd (absorb j) s1) A" proof assume normal: "normal (abupd (absorb j) s1)" show "nrm A ⊆ dom (locals (store (abupd (absorb j) s1)))" proof (cases "abrupt s1") case None with norm_c A show ?thesis by auto next case Some with normal j have "abrupt s1 = Some (Jump (Break l))" by (auto dest: absorb_Some_NoneD) with brk_c A show ?thesis by auto qed qed moreover have "?BreakAssigned (Norm s0) (abupd (absorb j) s1) A" proof - { fix l' assume break: "abrupt (abupd (absorb j) s1) = Some (Jump (Break l'))" with j have "l≠l'" by (cases s1) (auto dest!: absorb_Some_JumpD) hence "(rmlab l (brk C)) l'= (brk C) l'" by (simp) with break brk_c A have "(brk A l' ⊆ dom (locals (store (abupd (absorb j) s1))))" by (cases s1) auto } then show ?thesis by simp qed moreover from res_c have "?ResAssigned (Norm s0) (abupd (absorb j) s1)" by (cases s1) (simp add: absorb_def) ultimately show ?case by (intro conjI) next case (Comp s0 c1 s1 c2 s2 Env T A) note G = ‹prg Env = G› from Comp.prems obtain C1 C2 where da_c1: "Env⊢ dom (locals (snd (Norm s0))) »⟨c1⟩» C1" and da_c2: "Env⊢ nrm C1 »⟨c2⟩» C2" and A: "nrm A = nrm C2" "brk A = (brk C1) ⇒∩ (brk C2)" by (elim da_elim_cases) simp from Comp.prems obtain wt_c1: "Env⊢c1∷√" and wt_c2: "Env⊢c2∷√" by (elim wt_elim_cases) simp note ‹PROP ?Hyp (In1r c1) (Norm s0) s1› with wt_c1 da_c1 G obtain nrm_c1: "?NormalAssigned s1 C1" and brk_c1: "?BreakAssigned (Norm s0) s1 C1" and res_c1: "?ResAssigned (Norm s0) s1" by simp show ?case proof (cases "normal s1") case True with nrm_c1 have "nrm C1 ⊆ dom (locals (snd s1))" by iprover with da_c2 obtain C2' where da_c2': "Env⊢ dom (locals (snd s1)) »⟨c2⟩» C2'" and nrm_c2: "nrm C2 ⊆ nrm C2'" and brk_c2: "∀ l. brk C2 l ⊆ brk C2' l" by (rule da_weakenE) iprover note ‹PROP ?Hyp (In1r c2) s1 s2› with wt_c2 da_c2' G obtain nrm_c2': "?NormalAssigned s2 C2'" and brk_c2': "?BreakAssigned s1 s2 C2'" and res_c2 : "?ResAssigned s1 s2" by simp from nrm_c2' nrm_c2 A have "?NormalAssigned s2 A" by blast moreover from brk_c2' brk_c2 A have "?BreakAssigned s1 s2 A" by fastforce with True have "?BreakAssigned (Norm s0) s2 A" by simp moreover from res_c2 True have "?ResAssigned (Norm s0) s2" by simp ultimately show ?thesis by (intro conjI) next case False with ‹G⊢s1 ─c2→ s2› have eq_s1_s2: "s2=s1" by auto with False have "?NormalAssigned s2 A" by blast moreover have "?BreakAssigned (Norm s0) s2 A" proof (cases "∃ l. abrupt s1 = Some (Jump (Break l))") case True then obtain l where l: "abrupt s1 = Some (Jump (Break l))" .. with brk_c1 have "brk C1 l ⊆ dom (locals (store s1))" by simp with A eq_s1_s2 have "brk A l ⊆ dom (locals (store s2))" by auto with l eq_s1_s2 show ?thesis by simp next case False with eq_s1_s2 show ?thesis by simp qed moreover from False res_c1 eq_s1_s2 have "?ResAssigned (Norm s0) s2" by simp ultimately show ?thesis by (intro conjI) qed next case (If s0 e b s1 c1 c2 s2 Env T A) note G = ‹prg Env = G› with If.hyps have eval_e: "prg Env ⊢Norm s0 ─e-≻b→ s1" by simp from If.prems obtain E C1 C2 where da_e: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨e⟩» E" and da_c1: "Env⊢ (dom (locals (store ((Norm s0)::state))) ∪ assigns_if True e) »⟨c1⟩» C1" and da_c2: "Env⊢ (dom (locals (store ((Norm s0)::state))) ∪ assigns_if False e) »⟨c2⟩» C2" and A: "nrm A = nrm C1 ∩ nrm C2" "brk A = brk C1 ⇒∩ brk C2" by (elim da_elim_cases) from If.prems obtain wt_e: "Env⊢e∷- PrimT Boolean" and wt_c1: "Env⊢c1∷√" and wt_c2: "Env⊢c2∷√" by (elim wt_elim_cases) from If.hyps have s0_s1:"dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by (elim dom_locals_eval_mono_elim) show ?case proof (cases "normal s1") case True note normal_s1 = this show ?thesis proof (cases "the_Bool b") case True from eval_e normal_s1 wt_e have "assigns_if True e ⊆ dom (locals (store s1))" by (rule assigns_if_good_approx [elim_format]) (simp add: True) with s0_s1 have "dom (locals (store ((Norm s0)::state))) ∪ assigns_if True e ⊆ …" by (rule Un_least) with da_c1 obtain C1' where da_c1': "Env⊢ dom (locals (store s1)) »⟨c1⟩» C1'" and nrm_c1: "nrm C1 ⊆ nrm C1'" and brk_c1: "∀ l. brk C1 l ⊆ brk C1' l" by (rule da_weakenE) iprover from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp with wt_c1 da_c1' obtain nrm_c1': "?NormalAssigned s2 C1'" and brk_c1': "?BreakAssigned s1 s2 C1'" and res_c1: "?ResAssigned s1 s2" using G by simp from nrm_c1' nrm_c1 A have "?NormalAssigned s2 A" by blast moreover from brk_c1' brk_c1 A have "?BreakAssigned s1 s2 A" by fastforce with normal_s1 have "?BreakAssigned (Norm s0) s2 A" by simp moreover from res_c1 normal_s1 have "?ResAssigned (Norm s0) s2" by simp ultimately show ?thesis by (intro conjI) next case False from eval_e normal_s1 wt_e have "assigns_if False e ⊆ dom (locals (store s1))" by (rule assigns_if_good_approx [elim_format]) (simp add: False) with s0_s1 have "dom (locals (store ((Norm s0)::state)))∪ assigns_if False e ⊆ …" by (rule Un_least) with da_c2 obtain C2' where da_c2': "Env⊢ dom (locals (store s1)) »⟨c2⟩» C2'" and nrm_c2: "nrm C2 ⊆ nrm C2'" and brk_c2: "∀ l. brk C2 l ⊆ brk C2' l" by (rule da_weakenE) iprover from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp with wt_c2 da_c2' obtain nrm_c2': "?NormalAssigned s2 C2'" and brk_c2': "?BreakAssigned s1 s2 C2'" and res_c2: "?ResAssigned s1 s2" using G by simp from nrm_c2' nrm_c2 A have "?NormalAssigned s2 A" by blast moreover from brk_c2' brk_c2 A have "?BreakAssigned s1 s2 A" by fastforce with normal_s1 have "?BreakAssigned (Norm s0) s2 A" by simp moreover from res_c2 normal_s1 have "?ResAssigned (Norm s0) s2" by simp ultimately show ?thesis by (intro conjI) qed next case False then obtain abr where abr: "abrupt s1 = Some abr" by (cases s1) auto moreover from eval_e _ wt_e have "⋀ j. abrupt s1 ≠ Some (Jump j)" by (rule eval_expression_no_jump) (simp_all add: G wf) moreover have "s2 = s1" proof - from abr and ‹G⊢s1 ─(if the_Bool b then c1 else c2)→ s2› show ?thesis by (cases s1) simp qed ultimately show ?thesis by simp qed next case (Loop s0 e b s1 c s2 l s3 Env T A) note G = ‹prg Env = G› with Loop.hyps have eval_e: "prg Env⊢Norm s0 ─e-≻b→ s1" by (simp (no_asm_simp)) from Loop.prems obtain E C where da_e: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨e⟩» E" and da_c: "Env⊢ (dom (locals (store ((Norm s0)::state))) ∪ assigns_if True e) »⟨c⟩» C" and A: "nrm A = nrm C ∩ (dom (locals (store ((Norm s0)::state))) ∪ assigns_if False e)" "brk A = brk C" by (elim da_elim_cases) from Loop.prems obtain wt_e: "Env⊢e∷-PrimT Boolean" and wt_c: "Env⊢c∷√" by (elim wt_elim_cases) from wt_e da_e G obtain res_s1: "?ResAssigned (Norm s0) s1" by (elim Loop.hyps [elim_format]) simp+ from Loop.hyps have s0_s1:"dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by (elim dom_locals_eval_mono_elim) show ?case proof (cases "normal s1") case True note normal_s1 = this show ?thesis proof (cases "the_Bool b") case True with Loop.hyps obtain eval_c: "G⊢s1 ─c→ s2" and eval_while: "G⊢abupd (absorb (Cont l)) s2 ─l∙ While(e) c→ s3" by simp from Loop.hyps True have "?HypObj (In1r c) s1 s2" by simp note hyp_c = this [rule_format] from Loop.hyps True have "?HypObj (In1r (l∙ While(e) c)) (abupd (absorb (Cont l)) s2) s3" by simp note hyp_while = this [rule_format] from eval_e normal_s1 wt_e have "assigns_if True e ⊆ dom (locals (store s1))" by (rule assigns_if_good_approx [elim_format]) (simp add: True) with s0_s1 have "dom (locals (store ((Norm s0)::state))) ∪ assigns_if True e ⊆ …" by (rule Un_least) with da_c obtain C' where da_c': "Env⊢ dom (locals (store s1)) »⟨c⟩» C'" and nrm_C_C': "nrm C ⊆ nrm C'" and brk_C_C': "∀ l. brk C l ⊆ brk C' l" by (rule da_weakenE) iprover from hyp_c wt_c da_c' obtain nrm_C': "?NormalAssigned s2 C'" and brk_C': "?BreakAssigned s1 s2 C'" and res_s2: "?ResAssigned s1 s2" using G by simp show ?thesis proof (cases "normal s2 ∨ abrupt s2 = Some (Jump (Cont l))") case True from Loop.prems obtain wt_while: "Env⊢In1r (l∙ While(e) c)∷T" and da_while: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨l∙ While(e) c⟩» A" by simp have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store (abupd (absorb (Cont l)) s2)))" proof - note s0_s1 also from eval_c have "dom (locals (store s1)) ⊆ dom (locals (store s2))" by (rule dom_locals_eval_mono_elim) also have "… ⊆ dom (locals (store (abupd (absorb (Cont l)) s2)))" by simp finally show ?thesis . qed with da_while obtain A' where da_while': "Env⊢ dom (locals (store (abupd (absorb (Cont l)) s2))) »⟨l∙ While(e) c⟩» A'" and nrm_A_A': "nrm A ⊆ nrm A'" and brk_A_A': "∀ l. brk A l ⊆ brk A' l" by (rule da_weakenE) simp with wt_while hyp_while obtain nrm_A': "?NormalAssigned s3 A'" and brk_A': "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A'" and res_s3: "?ResAssigned (abupd (absorb (Cont l)) s2) s3" using G by simp from nrm_A_A' nrm_A' have "?NormalAssigned s3 A" by blast moreover have "?BreakAssigned (Norm s0) s3 A" proof - from brk_A_A' brk_A' have "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A" by fastforce moreover from True have "normal (abupd (absorb (Cont l)) s2)" by (cases s2) auto ultimately show ?thesis by simp qed moreover from res_s3 True have "?ResAssigned (Norm s0) s3" by auto ultimately show ?thesis by (intro conjI) next case False then obtain abr where "abrupt s2 = Some abr" and "abrupt (abupd (absorb (Cont l)) s2) = Some abr" by auto with eval_while have eq_s3_s2: "s3=s2" by auto with nrm_C_C' nrm_C' A have "?NormalAssigned s3 A" by auto moreover from eq_s3_s2 brk_C_C' brk_C' normal_s1 A have "?BreakAssigned (Norm s0) s3 A" by fastforce moreover from eq_s3_s2 res_s2 normal_s1 have "?ResAssigned (Norm s0) s3" by simp ultimately show ?thesis by (intro conjI) qed next case False with Loop.hyps have eq_s3_s1: "s3=s1" by simp from eq_s3_s1 res_s1 have res_s3: "?ResAssigned (Norm s0) s3" by simp from eval_e True wt_e have "assigns_if False e ⊆ dom (locals (store s1))" by (rule assigns_if_good_approx [elim_format]) (simp add: False) with s0_s1 have "dom (locals (store ((Norm s0)::state)))∪assigns_if False e ⊆ …" by (rule Un_least) hence "nrm C ∩ (dom (locals (store ((Norm s0)::state))) ∪ assigns_if False e) ⊆ dom (locals (store s1))" by (rule subset_Intr) with normal_s1 A eq_s3_s1 have "?NormalAssigned s3 A" by simp moreover from normal_s1 eq_s3_s1 have "?BreakAssigned (Norm s0) s3 A" by simp moreover note res_s3 ultimately show ?thesis by (intro conjI) qed next case False then obtain abr where abr: "abrupt s1 = Some abr" by (cases s1) auto moreover from eval_e _ wt_e have no_jmp: "⋀ j. abrupt s1 ≠ Some (Jump j)" by (rule eval_expression_no_jump) (simp_all add: wf G) moreover have eq_s3_s1: "s3=s1" proof (cases "the_Bool b") case True with Loop.hyps obtain eval_c: "G⊢s1 ─c→ s2" and eval_while: "G⊢abupd (absorb (Cont l)) s2 ─l∙ While(e) c→ s3" by simp from eval_c abr have "s2=s1" by auto moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2" by (cases s1) (simp add: absorb_def) ultimately show ?thesis using eval_while abr by auto next case False with Loop.hyps show ?thesis by simp qed moreover from eq_s3_s1 res_s1 have res_s3: "?ResAssigned (Norm s0) s3" by simp ultimately show ?thesis by simp qed next case (Jmp s j Env T A) have "?NormalAssigned (Some (Jump j),s) A" by simp moreover from Jmp.prems obtain ret: "j = Ret ⟶ Result ∈ dom (locals (store (Norm s)))" and brk: "brk A = (case j of Break l ⇒ λ k. if k=l then dom (locals (store ((Norm s)::state))) else UNIV | Cont l ⇒ λ k. UNIV | Ret ⇒ λ k. UNIV)" by (elim da_elim_cases) simp from brk have "?BreakAssigned (Norm s) (Some (Jump j),s) A" by simp moreover from ret have "?ResAssigned (Norm s) (Some (Jump j),s)" by simp ultimately show ?case by (intro conjI) next case (Throw s0 e a s1 Env T A) note G = ‹prg Env = G› from Throw.prems obtain E where da_e: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨e⟩» E" by (elim da_elim_cases) from Throw.prems obtain eT where wt_e: "Env⊢e∷-eT" by (elim wt_elim_cases) have "?NormalAssigned (abupd (throw a) s1) A" by (cases s1) (simp add: throw_def) moreover have "?BreakAssigned (Norm s0) (abupd (throw a) s1) A" proof - from G Throw.hyps have eval_e: "prg Env⊢Norm s0 ─e-≻a→ s1" by (simp (no_asm_simp)) from eval_e _ wt_e have "⋀ l. abrupt s1 ≠ Some (Jump (Break l))" by (rule eval_expression_no_jump) (simp_all add: wf G) hence "⋀ l. abrupt (abupd (throw a) s1) ≠ Some (Jump (Break l))" by (cases s1) (simp add: throw_def abrupt_if_def) thus ?thesis by simp qed moreover from wt_e da_e G have "?ResAssigned (Norm s0) s1" by (elim Throw.hyps [elim_format]) simp+ hence "?ResAssigned (Norm s0) (abupd (throw a) s1)" by (cases s1) (simp add: throw_def abrupt_if_def) ultimately show ?case by (intro conjI) next case (Try s0 c1 s1 s2 C vn c2 s3 Env T A) note G = ‹prg Env = G› from Try.prems obtain C1 C2 where da_c1: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨c1⟩» C1" and da_c2: "Env⦇lcl := lcl Env(VName vn↦Class C)⦈ ⊢ (dom (locals (store ((Norm s0)::state))) ∪ {VName vn}) »⟨c2⟩» C2" and A: "nrm A = nrm C1 ∩ nrm C2" "brk A = brk C1 ⇒∩ brk C2" by (elim da_elim_cases) simp from Try.prems obtain wt_c1: "Env⊢c1∷√" and wt_c2: "Env⦇lcl := lcl Env(VName vn↦Class C)⦈⊢c2∷√" by (elim wt_elim_cases) have sxalloc: "prg Env⊢s1 ─sxalloc→ s2" using Try.hyps G by (simp (no_asm_simp)) note ‹PROP ?Hyp (In1r c1) (Norm s0) s1› with wt_c1 da_c1 G obtain nrm_C1: "?NormalAssigned s1 C1" and brk_C1: "?BreakAssigned (Norm s0) s1 C1" and res_s1: "?ResAssigned (Norm s0) s1" by simp show ?case proof (cases "normal s1") case True with nrm_C1 have "nrm C1 ∩ nrm C2 ⊆ dom (locals (store s1))" by auto moreover have "s3=s1" proof - from sxalloc True have eq_s2_s1: "s2=s1" by (cases s1) (auto elim: sxalloc_elim_cases) with True have "¬ G,s2⊢catch C" by (simp add: catch_def) with Try.hyps have "s3=s2" by simp with eq_s2_s1 show ?thesis by simp qed ultimately show ?thesis using True A res_s1 by simp next case False note not_normal_s1 = this show ?thesis proof (cases "∃ l. abrupt s1 = Some (Jump (Break l))") case True then obtain l where l: "abrupt s1 = Some (Jump (Break l))" by auto with brk_C1 have "(brk C1 ⇒∩ brk C2) l ⊆ dom (locals (store s1))" by auto moreover have "s3=s1" proof - from sxalloc l have eq_s2_s1: "s2=s1" by (cases s1) (auto elim: sxalloc_elim_cases) with l have "¬ G,s2⊢catch C" by (simp add: catch_def) with Try.hyps have "s3=s2" by simp with eq_s2_s1 show ?thesis by simp qed ultimately show ?thesis using l A res_s1 by simp next case False note abrupt_no_break = this show ?thesis proof (cases "G,s2⊢catch C") case True with Try.hyps have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3" by simp note hyp_c2 = this [rule_format] have "(dom (locals (store ((Norm s0)::state))) ∪ {VName vn}) ⊆ dom (locals (store (new_xcpt_var vn s2)))" proof - from ‹G⊢Norm s0 ─c1→ s1› have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) also from sxalloc have "… ⊆ dom (locals (store s2))" by (rule dom_locals_sxalloc_mono) also have "… ⊆ dom (locals (store (new_xcpt_var vn s2)))" by (cases s2) (simp add: new_xcpt_var_def, blast) also have "{VName vn} ⊆ …" by (cases s2) simp ultimately show ?thesis by (rule Un_least) qed with da_c2 obtain C2' where da_C2': "Env⦇lcl := lcl Env(VName vn↦Class C)⦈ ⊢ dom (locals (store (new_xcpt_var vn s2))) »⟨c2⟩» C2'" and nrm_C2': "nrm C2 ⊆ nrm C2'" and brk_C2': "∀ l. brk C2 l ⊆ brk C2' l" by (rule da_weakenE) simp from wt_c2 da_C2' G and hyp_c2 obtain nrmAss_C2: "?NormalAssigned s3 C2'" and brkAss_C2: "?BreakAssigned (new_xcpt_var vn s2) s3 C2'" and resAss_s3: "?ResAssigned (new_xcpt_var vn s2) s3" by simp from nrmAss_C2 nrm_C2' A have "?NormalAssigned s3 A" by auto moreover have "?BreakAssigned (Norm s0) s3 A" proof - from brkAss_C2 have "?BreakAssigned (Norm s0) s3 C2'" by (cases s2) (auto simp add: new_xcpt_var_def) with brk_C2' A show ?thesis by fastforce qed moreover from resAss_s3 have "?ResAssigned (Norm s0) s3" by (cases s2) ( simp add: new_xcpt_var_def) ultimately show ?thesis by (intro conjI) next case False with Try.hyps have eq_s3_s2: "s3=s2" by simp moreover from sxalloc not_normal_s1 abrupt_no_break obtain "¬ normal s2" "∀ l. abrupt s2 ≠ Some (Jump (Break l))" by - (rule sxalloc_cases,auto) ultimately obtain "?NormalAssigned s3 A" and "?BreakAssigned (Norm s0) s3 A" by (cases s2) auto moreover have "?ResAssigned (Norm s0) s3" proof (cases "abrupt s1 = Some (Jump Ret)") case True with sxalloc have "s2=s1" by (elim sxalloc_cases) auto with res_s1 eq_s3_s2 show ?thesis by simp next case False with sxalloc have "abrupt s2 ≠ Some (Jump Ret)" by (rule sxalloc_no_jump) with eq_s3_s2 show ?thesis by simp qed ultimately show ?thesis by (intro conjI) qed qed qed next case (Fin s0 c1 x1 s1 c2 s2 s3 Env T A) note G = ‹prg Env = G› from Fin.prems obtain C1 C2 where da_C1: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨c1⟩» C1" and da_C2: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨c2⟩» C2" and nrm_A: "nrm A = nrm C1 ∪ nrm C2" and brk_A: "brk A = ((brk C1) ⇒∪⇩_{∀}(nrm C2)) ⇒∩ (brk C2)" by (elim da_elim_cases) simp from Fin.prems obtain wt_c1: "Env⊢c1∷√" and wt_c2: "Env⊢c2∷√" by (elim wt_elim_cases) note ‹PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)› with wt_c1 da_C1 G obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and resAss_s1: "?ResAssigned (Norm s0) (x1,s1)" by simp obtain nrmAss_C2: "?NormalAssigned s2 C2" and brkAss_C2: "?BreakAssigned (Norm s1) s2 C2" and resAss_s2: "?ResAssigned (Norm s1) s2" proof - from Fin.hyps have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store (x1,s1)))" by - (rule dom_locals_eval_mono_elim) with da_C2 obtain C2' where da_C2': "Env⊢ dom (locals (store (x1,s1))) »⟨c2⟩» C2'" and nrm_C2': "nrm C2 ⊆ nrm C2'" and brk_C2': "∀ l. brk C2 l ⊆ brk C2' l" by (rule da_weakenE) simp note ‹PROP ?Hyp (In1r c2) (Norm s1) s2› with wt_c2 da_C2' G obtain nrmAss_C2': "?NormalAssigned s2 C2'" and brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and resAss_s2': "?ResAssigned (Norm s1) s2" by simp from nrmAss_C2' nrm_C2' have "?NormalAssigned s2 C2" by blast moreover from brkAss_C2' brk_C2' have "?BreakAssigned (Norm s1) s2 C2" by fastforce ultimately show ?thesis using that resAss_s2' by simp qed note s3 = ‹s3 = (if ∃err. x1 = Some (Error err) then (x1, s1) else abupd (abrupt_if (x1 ≠ None) x1) s2)› have s1_s2: "dom (locals s1) ⊆ dom (locals (store s2))" proof - from ‹G⊢Norm s1 ─c2→ s2› show ?thesis by (rule dom_locals_eval_mono_elim) simp qed have "?NormalAssigned s3 A" proof assume normal_s3: "normal s3" show "nrm A ⊆ dom (locals (snd s3))" proof - have "nrm C1 ⊆ dom (locals (snd s3))" proof - from normal_s3 s3 have "normal (x1,s1)" by (cases s2) (simp add: abrupt_if_def) with normal_s3 nrmAss_C1 s3 s1_s2 show ?thesis by fastforce qed moreover have "nrm C2 ⊆ dom (locals (snd s3))" proof - from normal_s3 s3 have "normal s2" by (cases s2) (simp add: abrupt_if_def) with normal_s3 nrmAss_C2 s3 s1_s2 show ?thesis by fastforce qed ultimately have "nrm C1 ∪ nrm C2 ⊆ …" by (rule Un_least) with nrm_A show ?thesis by simp qed qed moreover { fix l assume brk_s3: "abrupt s3 = Some (Jump (Break l))" have "brk A l ⊆ dom (locals (store s3))" proof (cases "normal s2") case True with brk_s3 s3 have s2_s3: "dom (locals (store s2)) ⊆ dom (locals (store s3))" by simp have "brk C1 l ⊆ dom (locals (store s3))" proof - from True brk_s3 s3 have "x1=Some (Jump (Break l))" by (cases s2) (simp add: abrupt_if_def) with brkAss_C1 s1_s2 s2_s3 show ?thesis by simp qed moreover from True nrmAss_C2 s2_s3 have "nrm C2 ⊆ dom (locals (store s3))" by - (rule subset_trans, simp_all) ultimately have "((brk C1) ⇒∪⇩_{∀}(nrm C2)) l ⊆ …" by blast with brk_A show ?thesis by simp blast next case False note not_normal_s2 = this have "s3=s2" proof (cases "normal (x1,s1)") case True with not_normal_s2 s3 show ?thesis by (cases s2) (simp add: abrupt_if_def) next case False with not_normal_s2 s3 brk_s3 show ?thesis by (cases s2) (simp add: abrupt_if_def) qed with brkAss_C2 brk_s3 have "brk C2 l ⊆ dom (locals (store s3))" by simp with brk_A show ?thesis by simp blast qed } hence "?BreakAssigned (Norm s0) s3 A" by simp moreover { assume abr_s3: "abrupt s3 = Some (Jump Ret)" have "Result ∈ dom (locals (store s3))" proof (cases "x1 = Some (Jump Ret)") case True note ret_x1 = this with resAss_s1 have res_s1: "Result ∈ dom (locals s1)" by simp moreover have "dom (locals (store ((Norm s1)::state))) ⊆ dom (locals (store s2))" by (rule dom_locals_eval_mono_elim) (rule Fin.hyps) ultimately have "Result ∈ dom (locals (store s2))" by - (rule subsetD,auto) with res_s1 s3 show ?thesis by simp next case False with s3 abr_s3 obtain "abrupt s2 = Some (Jump Ret)" and "s3=s2" by (cases s2) (simp add: abrupt_if_def) with resAss_s2 show ?thesis by simp qed } hence "?ResAssigned (Norm s0) s3" by simp ultimately show ?case by (intro conjI) next case (Init C c s0 s3 s1 s2 Env T A) note G = ‹prg Env = G› from Init.hyps have eval: "prg Env⊢ Norm s0 ─Init C→ s3" apply (simp only: G) apply (rule eval.Init, assumption) apply (cases "inited C (globs s0) ") apply simp apply (simp only: if_False ) apply (elim conjE,intro conjI,assumption+,simp) done (* auto or simp alone always do too much *) from Init.prems and ‹the (class G C) = c› have c: "class G C = Some c" by (elim wt_elim_cases) auto from Init.prems obtain nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))" by (elim da_elim_cases) simp show ?case proof (cases "inited C (globs s0)") case True with Init.hyps have "s3=Norm s0" by simp thus ?thesis using nrm_A by simp next case False from Init.hyps False G obtain eval_initC: "prg Env⊢Norm ((init_class_obj G C) s0) ─(if C = Object then Skip else Init (super c))→ s1" and eval_init: "prg Env⊢(set_lvars Map.empty) s1 ─init c→ s2" and s3: "s3=(set_lvars (locals (store s1))) s2" by simp have "?NormalAssigned s3 A" proof show "nrm A ⊆ dom (locals (store s3))" proof - from nrm_A have "nrm A ⊆ dom (locals (init_class_obj G C s0))" by simp also from eval_initC have "… ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) simp also from s3 have "… ⊆ dom (locals (store s3))" by (cases s1) (cases s2, simp add: init_lvars_def2) finally show ?thesis . qed qed moreover from eval have "⋀ j. abrupt s3 ≠ Some (Jump j)" by (rule eval_statement_no_jump) (auto simp add: wf c G) then obtain "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3" by simp ultimately show ?thesis by (intro conjI) qed next case (NewC s0 C s1 a s2 Env T A) note G = ‹prg Env = G› from NewC.prems obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))" "brk A = (λ l. UNIV)" by (elim da_elim_cases) simp from wf NewC.prems have wt_init: "Env⊢(Init C)∷√" by (elim wt_elim_cases) (drule is_acc_classD,simp) have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s2))" proof - have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) (rule NewC.hyps) also have "… ⊆ dom (locals (store s2))" by (rule dom_locals_halloc_mono) (rule NewC.hyps) finally show ?thesis . qed with A have "?NormalAssigned s2 A" by simp moreover { fix j have "abrupt s2 ≠ Some (Jump j)" proof - have eval: "prg Env⊢ Norm s0 ─NewC C-≻Addr a→ s2" unfolding G by (rule eval.NewC NewC.hyps)+ from NewC.prems obtain T' where "T=Inl T'" by (elim wt_elim_cases) simp with NewC.prems have "Env⊢NewC C∷-T'" by simp from eval _ this show ?thesis by (rule eval_expression_no_jump) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2" by simp_all ultimately show ?case by (intro conjI) next case (NewA s0 elT s1 e i s2 a s3 Env T A) note G = ‹prg Env = G› from NewA.prems obtain da_e: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨e⟩» A" by (elim da_elim_cases) from NewA.prems obtain wt_init: "Env⊢init_comp_ty elT∷√" and wt_size: "Env⊢e∷-PrimT Integer" by (elim wt_elim_cases) (auto dest: wt_init_comp_ty') note halloc = ‹G⊢abupd (check_neg i) s2─halloc Arr elT (the_Intg i)≻a→s3› have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) (rule NewA.hyps) with da_e obtain A' where da_e': "Env⊢ dom (locals (store s1)) »⟨e⟩» A'" and nrm_A_A': "nrm A ⊆ nrm A'" and brk_A_A': "∀ l. brk A l ⊆ brk A' l" by (rule da_weakenE) simp note ‹PROP ?Hyp (In1l e) s1 s2› with wt_size da_e' G obtain nrmAss_A': "?NormalAssigned s2 A'" and brkAss_A': "?BreakAssigned s1 s2 A'" by simp have s2_s3: "dom (locals (store s2)) ⊆ dom (locals (store s3))" proof - have "dom (locals (store s2)) ⊆ dom (locals (store (abupd (check_neg i) s2)))" by (simp) also have "… ⊆ dom (locals (store s3))" by (rule dom_locals_halloc_mono) (rule NewA.hyps) finally show ?thesis . qed have "?NormalAssigned s3 A" proof assume normal_s3: "normal s3" show "nrm A ⊆ dom (locals (store s3))" proof - from halloc normal_s3 have "normal (abupd (check_neg i) s2)" by cases simp_all hence "normal s2" by (cases s2) simp with nrmAss_A' nrm_A_A' s2_s3 show ?thesis by blast qed qed moreover { fix j have "abrupt s3 ≠ Some (Jump j)" proof - have eval: "prg Env⊢ Norm s0 ─New elT[e]-≻Addr a→ s3" unfolding G by (rule eval.NewA NewA.hyps)+ from NewA.prems obtain T' where "T=Inl T'" by (elim wt_elim_cases) simp with NewA.prems have "Env⊢New elT[e]∷-T'" by simp from eval _ this show ?thesis by (rule eval_expression_no_jump) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3" by simp_all ultimately show ?case by (intro conjI) next case (Cast s0 e v s1 s2 cT Env T A) note G = ‹prg Env = G› from Cast.prems obtain da_e: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨e⟩» A" by (elim da_elim_cases) from Cast.prems obtain eT where wt_e: "Env⊢e∷-eT" by (elim wt_elim_cases) note ‹PROP ?Hyp (In1l e) (Norm s0) s1› with wt_e da_e G obtain nrmAss_A: "?NormalAssigned s1 A" and brkAss_A: "?BreakAssigned (Norm s0) s1 A" by simp note s2 = ‹s2 = abupd (raise_if (¬ G,snd s1⊢v fits cT) ClassCast) s1› hence s1_s2: "dom (locals (store s1)) ⊆ dom (locals (store s2))" by simp have "?NormalAssigned s2 A" proof assume "normal s2" with s2 have "normal s1" by (cases s1) simp with nrmAss_A s1_s2 show "nrm A ⊆ dom (locals (store s2))" by blast qed moreover { fix j have "abrupt s2 ≠ Some (Jump j)" proof - have eval: "prg Env⊢ Norm s0 ─Cast cT e-≻v→ s2" unfolding G by (rule eval.Cast Cast.hyps)+ from Cast.prems obtain T' where "T=Inl T'" by (elim wt_elim_cases) simp with Cast.prems have "Env⊢Cast cT e∷-T'" by simp from eval _ this show ?thesis by (rule eval_expression_no_jump) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2" by simp_all ultimately show ?case by (intro conjI) next case (Inst s0 e v s1 b iT Env T A) note G = ‹prg Env = G› from Inst.prems obtain da_e: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨e⟩» A" by (elim da_elim_cases) from Inst.prems obtain eT where wt_e: "Env⊢e∷-eT" by (elim wt_elim_cases) note ‹PROP ?Hyp (In1l e) (Norm s0) s1› with wt_e da_e G obtain "?NormalAssigned s1 A" and "?BreakAssigned (Norm s0) s1 A" and "?ResAssigned (Norm s0) s1" by simp thus ?case by (intro conjI) next case (Lit s v Env T A) from Lit.prems have "nrm A = dom (locals (store ((Norm s)::state)))" by (elim da_elim_cases) simp thus ?case by simp next case (UnOp s0 e v s1 unop Env T A) note G = ‹prg Env = G› from UnOp.prems obtain da_e: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨e⟩» A" by (elim da_elim_cases) from UnOp.prems obtain eT where wt_e: "Env⊢e∷-eT" by (elim wt_elim_cases) note ‹PROP ?Hyp (In1l e) (Norm s0) s1› with wt_e da_e G obtain "?NormalAssigned s1 A" and "?BreakAssigned (Norm s0) s1 A" and "?ResAssigned (Norm s0) s1" by simp thus ?case by (intro conjI) next case (BinOp s0 e1 v1 s1 binop e2 v2 s2 Env T A) note G = ‹prg Env = G› from BinOp.hyps have eval: "prg Env⊢Norm s0 ─BinOp binop e1 e2-≻(eval_binop binop v1 v2)→ s2" by (simp only: G) (rule eval.BinOp) have s0_s1: "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) (rule BinOp) also have s1_s2: "dom (locals (store s1)) ⊆ dom (locals (store s2))" by (rule dom_locals_eval_mono_elim) (rule BinOp) finally have s0_s2: "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s2))" . from BinOp.prems obtain e1T e2T where wt_e1: "Env⊢e1∷-e1T" and wt_e2: "Env⊢e2∷-e2T" and wt_binop: "wt_binop (prg Env) binop e1T e2T" and T: "T=Inl (PrimT (binop_type binop))" by (elim wt_elim_cases) simp have "?NormalAssigned s2 A" proof assume normal_s2: "normal s2" have normal_s1: "normal s1" by (rule eval_no_abrupt_lemma [rule_format]) (rule BinOp.hyps, rule normal_s2) show "nrm A ⊆ dom (locals (store s2))" proof (cases "binop=CondAnd") case True note CondAnd = this from BinOp.prems obtain nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) ∪ (assigns_if True (BinOp CondAnd e1 e2) ∩ assigns_if False (BinOp CondAnd e1 e2))" by (elim da_elim_cases) (simp_all add: CondAnd) from T BinOp.prems CondAnd have "Env⊢BinOp binop e1 e2∷-PrimT Boolean" by (simp) with eval normal_s2 have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2) ⊆ dom (locals (store s2))" by (rule assigns_if_good_approx) have "(assigns_if True (BinOp CondAnd e1 e2) ∩ assigns_if False (BinOp CondAnd e1 e2)) ⊆ …" proof (cases "the_Bool (eval_binop binop v1 v2)") case True with ass_if CondAnd have "assigns_if True (BinOp CondAnd e1 e2) ⊆ dom (locals (store s2))" by simp thus ?thesis by blast next case False with ass_if CondAnd have "assigns_if False (BinOp CondAnd e1 e2) ⊆ dom (locals (store s2))" by (simp only: False) thus ?thesis by blast qed with s0_s2 have "dom (locals (store ((Norm s0)::state))) ∪ (assigns_if True (BinOp CondAnd e1 e2) ∩ assigns_if False (BinOp CondAnd e1 e2)) ⊆ …" by (rule Un_least) thus ?thesis by (simp only: nrm_A) next case False note notCondAnd = this show ?thesis proof (cases "binop=CondOr") case True note CondOr = this from BinOp.prems obtain nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) ∪ (assigns_if True (BinOp CondOr e1 e2) ∩ assigns_if False (BinOp CondOr e1 e2))" by (elim da_elim_cases) (simp_all add: CondOr) from T BinOp.prems CondOr have "Env⊢BinOp binop e1 e2∷-PrimT Boolean" by (simp) with eval normal_s2 have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2) ⊆ dom (locals (store s2))" by (rule assigns_if_good_approx) have "(assigns_if True (BinOp CondOr e1 e2) ∩ assigns_if False (BinOp CondOr e1 e2)) ⊆ …" proof (cases "the_Bool (eval_binop binop v1 v2)") case True with ass_if CondOr have "assigns_if True (BinOp CondOr e1 e2) ⊆ dom (locals (store s2))" by (simp) thus ?thesis by blast next case False with ass_if CondOr have "assigns_if False (BinOp CondOr e1 e2) ⊆ dom (locals (store s2))" by (simp) thus ?thesis by blast qed with s0_s2 have "dom (locals (store ((Norm s0)::state))) ∪ (assigns_if True (BinOp CondOr e1 e2) ∩ assigns_if False (BinOp CondOr e1 e2)) ⊆ …" by (rule Un_least) thus ?thesis by (simp only: nrm_A) next case False with notCondAnd obtain notAndOr: "binop≠CondAnd" "binop≠CondOr" by simp from BinOp.prems obtain E1 where da_e1: "Env⊢ dom (locals (snd (Norm s0))) »⟨e1⟩» E1" and da_e2: "Env⊢ nrm E1 »⟨e2⟩» A" by (elim da_elim_cases) (simp_all add: notAndOr) note ‹PROP ?Hyp (In1l e1) (Norm s0) s1› with wt_e1 da_e1 G normal_s1 obtain "?NormalAssigned s1 E1" by simp with normal_s1 have "nrm E1 ⊆ dom (locals (store s1))" by iprover with da_e2 obtain A' where da_e2': "Env⊢ dom (locals (store s1)) »⟨e2⟩» A'" and nrm_A_A': "nrm A ⊆ nrm A'" by (rule da_weakenE) iprover from notAndOr have "need_second_arg binop v1" by simp with BinOp.hyps have "PROP ?Hyp (In1l e2) s1 s2" by simp with wt_e2 da_e2' G obtain "?NormalAssigned s2 A'" by simp with nrm_A_A' normal_s2 show "nrm A ⊆ dom (locals (store s2))" by blast qed qed qed moreover { fix j have "abrupt s2 ≠ Some (Jump j)" proof - from BinOp.prems T have "Env⊢In1l (BinOp binop e1 e2)∷Inl (PrimT (binop_type binop))" by simp from eval _ this show ?thesis by (rule eval_expression_no_jump) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2" by simp_all ultimately show ?case by (intro conjI) next case (Super s Env T A) from Super.prems have "nrm A = dom (locals (store ((Norm s)::state)))" by (elim da_elim_cases) simp thus ?case by simp next case (Acc s0 v w upd s1 Env T A) show ?case proof (cases "∃ vn. v = LVar vn") case True then obtain vn where vn: "v=LVar vn".. from Acc.prems have "nrm A = dom (locals (store ((Norm s0)::state)))" by (simp only: vn) (elim da_elim_cases,simp_all) moreover from ‹G⊢Norm s0 ─v=≻(w, upd)→ s1› have "s1=Norm s0" by (simp only: vn) (elim eval_elim_cases,simp) ultimately show ?thesis by simp next case False note G = ‹prg Env = G› from False Acc.prems have da_v: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨v⟩» A" by (elim da_elim_cases) simp_all from Acc.prems obtain vT where wt_v: "Env⊢v∷=vT" by (elim wt_elim_cases) note ‹PROP ?Hyp (In2 v) (Norm s0) s1› with wt_v da_v G obtain "?NormalAssigned s1 A" and "?BreakAssigned (Norm s0) s1 A" and "?ResAssigned (Norm s0) s1" by simp thus ?thesis by (intro conjI) qed next case (Ass s0 var w upd s1 e v s2 Env T A) note G = ‹prg Env = G› from Ass.prems obtain varT eT where wt_var: "Env⊢var∷=varT" and wt_e: "Env⊢e∷-eT" by (elim wt_elim_cases) simp have eval_var: "prg Env⊢Norm s0 ─var=≻(w, upd)→ s1" using Ass.hyps by (simp only: G) have "?NormalAssigned (assign upd v s2) A" proof assume normal_ass_s2: "normal (assign upd v s2)" from normal_ass_s2 have normal_s2: "normal s2" by (cases s2) (simp add: assign_def Let_def) hence normal_s1: "normal s1" by - (rule eval_no_abrupt_lemma [rule_format], rule Ass.hyps) note hyp_var = ‹PROP ?Hyp (In2 var) (Norm s0) s1› note hyp_e = ‹PROP ?Hyp (In1l e) s1 s2› show "nrm A ⊆ dom (locals (store (assign upd v s2)))" proof (cases "∃ vn. var = LVar vn") case True then obtain vn where vn: "var=LVar vn".. from Ass.prems obtain E where da_e: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨e⟩» E" and nrm_A: "nrm A = nrm E ∪ {vn}" by (elim da_elim_cases) (insert vn,auto) obtain E' where da_e': "Env⊢ dom (locals (store s1)) »⟨e⟩» E'" and E_E': "nrm E ⊆ nrm E'" proof - have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) (rule Ass.hyps) with da_e show thesis by (rule da_weakenE) (rule that) qed from G eval_var vn have eval_lvar: "G⊢Norm s0 ─LVar vn=≻(w, upd)→ s1" by simp then have upd: "upd = snd (lvar vn (store s1))" by cases (cases "lvar vn (store s1)",simp) have "nrm E ⊆ dom (locals (store (assign upd v s2)))" proof - from hyp_e wt_e da_e' G normal_s2 have "nrm E' ⊆ dom (locals (store s2))" by simp also from upd have "dom (locals (store s2)) ⊆ dom (locals (store (upd v s2)))" by (simp add: lvar_def) blast hence "dom (locals (store s2)) ⊆ dom (locals (store (assign upd v s2)))" by (rule dom_locals_assign_mono) finally show ?thesis using E_E' by blast qed moreover from upd normal_s2 have "{vn} ⊆ dom (locals (store (assign upd v s2)))" by (auto simp add: assign_def Let_def lvar_def upd split: prod.split) ultimately show "nrm A ⊆ …" by (rule Un_least [elim_format]) (simp add: nrm_A) next case False from Ass.prems obtain V where da_var: "Env⊢ dom (locals (store ((Norm s0)::state))) »⟨var⟩» V" and da_e: "Env⊢ nrm V »⟨e⟩» A" by (elim da_elim_cases) (insert False,simp+) from hyp_var wt_var da_var G normal_s1 have "nrm V ⊆ dom (locals (store s1))" by simp with da_e obtain A' where da_e': "Env⊢ dom (locals (store s1)) »⟨e⟩» A'" and nrm_A_A': "nrm A ⊆ nrm A'" by (rule da_weakenE) iprover from hyp_e wt_e da_e' G normal_s2 obtain "nrm A' ⊆ dom (locals (store s2))" by simp with nrm_A_A' have "nrm A ⊆ …" by blast also have "… ⊆ dom (locals (store (assign upd v s2)))" proof - from eval_var normal_s1 have "dom (locals (store s2)) ⊆ dom (locals (store (upd v s2)))" by (cases rule: dom_locals_eval_mono_elim) (cases s2, simp) thus ?thesis by (rule dom_locals_assign_mono) qed finally show ?thesis . qed qed moreover { fix j have "abrupt (assign upd v s2) ≠ Some (Jump j)" proof - have eval: "prg Env⊢Norm s0 ─var:=e-≻v→ (assign upd v s2)" by (simp only: G) (rule eval.Ass Ass.hyps)+ from Ass.prems obtain T' where "T=Inl T'" by (elim wt_elim_cases) simp with Ass.prems have "Env⊢var:=e∷-T'" by simp from eval _ this show ?thesis by (rule eval_expression_no_jump) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) (assign upd v s2) A" and "?ResAssigned (Norm s0) (assign upd v s2)" by simp_all ultimately show ?case by (intro conjI) next case (Cond s0 e0 b s1 e1 e2 v s2 Env T A) note G = ‹prg Env = G› have "?NormalAssigned s2 A" proof assume normal_s2: "normal s2" show "nrm A ⊆ dom (locals (store s2))" proof (cases "Env⊢(e0 ? e1 : e2)∷-(PrimT Boolean)") case True with Cond.prems have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) ∪ (assigns_if True (e0 ? e1 : e2) ∩ assigns_if False (e0 ? e1 : e2))" by (elim da_elim_cases) simp_all have eval: "prg Env⊢Norm s0 ─(e0 ? e1 : e2)-≻v→ s2" unfolding G by (rule eval.Cond Cond.hyps)+ from eval have "dom (locals (store ((Norm s0)::state)))⊆dom (locals (store s2))" by (rule dom_locals_eval_mono_elim) moreover from eval normal_s2 True have ass_if: "assigns_if (the_Bool v) (e0 ? e1 : e2) ⊆ dom (locals (store s2))" by (rule assigns_if_good_approx) have "assigns_if True (e0 ? e1:e2) ∩ assigns_if False (e0 ? e1:e2) ⊆ dom (locals (store s2))" proof (cases "the_Bool v") case True from ass_if have "assigns_if True (e0 ? e1:e2) ⊆ dom (locals (store s2))" by (simp only: True) thus ?thesis by blast next case False from ass_if have "assigns_if False (e0 ? e1:e2) ⊆ dom (locals (store s2))" by (simp only: False) thus ?thesis by blast qed ultimately show "nrm A ⊆ dom (locals (store s2))" by (simp only: nrm_A) (rule Un_least) next case False with Cond.prems obtain E1 E2 where da_e1: "Env⊢ (dom (locals (store ((Norm s0)::state))) ∪ assigns_if True e0) »⟨e1⟩» E1" and da_e2: "Env⊢ (dom (locals (store ((Norm s0)::state))) ∪ assigns_if False e0) »⟨e2⟩» E2" and nrm_A: "nrm A = nrm E1 ∩ nrm E2" by (elim da_elim_cases) simp_all from Cond.prems obtain e1T e2T where wt_e0: "Env⊢e0∷- PrimT Boolean" and wt_e1: "Env⊢e1∷-e1T" and wt_e2: "Env⊢e2∷-e2T" by (elim wt_elim_cases) have s0_s1: "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) (rule Cond.hyps) have eval_e0: "prg Env⊢Norm s0 ─e0-≻b→ s1" unfolding G by (rule Cond.hyps) have normal_s1: "normal s1" by (rule eval_no_abrupt_lemma [rule_format]) (rule Cond.hyps, rule normal_s2) show ?thesis proof (cases "the_Bool b") case True from True Cond.hyps have "PROP ?Hyp (In1l e1) s1 s2" by simp moreover from eval_e0 normal_s1 wt_e0 have "assigns_if True e0 ⊆ dom (locals (store s1))" by (rule assigns_if_good_approx [elim_format]) (simp only: True) with s0_s1 have "dom (locals (store ((Norm s0)::state))) ∪ assigns_if True e0 ⊆ …" by (rule Un_least) with da_e1 obtain E1' where da_e1': "Env⊢ dom (locals (store s1)) »⟨e1⟩» E1'" and nrm_E1_E1': "nrm E1 ⊆ nrm E1'" by (rule da_weakenE) iprover ultimately have "nrm E1' ⊆ dom (locals (store s2))" using wt_e1 G normal_s2 by simp with nrm_E1_E1' show ?thesis by (simp only: nrm_A) blast next case False from False Cond.hyps have "PROP ?Hyp (In1l e2) s1 s2" by simp moreover from eval_e0 normal_s1 wt_e0 have "assigns_if False e0 ⊆ dom (locals (store s1))" by (rule assigns_if_good_approx [elim_format]) (simp only: False) with s0_s1 have "dom (locals (store ((Norm s0)::state))) ∪ assigns_if False e0 ⊆ …" by (rule Un_least) with da_e2 obtain E2' where da_e2': "Env⊢ dom (locals (store s1)) »⟨e2⟩» E2'" and nrm_E2_E2': "nrm E2 ⊆ nrm E2'" by (rule da_weakenE) iprover ultimately have "nrm E2' ⊆ dom (locals (store s2))" using wt_e2 G normal_s2 by simp with nrm_E2_E2' show ?thesis by (simp only: nrm_A) blast qed qed qed moreover { fix j have "abrupt s2 ≠ Some (Jump j)" proof - have eval: "prg Env⊢Norm s0 ─e0 ? e1 : e2-≻v→ s2" unfolding G by (rule eval.Cond Cond.hyps)+ from Cond.prems obtain T' where "T=Inl T'" by (elim wt_elim_cases) simp with Cond.prems have "Env⊢e0 ? e1 : e2∷-T'" by simp from eval _ this show ?thesis by (rule eval_expression_no_jump) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2" by simp_all ultimately show ?case by (intro conjI) next case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4 Env T A) note G = ‹prg Env = G› have "?NormalAssigned (restore_lvars s2 s4) A" proof assume normal_restore_lvars: "normal (restore_lvars s2 s4)" show "nrm A ⊆ dom (locals (store (restore_lvars s2 s4)))" proof - from Call.prems obtain E where da_e: "Env⊢ (dom (locals (store ((Norm s0)::state))))»⟨e⟩» E" and da_args: "Env⊢ nrm E »⟨args⟩» A" by (elim da_elim_cases) from Call.prems obtain eT argsT where wt_e: "Env⊢e∷-eT" and wt_args: "Env⊢args∷≐argsT" by (elim wt_elim_cases) note s3 = ‹s3 = init_lvars G D ⦇name = mn, parTs = pTs⦈ mode a vs s2› note s3' = ‹s3' = check_method_access G accC statT mode ⦇name=mn,parTs=pTs⦈ a s3› have normal_s2: "normal s2" proof - from normal_restore_lvars have "normal s4" by simp then have "normal s3'" by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps) with s3' have "normal s3" by (cases s3) (simp add: check_method_access_def Let_def) with s3 show "normal s2" by (cases s2) (simp add: init_lvars_def Let_def) qed then have normal_s1: "normal s1" by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps) note ‹PROP ?Hyp (In1l e) (Norm s0) s1› with da_e wt_e G normal_s1 have "nrm E ⊆ dom (locals (store s1))" by simp with da_args obtain A' where da_args': "Env⊢ dom (locals (store s1)) »⟨args⟩» A'" and nrm_A_A': "nrm A ⊆ nrm A'" by (rule da_weakenE) iprover note ‹PROP ?Hyp (In3 args) s1 s2› with da_args' wt_args G normal_s2 have "nrm A' ⊆ dom (locals (store s2))" by simp with nrm_A_A' have "nrm A ⊆ dom (locals (store s2))" by blast also have "… ⊆ dom (locals (store (restore_lvars s2 s4)))" by (cases s4) simp finally show ?thesis . qed qed moreover { fix j have "abrupt (restore_lvars s2 s4) ≠ Some (Jump j)" proof - have eval: "prg Env⊢Norm s0 ─({accC,statT,mode}e⋅mn( {pTs}args))-≻v → (restore_lvars s2 s4)" unfolding G by (rule eval.Call Call)+ from Call.prems obtain T' where "T=Inl T'" by (elim wt_elim_cases) simp with Call.prems have "Env⊢({accC,statT,mode}e⋅mn( {pTs}args))∷-T'" by simp from eval _ this show ?thesis by (rule eval_expression_no_jump) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) (restore_lvars s2 s4) A" and "?ResAssigned (Norm s0) (restore_lvars s2 s4)" by simp_all ultimately show ?case by (intro conjI) next case (Methd s0 D sig v s1 Env T A) note G = ‹prg Env = G› from Methd.prems obtain m where m: "methd (prg Env) D sig = Some m" and da_body: "Env⊢(dom (locals (store ((Norm s0)::state)))) »⟨Body (declclass m) (stmt (mbody (mthd m)))⟩» A" by - (erule da_elim_cases) from Methd.prems m obtain isCls: "is_class (prg Env) D" and wt_body: "Env ⊢In1l (Body (declclass m) (stmt (mbody (mthd m))))∷T" by - (erule wt_elim_cases,simp) note ‹PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1› moreover from wt_body have "Env⊢In1l (body G D sig)∷T" using isCls m G by (simp add: body_def2) moreover from da_body have "Env⊢(dom (locals (store ((Norm s0)::state)))) »⟨body G D sig⟩» A" using isCls m G by (simp add: body_def2) ultimately show ?case using G by simp next case (Body s0 D s1 c s2 s3 Env T A) note G = ‹prg Env = G› from Body.prems have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))" by (elim da_elim_cases) simp have eval: "prg Env⊢Norm s0 ─Body D c-≻the (locals (store s2) Result) →abupd (absorb Ret) s3" unfolding G by (rule eval.Body Body.hyps)+ hence "nrm A ⊆ dom (locals (store (abupd (absorb Ret) s3)))" by (simp only: nrm_A) (rule dom_locals_eval_mono_elim) hence "?NormalAssigned (abupd (absorb Ret) s3) A" by simp moreover from eval have "⋀ j. abrupt (abupd (absorb Ret) s3) ≠ Some (Jump j)" by (rule Body_no_jump) simp hence "?BreakAssigned (Norm s0) (abupd (absorb Ret) s3) A" and "?ResAssigned (Norm s0) (abupd (absorb Ret) s3)" by simp_all ultimately show ?case by (intro conjI) next case (LVar s vn Env T A) from LVar.prems have "nrm A = dom (locals (store ((Norm s)::state)))" by (elim da_elim_cases) simp thus ?case by simp next case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC Env T A) note G = ‹prg Env = G› have "?NormalAssigned s3 A" proof assume normal_s3: "normal s3" show "nrm A ⊆ dom (locals (store s3))" proof - note fvar = ‹(v, s2') = fvar statDeclC stat fn a s2› and s3 = ‹s3 = check_field_access G accC statDeclC fn stat a s2'› from FVar.prems have da_e: "Env⊢ (dom (locals (store ((Norm s0)::state))))»⟨e⟩» A" by (elim da_elim_cases) from FVar.prems obtain eT where wt_e: "Env⊢e∷-eT" by (elim wt_elim_cases) have "(dom (locals (store ((Norm s0)::state)))) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) (rule FVar.hyps) with da_e obtain A' where da_e': "Env⊢ dom (locals (store s1)) »⟨e⟩» A'" and nrm_A_A': "nrm A ⊆ nrm A'" by (rule da_weakenE) iprover have normal_s2: "normal s2" proof - from normal_s3 s3 have "normal s2'" by (cases s2') (simp add: check_field_access_def Let_def) with fvar show "normal s2" by (cases s2) (simp add: fvar_def2) qed note ‹PROP ?Hyp (In1l e) s1 s2› with da_e' wt_e G normal_s2 have "nrm A' ⊆ dom (locals (store s2))" by simp with nrm_A_A' have "nrm A ⊆ dom (locals (store s2))" by blast also have "… ⊆ dom (locals (store s3))" proof - from fvar have "s2' = snd (fvar statDeclC stat fn a s2)" by (cases "fvar statDeclC stat fn a s2") simp hence "dom (locals (store s2)) ⊆ dom (locals (store s2'))" by (simp) (rule dom_locals_fvar_mono) also from s3 have "… ⊆ dom (locals (store s3))" by (cases s2') (simp add: check_field_access_def Let_def) finally show ?thesis . qed finally show ?thesis . qed qed moreover { fix j have "abrupt s3 ≠ Some (Jump j)" proof - obtain w upd where v: "(w,upd)=v" by (cases v) auto have eval: "prg Env⊢Norm s0─({accC,statDeclC,stat}e..fn)=≻(w,upd)→s3" by (simp only: G v) (rule eval.FVar FVar.hyps)+ from FVar.prems obtain T' where "T=Inl T'" by (elim wt_elim_cases) simp with FVar.prems have "Env⊢({accC,statDeclC,stat}e..fn)∷=T'" by simp from eval _ this show ?thesis by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3" by simp_all ultimately show ?case by (intro conjI) next case (AVar s0 e1 a s1 e2 i s2 v s2' Env T A) note G = ‹prg Env = G› have "?NormalAssigned s2' A" proof assume normal_s2': "normal s2'" show "nrm A ⊆ dom (locals (store s2'))" proof - note avar = ‹(v, s2') = avar G i a s2› from AVar.prems obtain E1 where da_e1: "Env⊢ (dom (locals (store ((Norm s0)::state))))»⟨e1⟩» E1" and da_e2: "Env⊢ nrm E1 »⟨e2⟩» A" by (elim da_elim_cases) from AVar.prems obtain e1T e2T where wt_e1: "Env⊢e1∷-e1T" and wt_e2: "Env⊢e2∷-e2T" by (elim wt_elim_cases) from avar normal_s2' have normal_s2: "normal s2" by (cases s2) (simp add: avar_def2) hence "normal s1" by - (rule eval_no_abrupt_lemma [rule_format], rule AVar, rule normal_s2) moreover note ‹PROP ?Hyp (In1l e1) (Norm s0) s1› ultimately have "nrm E1 ⊆ dom (locals (store s1))" using da_e1 wt_e1 G by simp with da_e2 obtain A' where da_e2': "Env⊢ dom (locals (store s1)) »⟨e2⟩» A'" and nrm_A_A': "nrm A ⊆ nrm A'" by (rule da_weakenE) iprover note ‹PROP ?Hyp (In1l e2) s1 s2› with da_e2' wt_e2 G normal_s2 have "nrm A' ⊆ dom (locals (store s2))" by simp with nrm_A_A' have "nrm A ⊆ dom (locals (store s2))" by blast also have "… ⊆ dom (locals (store s2'))" proof - from avar have "s2' = snd (avar G i a s2)" by (cases "(avar G i a s2)") simp thus "dom (locals (store s2)) ⊆ dom (locals (store s2'))" by (simp) (rule dom_locals_avar_mono) qed finally show ?thesis . qed qed moreover { fix j have "abrupt s2' ≠ Some (Jump j)" proof - obtain w upd where v: "(w,upd)=v" by (cases v) auto have eval: "prg Env⊢Norm s0─(e1.[e2])=≻(w,upd)→s2'" unfolding G v by (rule eval.AVar AVar.hyps)+ from AVar.prems obtain T' where "T=Inl T'" by (elim wt_elim_cases) simp with AVar.prems have "Env⊢(e1.[e2])∷=T'" by simp from eval _ this show ?thesis by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) s2' A" and "?ResAssigned (Norm s0) s2'" by simp_all ultimately show ?case by (intro conjI) next case (Nil s0 Env T A) from Nil.prems have "nrm A = dom (locals (store ((Norm s0)::state)))" by (elim da_elim_cases) simp thus ?case by simp next case (Cons s0 e v s1 es vs s2 Env T A) note G = ‹prg Env = G› have "?NormalAssigned s2 A" proof assume normal_s2: "normal s2" show "nrm A ⊆ dom (locals (store s2))" proof - from Cons.prems obtain E where da_e: "Env⊢ (dom (locals (store ((Norm s0)::state))))»⟨e⟩» E" and da_es: "Env⊢ nrm E »⟨es⟩» A" by (elim da_elim_cases) from Cons.prems obtain eT esT where wt_e: "Env⊢e∷-eT" and wt_es: "Env⊢es∷≐esT" by (elim wt_elim_cases) have "normal s1" by - (rule eval_no_abrupt_lemma [rule_format], rule Cons.hyps, rule normal_s2) moreover note ‹PROP ?Hyp (In1l e) (Norm s0) s1› ultimately have "nrm E ⊆ dom (locals (store s1))" using da_e wt_e G by simp with da_es obtain A' where da_es': "Env⊢ dom (locals (store s1)) »⟨es⟩» A'" and nrm_A_A': "nrm A ⊆ nrm A'" by (rule da_weakenE) iprover note ‹PROP ?Hyp (In3 es) s1 s2› with da_es' wt_es G normal_s2 have "nrm A' ⊆ dom (locals (store s2))" by simp with nrm_A_A' show "nrm A ⊆ dom (locals (store s2))" by blast qed qed moreover { fix j have "abrupt s2 ≠ Some (Jump j)" proof - have eval: "prg Env⊢Norm s0─(e # es)≐≻v#vs→s2" unfolding G by (rule eval.Cons Cons.hyps)+ from Cons.prems obtain T' where "T=Inr T'" by (elim wt_elim_cases) simp with Cons.prems have "Env⊢(e # es)∷≐T'" by simp from eval _ this show ?thesis by (rule eval_expression_list_no_jump) (simp_all add: G wf) qed } hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2" by simp_all ultimately show ?case by (intro conjI) qed qed lemma da_good_approxE: assumes "prg Env⊢s0 ─t≻→ (v, s1)" and "Env⊢t∷T" and "Env⊢ dom (locals (store s0)) »t» A" and "wf_prog (prg Env)" obtains "normal s1 ⟹ nrm A ⊆ dom (locals (store s1))" and "⋀ l. ⟦abrupt s1 = Some (Jump (Break l)); normal s0⟧ ⟹ brk A l ⊆ dom (locals (store s1))" and "⟦abrupt s1 = Some (Jump Ret);normal s0⟧⟹Result ∈ dom (locals (store s1))" using assms by - (drule (3) da_good_approx, simp) (* Same as above but with explicit environment; It would be nicer to find a "normalized" way to right down those things in Bali. *) lemma da_good_approxE': assumes eval: "G⊢s0 ─t≻→ (v, s1)" and wt: "⦇prg=G,cls=C,lcl=L⦈⊢t∷T" and da: "⦇prg=G,cls=C,lcl=L⦈⊢ dom (locals (store s0)) »t» A" and wf: "wf_prog G" obtains "normal s1 ⟹ nrm A ⊆ dom (locals (store s1))" and "⋀ l. ⟦abrupt s1 = Some (Jump (Break l)); normal s0⟧ ⟹ brk A l ⊆ dom (locals (store s1))" and "⟦abrupt s1 = Some (Jump Ret);normal s0⟧ ⟹ Result ∈ dom (locals (store s1))" proof - from eval have "prg ⦇prg=G,cls=C,lcl=L⦈⊢s0 ─t≻→ (v, s1)" by simp moreover note wt da moreover from wf have "wf_prog (prg ⦇prg=G,cls=C,lcl=L⦈)" by simp ultimately show thesis using that by (rule da_good_approxE) iprover+ qed declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]] end