(* Title: HOL/Bali/AxSound.thy Author: David von Oheimb and Norbert Schirmer *) subsection ‹Soundness proof for Axiomatic semantics of Java expressions and statements › theory AxSound imports AxSem begin subsubsection "validity" definition triple_valid2 :: "prog ⇒ nat ⇒ 'a triple ⇒ bool" ("_⊨_∷_"[61,0, 58] 57) where "G⊨n∷t = (case t of {P} t≻ {Q} ⇒ ∀Y s Z. P Y s Z ⟶ (∀L. s∷≼(G,L) ⟶ (∀T C A. (normal s ⟶ (⦇prg=G,cls=C,lcl=L⦈⊢t∷T ∧ ⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store s))»t»A)) ⟶ (∀Y' s'. G⊢s ─t≻─n→ (Y',s') ⟶ Q Y' s' Z ∧ s'∷≼(G,L)))))" text ‹This definition differs from the ordinary ‹triple_valid_def› manly in the conclusion: We also ensures conformance of the result state. So we don't have to apply the type soundness lemma all the time during induction. This definition is only introduced for the soundness proof of the axiomatic semantics, in the end we will conclude to the ordinary definition. › definition ax_valids2 :: "prog ⇒ 'a triples ⇒ 'a triples ⇒ bool" ("_,_|⊨∷_" [61,58,58] 57) where "G,A|⊨∷ts = (∀n. (∀t∈A. G⊨n∷t) ⟶ (∀t∈ts. G⊨n∷t))" lemma triple_valid2_def2: "G⊨n∷{P} t≻ {Q} = (∀Y s Z. P Y s Z ⟶ (∀Y' s'. G⊢s ─t≻─n→ (Y',s')⟶ (∀L. s∷≼(G,L) ⟶ (∀T C A. (normal s ⟶ (⦇prg=G,cls=C,lcl=L⦈⊢t∷T ∧ ⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store s))»t»A)) ⟶ Q Y' s' Z ∧ s'∷≼(G,L)))))" apply (unfold triple_valid2_def) apply (simp (no_asm) add: split_paired_All) apply blast done lemma triple_valid2_eq [rule_format (no_asm)]: "wf_prog G ==> triple_valid2 G = triple_valid G" apply (rule ext) apply (rule ext) apply (rule triple.induct) apply (simp (no_asm) add: triple_valid_def2 triple_valid2_def2) apply (rule iffI) apply fast apply clarify apply (tactic "smp_tac @{context} 3 1") apply (case_tac "normal s") apply clarsimp apply (elim conjE impE) apply blast apply (tactic "smp_tac @{context} 2 1") apply (drule evaln_eval) apply (drule (1) eval_type_sound [THEN conjunct1],simp, assumption+) apply simp apply clarsimp done lemma ax_valids2_eq: "wf_prog G ⟹ G,A|⊨∷ts = G,A|⊨ts" apply (unfold ax_valids_def ax_valids2_def) apply (force simp add: triple_valid2_eq) done lemma triple_valid2_Suc [rule_format (no_asm)]: "G⊨Suc n∷t ⟶ G⊨n∷t" apply (induct_tac "t") apply (subst triple_valid2_def2) apply (subst triple_valid2_def2) apply (fast intro: evaln_nonstrict_Suc) done lemma Methd_triple_valid2_0: "G⊨0∷{Normal P} Methd C sig-≻ {Q}" by (auto elim!: evaln_elim_cases simp add: triple_valid2_def2) lemma Methd_triple_valid2_SucI: "⟦G⊨n∷{Normal P} body G C sig-≻{Q}⟧ ⟹ G⊨Suc n∷{Normal P} Methd C sig-≻ {Q}" apply (simp (no_asm_use) add: triple_valid2_def2) apply (intro strip, tactic "smp_tac @{context} 3 1", clarify) apply (erule wt_elim_cases, erule da_elim_cases, erule evaln_elim_cases) apply (unfold body_def Let_def) apply (clarsimp simp add: inj_term_simps) apply blast done lemma triples_valid2_Suc: "Ball ts (triple_valid2 G (Suc n)) ⟹ Ball ts (triple_valid2 G n)" apply (fast intro: triple_valid2_Suc) done lemma "G|⊨n:insert t A = (G⊨n:t ∧ G|⊨n:A)" oops subsubsection "soundness" lemma Methd_sound: assumes recursive: "G,A∪ {{P} Methd-≻ {Q} | ms}|⊨∷{{P} body G-≻ {Q} | ms}" shows "G,A|⊨∷{{P} Methd-≻ {Q} | ms}" proof - { fix n assume recursive: "⋀ n. ∀t∈(A ∪ {{P} Methd-≻ {Q} | ms}). G⊨n∷t ⟹ ∀t∈{{P} body G-≻ {Q} | ms}. G⊨n∷t" have "∀t∈A. G⊨n∷t ⟹ ∀t∈{{P} Methd-≻ {Q} | ms}. G⊨n∷t" proof (induct n) case 0 show "∀t∈{{P} Methd-≻ {Q} | ms}. G⊨0∷t" proof - { fix C sig assume "(C,sig) ∈ ms" have "G⊨0∷{Normal (P C sig)} Methd C sig-≻ {Q C sig}" by (rule Methd_triple_valid2_0) } thus ?thesis by (simp add: mtriples_def split_def) qed next case (Suc m) note hyp = ‹∀t∈A. G⊨m∷t ⟹ ∀t∈{{P} Methd-≻ {Q} | ms}. G⊨m∷t› note prem = ‹∀t∈A. G⊨Suc m∷t› show "∀t∈{{P} Methd-≻ {Q} | ms}. G⊨Suc m∷t" proof - { fix C sig assume m: "(C,sig) ∈ ms" have "G⊨Suc m∷{Normal (P C sig)} Methd C sig-≻ {Q C sig}" proof - from prem have prem_m: "∀t∈A. G⊨m∷t" by (rule triples_valid2_Suc) hence "∀t∈{{P} Methd-≻ {Q} | ms}. G⊨m∷t" by (rule hyp) with prem_m have "∀t∈(A ∪ {{P} Methd-≻ {Q} | ms}). G⊨m∷t" by (simp add: ball_Un) hence "∀t∈{{P} body G-≻ {Q} | ms}. G⊨m∷t" by (rule recursive) with m have "G⊨m∷{Normal (P C sig)} body G C sig-≻ {Q C sig}" by (auto simp add: mtriples_def split_def) thus ?thesis by (rule Methd_triple_valid2_SucI) qed } thus ?thesis by (simp add: mtriples_def split_def) qed qed } with recursive show ?thesis by (unfold ax_valids2_def) blast qed lemma valids2_inductI: "∀s t n Y' s'. G⊢s─t≻─n→ (Y',s') ⟶ t = c ⟶ Ball A (triple_valid2 G n) ⟶ (∀Y Z. P Y s Z ⟶ (∀L. s∷≼(G,L) ⟶ (∀T C A. (normal s ⟶ (⦇prg=G,cls=C,lcl=L⦈⊢t∷T) ∧ ⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store s))»t»A) ⟶ Q Y' s' Z ∧ s'∷≼(G, L)))) ⟹ G,A|⊨∷{ {P} c≻ {Q}}" apply (simp (no_asm) add: ax_valids2_def triple_valid2_def2) apply clarsimp done lemma da_good_approx_evalnE [consumes 4]: assumes evaln: "G⊢s0 ─t≻─n→ (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" and elim: "⟦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)) ⟧ ⟹ P" shows "P" proof - from evaln have "G⊢s0 ─t≻→ (v, s1)" by (rule evaln_eval) from this wt da wf elim show P by (rule da_good_approxE') iprover+ qed lemma validI: assumes I: "⋀ n s0 L accC T C v s1 Y Z. ⟦∀t∈A. G⊨n∷t; s0∷≼(G,L); normal s0 ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢t∷T; normal s0 ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»t»C; G⊢s0 ─t≻─n→ (v,s1); P Y s0 Z⟧ ⟹ Q v s1 Z ∧ s1∷≼(G,L)" shows "G,A|⊨∷{ {P} t≻ {Q} }" apply (simp add: ax_valids2_def triple_valid2_def2) apply (intro allI impI) apply (case_tac "normal s") apply clarsimp apply (rule I,(assumption|simp)+) apply (rule I,auto) done declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]] lemma valid_stmtI: assumes I: "⋀ n s0 L accC C s1 Y Z. ⟦∀t∈A. G⊨n∷t; s0∷≼(G,L); normal s0⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢c∷√; normal s0⟹⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨c⟩⇩_{s}»C; G⊢s0 ─c─n→ s1; P Y s0 Z⟧ ⟹ Q ♢ s1 Z ∧ s1∷≼(G,L)" shows "G,A|⊨∷{ {P} ⟨c⟩⇩_{s}≻ {Q} }" apply (simp add: ax_valids2_def triple_valid2_def2) apply (intro allI impI) apply (case_tac "normal s") apply clarsimp apply (rule I,(assumption|simp)+) apply (rule I,auto) done lemma valid_stmt_NormalI: assumes I: "⋀ n s0 L accC C s1 Y Z. ⟦∀t∈A. G⊨n∷t; s0∷≼(G,L); normal s0; ⦇prg=G,cls=accC,lcl=L⦈⊢c∷√; ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨c⟩⇩_{s}»C; G⊢s0 ─c─n→ s1; (Normal P) Y s0 Z⟧ ⟹ Q ♢ s1 Z ∧ s1∷≼(G,L)" shows "G,A|⊨∷{ {Normal P} ⟨c⟩⇩_{s}≻ {Q} }" apply (simp add: ax_valids2_def triple_valid2_def2) apply (intro allI impI) apply (elim exE conjE) apply (rule I) by auto lemma valid_var_NormalI: assumes I: "⋀ n s0 L accC T C vf s1 Y Z. ⟦∀t∈A. G⊨n∷t; s0∷≼(G,L); normal s0; ⦇prg=G,cls=accC,lcl=L⦈⊢t∷=T; ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨t⟩⇩_{v}»C; G⊢s0 ─t=≻vf─n→ s1; (Normal P) Y s0 Z⟧ ⟹ Q (In2 vf) s1 Z ∧ s1∷≼(G,L)" shows "G,A|⊨∷{ {Normal P} ⟨t⟩⇩_{v}≻ {Q} }" apply (simp add: ax_valids2_def triple_valid2_def2) apply (intro allI impI) apply (elim exE conjE) apply simp apply (rule I) by auto lemma valid_expr_NormalI: assumes I: "⋀ n s0 L accC T C v s1 Y Z. ⟦∀t∈A. G⊨n∷t; s0∷≼(G,L); normal s0; ⦇prg=G,cls=accC,lcl=L⦈⊢t∷-T; ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨t⟩⇩_{e}»C; G⊢s0 ─t-≻v─n→ s1; (Normal P) Y s0 Z⟧ ⟹ Q (In1 v) s1 Z ∧ s1∷≼(G,L)" shows "G,A|⊨∷{ {Normal P} ⟨t⟩⇩_{e}≻ {Q} }" apply (simp add: ax_valids2_def triple_valid2_def2) apply (intro allI impI) apply (elim exE conjE) apply simp apply (rule I) by auto lemma valid_expr_list_NormalI: assumes I: "⋀ n s0 L accC T C vs s1 Y Z. ⟦∀t∈A. G⊨n∷t; s0∷≼(G,L); normal s0; ⦇prg=G,cls=accC,lcl=L⦈⊢t∷≐T; ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨t⟩⇩_{l}»C; G⊢s0 ─t≐≻vs─n→ s1; (Normal P) Y s0 Z⟧ ⟹ Q (In3 vs) s1 Z ∧ s1∷≼(G,L)" shows "G,A|⊨∷{ {Normal P} ⟨t⟩⇩_{l}≻ {Q} }" apply (simp add: ax_valids2_def triple_valid2_def2) apply (intro allI impI) apply (elim exE conjE) apply simp apply (rule I) by auto lemma validE [consumes 5]: assumes valid: "G,A|⊨∷{ {P} t≻ {Q} }" and P: "P Y s0 Z" and valid_A: "∀t∈A. G⊨n∷t" and conf: "s0∷≼(G,L)" and eval: "G⊢s0 ─t≻─n→ (v,s1)" and wt: "normal s0 ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢t∷T" and da: "normal s0 ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»t»C" and elim: "⟦Q v s1 Z; s1∷≼(G,L)⟧ ⟹ concl" shows concl using assms by (simp add: ax_valids2_def triple_valid2_def2) fast (* why consumes 5?. If I want to apply this lemma in a context wgere ¬ normal s0 holds, I can chain "¬ normal s0" as fact number 6 and apply the rule with cases. Auto will then solve premise 6 and 7. *) lemma all_empty: "(∀x. P) = P" by simp corollary evaln_type_sound: assumes evaln: "G⊢s0 ─t≻─n→ (v,s1)" and wt: "⦇prg=G,cls=accC,lcl=L⦈⊢t∷T" and da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »t» A" and conf_s0: "s0∷≼(G,L)" and wf: "wf_prog G" shows "s1∷≼(G,L) ∧ (normal s1 ⟶ G,L,store s1⊢t≻v∷≼T) ∧ (error_free s0 = error_free s1)" proof - from evaln have "G⊢s0 ─t≻→ (v,s1)" by (rule evaln_eval) from this wt da wf conf_s0 show ?thesis by (rule eval_type_sound) qed corollary dom_locals_evaln_mono_elim [consumes 1]: assumes evaln: "G⊢ s0 ─t≻─n→ (v,s1)" and hyps: "⟦dom (locals (store s0)) ⊆ dom (locals (store s1)); ⋀ vv s val. ⟦v=In2 vv; normal s1⟧ ⟹ dom (locals (store s)) ⊆ dom (locals (store ((snd vv) val s)))⟧ ⟹ P" shows "P" proof - from evaln have "G⊢ s0 ─t≻→ (v,s1)" by (rule evaln_eval) from this hyps show ?thesis by (rule dom_locals_eval_mono_elim) iprover+ qed lemma evaln_no_abrupt: "⋀s s'. ⟦G⊢s ─t≻─n→ (w,s'); normal s'⟧ ⟹ normal s" by (erule evaln_cases,auto) declare inj_term_simps [simp] lemma ax_sound2: assumes wf: "wf_prog G" and deriv: "G,A|⊢ts" shows "G,A|⊨∷ts" using deriv proof (induct) case (empty A) show ?case by (simp add: ax_valids2_def triple_valid2_def2) next case (insert A t ts) note valid_t = ‹G,A|⊨∷{t}› moreover note valid_ts = ‹G,A|⊨∷ts› { fix n assume valid_A: "∀t∈A. G⊨n∷t" have "G⊨n∷t" and "∀t∈ts. G⊨n∷t" proof - from valid_A valid_t show "G⊨n∷t" by (simp add: ax_valids2_def) next from valid_A valid_ts show "∀t∈ts. G⊨n∷t" by (unfold ax_valids2_def) blast qed hence "∀t'∈insert t ts. G⊨n∷t'" by simp } thus ?case by (unfold ax_valids2_def) blast next case (asm ts A) from ‹ts ⊆ A› show "G,A|⊨∷ts" by (auto simp add: ax_valids2_def triple_valid2_def) next case (weaken A ts' ts) note ‹G,A|⊨∷ts'› moreover note ‹ts ⊆ ts'› ultimately show "G,A|⊨∷ts" by (unfold ax_valids2_def triple_valid2_def) blast next case (conseq P A t Q) note con = ‹∀Y s Z. P Y s Z ⟶ (∃P' Q'. (G,A⊢{P'} t≻ {Q'} ∧ G,A|⊨∷{ {P'} t≻ {Q'} }) ∧ (∀Y' s'. (∀Y Z'. P' Y s Z' ⟶ Q' Y' s' Z') ⟶ Q Y' s' Z))› show "G,A|⊨∷{ {P} t≻ {Q} }" proof (rule validI) fix n s0 L accC T C v s1 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf: "s0∷≼(G,L)" assume wt: "normal s0 ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢t∷T" assume da: "normal s0 ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »t» C" assume eval: "G⊢s0 ─t≻─n→ (v, s1)" assume P: "P Y s0 Z" show "Q v s1 Z ∧ s1∷≼(G, L)" proof - from valid_A conf wt da eval P con have "Q v s1 Z" apply (simp add: ax_valids2_def triple_valid2_def2) apply (tactic "smp_tac @{context} 3 1") apply clarify apply (tactic "smp_tac @{context} 1 1") apply (erule allE,erule allE, erule mp) apply (intro strip) apply (tactic "smp_tac @{context} 3 1") apply (tactic "smp_tac @{context} 2 1") apply (tactic "smp_tac @{context} 1 1") by blast moreover have "s1∷≼(G, L)" proof (cases "normal s0") case True from eval wt [OF True] da [OF True] conf wf show ?thesis by (rule evaln_type_sound [elim_format]) simp next case False with eval have "s1=s0" by auto with conf show ?thesis by simp qed ultimately show ?thesis .. qed qed next case (hazard A P t Q) show "G,A|⊨∷{ {P ∧. Not ∘ type_ok G t} t≻ {Q} }" by (simp add: ax_valids2_def triple_valid2_def2 type_ok_def) fast next case (Abrupt A P t) show "G,A|⊨∷{ {P←undefined3 t ∧. Not ∘ normal} t≻ {P} }" proof (rule validI) fix n s0 L accC T C v s1 Y Z assume conf_s0: "s0∷≼(G, L)" assume eval: "G⊢s0 ─t≻─n→ (v, s1)" assume "(P←undefined3 t ∧. Not ∘ normal) Y s0 Z" then obtain P: "P (undefined3 t) s0 Z" and abrupt_s0: "¬ normal s0" by simp from eval abrupt_s0 obtain "s1=s0" and "v=undefined3 t" by auto with P conf_s0 show "P v s1 Z ∧ s1∷≼(G, L)" by simp qed next case (LVar A P vn) show "G,A|⊨∷{ {Normal (λs.. P←In2 (lvar vn s))} LVar vn=≻ {P} }" proof (rule valid_var_NormalI) fix n s0 L accC T C vf s1 Y Z assume conf_s0: "s0∷≼(G, L)" assume normal_s0: "normal s0" assume wt: "⦇prg = G, cls = accC, lcl = L⦈⊢LVar vn∷=T" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨LVar vn⟩⇩_{v}» C" assume eval: "G⊢s0 ─LVar vn=≻vf─n→ s1" assume P: "(Normal (λs.. P←In2 (lvar vn s))) Y s0 Z" show "P (In2 vf) s1 Z ∧ s1∷≼(G, L)" proof from eval normal_s0 obtain "s1=s0" "vf=lvar vn (store s0)" by (fastforce elim: evaln_elim_cases) with P show "P (In2 vf) s1 Z" by simp next from eval wt da conf_s0 wf show "s1∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp qed qed next case (FVar A P statDeclC Q e stat fn R accC) note valid_init = ‹G,A|⊨∷{ {Normal P} .Init statDeclC. {Q} }› note valid_e = ‹G,A|⊨∷{ {Q} e-≻ {λVal:a:. fvar statDeclC stat fn a ..; R} }› show "G,A|⊨∷{ {Normal P} {accC,statDeclC,stat}e..fn=≻ {R} }" proof (rule valid_var_NormalI) fix n s0 L accC' T V vf s3 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC',lcl=L⦈⊢{accC,statDeclC,stat}e..fn∷=T" assume da: "⦇prg=G,cls=accC',lcl=L⦈ ⊢ dom (locals (store s0)) »⟨{accC,statDeclC,stat}e..fn⟩⇩_{v}» V" assume eval: "G⊢s0 ─{accC,statDeclC,stat}e..fn=≻vf─n→ s3" assume P: "(Normal P) Y s0 Z" show "R ⌊vf⌋⇩_{v}s3 Z ∧ s3∷≼(G, L)" proof - from wt obtain statC f where wt_e: "⦇prg=G, cls=accC, lcl=L⦈⊢e∷-Class statC" and accfield: "accfield G accC statC fn = Some (statDeclC,f)" and eq_accC: "accC=accC'" and stat: "stat=is_static f" and T: "T=(type f)" by (cases) (auto simp add: member_is_static_simp) from da eq_accC have da_e: "⦇prg=G, cls=accC, lcl=L⦈⊢dom (locals (store s0))»⟨e⟩⇩_{e}» V" by cases simp from eval obtain a s1 s2 s2' where eval_init: "G⊢s0 ─Init statDeclC─n→ s1" and eval_e: "G⊢s1 ─e-≻a─n→ s2" and fvar: "(vf,s2')=fvar statDeclC stat fn a s2" and s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" using normal_s0 by (fastforce elim: evaln_elim_cases) have wt_init: "⦇prg=G, cls=accC, lcl=L⦈⊢(Init statDeclC)∷√" proof - from wf wt_e have iscls_statC: "is_class G statC" by (auto dest: ty_expr_is_type type_is_class) with wf accfield have iscls_statDeclC: "is_class G statDeclC" by (auto dest!: accfield_fields dest: fields_declC) thus ?thesis by simp qed obtain I where da_init: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨Init statDeclC⟩⇩_{s}» I" by (auto intro: da_Init [simplified] assigned.select_convs) from valid_init P valid_A conf_s0 eval_init wt_init da_init obtain Q: "Q ♢ s1 Z" and conf_s1: "s1∷≼(G, L)" by (rule validE) obtain R: "R ⌊vf⌋⇩_{v}s2' Z" and conf_s2: "s2∷≼(G, L)" and conf_a: "normal s2 ⟶ G,store s2⊢a∷≼Class statC" proof (cases "normal s1") case True obtain V' where da_e': "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s1))»⟨e⟩⇩_{e}» V'" proof - from eval_init have "(dom (locals (store s0))) ⊆ (dom (locals (store s1)))" by (rule dom_locals_evaln_mono_elim) with da_e show thesis by (rule da_weakenE) (rule that) qed with valid_e Q valid_A conf_s1 eval_e wt_e obtain "R ⌊vf⌋⇩_{v}s2' Z" and "s2∷≼(G, L)" by (rule validE) (simp add: fvar [symmetric]) moreover from eval_e wt_e da_e' conf_s1 wf have "normal s2 ⟶ G,store s2⊢a∷≼Class statC" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. next case False with valid_e Q valid_A conf_s1 eval_e obtain "R ⌊vf⌋⇩_{v}s2' Z" and "s2∷≼(G, L)" by (cases rule: validE) (simp add: fvar [symmetric])+ moreover from False eval_e have "¬ normal s2" by auto hence "normal s2 ⟶ G,store s2⊢a∷≼Class statC" by auto ultimately show ?thesis .. qed from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat s3 wf have eq_s3_s2': "s3=s2'" using normal_s0 by (auto dest!: error_free_field_access evaln_eval) moreover from eval wt da conf_s0 wf have "s3∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis using Q R by simp qed qed next case (AVar A P e1 Q e2 R) note valid_e1 = ‹G,A|⊨∷{ {Normal P} e1-≻ {Q} }› have valid_e2: "⋀ a. G,A|⊨∷{ {Q←In1 a} e2-≻ {λVal:i:. avar G i a ..; R} }" using AVar.hyps by simp show "G,A|⊨∷{ {Normal P} e1.[e2]=≻ {R} }" proof (rule valid_var_NormalI) fix n s0 L accC T V vf s2' Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢e1.[e2]∷=T" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨e1.[e2]⟩⇩_{v}» V" assume eval: "G⊢s0 ─e1.[e2]=≻vf─n→ s2'" assume P: "(Normal P) Y s0 Z" show "R ⌊vf⌋⇩_{v}s2' Z ∧ s2'∷≼(G, L)" proof - from wt obtain wt_e1: "⦇prg=G,cls=accC,lcl=L⦈⊢e1∷-T.[]" and wt_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢e2∷-PrimT Integer" by (rule wt_elim_cases) simp from da obtain E1 where da_e1: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0))»⟨e1⟩⇩_{e}» E1" and da_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢ nrm E1 »⟨e2⟩⇩_{e}» V" by (rule da_elim_cases) simp from eval obtain s1 a i s2 where eval_e1: "G⊢s0 ─e1-≻a─n→ s1" and eval_e2: "G⊢s1 ─e2-≻i─n→ s2" and avar: "avar G i a s2 =(vf, s2')" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_e1 P valid_A conf_s0 eval_e1 wt_e1 da_e1 obtain Q: "Q ⌊a⌋⇩_{e}s1 Z" and conf_s1: "s1∷≼(G, L)" by (rule validE) from Q have Q': "⋀ v. (Q←In1 a) v s1 Z" by simp have "R ⌊vf⌋⇩_{v}s2' Z" proof (cases "normal s1") case True obtain V' where "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s1))»⟨e2⟩⇩_{e}» V'" proof - from eval_e1 wt_e1 da_e1 wf True have "nrm E1 ⊆ dom (locals (store s1))" by (cases rule: da_good_approx_evalnE) iprover with da_e2 show thesis by (rule da_weakenE) (rule that) qed with valid_e2 Q' valid_A conf_s1 eval_e2 wt_e2 show ?thesis by (rule validE) (simp add: avar) next case False with valid_e2 Q' valid_A conf_s1 eval_e2 show ?thesis by (cases rule: validE) (simp add: avar)+ qed moreover from eval wt da conf_s0 wf have "s2'∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (NewC A P C Q) note valid_init = ‹G,A|⊨∷{ {Normal P} .Init C. {Alloc G (CInst C) Q} }› show "G,A|⊨∷{ {Normal P} NewC C-≻ {Q} }" proof (rule valid_expr_NormalI) fix n s0 L accC T E v s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢NewC C∷-T" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨NewC C⟩⇩_{e}» E" assume eval: "G⊢s0 ─NewC C-≻v─n→ s2" assume P: "(Normal P) Y s0 Z" show "Q ⌊v⌋⇩_{e}s2 Z ∧ s2∷≼(G, L)" proof - from wt obtain is_cls_C: "is_class G C" by (rule wt_elim_cases) (auto dest: is_acc_classD) hence wt_init: "⦇prg=G, cls=accC, lcl=L⦈⊢Init C∷√" by auto obtain I where da_init: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨Init C⟩⇩_{s}» I" by (auto intro: da_Init [simplified] assigned.select_convs) from eval obtain s1 a where eval_init: "G⊢s0 ─Init C─n→ s1" and alloc: "G⊢s1 ─halloc CInst C≻a→ s2" and v: "v=Addr a" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_init P valid_A conf_s0 eval_init wt_init da_init obtain "(Alloc G (CInst C) Q) ♢ s1 Z" by (rule validE) with alloc v have "Q ⌊v⌋⇩_{e}s2 Z" by simp moreover from eval wt da conf_s0 wf have "s2∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (NewA A P T Q e R) note valid_init = ‹G,A|⊨∷{ {Normal P} .init_comp_ty T. {Q} }› note valid_e = ‹G,A|⊨∷{ {Q} e-≻ {λVal:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}}› show "G,A|⊨∷{ {Normal P} New T[e]-≻ {R} }" proof (rule valid_expr_NormalI) fix n s0 L accC arrT E v s3 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢New T[e]∷-arrT" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »⟨New T[e]⟩⇩_{e}» E" assume eval: "G⊢s0 ─New T[e]-≻v─n→ s3" assume P: "(Normal P) Y s0 Z" show "R ⌊v⌋⇩_{e}s3 Z ∧ s3∷≼(G, L)" proof - from wt obtain wt_init: "⦇prg=G,cls=accC,lcl=L⦈⊢init_comp_ty T∷√" and wt_e: "⦇prg=G,cls=accC,lcl=L⦈⊢e∷-PrimT Integer" by (rule wt_elim_cases) (auto intro: wt_init_comp_ty ) from da obtain da_e:"⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨e⟩⇩_{e}» E" by cases simp from eval obtain s1 i s2 a where eval_init: "G⊢s0 ─init_comp_ty T─n→ s1" and eval_e: "G⊢s1 ─e-≻i─n→ s2" and alloc: "G⊢abupd (check_neg i) s2 ─halloc Arr T (the_Intg i)≻a→ s3" and v: "v=Addr a" using normal_s0 by (fastforce elim: evaln_elim_cases) obtain I where da_init: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »⟨init_comp_ty T⟩⇩_{s}» I" proof (cases "∃C. T = Class C") case True thus ?thesis by - (rule that, (auto intro: da_Init [simplified] assigned.select_convs simp add: init_comp_ty_def)) (* simplified: to rewrite ⟨Init C⟩ to In1r (Init C) *) next case False thus ?thesis by - (rule that, (auto intro: da_Skip [simplified] assigned.select_convs simp add: init_comp_ty_def)) (* simplified: to rewrite ⟨Skip⟩ to In1r (Skip) *) qed with valid_init P valid_A conf_s0 eval_init wt_init obtain Q: "Q ♢ s1 Z" and conf_s1: "s1∷≼(G, L)" by (rule validE) obtain E' where "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »⟨e⟩⇩_{e}» E'" proof - from eval_init have "dom (locals (store s0)) ⊆ dom (locals (store s1))" by (rule dom_locals_evaln_mono_elim) with da_e show thesis by (rule da_weakenE) (rule that) qed with valid_e Q valid_A conf_s1 eval_e wt_e have "(λVal:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R) ⌊i⌋⇩_{e}s2 Z" by (rule validE) with alloc v have "R ⌊v⌋⇩_{e}s3 Z" by simp moreover from eval wt da conf_s0 wf have "s3∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Cast A P e T Q) note valid_e = ‹G,A|⊨∷{ {Normal P} e-≻ {λVal:v:. λs.. abupd (raise_if (¬ G,s⊢v fits T) ClassCast) .; Q←In1 v} }› show "G,A|⊨∷{ {Normal P} Cast T e-≻ {Q} }" proof (rule valid_expr_NormalI) fix n s0 L accC castT E v s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Cast T e∷-castT" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »⟨Cast T e⟩⇩_{e}» E" assume eval: "G⊢s0 ─Cast T e-≻v─n→ s2" assume P: "(Normal P) Y s0 Z" show "Q ⌊v⌋⇩_{e}s2 Z ∧ s2∷≼(G, L)" proof - from wt obtain eT where wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT" by cases simp from da obtain da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨e⟩⇩_{e}» E" by cases simp from eval obtain s1 where eval_e: "G⊢s0 ─e-≻v─n→ s1" and s2: "s2 = abupd (raise_if (¬ G,snd s1⊢v fits T) ClassCast) s1" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_e P valid_A conf_s0 eval_e wt_e da_e have "(λVal:v:. λs.. abupd (raise_if (¬ G,s⊢v fits T) ClassCast) .; Q←In1 v) ⌊v⌋⇩_{e}s1 Z" by (rule validE) with s2 have "Q ⌊v⌋⇩_{e}s2 Z" by simp moreover from eval wt da conf_s0 wf have "s2∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Inst A P e Q T) assume valid_e: "G,A|⊨∷{ {Normal P} e-≻ {λVal:v:. λs.. Q←In1 (Bool (v ≠ Null ∧ G,s⊢v fits RefT T))} }" show "G,A|⊨∷{ {Normal P} e InstOf T-≻ {Q} }" proof (rule valid_expr_NormalI) fix n s0 L accC instT E v s1 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢e InstOf T∷-instT" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨e InstOf T⟩⇩_{e}» E" assume eval: "G⊢s0 ─e InstOf T-≻v─n→ s1" assume P: "(Normal P) Y s0 Z" show "Q ⌊v⌋⇩_{e}s1 Z ∧ s1∷≼(G, L)" proof - from wt obtain eT where wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT" by cases simp from da obtain da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨e⟩⇩_{e}» E" by cases simp from eval obtain a where eval_e: "G⊢s0 ─e-≻a─n→ s1" and v: "v = Bool (a ≠ Null ∧ G,store s1⊢a fits RefT T)" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_e P valid_A conf_s0 eval_e wt_e da_e have "(λVal:v:. λs.. Q←In1 (Bool (v ≠ Null ∧ G,s⊢v fits RefT T))) ⌊a⌋⇩_{e}s1 Z" by (rule validE) with v have "Q ⌊v⌋⇩_{e}s1 Z" by simp moreover from eval wt da conf_s0 wf have "s1∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Lit A P v) show "G,A|⊨∷{ {Normal (P←In1 v)} Lit v-≻ {P} }" proof (rule valid_expr_NormalI) fix n L s0 s1 v' Y Z assume conf_s0: "s0∷≼(G, L)" assume normal_s0: " normal s0" assume eval: "G⊢s0 ─Lit v-≻v'─n→ s1" assume P: "(Normal (P←In1 v)) Y s0 Z" show "P ⌊v'⌋⇩_{e}s1 Z ∧ s1∷≼(G, L)" proof - from eval have "s1=s0" and "v'=v" using normal_s0 by (auto elim: evaln_elim_cases) with P conf_s0 show ?thesis by simp qed qed next case (UnOp A P e Q unop) assume valid_e: "G,A|⊨∷{ {Normal P}e-≻{λVal:v:. Q←In1 (eval_unop unop v)} }" show "G,A|⊨∷{ {Normal P} UnOp unop e-≻ {Q} }" proof (rule valid_expr_NormalI) fix n s0 L accC T E v s1 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢UnOp unop e∷-T" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨UnOp unop e⟩⇩_{e}»E" assume eval: "G⊢s0 ─UnOp unop e-≻v─n→ s1" assume P: "(Normal P) Y s0 Z" show "Q ⌊v⌋⇩_{e}s1 Z ∧ s1∷≼(G, L)" proof - from wt obtain eT where wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT" by cases simp from da obtain da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨e⟩⇩_{e}» E" by cases simp from eval obtain ve where eval_e: "G⊢s0 ─e-≻ve─n→ s1" and v: "v = eval_unop unop ve" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_e P valid_A conf_s0 eval_e wt_e da_e have "(λVal:v:. Q←In1 (eval_unop unop v)) ⌊ve⌋⇩_{e}s1 Z" by (rule validE) with v have "Q ⌊v⌋⇩_{e}s1 Z" by simp moreover from eval wt da conf_s0 wf have "s1∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (BinOp A P e1 Q binop e2 R) assume valid_e1: "G,A|⊨∷{ {Normal P} e1-≻ {Q} }" have valid_e2: "⋀ v1. G,A|⊨∷{ {Q←In1 v1} (if need_second_arg binop v1 then In1l e2 else In1r Skip)≻ {λVal:v2:. R←In1 (eval_binop binop v1 v2)} }" using BinOp.hyps by simp show "G,A|⊨∷{ {Normal P} BinOp binop e1 e2-≻ {R} }" proof (rule valid_expr_NormalI) fix n s0 L accC T E v s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢BinOp binop e1 e2∷-T" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0)) »⟨BinOp binop e1 e2⟩⇩_{e}» E" assume eval: "G⊢s0 ─BinOp binop e1 e2-≻v─n→ s2" assume P: "(Normal P) Y s0 Z" show "R ⌊v⌋⇩_{e}s2 Z ∧ s2∷≼(G, L)" proof - from wt obtain e1T e2T where wt_e1: "⦇prg=G,cls=accC,lcl=L⦈⊢e1∷-e1T" and wt_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢e2∷-e2T" and wt_binop: "wt_binop G binop e1T e2T" by cases simp have wt_Skip: "⦇prg = G, cls = accC, lcl = L⦈⊢Skip∷√" by simp (* obtain S where daSkip: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s1)) »In1r Skip» S" by (auto intro: da_Skip [simplified] assigned.select_convs) *) from da obtain E1 where da_e1: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨e1⟩⇩_{e}» E1" by cases simp+ from eval obtain v1 s1 v2 where eval_e1: "G⊢s0 ─e1-≻v1─n→ s1" and eval_e2: "G⊢s1 ─(if need_second_arg binop v1 then ⟨e2⟩⇩_{e}else ⟨Skip⟩⇩_{s}) ≻─n→ (⌊v2⌋⇩_{e}, s2)" and v: "v=eval_binop binop v1 v2" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_e1 P valid_A conf_s0 eval_e1 wt_e1 da_e1 obtain Q: "Q ⌊v1⌋⇩_{e}s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) from Q have Q': "⋀ v. (Q←In1 v1) v s1 Z" by simp have "(λVal:v2:. R←In1 (eval_binop binop v1 v2)) ⌊v2⌋⇩_{e}s2 Z" proof (cases "normal s1") case True from eval_e1 wt_e1 da_e1 conf_s0 wf have conf_v1: "G,store s1⊢v1∷≼e1T" by (rule evaln_type_sound [elim_format]) (insert True,simp) from eval_e1 have "G⊢s0 ─e1-≻v1→ s1" by (rule evaln_eval) from da wt_e1 wt_e2 wt_binop conf_s0 True this conf_v1 wf obtain E2 where da_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »(if need_second_arg binop v1 then ⟨e2⟩⇩_{e}else ⟨Skip⟩⇩_{s})» E2" by (rule da_e2_BinOp [elim_format]) iprover from wt_e2 wt_Skip obtain T2 where "⦇prg=G,cls=accC,lcl=L⦈ ⊢(if need_second_arg binop v1 then ⟨e2⟩⇩_{e}else ⟨Skip⟩⇩_{s})∷T2" by (cases "need_second_arg binop v1") auto note ve=validE [OF valid_e2,OF Q' valid_A conf_s1 eval_e2 this da_e2] (* chaining Q', without extra OF causes unification error *) thus ?thesis by (rule ve) next case False note ve=validE [OF valid_e2,OF Q' valid_A conf_s1 eval_e2] with False show ?thesis by iprover qed with v have "R ⌊v⌋⇩_{e}s2 Z" by simp moreover from eval wt da conf_s0 wf have "s2∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Super A P) show "G,A|⊨∷{ {Normal (λs.. P←In1 (val_this s))} Super-≻ {P} }" proof (rule valid_expr_NormalI) fix n L s0 s1 v Y Z assume conf_s0: "s0∷≼(G, L)" assume normal_s0: " normal s0" assume eval: "G⊢s0 ─Super-≻v─n→ s1" assume P: "(Normal (λs.. P←In1 (val_this s))) Y s0 Z" show "P ⌊v⌋⇩_{e}s1 Z ∧ s1∷≼(G, L)" proof - from eval have "s1=s0" and "v=val_this (store s0)" using normal_s0 by (auto elim: evaln_elim_cases) with P conf_s0 show ?thesis by simp qed qed next case (Acc A P var Q) note valid_var = ‹G,A|⊨∷{ {Normal P} var=≻ {λVar:(v, f):. Q←In1 v} }› show "G,A|⊨∷{ {Normal P} Acc var-≻ {Q} }" proof (rule valid_expr_NormalI) fix n s0 L accC T E v s1 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Acc var∷-T" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨Acc var⟩⇩_{e}»E" assume eval: "G⊢s0 ─Acc var-≻v─n→ s1" assume P: "(Normal P) Y s0 Z" show "Q ⌊v⌋⇩_{e}s1 Z ∧ s1∷≼(G, L)" proof - from wt obtain wt_var: "⦇prg=G,cls=accC,lcl=L⦈⊢var∷=T" by cases simp from da obtain V where da_var: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨var⟩⇩_{v}» V" by (cases "∃ n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases) from eval obtain upd where eval_var: "G⊢s0 ─var=≻(v, upd)─n→ s1" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_var P valid_A conf_s0 eval_var wt_var da_var have "(λVar:(v, f):. Q←In1 v) ⌊(v, upd)⌋⇩_{v}s1 Z" by (rule validE) then have "Q ⌊v⌋⇩_{e}s1 Z" by simp moreover from eval wt da conf_s0 wf have "s1∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Ass A P var Q e R) note valid_var = ‹G,A|⊨∷{ {Normal P} var=≻ {Q} }› have valid_e: "⋀ vf. G,A|⊨∷{ {Q←In2 vf} e-≻ {λVal:v:. assign (snd vf) v .; R} }" using Ass.hyps by simp show "G,A|⊨∷{ {Normal P} var:=e-≻ {R} }" proof (rule valid_expr_NormalI) fix n s0 L accC T E v s3 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢var:=e∷-T" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨var:=e⟩⇩_{e}»E" assume eval: "G⊢s0 ─var:=e-≻v─n→ s3" assume P: "(Normal P) Y s0 Z" show "R ⌊v⌋⇩_{e}s3 Z ∧ s3∷≼(G, L)" proof - from wt obtain varT where wt_var: "⦇prg=G,cls=accC,lcl=L⦈⊢var∷=varT" and wt_e: "⦇prg=G,cls=accC,lcl=L⦈⊢e∷-T" by cases simp from eval obtain w upd s1 s2 where eval_var: "G⊢s0 ─var=≻(w, upd)─n→ s1" and eval_e: "G⊢s1 ─e-≻v─n→ s2" and s3: "s3=assign upd v s2" using normal_s0 by (auto elim: evaln_elim_cases) have "R ⌊v⌋⇩_{e}s3 Z" proof (cases "∃ vn. var = LVar vn") case False with da obtain V where da_var: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨var⟩⇩_{v}» V" and da_e: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ nrm V »⟨e⟩⇩_{e}» E" by cases simp+ from valid_var P valid_A conf_s0 eval_var wt_var da_var obtain Q: "Q ⌊(w,upd)⌋⇩_{v}s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) hence Q': "⋀ v. (Q←In2 (w,upd)) v s1 Z" by simp have "(λVal:v:. assign (snd (w,upd)) v .; R) ⌊v⌋⇩_{e}s2 Z" proof (cases "normal s1") case True obtain E' where da_e': "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »⟨e⟩⇩_{e}» E'" proof - from eval_var wt_var da_var wf True have "nrm V ⊆ dom (locals (store s1))" by (cases rule: da_good_approx_evalnE) iprover with da_e show thesis by (rule da_weakenE) (rule that) qed note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e wt_e da_e'] show ?thesis by (rule ve) next case False note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e] with False show ?thesis by iprover qed with s3 show "R ⌊v⌋⇩_{e}s3 Z" by simp next case True then obtain vn where vn: "var = LVar vn" by auto with da obtain E where da_e: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨e⟩⇩_{e}» E" by cases simp+ from da.LVar vn obtain V where da_var: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨var⟩⇩_{v}» V" by auto from valid_var P valid_A conf_s0 eval_var wt_var da_var obtain Q: "Q ⌊(w,upd)⌋⇩_{v}s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) hence Q': "⋀ v. (Q←In2 (w,upd)) v s1 Z" by simp have "(λVal:v:. assign (snd (w,upd)) v .; R) ⌊v⌋⇩_{e}s2 Z" proof (cases "normal s1") case True obtain E' where da_e': "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s1)) »⟨e⟩⇩_{e}» E'" proof - from eval_var have "dom (locals (store s0)) ⊆ dom (locals (store (s1)))" by (rule dom_locals_evaln_mono_elim) with da_e show thesis by (rule da_weakenE) (rule that) qed note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e wt_e da_e'] show ?thesis by (rule ve) next case False note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e] with False show ?thesis by iprover qed with s3 show "R ⌊v⌋⇩_{e}s3 Z" by simp qed moreover from eval wt da conf_s0 wf have "s3∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Cond A P e0 P' e1 e2 Q) note valid_e0 = ‹G,A|⊨∷{ {Normal P} e0-≻ {P'} }› have valid_then_else:"⋀ b. G,A|⊨∷{ {P'←=b} (if b then e1 else e2)-≻ {Q} }" using Cond.hyps by simp show "G,A|⊨∷{ {Normal P} e0 ? e1 : e2-≻ {Q} }" proof (rule valid_expr_NormalI) fix n s0 L accC T E v s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢e0 ? e1 : e2∷-T" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨e0 ? e1:e2⟩⇩_{e}»E" assume eval: "G⊢s0 ─e0 ? e1 : e2-≻v─n→ s2" assume P: "(Normal P) Y s0 Z" show "Q ⌊v⌋⇩_{e}s2 Z ∧ s2∷≼(G, L)" proof - from wt obtain T1 T2 where wt_e0: "⦇prg=G,cls=accC,lcl=L⦈⊢e0∷-PrimT Boolean" and wt_e1: "⦇prg=G,cls=accC,lcl=L⦈⊢e1∷-T1" and wt_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢e2∷-T2" by cases simp from da obtain E0 E1 E2 where da_e0: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨e0⟩⇩_{e}» E0" and da_e1: "⦇prg=G,cls=accC,lcl=L⦈ ⊢(dom (locals (store s0)) ∪ assigns_if True e0)»⟨e1⟩⇩_{e}» E1" and da_e2: "⦇prg=G,cls=accC,lcl=L⦈ ⊢(dom (locals (store s0)) ∪ assigns_if False e0)»⟨e2⟩⇩_{e}» E2" by cases simp+ from eval obtain b s1 where eval_e0: "G⊢s0 ─e0-≻b─n→ s1" and eval_then_else: "G⊢s1 ─(if the_Bool b then e1 else e2)-≻v─n→ s2" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_e0 P valid_A conf_s0 eval_e0 wt_e0 da_e0 obtain "P' ⌊b⌋⇩_{e}s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) hence P': "⋀ v. (P'←=(the_Bool b)) v s1 Z" by (cases "normal s1") auto have "Q ⌊v⌋⇩_{e}s2 Z" proof (cases "normal s1") case True note normal_s1=this from wt_e1 wt_e2 obtain T' where wt_then_else: "⦇prg=G,cls=accC,lcl=L⦈⊢(if the_Bool b then e1 else e2)∷-T'" by (cases "the_Bool b") simp+ have s0_s1: "dom (locals (store s0)) ∪ assigns_if (the_Bool b) e0 ⊆ dom (locals (store s1))" proof - from eval_e0 have eval_e0': "G⊢s0 ─e0-≻b→ s1" by (rule evaln_eval) hence "dom (locals (store s0)) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) moreover from eval_e0' True wt_e0 have "assigns_if (the_Bool b) e0 ⊆ dom (locals (store s1))" by (rule assigns_if_good_approx') ultimately show ?thesis by (rule Un_least) qed obtain E' where da_then_else: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s1))»⟨if the_Bool b then e1 else e2⟩⇩_{e}» E'" proof (cases "the_Bool b") case True with that da_e1 s0_s1 show ?thesis by simp (erule da_weakenE,auto) next case False with that da_e2 s0_s1 show ?thesis by simp (erule da_weakenE,auto) qed with valid_then_else P' valid_A conf_s1 eval_then_else wt_then_else show ?thesis by (rule validE) next case False with valid_then_else P' valid_A conf_s1 eval_then_else show ?thesis by (cases rule: validE) iprover+ qed moreover from eval wt da conf_s0 wf have "s2∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Call A P e Q args R mode statT mn pTs' S accC') note valid_e = ‹G,A|⊨∷{ {Normal P} e-≻ {Q} }› have valid_args: "⋀ a. G,A|⊨∷{ {Q←In1 a} args≐≻ {R a} }" using Call.hyps by simp have valid_methd: "⋀ a vs invC declC l. G,A|⊨∷{ {R a←In3 vs ∧. (λs. declC = invocation_declclass G mode (store s) a statT ⦇name = mn, parTs = pTs'⦈ ∧ invC = invocation_class mode (store s) a statT ∧ l = locals (store s)) ;. init_lvars G declC ⦇name = mn, parTs = pTs'⦈ mode a vs ∧. (λs. normal s ⟶ G⊢mode→invC≼statT)} Methd declC ⦇name=mn,parTs=pTs'⦈-≻ {set_lvars l .; S} }" using Call.hyps by simp show "G,A|⊨∷{ {Normal P} {accC',statT,mode}e⋅mn( {pTs'}args)-≻ {S} }" proof (rule valid_expr_NormalI) fix n s0 L accC T E v s5 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢{accC',statT,mode}e⋅mn( {pTs'}args)∷-T" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »⟨{accC',statT,mode}e⋅mn( {pTs'}args)⟩⇩_{e}» E" assume eval: "G⊢s0 ─{accC',statT,mode}e⋅mn( {pTs'}args)-≻v─n→ s5" assume P: "(Normal P) Y s0 Z" show "S ⌊v⌋⇩_{e}s5 Z ∧ s5∷≼(G, L)" proof - from wt obtain pTs statDeclT statM where wt_e: "⦇prg=G,cls=accC,lcl=L⦈⊢e∷-RefT statT" and wt_args: "⦇prg=G,cls=accC,lcl=L⦈⊢args∷≐pTs" and statM: "max_spec G accC statT ⦇name=mn,parTs=pTs⦈ = {((statDeclT,statM),pTs')}" and mode: "mode = invmode statM e" and T: "T =(resTy statM)" and eq_accC_accC': "accC=accC'" by cases fastforce+ from da obtain C where da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s0)))»⟨e⟩⇩_{e}» C" and da_args: "⦇prg=G,cls=accC,lcl=L⦈⊢ nrm C »⟨args⟩⇩_{l}» E" by cases simp from eval eq_accC_accC' obtain a s1 vs s2 s3 s3' s4 invDeclC where evaln_e: "G⊢s0 ─e-≻a─n→ s1" and evaln_args: "G⊢s1 ─args≐≻vs─n→ s2" and invDeclC: "invDeclC = invocation_declclass G mode (store s2) a statT ⦇name=mn,parTs=pTs'⦈" and s3: "s3 = init_lvars G invDeclC ⦇name=mn,parTs=pTs'⦈ mode a vs s2" and check: "s3' = check_method_access G accC' statT mode ⦇name = mn, parTs = pTs'⦈ a s3" and evaln_methd: "G⊢s3' ─Methd invDeclC ⦇name=mn,parTs=pTs'⦈-≻v─n→ s4" and s5: "s5=(set_lvars (locals (store s2))) s4" using normal_s0 by (auto elim: evaln_elim_cases) from evaln_e have eval_e: "G⊢s0 ─e-≻a→ s1" by (rule evaln_eval) from eval_e _ wt_e wf have s1_no_return: "abrupt s1 ≠ Some (Jump Ret)" by (rule eval_expression_no_jump [where ?Env="⦇prg=G,cls=accC,lcl=L⦈",simplified]) (insert normal_s0,auto) from valid_e P valid_A conf_s0 evaln_e wt_e da_e obtain "Q ⌊a⌋⇩_{e}s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) hence Q: "⋀ v. (Q←In1 a) v s1 Z" by simp obtain R: "(R a) ⌊vs⌋⇩_{l}s2 Z" and conf_s2: "s2∷≼(G,L)" and s2_no_return: "abrupt s2 ≠ Some (Jump Ret)" proof (cases "normal s1") case True obtain E' where da_args': "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »⟨args⟩⇩_{l}» E'" proof - from evaln_e wt_e da_e wf True have "nrm C ⊆ dom (locals (store s1))" by (cases rule: da_good_approx_evalnE) iprover with da_args show thesis by (rule da_weakenE) (rule that) qed with valid_args Q valid_A conf_s1 evaln_args wt_args obtain "(R a) ⌊vs⌋⇩_{l}s2 Z" "s2∷≼(G,L)" by (rule validE) moreover from evaln_args have e: "G⊢s1 ─args≐≻vs→ s2" by (rule evaln_eval) from this s1_no_return wt_args wf have "abrupt s2 ≠ Some (Jump Ret)" by (rule eval_expression_list_no_jump [where ?Env="⦇prg=G,cls=accC,lcl=L⦈",simplified]) ultimately show ?thesis .. next case False with valid_args Q valid_A conf_s1 evaln_args obtain "(R a) ⌊vs⌋⇩_{l}s2 Z" "s2∷≼(G,L)" by (cases rule: validE) iprover+ moreover from False evaln_args have "s2=s1" by auto with s1_no_return have "abrupt s2 ≠ Some (Jump Ret)" by simp ultimately show ?thesis .. qed obtain invC where invC: "invC = invocation_class mode (store s2) a statT" by simp with s3 have invC': "invC = (invocation_class mode (store s3) a statT)" by (cases s2,cases mode) (auto simp add: init_lvars_def2 ) obtain l where l: "l = locals (store s2)" by simp from eval wt da conf_s0 wf have conf_s5: "s5∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp let "PROP ?R" = "⋀ v. (R a←In3 vs ∧. (λs. invDeclC = invocation_declclass G mode (store s) a statT ⦇name = mn, parTs = pTs'⦈ ∧ invC = invocation_class mode (store s) a statT ∧ l = locals (store s)) ;. init_lvars G invDeclC ⦇name = mn, parTs = pTs'⦈ mode a vs ∧. (λs. normal s ⟶ G⊢mode→invC≼statT) ) v s3' Z" { assume abrupt_s3: "¬ normal s3" have "S ⌊v⌋⇩_{e}s5 Z" proof - from abrupt_s3 check have eq_s3'_s3: "s3'=s3" by (auto simp add: check_method_access_def Let_def) with R s3 invDeclC invC l abrupt_s3 have R': "PROP ?R" by auto have conf_s3': "s3'∷≼(G, Map.empty)" (* we need an arbirary environment (here empty) that s2' conforms to to apply validE *) proof - from s2_no_return s3 have "abrupt s3 ≠ Some (Jump Ret)" by (cases s2) (auto simp add: init_lvars_def2 split: if_split_asm) moreover obtain abr2 str2 where s2: "s2=(abr2,str2)" by (cases s2) from s3 s2 conf_s2 have "(abrupt s3,str2)∷≼(G, L)" by (auto simp add: init_lvars_def2 split: if_split_asm) ultimately show ?thesis using s3 s2 eq_s3'_s3 apply (simp add: init_lvars_def2) apply (rule conforms_set_locals [OF _ wlconf_empty]) by auto qed from valid_methd R' valid_A conf_s3' evaln_methd abrupt_s3 eq_s3'_s3 have "(set_lvars l .; S) ⌊v⌋⇩_{e}s4 Z" by (cases rule: validE) simp+ with s5 l show ?thesis by simp qed } note abrupt_s3_lemma = this have "S ⌊v⌋⇩_{e}s5 Z" proof (cases "normal s2") case False with s3 have abrupt_s3: "¬ normal s3" by (cases s2) (simp add: init_lvars_def2) thus ?thesis by (rule abrupt_s3_lemma) next case True note normal_s2 = this with evaln_args have normal_s1: "normal s1" by (rule evaln_no_abrupt) obtain E' where da_args': "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »⟨args⟩⇩_{l}» E'" proof - from evaln_e wt_e da_e wf normal_s1 have "nrm C ⊆ dom (locals (store s1))" by (cases rule: da_good_approx_evalnE) iprover with da_args show thesis by (rule da_weakenE) (rule that) qed from evaln_args have eval_args: "G⊢s1 ─args≐≻vs→ s2" by (rule evaln_eval) from evaln_e wt_e da_e conf_s0 wf have conf_a: "G, store s1⊢a∷≼RefT statT" by (rule evaln_type_sound [elim_format]) (insert normal_s1,simp) with normal_s1 normal_s2 eval_args have conf_a_s2: "G, store s2⊢a∷≼RefT statT" by (auto dest: eval_gext) from evaln_args wt_args da_args' conf_s1 wf have conf_args: "list_all2 (conf G (store s2)) vs pTs" by (rule evaln_type_sound [elim_format]) (insert normal_s2,simp) from statM obtain statM': "(statDeclT,statM)∈mheads G accC statT ⦇name=mn,parTs=pTs'⦈" and pTs_widen: "G⊢pTs[≼]pTs'" by (blast dest: max_spec2mheads) show ?thesis proof (cases "normal s3") case False thus ?thesis by (rule abrupt_s3_lemma) next case True note normal_s3 = this with s3 have notNull: "mode = IntVir ⟶ a ≠ Null" by (cases s2) (auto simp add: init_lvars_def2) from conf_s2 conf_a_s2 wf notNull invC have dynT_prop: "G⊢mode→invC≼statT" by (cases s2) (auto intro: DynT_propI) with wt_e statM' invC mode wf obtain dynM where dynM: "dynlookup G statT invC ⦇name=mn,parTs=pTs'⦈ = Some dynM" and acc_dynM: "G ⊢Methd ⦇name=mn,parTs=pTs'⦈ dynM in invC dyn_accessible_from accC" by (force dest!: call_access_ok) with invC' check eq_accC_accC' have eq_s3'_s3: "s3'=s3" by (auto simp add: check_method_access_def Let_def) with dynT_prop R s3 invDeclC invC l have R': "PROP ?R" by auto from dynT_prop wf wt_e statM' mode invC invDeclC dynM obtain dynM: "dynlookup G statT invC ⦇name=mn,parTs=pTs'⦈ = Some dynM" and wf_dynM: "wf_mdecl G invDeclC (⦇name=mn,parTs=pTs'⦈,mthd dynM)" and dynM': "methd G invDeclC ⦇name=mn,parTs=pTs'⦈ = Some dynM" and iscls_invDeclC: "is_class G invDeclC" and invDeclC': "invDeclC = declclass dynM" and invC_widen: "G⊢invC≼⇩_{C}invDeclC" and resTy_widen: "G⊢resTy dynM≼resTy statM" and is_static_eq: "is_static dynM = is_static statM" and involved_classes_prop: "(if invmode statM e = IntVir then ∀statC. statT = ClassT statC ⟶ G⊢invC≼⇩_{C}statC else ((∃statC. statT = ClassT statC ∧ G⊢statC≼⇩_{C}invDeclC) ∨ (∀statC. statT ≠ ClassT statC ∧ invDeclC = Object)) ∧ statDeclT = ClassT invDeclC)" by (cases rule: DynT_mheadsE) simp obtain L' where L':"L'=(λ k. (case k of EName e ⇒ (case e of VNam v ⇒(table_of (lcls (mbody (mthd dynM))) (pars (mthd dynM)[↦]pTs')) v | Res ⇒ Some (resTy dynM)) | This ⇒ if is_static statM then None else Some (Class invDeclC)))" by simp from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e wf eval_args conf_a mode notNull wf_dynM involved_classes_prop have conf_s3: "s3∷≼(G,L')" apply - (* FIXME confomrs_init_lvars should be adjusted to be more directy applicable *) apply (drule conforms_init_lvars [of G invDeclC "⦇name=mn,parTs=pTs'⦈" dynM "store s2" vs pTs "abrupt s2" L statT invC a "(statDeclT,statM)" e]) apply (rule wf) apply (rule conf_args) apply (simp add: pTs_widen) apply (cases s2,simp) apply (rule dynM') apply (force dest: ty_expr_is_type) apply (rule invC_widen) apply (force dest: eval_gext) apply simp apply simp apply (simp add: invC) apply (simp add: invDeclC) apply (simp add: normal_s2) apply (cases s2, simp add: L' init_lvars_def2 s3 cong add: lname.case_cong ename.case_cong) done with eq_s3'_s3 have conf_s3': "s3'∷≼(G,L')" by simp from is_static_eq wf_dynM L' obtain mthdT where "⦇prg=G,cls=invDeclC,lcl=L'⦈ ⊢Body invDeclC (stmt (mbody (mthd dynM)))∷-mthdT" and mthdT_widen: "G⊢mthdT≼resTy dynM" by - (drule wf_mdecl_bodyD, auto simp add: callee_lcl_def cong add: lname.case_cong ename.case_cong) with dynM' iscls_invDeclC invDeclC' have wt_methd: "⦇prg=G,cls=invDeclC,lcl=L'⦈ ⊢(Methd invDeclC ⦇name = mn, parTs = pTs'⦈)∷-mthdT" by (auto intro: wt.Methd) obtain M where da_methd: "⦇prg=G,cls=invDeclC,lcl=L'⦈ ⊢ dom (locals (store s3')) »⟨Methd invDeclC ⦇name=mn,parTs=pTs'⦈⟩⇩_{e}» M" proof - from wf_dynM obtain M' where da_body: "⦇prg=G, cls=invDeclC ,lcl=callee_lcl invDeclC ⦇name = mn, parTs = pTs'⦈ (mthd dynM) ⦈ ⊢ parameters (mthd dynM) »⟨stmt (mbody (mthd dynM))⟩» M'" and res: "Result ∈ nrm M'" by (rule wf_mdeclE) iprover from da_body is_static_eq L' have "⦇prg=G, cls=invDeclC,lcl=L'⦈ ⊢ parameters (mthd dynM) »⟨stmt (mbody (mthd dynM))⟩» M'" by (simp add: callee_lcl_def cong add: lname.case_cong ename.case_cong) moreover have "parameters (mthd dynM) ⊆ dom (locals (store s3'))" proof - from is_static_eq have "(invmode (mthd dynM) e) = (invmode statM e)" by (simp add: invmode_def) moreover have "length (pars (mthd dynM)) = length vs" proof - from normal_s2 conf_args have "length vs = length pTs" by (simp add: list_all2_iff) also from pTs_widen have "… = length pTs'" by (simp add: widens_def list_all2_iff) also from wf_dynM have "… = length (pars (mthd dynM))" by (simp add: wf_mdecl_def wf_mhead_def) finally show ?thesis .. qed moreover note s3 dynM' is_static_eq normal_s2 mode ultimately have "parameters (mthd dynM) = dom (locals (store s3))" using dom_locals_init_lvars [of "mthd dynM" G invDeclC "⦇name=mn,parTs=pTs'⦈" vs e a s2] by simp thus ?thesis using eq_s3'_s3 by simp qed ultimately obtain M2 where da: "⦇prg=G, cls=invDeclC,lcl=L'⦈ ⊢ dom (locals (store s3')) »⟨stmt (mbody (mthd dynM))⟩» M2" and M2: "nrm M' ⊆ nrm M2" by (rule da_weakenE) from res M2 have "Result ∈ nrm M2" by blast moreover from wf_dynM have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))" by (rule wf_mdeclE) ultimately obtain M3 where "⦇prg=G, cls=invDeclC,lcl=L'⦈ ⊢ dom (locals (store s3')) »⟨Body (declclass dynM) (stmt (mbody (mthd dynM)))⟩» M3" using da by (iprover intro: da.Body assigned.select_convs) from _ this [simplified] show thesis by (rule da.Methd [simplified,elim_format]) (auto intro: dynM' that) qed from valid_methd R' valid_A conf_s3' evaln_methd wt_methd da_methd have "(set_lvars l .; S) ⌊v⌋⇩_{e}s4 Z" by (cases rule: validE) iprover+ with s5 l show ?thesis by simp qed qed with conf_s5 show ?thesis by iprover qed qed next case (Methd A P Q ms) note valid_body = ‹G,A ∪ {{P} Methd-≻ {Q} | ms}|⊨∷{{P} body G-≻ {Q} | ms}› show "G,A|⊨∷{{P} Methd-≻ {Q} | ms}" by (rule Methd_sound) (rule Methd.hyps) next case (Body A P D Q c R) note valid_init = ‹G,A|⊨∷{ {Normal P} .Init D. {Q} }› note valid_c = ‹G,A|⊨∷{ {Q} .c. {λs.. abupd (absorb Ret) .; R←In1 (the (locals s Result))} }› show "G,A|⊨∷{ {Normal P} Body D c-≻ {R} }" proof (rule valid_expr_NormalI) fix n s0 L accC T E v s4 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Body D c∷-T" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨Body D c⟩⇩_{e}»E" assume eval: "G⊢s0 ─Body D c-≻v─n→ s4" assume P: "(Normal P) Y s0 Z" show "R ⌊v⌋⇩_{e}s4 Z ∧ s4∷≼(G, L)" proof - from wt obtain iscls_D: "is_class G D" and wt_init: "⦇prg=G,cls=accC,lcl=L⦈⊢Init D∷√" and wt_c: "⦇prg=G,cls=accC,lcl=L⦈⊢c∷√" by cases auto obtain I where da_init:"⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨Init D⟩⇩_{s}» I" by (auto intro: da_Init [simplified] assigned.select_convs) from da obtain C where da_c: "⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s0)))»⟨c⟩⇩_{s}» C" and jmpOk: "jumpNestingOkS {Ret} c" by cases simp from eval obtain s1 s2 s3 where eval_init: "G⊢s0 ─Init D─n→ s1" and eval_c: "G⊢s1 ─c─n→ s2" and v: "v = the (locals (store s2) Result)" and s3: "s3 =(if ∃l. abrupt s2 = Some (Jump (Break l)) ∨ abrupt s2 = Some (Jump (Cont l)) then abupd (λx. Some (Error CrossMethodJump)) s2 else s2)"and s4: "s4 = abupd (absorb Ret) s3" using normal_s0 by (fastforce elim: evaln_elim_cases) obtain C' where da_c': "⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s1)))»⟨c⟩⇩_{s}» C'" proof - from eval_init have "(dom (locals (store s0))) ⊆ (dom (locals (store s1)))" by (rule dom_locals_evaln_mono_elim) with da_c show thesis by (rule da_weakenE) (rule that) qed from valid_init P valid_A conf_s0 eval_init wt_init da_init obtain Q: "Q ♢ s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) from valid_c Q valid_A conf_s1 eval_c wt_c da_c' have R: "(λs.. abupd (absorb Ret) .; R←In1 (the (locals s Result))) ♢ s2 Z" by (rule validE) have "s3=s2" proof - from eval_init [THEN evaln_eval] wf have s1_no_jmp: "⋀ j. abrupt s1 ≠ Some (Jump j)" by - (rule eval_statement_no_jump [OF _ _ _ wt_init], insert normal_s0,auto) from eval_c [THEN evaln_eval] _ wt_c wf have "⋀ j. abrupt s2 = Some (Jump j) ⟹ j=Ret" by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp) moreover note s3 ultimately show ?thesis by (force split: if_split) qed with R v s4 have "R ⌊v⌋⇩_{e}s4 Z" by simp moreover from eval wt da conf_s0 wf have "s4∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Nil A P) show "G,A|⊨∷{ {Normal (P←⌊[]⌋⇩_{l})} []≐≻ {P} }" proof (rule valid_expr_list_NormalI) fix s0 s1 vs n L Y Z assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume eval: "G⊢s0 ─[]≐≻vs─n→ s1" assume P: "(Normal (P←⌊[]⌋⇩_{l})) Y s0 Z" show "P ⌊vs⌋⇩_{l}s1 Z ∧ s1∷≼(G, L)" proof - from eval obtain "vs=[]" "s1=s0" using normal_s0 by (auto elim: evaln_elim_cases) with P conf_s0 show ?thesis by simp qed qed next case (Cons A P e Q es R) note valid_e = ‹G,A|⊨∷{ {Normal P} e-≻ {Q} }› have valid_es: "⋀ v. G,A|⊨∷{ {Q←⌊v⌋⇩_{e}} es≐≻ {λVals:vs:. R←⌊(v # vs)⌋⇩_{l}} }" using Cons.hyps by simp show "G,A|⊨∷{ {Normal P} e # es≐≻ {R} }" proof (rule valid_expr_list_NormalI) fix n s0 L accC T E v s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢e # es∷≐T" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »⟨e # es⟩⇩_{l}» E" assume eval: "G⊢s0 ─e # es≐≻v─n→ s2" assume P: "(Normal P) Y s0 Z" show "R ⌊v⌋⇩_{l}s2 Z ∧ s2∷≼(G, L)" proof - from wt obtain eT esT where wt_e: "⦇prg=G,cls=accC,lcl=L⦈⊢e∷-eT" and wt_es: "⦇prg=G,cls=accC,lcl=L⦈⊢es∷≐esT" by cases simp from da obtain E1 where da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s0)))»⟨e⟩⇩_{e}» E1" and da_es: "⦇prg=G,cls=accC,lcl=L⦈⊢ nrm E1 »⟨es⟩⇩_{l}» E" by cases simp from eval obtain s1 ve vs where eval_e: "G⊢s0 ─e-≻ve─n→ s1" and eval_es: "G⊢s1 ─es≐≻vs─n→ s2" and v: "v=ve#vs" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_e P valid_A conf_s0 eval_e wt_e da_e obtain Q: "Q ⌊ve⌋⇩_{e}s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) from Q have Q': "⋀ v. (Q←⌊ve⌋⇩_{e}) v s1 Z" by simp have "(λVals:vs:. R←⌊(ve # vs)⌋⇩_{l}) ⌊vs⌋⇩_{l}s2 Z" proof (cases "normal s1") case True obtain E' where da_es': "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »⟨es⟩⇩_{l}» E'" proof - from eval_e wt_e da_e wf True have "nrm E1 ⊆ dom (locals (store s1))" by (cases rule: da_good_approx_evalnE) iprover with da_es show thesis by (rule da_weakenE) (rule that) qed from valid_es Q' valid_A conf_s1 eval_es wt_es da_es' show ?thesis by (rule validE) next case False with valid_es Q' valid_A conf_s1 eval_es show ?thesis by (cases rule: validE) iprover+ qed with v have "R ⌊v⌋⇩_{l}s2 Z" by simp moreover from eval wt da conf_s0 wf have "s2∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Skip A P) show "G,A|⊨∷{ {Normal (P←♢)} .Skip. {P} }" proof (rule valid_stmt_NormalI) fix s0 s1 n L Y Z assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume eval: "G⊢s0 ─Skip─n→ s1" assume P: "(Normal (P←♢)) Y s0 Z" show "P ♢ s1 Z ∧ s1∷≼(G, L)" proof - from eval obtain "s1=s0" using normal_s0 by (fastforce elim: evaln_elim_cases) with P conf_s0 show ?thesis by simp qed qed next case (Expr A P e Q) note valid_e = ‹G,A|⊨∷{ {Normal P} e-≻ {Q←♢} }› show "G,A|⊨∷{ {Normal P} .Expr e. {Q} }" proof (rule valid_stmt_NormalI) fix n s0 L accC C s1 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Expr e∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »⟨Expr e⟩⇩_{s}» C" assume eval: "G⊢s0 ─Expr e─n→ s1" assume P: "(Normal P) Y s0 Z" show "Q ♢ s1 Z ∧ s1∷≼(G, L)" proof - from wt obtain eT where wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT" by cases simp from da obtain E where da_e: "⦇prg=G,cls=accC, lcl=L⦈⊢dom (locals (store s0))»⟨e⟩⇩_{e}»E" by cases simp from eval obtain v where eval_e: "G⊢s0 ─e-≻v─n→ s1" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_e P valid_A conf_s0 eval_e wt_e da_e obtain Q: "(Q←♢) ⌊v⌋⇩_{e}s1 Z" and "s1∷≼(G,L)" by (rule validE) thus ?thesis by simp qed qed next case (Lab A P c l Q) note valid_c = ‹G,A|⊨∷{ {Normal P} .c. {abupd (absorb l) .; Q} }› show "G,A|⊨∷{ {Normal P} .l∙ c. {Q} }" proof (rule valid_stmt_NormalI) fix n s0 L accC C s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢l∙ c∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0)) »⟨l∙ c⟩⇩_{s}» C" assume eval: "G⊢s0 ─l∙ c─n→ s2" assume P: "(Normal P) Y s0 Z" show "Q ♢ s2 Z ∧ s2∷≼(G, L)" proof - from wt obtain wt_c: "⦇prg = G, cls = accC, lcl = L⦈⊢c∷√" by cases simp from da obtain E where da_c: "⦇prg=G,cls=accC, lcl=L⦈⊢dom (locals (store s0))»⟨c⟩⇩_{s}»E" by cases simp from eval obtain s1 where eval_c: "G⊢s0 ─c─n→ s1" and s2: "s2 = abupd (absorb l) s1" using normal_s0 by (fastforce elim: evaln_elim_cases) from valid_c P valid_A conf_s0 eval_c wt_c da_c obtain Q: "(abupd (absorb l) .; Q) ♢ s1 Z" by (rule validE) with s2 have "Q ♢ s2 Z" by simp moreover from eval wt da conf_s0 wf have "s2∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Comp A P c1 Q c2 R) note valid_c1 = ‹G,A|⊨∷{ {Normal P} .c1. {Q} }› note valid_c2 = ‹G,A|⊨∷{ {Q} .c2. {R} }› show "G,A|⊨∷{ {Normal P} .c1;; c2. {R} }" proof (rule valid_stmt_NormalI) fix n s0 L accC C s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢(c1;; c2)∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»⟨c1;;c2⟩⇩_{s}»C" assume eval: "G⊢s0 ─c1;; c2─n→ s2" assume P: "(Normal P) Y s0 Z" show "R ♢ s2 Z ∧ s2∷≼(G,L)" proof - from eval obtain s1 where eval_c1: "G⊢s0 ─c1 ─n→ s1" and eval_c2: "G⊢s1 ─c2 ─n→ s2" using normal_s0 by (fastforce elim: evaln_elim_cases) from wt obtain wt_c1: "⦇prg = G, cls = accC, lcl = L⦈⊢c1∷√" and wt_c2: "⦇prg = G, cls = accC, lcl = L⦈⊢c2∷√" by cases simp from da obtain C1 C2 where da_c1: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨c1⟩⇩_{s}» C1" and da_c2: "⦇prg=G,cls=accC,lcl=L⦈⊢nrm C1 »⟨c2⟩⇩_{s}» C2" by cases simp from valid_c1 P valid_A conf_s0 eval_c1 wt_c1 da_c1 obtain Q: "Q ♢ s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) have "R ♢ s2 Z" proof (cases "normal s1") case True obtain C2' where "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »⟨c2⟩⇩_{s}» C2'" proof - from eval_c1 wt_c1 da_c1 wf True have "nrm C1 ⊆ dom (locals (store s1))" by (cases rule: da_good_approx_evalnE) iprover with da_c2 show thesis by (rule da_weakenE) (rule that) qed with valid_c2 Q valid_A conf_s1 eval_c2 wt_c2 show ?thesis by (rule validE) next case False from valid_c2 Q valid_A conf_s1 eval_c2 False show ?thesis by (cases rule: validE) iprover+ qed moreover from eval wt da conf_s0 wf have "s2∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (If A P e P' c1 c2 Q) note valid_e = ‹G,A|⊨∷{ {Normal P} e-≻ {P'} }› have valid_then_else: "⋀ b. G,A|⊨∷{ {P'←=b} .(if b then c1 else c2). {Q} }" using If.hyps by simp show "G,A|⊨∷{ {Normal P} .If(e) c1 Else c2. {Q} }" proof (rule valid_stmt_NormalI) fix n s0 L accC C s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢If(e) c1 Else c2∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0))»⟨If(e) c1 Else c2⟩⇩_{s}»C" assume eval: "G⊢s0 ─If(e) c1 Else c2─n→ s2" assume P: "(Normal P) Y s0 Z" show "Q ♢ s2 Z ∧ s2∷≼(G,L)" proof - from eval obtain b s1 where eval_e: "G⊢s0 ─e-≻b─n→ s1" and eval_then_else: "G⊢s1 ─(if the_Bool b then c1 else c2)─n→ s2" using normal_s0 by (auto elim: evaln_elim_cases) from wt obtain wt_e: "⦇prg=G, cls=accC, lcl=L⦈⊢e∷-PrimT Boolean" and wt_then_else: "⦇prg=G,cls=accC,lcl=L⦈⊢(if the_Bool b then c1 else c2)∷√" by cases (simp split: if_split) from da obtain E S where da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨e⟩⇩_{e}» E" and da_then_else: "⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s0)) ∪ assigns_if (the_Bool b) e) »⟨if the_Bool b then c1 else c2⟩⇩_{s}» S" by cases (cases "the_Bool b",auto) from valid_e P valid_A conf_s0 eval_e wt_e da_e obtain "P' ⌊b⌋⇩_{e}s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) hence P': "⋀v. (P'←=the_Bool b) v s1 Z" by (cases "normal s1") auto have "Q ♢ s2 Z" proof (cases "normal s1") case True have s0_s1: "dom (locals (store s0)) ∪ assigns_if (the_Bool b) e ⊆ dom (locals (store s1))" proof - from eval_e have eval_e': "G⊢s0 ─e-≻b→ s1" by (rule evaln_eval) hence "dom (locals (store s0)) ⊆ dom (locals (store s1))" by (rule dom_locals_eval_mono_elim) moreover from eval_e' True wt_e have "assigns_if (the_Bool b) e ⊆ dom (locals (store s1))" by (rule assigns_if_good_approx') ultimately show ?thesis by (rule Un_least) qed with da_then_else obtain S' where "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s1))»⟨if the_Bool b then c1 else c2⟩⇩_{s}» S'" by (rule da_weakenE) with valid_then_else P' valid_A conf_s1 eval_then_else wt_then_else show ?thesis by (rule validE) next case False with valid_then_else P' valid_A conf_s1 eval_then_else show ?thesis by (cases rule: validE) iprover+ qed moreover from eval wt da conf_s0 wf have "s2∷≼(G, L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Loop A P e P' c l) note valid_e = ‹G,A|⊨∷{ {P} e-≻ {P'} }› note valid_c = ‹G,A|⊨∷{ {Normal (P'←=True)} .c. {abupd (absorb (Cont l)) .; P} }› show "G,A|⊨∷{ {P} .l∙ While(e) c. {P'←=False↓=♢} }" proof (rule valid_stmtI) fix n s0 L accC C s3 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume wt: "normal s0 ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢l∙ While(e) c∷√" assume da: "normal s0 ⟹ ⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨l∙ While(e) c⟩⇩_{s}» C" assume eval: "G⊢s0 ─l∙ While(e) c─n→ s3" assume P: "P Y s0 Z" show "(P'←=False↓=♢) ♢ s3 Z ∧ s3∷≼(G,L)" proof - ― ‹From the given hypothesises ‹valid_e› and ‹valid_c› we can only reach the state after unfolding the loop once, i.e. @{term "P ♢ s2 Z"}, where @{term s2} is the state after executing @{term c}. To gain validity of the further execution of while, to finally get @{term "(P'←=False↓=♢) ♢ s3 Z"} we have to get a hypothesis about the subsequent unfoldings (the whole loop again), too. We can achieve this, by performing induction on the evaluation relation, with all the necessary preconditions to apply ‹valid_e› and ‹valid_c› in the goal.› { fix t s s' v assume "G⊢s ─t≻─n→ (v, s')" hence "⋀ Y' T E. ⟦t = ⟨l∙ While(e) c⟩⇩_{s}; ∀t∈A. G⊨n∷t; P Y' s Z; s∷≼(G, L); normal s ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢t∷T; normal s ⟹ ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s))»t»E ⟧⟹ (P'←=False↓=♢) v s' Z" (is "PROP ?Hyp n t s v s'") proof (induct) case (Loop s0' e' b n' s1' c' s2' l' s3' Y' T E) note while = ‹(⟨l'∙ While(e') c'⟩⇩_{s}::term) = ⟨l∙ While(e) c⟩⇩_{s}› hence eqs: "l'=l" "e'=e" "c'=c" by simp_all note valid_A = ‹∀t∈A. G⊨n'∷t› note P = ‹P Y' (Norm s0') Z› note conf_s0' = ‹Norm s0'∷≼(G, L)› have wt: "⦇prg=G,cls=accC,lcl=L⦈⊢⟨l∙ While(e) c⟩⇩_{s}∷T" using Loop.prems eqs by simp have da: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store ((Norm s0')::state)))»⟨l∙ While(e) c⟩⇩_{s}»E" using Loop.prems eqs by simp have evaln_e: "G⊢Norm s0' ─e-≻b─n'→ s1'" using Loop.hyps eqs by simp show "(P'←=False↓=♢) ♢ s3' Z" proof - from wt obtain wt_e: "⦇prg=G,cls=accC,lcl=L⦈⊢e∷-PrimT Boolean" and wt_c: "⦇prg=G,cls=accC,lcl=L⦈⊢c∷√" by cases (simp add: eqs) from da obtain E S where da_e: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store ((Norm s0')::state))) »⟨e⟩⇩_{e}» E" and da_c: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ (dom (locals (store ((Norm s0')::state))) ∪ assigns_if True e) »⟨c⟩⇩_{s}» S" by cases (simp add: eqs) from evaln_e have eval_e: "G⊢Norm s0' ─e-≻b→ s1'" by (rule evaln_eval) from valid_e P valid_A conf_s0' evaln_e wt_e da_e obtain P': "P' ⌊b⌋⇩_{e}s1' Z" and conf_s1': "s1'∷≼(G,L)" by (rule validE) show "(P'←=False↓=♢) ♢ s3' Z" proof (cases "normal s1'") case True note normal_s1'=this show ?thesis proof (cases "the_Bool b") case True with P' normal_s1' have P'': "(Normal (P'←=True)) ⌊b⌋⇩_{e}s1' Z" by auto from True Loop.hyps obtain eval_c: "G⊢s1' ─c─n'→ s2'" and eval_while: "G⊢abupd (absorb (Cont l)) s2' ─l∙ While(e) c─n'→ s3'" by (simp add: eqs) from True Loop.hyps have hyp: "PROP ?Hyp n' ⟨l∙ While(e) c⟩⇩_{s}(abupd (absorb (Cont l')) s2') ♢ s3'" apply (simp only: True if_True eqs) apply (elim conjE) apply (tactic "smp_tac @{context} 3 1") apply fast done from eval_e have s0'_s1': "dom (locals (store ((Norm s0')::state))) ⊆ dom (locals (store s1'))" by (rule dom_locals_eval_mono_elim) obtain S' where da_c': "⦇prg=G,cls=accC,lcl=L⦈⊢(dom (locals (store s1')))»⟨c⟩⇩_{s}» S'" proof - note s0'_s1' moreover 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) ultimately have "dom (locals (store ((Norm s0')::state))) ∪ assigns_if True e ⊆ dom (locals (store s1'))" by (rule Un_least) with da_c show thesis by (rule da_weakenE) (rule that) qed with valid_c P'' valid_A conf_s1' eval_c wt_c obtain "(abupd (absorb (Cont l)) .; P) ♢ s2' Z" and conf_s2': "s2'∷≼(G,L)" by (rule validE) hence P_s2': "P ♢ (abupd (absorb (Cont l)) s2') Z" by simp from conf_s2' have conf_absorb: "abupd (absorb (Cont l)) s2' ∷≼(G, L)" by (cases s2') (auto intro: conforms_absorb) moreover obtain E' where da_while': "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals(store (abupd (absorb (Cont l)) s2'))) »⟨l∙ While(e) c⟩⇩_{s}» E'" proof - note s0'_s1' also from eval_c have "G⊢s1' ─c→ s2'" by (rule evaln_eval) hence "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 have "dom (locals (store ((Norm s0')::state))) ⊆ …" . with da show thesis by (rule da_weakenE) (rule that) qed from valid_A P_s2' conf_absorb wt da_while' show "(P'←=False↓=♢) ♢ s3' Z" using hyp by (simp add: eqs) next case False with Loop.hyps obtain "s3'=s1'" by simp with P' False show ?thesis by auto qed next case False note abnormal_s1'=this have "s3'=s1'" proof - from False obtain abr where abr: "abrupt s1' = Some abr" by (cases s1') auto from eval_e _ wt_e wf have no_jmp: "⋀ j. abrupt s1' ≠ Some (Jump j)" by (rule eval_expression_no_jump [where ?Env="⦇prg=G,cls=accC,lcl=L⦈",simplified]) simp show ?thesis proof (cases "the_Bool b") case True with Loop.hyps obtain eval_c: "G⊢s1' ─c─n'→ s2'" and eval_while: "G⊢abupd (absorb (Cont l)) s2' ─l∙ While(e) c─n'→ s3'" by (simp add: eqs) 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 qed with P' False show ?thesis by auto qed qed next case (Abrupt abr s t' n' Y' T E) note t' = ‹t' = ⟨l∙ While(e) c⟩⇩_{s}› note conf = ‹(Some abr, s)∷≼(G, L)› note P = ‹P Y' (Some abr, s) Z› note valid_A = ‹∀t∈A. G⊨n'∷t› show "(P'←=False↓=♢) (undefined3 t') (Some abr, s) Z" proof - have eval_e: "G⊢(Some abr,s) ─⟨e⟩⇩_{e}≻─n'→ (undefined3 ⟨e⟩⇩_{e},(Some abr,s))" by auto from valid_e P valid_A conf eval_e have "P' (undefined3 ⟨e⟩⇩_{e}) (Some abr,s) Z" by (cases rule: validE [where ?P="P"]) simp+ with t' show ?thesis by auto qed qed simp_all } note generalized=this from eval _ valid_A P conf_s0 wt da have "(P'←=False↓=♢) ♢ s3 Z" by (rule generalized) simp_all moreover have "s3∷≼(G, L)" proof (cases "normal s0") case True from eval wt [OF True] da [OF True] conf_s0 wf show ?thesis by (rule evaln_type_sound [elim_format]) simp next case False with eval have "s3=s0" by auto with conf_s0 show ?thesis by simp qed ultimately show ?thesis .. qed qed next case (Jmp A j P) show "G,A|⊨∷{ {Normal (abupd (λa. Some (Jump j)) .; P←♢)} .Jmp j. {P} }" proof (rule valid_stmt_NormalI) fix n s0 L accC C s1 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Jmp j∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0))»⟨Jmp j⟩⇩_{s}»C" assume eval: "G⊢s0 ─Jmp j─n→ s1" assume P: "(Normal (abupd (λa. Some (Jump j)) .; P←♢)) Y s0 Z" show "P ♢ s1 Z ∧ s1∷≼(G,L)" proof - from eval obtain s where s: "s0=Norm s" "s1=(Some (Jump j), s)" using normal_s0 by (auto elim: evaln_elim_cases) with P have "P ♢ s1 Z" by simp moreover from eval wt da conf_s0 wf have "s1∷≼(G,L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Throw A P e Q) note valid_e = ‹G,A|⊨∷{ {Normal P} e-≻ {λVal:a:. abupd (throw a) .; Q←♢} }› show "G,A|⊨∷{ {Normal P} .Throw e. {Q} }" proof (rule valid_stmt_NormalI) fix n s0 L accC C s2 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Throw e∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0))»⟨Throw e⟩⇩_{s}»C" assume eval: "G⊢s0 ─Throw e─n→ s2" assume P: "(Normal P) Y s0 Z" show "Q ♢ s2 Z ∧ s2∷≼(G,L)" proof - from eval obtain s1 a where eval_e: "G⊢s0 ─e-≻a─n→ s1" and s2: "s2 = abupd (throw a) s1" using normal_s0 by (auto elim: evaln_elim_cases) from wt obtain T where wt_e: "⦇prg=G,cls=accC,lcl=L⦈⊢e∷-T" by cases simp from da obtain E where da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨e⟩⇩_{e}» E" by cases simp from valid_e P valid_A conf_s0 eval_e wt_e da_e obtain "(λVal:a:. abupd (throw a) .; Q←♢) ⌊a⌋⇩_{e}s1 Z" by (rule validE) with s2 have "Q ♢ s2 Z" by simp moreover from eval wt da conf_s0 wf have "s2∷≼(G,L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Try A P c1 Q C vn c2 R) note valid_c1 = ‹G,A|⊨∷{ {Normal P} .c1. {SXAlloc G Q} }› note valid_c2 = ‹G,A|⊨∷{ {Q ∧. (λs. G,s⊢catch C) ;. new_xcpt_var vn} .c2. {R} }› note Q_R = ‹(Q ∧. (λs. ¬ G,s⊢catch C)) ⇒ R› show "G,A|⊨∷{ {Normal P} .Try c1 Catch(C vn) c2. {R} }" proof (rule valid_stmt_NormalI) fix n s0 L accC E s3 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Try c1 Catch(C vn) c2∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0)) »⟨Try c1 Catch(C vn) c2⟩⇩_{s}» E" assume eval: "G⊢s0 ─Try c1 Catch(C vn) c2─n→ s3" assume P: "(Normal P) Y s0 Z" show "R ♢ s3 Z ∧ s3∷≼(G,L)" proof - from eval obtain s1 s2 where eval_c1: "G⊢s0 ─c1─n→ s1" and sxalloc: "G⊢s1 ─sxalloc→ s2" and s3: "if G,s2⊢catch C then G⊢new_xcpt_var vn s2 ─c2─n→ s3 else s3 = s2" using normal_s0 by (fastforce elim: evaln_elim_cases) from wt obtain wt_c1: "⦇prg=G,cls=accC,lcl=L⦈⊢c1∷√" and wt_c2: "⦇prg=G,cls=accC,lcl=L(VName vn↦Class C)⦈⊢c2∷√" by cases simp from da obtain C1 C2 where da_c1: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s0)) »⟨c1⟩⇩_{s}» C1" and da_c2: "⦇prg=G,cls=accC,lcl=L(VName vn↦Class C)⦈ ⊢ (dom (locals (store s0)) ∪ {VName vn}) »⟨c2⟩⇩_{s}» C2" by cases simp from valid_c1 P valid_A conf_s0 eval_c1 wt_c1 da_c1 obtain sxQ: "(SXAlloc G Q) ♢ s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) from sxalloc sxQ have Q: "Q ♢ s2 Z" by auto have "R ♢ s3 Z" proof (cases "∃ x. abrupt s1 = Some (Xcpt x)") case False from sxalloc wf have "s2=s1" by (rule sxalloc_type_sound [elim_format]) (insert False, auto split: option.splits abrupt.splits ) with False have no_catch: "¬ G,s2⊢catch C" by (simp add: catch_def) moreover from no_catch s3 have "s3=s2" by simp ultimately show ?thesis using Q Q_R by simp next case True note exception_s1 = this show ?thesis proof (cases "G,s2⊢catch C") case False with s3 have "s3=s2" by simp with False Q Q_R show ?thesis by simp next case True with s3 have eval_c2: "G⊢new_xcpt_var vn s2 ─c2─n→ s3" by simp from conf_s1 sxalloc wf have conf_s2: "s2∷≼(G, L)" by (auto dest: sxalloc_type_sound split: option.splits abrupt.splits) from exception_s1 sxalloc wf obtain a where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))" by (auto dest!: sxalloc_type_sound split: option.splits abrupt.splits) with True have "G⊢obj_ty (the (globs (store s2) (Heap a)))≼Class C" by (cases s2) simp with xcpt_s2 conf_s2 wf have conf_new_xcpt: "new_xcpt_var vn s2 ∷≼(G, L(VName vn↦Class C))" by (auto dest: Try_lemma) obtain C2' where da_c2': "⦇prg=G,cls=accC,lcl=L(VName vn↦Class C)⦈ ⊢ (dom (locals (store (new_xcpt_var vn s2)))) »⟨c2⟩⇩_{s}» C2'" proof - have "(dom (locals (store s0)) ∪ {VName vn}) ⊆ dom (locals (store (new_xcpt_var vn s2)))" proof - from eval_c1 have "dom (locals (store s0)) ⊆ dom (locals (store s1))" by (rule dom_locals_evaln_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 show thesis by (rule da_weakenE) (rule that) qed from Q eval_c2 True have "(Q ∧. (λs. G,s⊢catch C) ;. new_xcpt_var vn) ♢ (new_xcpt_var vn s2) Z" by auto from valid_c2 this valid_A conf_new_xcpt eval_c2 wt_c2 da_c2' show "R ♢ s3 Z" by (rule validE) qed qed moreover from eval wt da conf_s0 wf have "s3∷≼(G,L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Fin A P c1 Q c2 R) note valid_c1 = ‹G,A|⊨∷{ {Normal P} .c1. {Q} }› have valid_c2: "⋀ abr. G,A|⊨∷{ {Q ∧. (λs. abr = fst s) ;. abupd (λx. None)} .c2. {abupd (abrupt_if (abr ≠ None) abr) .; R} }" using Fin.hyps by simp show "G,A|⊨∷{ {Normal P} .c1 Finally c2. {R} }" proof (rule valid_stmt_NormalI) fix n s0 L accC E s3 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢c1 Finally c2∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0)) »⟨c1 Finally c2⟩⇩_{s}» E" assume eval: "G⊢s0 ─c1 Finally c2─n→ s3" assume P: "(Normal P) Y s0 Z" show "R ♢ s3 Z ∧ s3∷≼(G,L)" proof - from eval obtain s1 abr1 s2 where eval_c1: "G⊢s0 ─c1─n→ (abr1, s1)" and eval_c2: "G⊢Norm s1 ─c2─n→ s2" and s3: "s3 = (if ∃err. abr1 = Some (Error err) then (abr1, s1) else abupd (abrupt_if (abr1 ≠ None) abr1) s2)" using normal_s0 by (fastforce elim: evaln_elim_cases) from wt obtain wt_c1: "⦇prg=G,cls=accC,lcl=L⦈⊢c1∷√" and wt_c2: "⦇prg=G,cls=accC,lcl=L⦈⊢c2∷√" by cases simp from da obtain C1 C2 where da_c1: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨c1⟩⇩_{s}» C1" and da_c2: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨c2⟩⇩_{s}» C2" by cases simp from valid_c1 P valid_A conf_s0 eval_c1 wt_c1 da_c1 obtain Q: "Q ♢ (abr1,s1) Z" and conf_s1: "(abr1,s1)∷≼(G,L)" by (rule validE) from Q have Q': "(Q ∧. (λs. abr1 = fst s) ;. abupd (λx. None)) ♢ (Norm s1) Z" by auto from eval_c1 wt_c1 da_c1 conf_s0 wf have "error_free (abr1,s1)" by (rule evaln_type_sound [elim_format]) (insert normal_s0,simp) with s3 have s3': "s3 = abupd (abrupt_if (abr1 ≠ None) abr1) s2" by (simp add: error_free_def) from conf_s1 have conf_Norm_s1: "Norm s1∷≼(G,L)" by (rule conforms_NormI) obtain C2' where da_c2': "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store ((Norm s1)::state))) »⟨c2⟩⇩_{s}» C2'" proof - from eval_c1 have "dom (locals (store s0)) ⊆ dom (locals (store (abr1,s1)))" by (rule dom_locals_evaln_mono_elim) hence "dom (locals (store s0)) ⊆ dom (locals (store ((Norm s1)::state)))" by simp with da_c2 show thesis by (rule da_weakenE) (rule that) qed from valid_c2 Q' valid_A conf_Norm_s1 eval_c2 wt_c2 da_c2' have "(abupd (abrupt_if (abr1 ≠ None) abr1) .; R) ♢ s2 Z" by (rule validE) with s3' have "R ♢ s3 Z" by simp moreover from eval wt da conf_s0 wf have "s3∷≼(G,L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (Done A P C) show "G,A|⊨∷{ {Normal (P←♢ ∧. initd C)} .Init C. {P} }" proof (rule valid_stmt_NormalI) fix n s0 L accC E s3 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Init C∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0)) »⟨Init C⟩⇩_{s}» E" assume eval: "G⊢s0 ─Init C─n→ s3" assume P: "(Normal (P←♢ ∧. initd C)) Y s0 Z" show "P ♢ s3 Z ∧ s3∷≼(G,L)" proof - from P have inited: "inited C (globs (store s0))" by simp with eval have "s3=s0" using normal_s0 by (auto elim: evaln_elim_cases) with P conf_s0 show ?thesis by simp qed qed next case (Init C c A P Q R) note c = ‹the (class G C) = c› note valid_super = ‹G,A|⊨∷{ {Normal (P ∧. Not ∘ initd C ;. supd (init_class_obj G C))} .(if C = Object then Skip else Init (super c)). {Q} }› have valid_init: "⋀ l. G,A|⊨∷{ {Q ∧. (λs. l = locals (snd s)) ;. set_lvars Map.empty} .init c. {set_lvars l .; R} }" using Init.hyps by simp show "G,A|⊨∷{ {Normal (P ∧. Not ∘ initd C)} .Init C. {R} }" proof (rule valid_stmt_NormalI) fix n s0 L accC E s3 Y Z assume valid_A: "∀t∈A. G⊨n∷t" assume conf_s0: "s0∷≼(G,L)" assume normal_s0: "normal s0" assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢Init C∷√" assume da: "⦇prg=G,cls=accC,lcl=L⦈ ⊢dom (locals (store s0)) »⟨Init C⟩⇩_{s}» E" assume eval: "G⊢s0 ─Init C─n→ s3" assume P: "(Normal (P ∧. Not ∘ initd C)) Y s0 Z" show "R ♢ s3 Z ∧ s3∷≼(G,L)" proof - from P have not_inited: "¬ inited C (globs (store s0))" by simp with eval c obtain s1 s2 where eval_super: "G⊢Norm ((init_class_obj G C) (store s0)) ─(if C = Object then Skip else Init (super c))─n→ s1" and eval_init: "G⊢(set_lvars Map.empty) s1 ─init c─n→ s2" and s3: "s3 = (set_lvars (locals (store s1))) s2" using normal_s0 by (auto elim!: evaln_elim_cases) from wt c have cls_C: "class G C = Some c" by cases auto from wf cls_C have wt_super: "⦇prg=G,cls=accC,lcl=L⦈ ⊢(if C = Object then Skip else Init (super c))∷√" by (cases "C=Object") (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD) obtain S where da_super: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store ((Norm ((init_class_obj G C) (store s0)))::state))) »⟨if C = Object then Skip else Init (super c)⟩⇩_{s}» S" proof (cases "C=Object") case True with da_Skip show ?thesis using that by (auto intro: assigned.select_convs) next case False with da_Init show ?thesis by - (rule that, auto intro: assigned.select_convs) qed from normal_s0 conf_s0 wf cls_C not_inited have conf_init_cls: "(Norm ((init_class_obj G C) (store s0)))∷≼(G, L)" by (auto intro: conforms_init_class_obj) from P have P': "(Normal (P ∧. Not ∘ initd C ;. supd (init_class_obj G C))) Y (Norm ((init_class_obj G C) (store s0))) Z" by auto from valid_super P' valid_A conf_init_cls eval_super wt_super da_super obtain Q: "Q ♢ s1 Z" and conf_s1: "s1∷≼(G,L)" by (rule validE) from cls_C wf have wt_init: "⦇prg=G, cls=C,lcl=Map.empty⦈⊢(init c)∷√" by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init]) from cls_C wf obtain I where "⦇prg=G,cls=C,lcl=Map.empty⦈⊢ {} »⟨init c⟩⇩_{s}» I" by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast (* simplified: to rewrite ⟨init c⟩ to In1r (init c) *) then obtain I' where da_init: "⦇prg=G,cls=C,lcl=Map.empty⦈⊢dom (locals (store ((set_lvars Map.empty) s1))) »⟨init c⟩⇩_{s}» I'" by (rule da_weakenE) simp have conf_s1_empty: "(set_lvars Map.empty) s1∷≼(G, Map.empty)" proof - from eval_super have "G⊢Norm ((init_class_obj G C) (store s0)) ─(if C = Object then Skip else Init (super c))→ s1" by (rule evaln_eval) from this wt_super wf have s1_no_ret: "⋀ j. abrupt s1 ≠ Some (Jump j)" by - (rule eval_statement_no_jump [where ?Env="⦇prg=G,cls=accC,lcl=L⦈"], auto split: if_split) with conf_s1 show ?thesis by (cases s1) (auto intro: conforms_set_locals) qed obtain l where l: "l = locals (store s1)" by simp with Q have Q': "(Q ∧. (λs. l = locals (snd s)) ;. set_lvars Map.empty) ♢ ((set_lvars Map.empty) s1) Z" by auto from valid_init Q' valid_A conf_s1_empty eval_init wt_init da_init have "(set_lvars l .; R) ♢ s2 Z" by (rule validE) with s3 l have "R ♢ s3 Z" by simp moreover from eval wt da conf_s0 wf have "s3∷≼(G,L)" by (rule evaln_type_sound [elim_format]) simp ultimately show ?thesis .. qed qed next case (InsInitV A P c v Q) show "G,A|⊨∷{ {Normal P} InsInitV c v=≻ {Q} }" proof (rule valid_var_NormalI) fix s0 vf n s1 L Z assume "normal s0" moreover assume "G⊢s0 ─InsInitV c v=≻vf─n→ s1" ultimately have "False" by (cases s0) (simp add: evaln_InsInitV) thus "Q ⌊vf⌋⇩_{v}s1 Z ∧ s1∷≼(G, L)".. qed next case (InsInitE A P c e Q) show "G,A|⊨∷{ {Normal P} InsInitE c e-≻ {Q} }" proof (rule valid_expr_NormalI) fix s0 v n s1 L Z assume "normal s0" moreover assume "G⊢s0 ─InsInitE c e-≻v─n→ s1" ultimately have "False" by (cases s0) (simp add: evaln_InsInitE) thus "Q ⌊v⌋⇩_{e}s1 Z ∧ s1∷≼(G, L)".. qed next case (Callee A P l e Q) show "G,A|⊨∷{ {Normal P} Callee l e-≻ {Q} }" proof (rule valid_expr_NormalI) fix s0 v n s1 L Z assume "normal s0" moreover assume "G⊢s0 ─Callee l e-≻v─n→ s1" ultimately have "False" by (cases s0) (simp add: evaln_Callee) thus "Q ⌊v⌋⇩_{e}s1 Z ∧ s1∷≼(G, L)".. qed next case (FinA A P a c Q) show "G,A|⊨∷{ {Normal P} .FinA a c. {Q} }" proof (rule valid_stmt_NormalI) fix s0 v n s1 L Z assume "normal s0" moreover assume "G⊢s0 ─FinA a c─n→ s1" ultimately have "False" by (cases s0) (simp add: evaln_FinA) thus "Q ♢ s1 Z ∧ s1∷≼(G, L)".. qed qed declare inj_term_simps [simp del] theorem ax_sound: "wf_prog G ⟹ G,(A::'a triple set)|⊢(ts::'a triple set) ⟹ G,A|⊨ts" apply (subst ax_valids2_eq [symmetric]) apply assumption apply (erule (1) ax_sound2) done lemma sound_valid2_lemma: "⟦∀v n. Ball A (triple_valid2 G n) ⟶ P v n; Ball A (triple_valid2 G n)⟧ ⟹P v n" by blast end