# Theory AxSound

```(*  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 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)
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 (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 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
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"
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
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 (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 (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 (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 (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 (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 (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
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"
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 (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
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
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
(* 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
(* 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
⊢ 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
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 (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'"
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)"
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 (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 (cases s2, simp add: L' init_lvars_def2 s3
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,
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'"