| products/Sources/formale Sprachen/Isabelle/HOL/Bali/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: jedit-changes Sprache: IsabelleUntersuchung Isabelle© |
|
||||||
|
subsection \<open>Correctness of Definite Assignment\<close>
theory DefiniteAssignmentCorrect imports WellForm Eval begin declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]] lemma sxalloc_no_jump: assumes sxalloc: "G\ no_jmp: "abrupt s0 \ shows "abrupt s1 \ using sxalloc no_jmp by cases simp_all lemma sxalloc_no_jump': assumes sxalloc: "G\ 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\ no_jmp: "abrupt s0 \ shows "abrupt s1 \ using halloc no_jmp by cases simp_all lemma halloc_no_jump': assumes halloc: "G\ 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\ jump: "abrupt s0 \ shows "abrupt s1 \ proof (cases "normal s0") case True with eval obtain s0' where eval': "G\ s0: "s0 = Norm s0'" by (cases s0) simp from eval' obtain s2 where s1: "s1 = abupd (absorb Ret) (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> abrupt s2 = Some (Jump (Cont l)) then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" by cases simp show ?thesis proof (cases "\ 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\ "s0 = (Some abr, s0')" by (cases s0) fastforce with this jump show ?thesis by (cases) (simp) qed lemma Methd_no_jump: assumes eval: "G\ jump: "abrupt s0 \ shows "abrupt s1 \ proof (cases "normal s0") case True with eval obtain s0' where "G\ "s0 = Norm s0'" by (cases s0) simp then obtain D' body where "G\ 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\ "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' \ shows "jumpNestingOkS jmps c" proof - have True and True and "\ proof (induct rule: var.induct expr.induct stmt.induct) case (Lab j c jmps' jmps) note jmpOk = \<open>jumpNestingOkS jmps' (j\<bullet> c)\<close> note jmps = \<open>jmps' \<subseteq> jmps\<close> with jmpOk have "jumpNestingOkS ({j} \ moreover from jmps have "({j} \ ultimately have "jumpNestingOkS ({j} \ 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 \<open>jumpNestingOkS jmps' (l\<bullet> While(e) c)\<close> have "jumpNestingOkS ({Cont l} \ moreover from \<open>jmps' \<subseteq> jmps\<close> have "{Cont l} \ ultimately have "jumpNestingOkS ({Cont l} \ 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' \ 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) \ 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 \ 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 \ shows "abrupt (upd val s) \ 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 \ shows "abrupt (upd val s) \ using upd noJmp by (cases s) (simp add: avar_def2 abrupt_if_def) text \<open> 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>\<open>jumpNestingOk\<close> 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>\<open>Lab\<close> and \<^term>\<open>While\<close>. The wellformedness of the program is used to enshure that for all classinitialisations and methods the nesting of jumps is wellformed, too. \<close> theorem jumpNestingOk_eval: assumes eval: "G\ and jmpOk: "jumpNestingOk jmps t" and wt: "Env\ and wf: "wf_prog G" and G: "prg Env = G" and no_jmp: "\ (is "?Jmp jmps s0") shows "(\ (normal s1 \<longrightarrow> (\<forall> w upd. v=In2 (w,upd) \<longrightarrow> (\<forall> s j val. abrupt s \<noteq> Some (Jump j) \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j))))" (is "?Jmp jmps s1 \ proof - let ?HypObj = "\ (\<forall> jmps T Env. ?Jmp jmps s0 \<longrightarrow> jumpNestingOk jmps t \<longrightarrow> Env\<turnstile>t\<Colon>T \< ?Jmp jmps s1 \<and> ?Upd v s1)" \<comment> \<open>Variable \<open>?HypObj\<close> 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.\<close> from eval have "\ \<Longrightarrow> ?Jmp jmps s1 \<and> ?Upd v s1" (is "PROP ?Hyp t s0 s1 v") \<comment> \<open>We need to abstract over \<^term>\<open>jmps\<close> since \<^term>\<open>jmps\<close> during analysis of \<^term>\<open>Lab\<close>. Also we need to abstract over \<^term>\<open>T\<close> and \<^term>\<open>Env\<close> since they are altered in various typing judgements.\<close> 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 = \<open>jumpNestingOk jmps (In1r (jmp\<bullet> c))\<close> note G = \<open>prg Env = G\<close> have wt_c: "Env\ using Lab.prems by (elim wt_elim_cases) { fix j assume ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)" have "j\ proof - from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)" by (cases s1) (simp add: absorb_def) note hyp_c = \<open>PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>\<close> from ab_s1 have "j \ by (cases s1) (simp add: absorb_def) moreover have "j \ proof - from jmpOK have "jumpNestingOk ({jmp} \ 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 = \<open>jumpNestingOk jmps (In1r (c1;; c2))\<close> note G = \<open>prg Env = G\<close> from Comp.prems obtain wt_c1: "Env\ by (elim wt_elim_cases) { fix j assume abr_s2: "abrupt s2 = Some (Jump j)" have "j\ proof - have jmp: "?Jmp jmps s1" proof - note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>\<close> with wt_c1 jmpOk G show ?thesis by simp qed moreover note hyp_c2 = \<open>PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)\<close> have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp moreover note wt_c2 G abr_s2 ultimately show "j \ 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 = \<open>jumpNestingOk jmps (In1r (If(e) c1 Else c2))\<close> note G = \<open>prg Env = G\<close> from If.prems obtain wt_e: "Env\ wt_then_else: "Env\ by (elim wt_elim_cases) simp { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j\ proof - note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close> with wt_e G have "?Jmp jmps s1" by simp moreover note hyp_then_else = \<open>PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>\<close> 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\ 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 = \<open>jumpNestingOk jmps (In1r (l\<bullet> While(e) c))\<close> note G = \<open>prg Env = G\<close> note wt = \<open>Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T\<close> then obtain wt_e: "Env\ wt_c: "Env\ by (elim wt_elim_cases) { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j\ proof - note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close> 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 \ 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 (\ 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} \ by simp moreover from jmp_s1 have "?Jmp ({Cont l} \ ultimately have jmp_s2: "?Jmp ({Cont l} \ 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' \ 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\ (abupd (absorb (Cont l)) s2) s3 (\<diamondsuit>::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\ 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 = \<open>jumpNestingOk jmps (In1r (Throw e))\<close> note G = \<open>prg Env = G\<close> from Throw.prems obtain Te where wt_e: "Env\ by (elim wt_elim_cases) { fix j assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)" have "j\ proof - from \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close> 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 \ qed } thus ?case by simp next case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env) note jmpOk = \<open>jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))\<close> note G = \<open>prg Env = G\<close> from Try.prems obtain wt_c1: "Env\ wt_c2: "Env\ by (elim wt_elim_cases) { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j\ proof - note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)\<close> with jmpOk wt_c1 G have jmp_s1: "?Jmp jmps s1" by simp note s2 = \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close> show "j \ proof (cases "G,s2\ 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 (\ 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\ 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 = \<open>jumpNestingOk jmps (In1r (c1 Finally c2))\<close> note G = \<open>prg Env = G\<close> from Fin.prems obtain wt_c1: "Env\ by (elim wt_elim_cases) { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j \ proof (cases "x1=Some (Jump j)") case True note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>\<close> 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 = \<open>PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>\<close> note \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1) else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close> 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 \<open>jumpNestingOk jmps (In1r (Init C))\<close> note G = \<open>prg Env = G\<close> note \<open>the (class G C) = c\<close> 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\ 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 (\<diamondsuit>::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\ 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 (\ 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: "\ 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\ proof - note \<open>prg Env = G\<close> moreover note hyp_init = \<open>PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>\<close> moreover from wf NewC.prems have "Env\ by (elim wt_elim_cases) (drule is_acc_classD,simp) moreover have "abrupt s1 = Some (Jump j)" proof - from \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close> and jmp show ?t by (rule halloc_no_jump') qed ultimately show "j \ 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\ proof - note G = \<open>prg Env = G\<close> from NewA.prems obtain wt_init: "Env\ wt_size: "Env\ by (elim wt_elim_cases) (auto dest: wt_init_comp_ty') note \<open>PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>\<close> with wt_init G have "?Jmp jmps s1" by (simp add: init_comp_ty_def) moreover note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 i)\<close> have "abrupt s2 = Some (Jump j)" proof - note \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<ri 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\ 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\ proof - note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close> note \<open>prg Env = G\<close> moreover from Cast.prems obtain eT where "Env\ moreover have "abrupt s1 = Some (Jump j)" proof - note \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close> 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\ proof - note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close> note \<open>prg Env = G\<close> moreover from Inst.prems obtain eT where "Env\ moreover note jmp ultimately show "j\ 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\ proof - note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close> note \<open>prg Env = G\<close> moreover from UnOp.prems obtain eT where "Env\ moreover note jmp ultimately show "j\ 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\ proof - note G = \<open>prg Env = G\<close> from BinOp.prems obtain e1T e2T where wt_e1: "Env\ wt_e2: "Env\ by (elim wt_elim_cases) note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)\<close> with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp note hyp_e2 = \<open>PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip) s1 s2 (In1 v2)\<close> show "j\ 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\ proof - note hyp_va = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))\<close> note \<open>prg Env = G\<close> moreover from Acc.prems obtain vT where "Env\ moreover note jmp ultimately show "j\ 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 = \<open>prg Env = G\<close> from Ass.prems obtain vT eT where wt_va: "Env\ wt_e: "Env\ by (elim wt_elim_cases) note hyp_v = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))\<close> note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 v)\<close> { fix j assume jmp: "abrupt (assign f v s2) = Some (Jump j)" have "j\ proof - have "abrupt s2 = Some (Jump j)" proof (cases "normal s2") case True from \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close> and True have nrm_s1: "nor by (rule eval_no_abrupt_lemma [rule_format]) with nrm_s1 wt_va G True have "abrupt (f v s2) \ 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 = \<open>prg Env = G\<close> note hyp_e0 = \<open>PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)\<close> note hyp_e1_e2 = \<open>PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)\<close> from Cond.prems obtain e1T e2T where wt_e0: "Env\ and wt_e1: "Env\ and wt_e2: "Env\ by (elim wt_elim_cases) { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j\ 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 = \<open>prg Env = G\<close> from Call.prems obtain eT argsT where wt_e: "Env\ by (elim wt_elim_cases) { fix j assume jmp: "abrupt ((set_lvars (locals (store s2))) s4) = Some (Jump j)" have "j\ proof - note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close> from wt_e G have jmp_s1: "?Jmp jmps s1" by - (rule hyp_e [THEN conjunct1],simp_all) note hyp_args = \<open>PROP ?Hyp (In3 args) s1 s2 (In3 vs)\<close> have "abrupt s2 = Some (Jump j)" proof - note \<open>G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<right 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 \<open>s3' = check_method_access G accC statT mode \<lparr>name = mn, parTs = pTs\<rparr> a s3\<close> ultimately have "abrupt s3 = Some (Jump j)" by (cases s3) (simp add: check_method_access_def abrupt_if_def Let_def) moreover note \<open>s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2\<close> 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 \<open>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<close> have "G\ by (rule eval.Methd) hence "\ by (rule Methd_no_jump) simp thus ?case by simp next case (Body s0 D s1 c s2 s3 jmps T Env) have "G\ \<rightarrow> abupd (absorb Ret) s3" by (rule eval.Body) (rule Body)+ hence "\ 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 = \<open>prg Env = G\<close> from wf FVar.prems obtain statC f where wt_e: "Env\ accfield: "accfield (prg Env) accC statC fn = Some (statDeclC,f)" by (elim wt_elim_cases) simp have wt_init: "Env\ 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 = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close> { fix j assume jmp: "abrupt s3 = Some (Jump j)" have "j\ proof - note hyp_init = \<open>PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>\<close> from G wt_init have "?Jmp jmps s1" by - (rule hyp_init [THEN conjunct1],auto) moreover note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 a)\<close> have "abrupt s2 = Some (Jump j)" proof - note \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close> 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, use surjective_pairing in blast) { fix j val fix s::state assume "normal s3" assume no_jmp: "abrupt s \ with upd have "abrupt (upd val s) \ 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 = \<open>prg Env = G\<close> from AVar.prems obtain e1T e2T where wt_e1: "Env\ by (elim wt_elim_cases) simp note avar = \<open>(v, s2') = avar G i a s2\<close> { fix j assume jmp: "abrupt s2' = Some (Jump j)" have "j\ proof - note hyp_e1 = \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)\<close> from G wt_e1 have "?Jmp jmps s1" by - (rule hyp_e1 [THEN conjunct1], auto) moreover note hyp_e2 = \<open>PROP ?Hyp (In1l e2) s1 s2 (In1 i)\<close> 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, use surjective_pairing in blast) { fix j val fix s::state assume "normal s2'" assume no_jmp: "abrupt s \ with upd have "abrupt (upd val s) \ 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 = \<open>prg Env = G\<close> from Cons.prems obtain eT esT where wt_e: "Env\ by (elim wt_elim_cases) simp { fix j assume jmp: "abrupt s2 = Some (Jump j)" have "j\ proof - note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close> from G wt_e have "?Jmp jmps s1" by - (rule hyp_e [THEN conjunct1],simp_all) moreover note hyp_es = \<open>PROP ?Hyp (In3 es) s1 s2 (In3 vs)\<close> 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\ jmpOk: "jumpNestingOk {} t" and no_jmp: "abrupt s0 \ wt: "Env\ wf: "wf_prog (prg Env)" shows "abrupt s1 \ (normal s1 \<longrightarrow> v=In2 (w,upd) \<longrightarrow> abrupt s \<noteq> Some (Jump j') \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j'))" proof (cases "\ case True then obtain j' where jmp: "abrupt s0 = Some (Jump j')" .. with no_jmp have "j'\ 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\ moreover note jmpOk wt moreover from G wf have "wf_prog G" by simp moreover note G moreover from False have "\ 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\ no_jmp: "abrupt s0 \ wt: "Env\ wf: "wf_prog (prg Env)" shows "abrupt s1 \ using eval _ no_jmp wt wf by (rule jumpNestingOk_eval_no_jumpE, simp_all) corollary eval_var_no_jump: assumes eval: "prg Env\ no_jmp: "abrupt s0 \ wt: "Env\ wf: "wf_prog (prg Env)" shows "abrupt s1 \ (normal s1 \<longrightarrow> (abrupt s \<noteq> Some (Jump j') \<longrightarrow> abrupt (upd val s) \<noteq> 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\ jmpOk: "jumpNestingOkS {} c" and no_jmp: "abrupt s0 \ wt: "Env\ wf: "wf_prog (prg Env)" shows "abrupt s1 \ 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\ no_jmp: "abrupt s0 \ wt: "Env\ wf: "wf_prog (prg Env)" shows "abrupt s1 \ using eval _ no_jmp wt wf by (rule jumpNestingOk_eval_no_jumpE, simp_all) (* ### FIXME: Do i need this *) lemma union_subseteq_elim [elim]: "\ by blast lemma dom_locals_halloc_mono: assumes halloc: "G\ shows "dom (locals (store s0)) \ proof - from halloc show ?thesis by cases simp_all qed lemma dom_locals_sxalloc_mono: assumes sxalloc: "G\ shows "dom (locals (store s0)) \ 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)) \ shows "dom (locals (store 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)) \<subseteq> 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)) \ by (simp add: lvar_def) blast lemma dom_locals_fvar_vvar_mono: "dom (locals (store s)) \<subseteq> 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)) \<subseteq> 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)) \<subseteq> 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)) \<subseteq> dom (locals (store (snd (avar G i a s))))" by (cases s, simp add: avar_def2) text \<open> 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\<close> lemma dom_locals_eval_mono: assumes eval: "G\ shows "dom (locals (store s0)) \ (\<forall> vv. v=In2 vv \<and> normal s1 \<longrightarrow> (\<forall> s val. dom (locals (store s)) \<subseteq> 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))) \ by simp also from Comp.hyps have "\ 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))) \ by simp also from If.hyps have "\ 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))) \ s1_s2: "dom (locals (store s1)) \ s2_s3: "dom (locals (store s2)) \ 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))) \<subseteq> dom (locals (store s1))" by simp from \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close> have s1_s2: "dom (locals (store s1)) \ by (rule dom_locals_sxalloc_mono) thus ?case proof (cases "G,s2\ case True note s0_s1 also note s1_s2 also from True Try.hyps have "dom (locals (store (new_xcpt_var vn s2))) \<subseteq> dom (locals (store s3))" by simp hence "dom (locals (store s2)) \ 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 "\ case True with Fin.hyps show ?thesis by simp next case False from Fin.hyps have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store (x1, s1)))" by simp hence "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store ((Norm s1)::state)))" by simp also from Fin.hyps have "\ 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)))) \<subseteq> dom (locals (store s1))" and s3: "s3 = (set_lvars (locals (snd s1))) s2" by simp from s0_s1 have "dom (locals (store (Norm s0))) \ by (cases s0) simp with s3 have "dom (locals (store (Norm s0))) \ by (cases s2) simp thus ?thesis by simp qed next case (NewC s0 C s1 a s2) note halloc = \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close> from NewC.hyps have "dom (locals (store ((Norm s0)::state))) \ by simp also from halloc have "\ finally show ?case by simp next case (NewA s0 T s1 e i s2 a s3) note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<suc from NewA.hyps have "dom (locals (store ((Norm s0)::state))) \ by simp also from NewA.hyps have "\ also from halloc have "\ 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))) \ by simp also from BinOp.hyps have "\ 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))) \ by simp show ?case proof (cases "normal s1") case True with Ass.hyps have ass_ok: "\ by simp note s0_s1 also from Ass.hyps have "dom (locals (store s1)) \ by simp also from ass_ok have "\ by (rule dom_locals_assign_mono [where f = f]) finally show ?thesis by simp next case False with \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close> have "s2=s1" by auto with s0_s1 False have "dom (locals (store ((Norm s0)::state))) \<subseteq> 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))) \ by simp also from Cond.hyps have "\ 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 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close> from Call.hyps have "dom (locals (store ((Norm s0)::state))) \ by simp also from Call.hyps have "\ by simp also have "\ 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))) \ by simp also from Body.hyps have "\ by simp also have "\ by simp also have "\ proof - from \<open>s3 = (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> abrupt s2 = Some (Jump (Cont l)) then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)\<close> 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 "\ \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok") by (simp add: dom_locals_fvar_vvar_mono) hence v_ok: "(\ by - (intro strip, simp) note s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close> from FVar.hyps have "dom (locals (store ((Norm s0)::state))) \ by simp also from FVar.hyps have "\ by simp also from s2' have "\ by (simp add: dom_locals_fvar_mono) also from s3 have "\ 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 "\ \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok") by (simp add: dom_locals_avar_vvar_mono) hence v_ok: "(\ by - (intro strip, simp) from AVar.hyps have "dom (locals (store ((Norm s0)::state))) \ by simp also from AVar.hyps have "\ by simp also from s2' have "\ 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))) \ by simp also from Cons.hyps have "\ by simp finally show ?case by simp qed qed lemma dom_locals_eval_mono_elim: assumes eval: "G\ obtains "dom (locals (store s0)) \ "\ \<Longrightarrow> dom (locals (store s)) \<subseteq> 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\ 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\ normal: "normal s1" shows "normal s0" proof - from sxalloc normal show ?thesis by cases simp_all qed lemma union_subseteqI: "\ by blast lemma union_subseteqIl: "\ by blast lemma union_subseteqIr: "\ by blast lemma subseteq_union_transl [trans]: "\ by blast lemma subseteq_union_transr [trans]: "\ by blast lemma union_subseteq_weaken: "\ by blast lemma assigns_good_approx: assumes eval: "G\ normal: "normal s1" shows "assigns t \ proof - from eval normal show ?thesis proof (induct) case Abrupt thus ?case by simp next \<comment> \<open>For statements its trivial, since then \<^term>\<open>assigns t = {}\<close>\<c 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 = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<suc have "assigns (In1l e) \ 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 "\ 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) \ by simp also from Cast.hyps have "\ 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) \ by iprover also have "\ proof - note \<open>G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2 else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)\<close> thus ?thesis by (rule dom_locals_eval_mono_elim) qed finally have s2: "assigns (In1l e1) \ show ?case proof (cases "binop=CondAnd \ case True with s2 show ?thesis by simp next case False with BinOp have "assigns (In1l e2) \ 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 = \<open>normal (assign f v s2)\<close> 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) \ by iprover also from Ass.hyps have "\ by - (erule dom_locals_eval_mono_elim) also from nrm_s2 Ass.hyps have "assigns (In1l e) \ by iprover ultimately have "assigns (In2 va) \ by (rule Un_least) also from Ass.hyps nrm_s1 have "\ by - (erule dom_locals_eval_mono_elim, cases s2,simp) then have "dom (locals (store s2)) \ by (rule dom_locals_assign_mono) finally have va_e: " assigns (In2 va) \ \<subseteq> dom (locals (snd (assign f v s2)))" . show ?case proof (cases "\ 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\ by simp hence "(w,f) = lvar n s0" by (rule eval_elim_cases) simp with nrm_ass_s2 have "n \ 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) \ by iprover also from Cond.hyps have "\ by - (erule dom_locals_eval_mono_elim) finally have e0: "assigns (In1l e0) \ show ?case proof (cases "the_Bool b") case True with Cond have "assigns (In1l e1) \ by simp hence "assigns (In1l e1) \ by blast with e0 have "assigns (In1l e0) \ \<subseteq> dom (locals (store s2))" by (rule Un_least) thus ?thesis using True by simp next case False with Cond --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.49 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
