Quelle  AxSound.thy

(*  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"  (‹_⊨_#x003a;_›[61,0, 58] 57)
  where
    "G⊨n#x003a;t =
      (case t of {P} t≻ {Q} ==>
        ∀Y s Z. P Y s Z ⟶ (∀L. s#x003a;⪯(G,L)
          ⟶ (∀T C A. (normal s ⟶ ((prg=G,cls=C,lcl=L)⊨t#x003a;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'#x003a;⪯(G,L)))))"

text ‹This definition differs from the ordinary ‹triple_valid_def›
  in the conclusion: We also ensures conformance of the result state. So
  don't have to apply the type soundness lemma all the time during
 . This definition is only introduced for the soundness
  of the axiomatic semantics, in the end we will conclude to
  ordinary definition.
 ›

definition
  ax_valids2 :: "prog ==> 'a triples ==> 'a triples ==> bool"  (‹_,_|⊨#x003a;_› [61,58,58] 57)
  where "G,A|⊨#x003a;ts = (∀n. (∀t∈A. G⊨n#x003a;t) ⟶ (∀t∈ts. G⊨n#x003a;t))"

lemma triple_valid2_def2: "G⊨n#x003a;{P} t≻ {Q} =
 (∀Y s Z. P Y s Z ⟶ (∀Y' s'. G⊨s ←-t≻←-n→ (Y',s')⟶
  (∀L. s#x003a;⪯(G,L) ⟶ (∀T C A. (normal s ⟶ ((prg=G,cls=C,lcl=L)⊨t#x003a;T ∧
                            (prg=G,cls=C,lcl=L)⊨dom (locals (store s))¬t¬A)) ⟶
  Q Y' s' Z ∧ s'#x003a;⪯(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 🍋 3 1")
apply (case_tac "normal s")
apply  clarsimp
apply  (elim conjE impE)
apply    blast

apply    (tactic "smp_tac 🍋 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|⊨#x003a;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#x003a;t ⟶ G⊨n#x003a;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#x003a;{Normal P} Methd C sig-≻ {Q}"
by (auto elim!: evaln_elim_cases simp add: triple_valid2_def2)

lemma Methd_triple_valid2_SucI: 
"[G⊨n#x003a;{Normal P} body G C sig-≻{Q}]
  ==> G⊨Suc n#x003a;{Normal P} Methd C sig-≻ {Q}"
apply (simp (no_asm_use) add: triple_valid2_def2)
apply (intro strip, tactic "smp_tac 🍋 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}|⊨#x003a;{{P} body G-≻ {Q} | ms}"
  shows "G,A|⊨#x003a;{{P} Methd-≻ {Q} | ms}"
proof -
  have "∀t∈A. G⊨n#x003a;t ==> ∀t∈{{P} Methd-≻ {Q} | ms}. G⊨n#x003a;t"
    if rec: "∧n. ∀t∈(A ∪ {{P} Methd-≻ {Q} | ms}). G⊨n#x003a;t
                  ==> ∀t∈{{P} body G-≻ {Q} | ms}. G⊨n#x003a;t"
    for n
  proof (induct n)
    case 0
    show "∀t∈{{P} Methd-≻ {Q} | ms}. G⊨0#x003a;t"
    proof -
      have "G⊨0#x003a;{Normal (P C sig)} Methd C sig-≻ {Q C sig}"
        if "(C,sig) ∈ ms"
        for 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#x003a;t ==> ∀t∈{{P} Methd-≻ {Q} | ms}. G⊨m#x003a;t›
    note prem = ‹∀t∈A. G⊨Suc m#x003a;t›
    show "∀t∈{{P} Methd-≻ {Q} | ms}. G⊨Suc m#x003a;t"
    proof -
      have "G⊨Suc m#x003a;{Normal (P C sig)} Methd C sig-≻ {Q C sig}"
        if m: "(C,sig) ∈ ms"
        for C sig
      proof -
        from prem have prem_m: "∀t∈A. G⊨m#x003a;t"
          by (rule triples_valid2_Suc)
        hence "∀t∈{{P} Methd-≻ {Q} | ms}. G⊨m#x003a;t"
          by (rule hyp)
        with prem_m
        have "∀t∈(A ∪ {{P} Methd-≻ {Q} | ms}). G⊨m#x003a;t"
          by (simp add: ball_Un)
        hence "∀t∈{{P} body G-≻ {Q} | ms}. G⊨m#x003a;t"
          by (rule rec)
        with m have "G⊨m#x003a;{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#x003a;⪯(G,L) ⟶
    (∀T C A. (normal s ⟶ ((prg=G,cls=C,lcl=L)⊨t#x003a;T) ∧
                            (prg=G,cls=C,lcl=L)⊨dom (locals (store s))¬t¬A) ⟶
    Q Y' s' Z ∧ s'#x003a;⪯(G, L)))) ==>
  G,A|⊨#x003a;{ {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#x003a;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#x003a;t; s0#x003a;⪯(G,L);
               normal s0 ==> (prg=G,cls=accC,lcl=L)⊨t#x003a;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#x003a;⪯(G,L)" 
  shows "G,A|⊨#x003a;{ {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#x003a;t; s0#x003a;⪯(G,L);
              normal s0==> (prg=G,cls=accC,lcl=L)⊨c#x003a;√;
              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#x003a;⪯(G,L)" 
  shows "G,A|⊨#x003a;{ {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#x003a;t; s0#x003a;⪯(G,L); normal s0; (prg=G,cls=accC,lcl=L)⊨c#x003a;√;
               (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#x003a;⪯(G,L)" 
  shows "G,A|⊨#x003a;{ {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#x003a;t; s0#x003a;⪯(G,L); normal s0;
                (prg=G,cls=accC,lcl=L)⊨t#x003a;=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#x003a;⪯(G,L)"
   shows "G,A|⊨#x003a;{ {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#x003a;t; s0#x003a;⪯(G,L); normal s0;
                (prg=G,cls=accC,lcl=L)⊨t#x003a;-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#x003a;⪯(G,L)"
   shows "G,A|⊨#x003a;{ {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#x003a;t; s0#x003a;⪯(G,L); normal s0;
                (prg=G,cls=accC,lcl=L)⊨t#x003a;≐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#x003a;⪯(G,L)"
   shows "G,A|⊨#x003a;{ {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|⊨#x003a;{ {P} t≻ {Q} }"
   and    P: "P Y s0 Z"
   and    valid_A: "∀t∈A. G⊨n#x003a;t"
   and    conf: "s0#x003a;⪯(G,L)"
   and    eval: "G⊨s0 ←-t≻←-n→ (v,s1)"
   and    wt: "normal s0 ==> (prg=G,cls=accC,lcl=L)⊨t#x003a;T"
   and    da: "normal s0 ==> (prg=G,cls=accC,lcl=L)⊨dom (locals (store s0))¬t¬C"
   and    elim: "[Q v s1 Z; s1#x003a;⪯(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
   \<not> normal s0 holds,
   I can chain "\<not> 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#x003a;T" and
             da: "(prg=G,cls=accC,lcl=L)⊨dom (locals (store s0)) ¬t¬ A" and
        conf_s0: "s0#x003a;⪯(G,L)" and
             wf: "wf_prog G"                         
  shows "s1#x003a;⪯(G,L) ∧ (normal s1 ⟶ G,L,store s1⊨t≻v#x003a;⪯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|⊨#x003a;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|⊨#x003a;{t}›
  moreover
  note valid_ts = ‹G,A|⊨#x003a;ts›
  have "∀t'∈insert t ts. G⊨n#x003a;t'"
    if valid_A: "∀t∈A. G⊨n#x003a;t"
    for n
  proof -
    have "G⊨n#x003a;t"
      using valid_A valid_t by (simp add: ax_valids2_def)
    moreover
    have "∀t∈ts. G⊨n#x003a;t"
      using valid_A valid_ts by (unfold ax_valids2_def) blast
    ultimately show "∀t'∈insert t ts. G⊨n#x003a;t'"
      by simp
  qed
  thus ?case
    by (unfold ax_valids2_def) blast
next
  case (asm ts A)
  from ‹ts ⊆ A›
  show "G,A|⊨#x003a;ts"
    by (auto simp add: ax_valids2_def triple_valid2_def)
next
  case (weaken A ts' ts)
  note ‹G,A|⊨#x003a;ts'›
  moreover note ‹ts ⊆ ts'›
  ultimately show "G,A|⊨#x003a;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|⊨#x003a;{ {P'} t≻ {Q'} }) ∧
 (∀Y' s'. (∀Y Z'. P' Y s Z' ⟶ Q' Y' s' Z') ⟶ Q Y' s' Z))›
  show "G,A|⊨#x003a;{ {P} t≻ {Q} }"
  proof (rule validI)
    fix n s0 L accC T C v s1 Y Z
    assume valid_A: "∀t∈A. G⊨n#x003a;t" 
    assume conf: "s0#x003a;⪯(G,L)"
    assume wt: "normal s0 ==> (prg=G,cls=accC,lcl=L)⊨t#x003a;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#x003a;⪯(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 🍋 3 1")
        apply clarify
        apply (tactic "smp_tac 🍋 1 1")
        apply (erule allE,erule allE, erule mp)
        apply (intro strip)
        apply (tactic "smp_tac 🍋 3 1")
        apply (tactic "smp_tac 🍋 2 1")
        apply (tactic "smp_tac 🍋 1 1")
        by blast
      moreover have "s1#x003a;⪯(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|⊨#x003a;{ {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|⊨#x003a;{ {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#x003a;⪯(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#x003a;⪯(G, L)"
      by simp
  qed
next
  case (LVar A P vn)
  show "G,A|⊨#x003a;{ {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#x003a;⪯(G, L)"
    assume normal_s0: "normal s0"
    assume wt: "(prg = G, cls = accC, lcl = L)⊨LVar vn#x003a;=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#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {Normal P} .Init statDeclC. {Q} }›
  note valid_e = ‹G,A|⊨#x003a;{ {Q} e-≻ {λVal:a:. fvar statDeclC stat fn a ..; R} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0:  "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC',lcl=L)⊨{accC,statDeclC,stat}e..fn#x003a;=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#x003a;⪯(G, L)"
    proof -
      from wt obtain statC f where
        wt_e: "(prg=G, cls=accC, lcl=L)⊨e#x003a;-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)#x003a;√"
      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#x003a;⪯(G, L)"
        by (rule validE)
      obtain 
        R: "R ⌊vf⌋_v s2' Z" and 
        conf_s2: "s2#x003a;⪯(G, L)" and
        conf_a: "normal s2 ⟶ G,store s2⊨a#x003a;⪯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#x003a;⪯(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#x003a;⪯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#x003a;⪯(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#x003a;⪯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#x003a;⪯(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|⊨#x003a;{ {Normal P} e1-≻ {Q} }›
  have valid_e2: "∧ a. G,A|⊨#x003a;{ {Q←In1 a} e2-≻ {λVal:i:. avar G i a ..; R} }"
    using AVar.hyps by simp
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨e1.[e2]#x003a;=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'#x003a;⪯(G, L)"
    proof -
      from wt obtain 
        wt_e1: "(prg=G,cls=accC,lcl=L)⊨e1#x003a;-T.[]" and
        wt_e2: "(prg=G,cls=accC,lcl=L)⊨e2#x003a;-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#x003a;⪯(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'#x003a;⪯(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|⊨#x003a;{ {Normal P} .Init C. {Alloc G (CInst C) Q} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨NewC C#x003a;-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#x003a;⪯(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#x003a;√" 
        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#x003a;⪯(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|⊨#x003a;{ {Normal P} .init_comp_ty T. {Q} }›
  note valid_e = ‹G,A|⊨#x003a;{ {Q} e-≻ {λVal:i:. abupd (check_neg i) .;
 Alloc G (Arr T (the_Intg i)) R}}›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨New T[e]#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain
        wt_init: "(prg=G,cls=accC,lcl=L)⊨init_comp_ty T#x003a;√" and 
        wt_e: "(prg=G,cls=accC,lcl=L)⊨e#x003a;-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
        show ?thesis
          by (rule that)
            (use True in
              ‹auto intro: da_Init [simplified] assigned.select_convs
 simp add: init_comp_ty_def›)
         (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
      next
        case False
        show ?thesis
          by (rule that)
            (use False in
              ‹auto intro: da_Skip [simplified] assigned.select_convs
 simp add: init_comp_ty_def›)
         (* simplified: to rewrite \<langle>Skip\<rangle> 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#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {Normal P} e-≻
 {λVal:v:. λs.. abupd (raise_if (¬ G,s⊨v fits T) ClassCast) .;
 Q←In1 v} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨Cast T e#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain eT where 
        wt_e: "(prg = G, cls = accC, lcl = L)⊨e#x003a;-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#x003a;⪯(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|⊨#x003a;{ {Normal P} e-≻
               {λVal:v:. λs.. Q←In1 (Bool (v ≠ Null ∧ G,s⊨v fits RefT T))} }"
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨e InstOf T#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain eT where 
        wt_e: "(prg = G, cls = accC, lcl = L)⊨e#x003a;-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#x003a;⪯(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Lit A P v)
  show "G,A|⊨#x003a;{ {Normal (P←In1 v)} Lit v-≻ {P} }"
  proof (rule valid_expr_NormalI)
    fix n L s0 s1 v'  Y Z
    assume conf_s0: "s0#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {Normal P}e-≻{λVal:v:. Q←In1 (eval_unop unop v)} }"
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨UnOp unop e#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain eT where 
        wt_e: "(prg = G, cls = accC, lcl = L)⊨e#x003a;-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#x003a;⪯(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|⊨#x003a;{ {Normal P} e1-≻ {Q} }" 
  have valid_e2: "∧ v1. G,A|⊨#x003a;{ {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|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨BinOp binop e1 e2#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain e1T e2T where
        wt_e1: "(prg=G,cls=accC,lcl=L)⊨e1#x003a;-e1T" and
        wt_e2: "(prg=G,cls=accC,lcl=L)⊨e2#x003a;-e2T" and
        wt_binop: "wt_binop G binop e1T e2T" 
        by cases simp
      have wt_Skip: "(prg = G, cls = accC, lcl = L)⊨Skip#x003a;√"
        by simp
      (*
      obtain S where
        daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> 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#x003a;⪯(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#x003a;⪯e1T" 
          by (rule evaln_type_sound [elim_format]) (use True in 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)#x003a;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#x003a;⪯(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Super A P)
  show "G,A|⊨#x003a;{ {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#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {Normal P} var=≻ {λVar:(v, f):. Q←In1 v} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨Acc var#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain 
        wt_var: "(prg=G,cls=accC,lcl=L)⊨var#x003a;=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") (use da.LVar in ‹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#x003a;⪯(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|⊨#x003a;{ {Normal P} var=≻ {Q} }›
  have valid_e: "∧ vf.
                  G,A|⊨#x003a;{ {Q←In2 vf} e-≻ {λVal:v:. assign (snd vf) v .; R} }"
    using Ass.hyps by simp
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨var:=e#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain varT  where
        wt_var: "(prg=G,cls=accC,lcl=L)⊨var#x003a;=varT" and
        wt_e: "(prg=G,cls=accC,lcl=L)⊨e#x003a;-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#x003a;⪯(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#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {Normal P} e0-≻ {P'} }›
  have valid_then_else:"∧ b. G,A|⊨#x003a;{ {P'←=b} (if b then e1 else e2)-≻ {Q} }"
    using Cond.hyps by simp
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨e0 ? e1 : e2#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain T1 T2 where
        wt_e0: "(prg=G,cls=accC,lcl=L)⊨e0#x003a;-PrimT Boolean" and
        wt_e1: "(prg=G,cls=accC,lcl=L)⊨e1#x003a;-T1" and
        wt_e2: "(prg=G,cls=accC,lcl=L)⊨e2#x003a;-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#x003a;⪯(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)#x003a;-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#x003a;⪯(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|⊨#x003a;{ {Normal P} e-≻ {Q} }›
  have valid_args: "∧ a. G,A|⊨#x003a;{ {Q←In1 a} args≐≻ {R a} }"
    using Call.hyps by simp
  have valid_methd: "∧ a vs invC declC l.
        G,A|⊨#x003a;{ {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|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨{accC',statT,mode}e⋅mn( {pTs'}args)#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain pTs statDeclT statM where
                 wt_e: "(prg=G,cls=accC,lcl=L)⊨e#x003a;-RefT statT" and
              wt_args: "(prg=G,cls=accC,lcl=L)⊨args#x003a;≐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])
           (use normal_s0 in 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#x003a;⪯(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#x003a;⪯(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#x003a;⪯(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#x003a;⪯(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#x003a;⪯(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"
      have abrupt_s3_lemma: "S ⌊v⌋_e s5 Z"
        if abrupt_s3: "¬ normal s3"
      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'#x003a;⪯(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)#x003a;⪯(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

      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#x003a;⪯RefT statT"
          by (rule evaln_type_sound [elim_format]) (use normal_s1 in simp)
        with normal_s1 normal_s2 eval_args 
        have conf_a_s2: "G, store s2⊨a#x003a;⪯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]) (use normal_s2 in 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#x003a;⪯(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'#x003a;⪯(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)))#x003a;-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'))#x003a;-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}|⊨#x003a;{{P} body G-≻ {Q} | ms}›
  show "G,A|⊨#x003a;{{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|⊨#x003a;{ {Normal P} .Init D. {Q} }›
  note valid_c = ‹G,A|⊨#x003a;{ {Q} .c.
 {λs.. abupd (absorb Ret) .; R←In1 (the (locals s Result))} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨Body D c#x003a;-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#x003a;⪯(G, L)"
    proof -
      from wt obtain 
        iscls_D: "is_class G D" and
        wt_init: "(prg=G,cls=accC,lcl=L)⊨Init D#x003a;√" and
        wt_c: "(prg=G,cls=accC,lcl=L)⊨c#x003a;√" 
        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#x003a;⪯(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 -
        have s1_no_jmp: "∧ j. abrupt s1 ≠ Some (Jump j)"
          by (rule eval_statement_no_jump [OF _ _ _ wt_init])
            (use eval_init [THEN evaln_eval] wf normal_s0 in 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#x003a;⪯(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Nil A P)
  show "G,A|⊨#x003a;{ {Normal (P←⌊[]⌋_l)} []≐≻ {P} }"
  proof (rule valid_expr_list_NormalI)
    fix s0 s1 vs n L Y Z
    assume conf_s0: "s0#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {Normal P} e-≻ {Q} }›
  have valid_es: "∧ v. G,A|⊨#x003a;{ {Q←⌊v⌋_e} es≐≻ {λVals:vs:. R←⌊(v # vs)⌋_l} }"
    using Cons.hyps by simp
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨e # es#x003a;≐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#x003a;⪯(G, L)"
    proof -
      from wt obtain eT esT where
        wt_e: "(prg=G,cls=accC,lcl=L)⊨e#x003a;-eT" and
        wt_es: "(prg=G,cls=accC,lcl=L)⊨es#x003a;≐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#x003a;⪯(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#x003a;⪯(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Skip A P)
  show "G,A|⊨#x003a;{ {Normal (P←♢)} .Skip. {P} }"
  proof (rule valid_stmt_NormalI)
    fix s0 s1 n L Y Z
    assume conf_s0: "s0#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {Normal P} e-≻ {Q←♢} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨Expr e#x003a;√"
    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#x003a;⪯(G, L)"
    proof -
      from wt obtain eT where 
        wt_e: "(prg = G, cls = accC, lcl = L)⊨e#x003a;-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#x003a;⪯(G,L)"
        by (rule validE)
      thus ?thesis by simp
    qed
  qed
next
  case (Lab A P c l Q)
  note valid_c = ‹G,A|⊨#x003a;{ {Normal P} .c. {abupd (absorb l) .; Q} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0: "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨l∙ c#x003a;√"
    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#x003a;⪯(G, L)"
    proof -
      from wt obtain 
        wt_c: "(prg = G, cls = accC, lcl = L)⊨c#x003a;√"
        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#x003a;⪯(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|⊨#x003a;{ {Normal P} .c1. {Q} }›
  note valid_c2 = ‹G,A|⊨#x003a;{ {Q} .c2. {R} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0:  "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨(c1;; c2)#x003a;√"
    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#x003a;⪯(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#x003a;√" and
        wt_c2: "(prg = G, cls = accC, lcl = L)⊨c2#x003a;√"
        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#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {Normal P} e-≻ {P'} }›
  have valid_then_else: "∧ b. G,A|⊨#x003a;{ {P'←=b} .(if b then c1 else c2). {Q} }"
    using If.hyps by simp
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0:  "s0#x003a;⪯(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "(prg=G,cls=accC,lcl=L)⊨If(e) c1 Else c2#x003a;√"
    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#x003a;⪯(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#x003a;-PrimT Boolean" and
        wt_then_else: "(prg=G,cls=accC,lcl=L)⊨(if the_Bool b then c1 else c2)#x003a;√"
        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#x003a;⪯(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#x003a;⪯(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|⊨#x003a;{ {P} e-≻ {P'} }›
  note valid_c = ‹G,A|⊨#x003a;{ {Normal (P'←=True)}
 .c.
 {abupd (absorb (Cont l)) .; P} }›
  show "G,A|⊨#x003a;{ {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#x003a;t"
    assume conf_s0:  "s0#x003a;⪯(G,L)"  
    assume wt: "normal s0 ==> (prg=G,cls=accC,lcl=L)⊨l∙ While(e) c#x003a;√"
    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#x003a;⪯(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.›
      have generalized:
          "∧ Y' T E.
              [t = ⟨l∙ While(e) c⟩_s; ∀t∈A. G⊨n#x003a;t; P Y' s Z; s#x003a;⪯(G, L);
               normal s ==> (prg=G,cls=accC,lcl=L)⊨t#x003a;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'")
        if "G⊨s ←-t≻←-n→ (v, s')"
        for t s s' v
        using that
      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'#x003a;t›
        note P = ‹P Y' (Norm s0') Z›
        note conf_s0' = \<open>Norm s0'\<Colon>\<preceq>(G, L)\<close>
        have wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
          using Loop.prems eqs by simp
        have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
                  dom (locals (store ((Norm s0')::state)))\<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright>E"
          using Loop.prems eqs by simp
        have evaln_e: "G\<turnstile>Norm s0' \<midarrow>e-\<succ>b\<midarrow>n'\<rightarrow> s1'" 
          using Loop.hyps eqs by simp
        show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z"
        proof -
          from wt  obtain 
            wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
            wt_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>"
            by cases (simp add: eqs)
          from da obtain E S where
            da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                     \<turnstile> dom (locals (store ((Norm s0')::state))) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
            da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                     \<turnstile> (dom (locals (store ((Norm s0')::state))) 
                            \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> S"
            by cases (simp add: eqs)
          from evaln_e 
          have eval_e: "G\<turnstile>Norm s0' \<midarrow>e-\<succ>b\<rightarrow> s1'"
            by (rule evaln_eval)
          from valid_e P valid_A conf_s0' evaln_e wt_e da_e
          obtain P': "P' \<lfloor>b\<rfloor>\<^sub>e s1' Z" and conf_s1': "s1'\<Colon>\<preceq>(G,L)"
            by (rule validE)
          show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> 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'\<leftarrow>=True)) \<lfloor>b\<rfloor>\<^sub>e s1' Z"
                by auto
              from True Loop.hyps obtain
                eval_c: "G\<turnstile>s1' \<midarrow>c\<midarrow>n'\<rightarrow> s2'" and 
                eval_while:  
                "G\<turnstile>abupd (absorb (Cont l)) s2' \<midarrow>l\<bullet> While(e) c\<midarrow>n'\<rightarrow> s3'"
                by (simp add: eqs)
              from True Loop.hyps have
                hyp: "PROP ?Hyp n' \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s 
                          (abupd (absorb (Cont l')) s2') \<diamondsuit> 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))) 
                                  \<subseteq> dom (locals (store s1'))"
                by (rule dom_locals_eval_mono_elim)
              obtain S' where
                da_c':
                "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(dom (locals (store s1')))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> S'" 
              proof -
                note s0'_s1'
                moreover
                from eval_e normal_s1' wt_e 
                have "assigns_if True e \<subseteq> dom (locals (store s1'))"
                  by (rule assigns_if_good_approx' [elim_format]) 
                    (simp add: True)
                ultimately 
                have "dom (locals (store ((Norm s0')::state)))
                           \<union> assigns_if True e \<subseteq> 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) \<diamondsuit> s2' Z" and 
                conf_s2': "s2'\<Colon>\<preceq>(G,L)"
                by (rule validE)
              hence P_s2': "P \<diamondsuit> (abupd (absorb (Cont l)) s2') Z"
                by simp
              from conf_s2'
              have conf_absorb: "abupd (absorb (Cont l)) s2' \<Colon>\<preceq>(G, L)"
                by (cases s2') (auto intro: conforms_absorb)
              moreover
              obtain E' where 
                da_while':
                "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
                     dom (locals(store (abupd (absorb (Cont l)) s2')))
                      \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright> E'"
              proof -
                note s0'_s1'
                also 
                from eval_c 
                have "G\<turnstile>s1' \<midarrow>c\<rightarrow> s2'"
                  by (rule evaln_eval)
                hence "dom (locals (store s1')) \<subseteq> dom (locals (store s2'))"
                  by (rule dom_locals_eval_mono_elim)
                also 
                have "\<dots>\<subseteq>dom (locals (store (abupd (absorb (Cont l)) s2')))"
                  by simp
                finally
                have "dom (locals (store ((Norm s0')::state))) \<subseteq> \<dots>" .
                with da show thesis
                  by (rule da_weakenE) (rule that)
              qed
              from valid_A P_s2' conf_absorb wt da_while'
              show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> 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: "\<And> j. abrupt s1' \<noteq> Some (Jump j)"
                by (rule eval_expression_no_jump 
                    [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
                  simp
              show ?thesis
              proof (cases "the_Bool b")
                case True  
                with Loop.hyps obtain
                  eval_c: "G\<turnstile>s1' \<midarrow>c\<midarrow>n'\<rightarrow> s2'" and 
                  eval_while:  
                  "G\<turnstile>abupd (absorb (Cont l)) s2' \<midarrow>l\<bullet> While(e) c\<midarrow>n'\<rightarrow> 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' = \<open>t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<close>
        note conf = \<open>(Some abr, s)\<Colon>\<preceq>(G, L)\<close>
        note P = \<open>P Y' (Some abr, s) Z\<close>
        note valid_A = \<open>\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t\<close>
        show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (undefined3 t') (Some abr, s) Z"
        proof -
          have eval_e: 
            "G\<turnstile>(Some abr,s) \<midarrow>\<langle>e\<rangle>\<^sub>e\<succ>\<midarrow>n'\<rightarrow> (undefined3 \<langle>e\<rangle>\<^sub>e,(Some abr,s))"
            by auto
          from valid_e P valid_A conf eval_e 
          have "P' (undefined3 \<langle>e\<rangle>\<^sub>e) (Some abr,s) Z"
            by (cases rule: validE [where ?P="P"]) simp+
          with t' show ?thesis
            by auto
        qed
      qed simp_all
      from eval _ valid_A P conf_s0 wt da
      have "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3 Z"
        by (rule generalized)  simp_all
      moreover
      have "s3\<Colon>\<preceq>(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|\<Turnstile>\<Colon>{ {Normal (abupd (\<lambda>a. Some (Jump j)) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P} }"
  proof (rule valid_stmt_NormalI)
    fix n s0 L accC C s1 Y Z
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
    assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Jmp j\<Colon>\<surd>"
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                    \<turnstile>dom (locals (store s0))\<guillemotright>\<langle>Jmp j\<rangle>\<^sub>s\<guillemotright>C"
    assume eval: "G\<turnstile>s0 \<midarrow>Jmp j\<midarrow>n\<rightarrow> s1"
    assume P: "(Normal (abupd (\<lambda>a. Some (Jump j)) .; P\<leftarrow>\<diamondsuit>)) Y s0 Z"
    show "P \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(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 \<diamondsuit> s1 Z"
        by simp
      moreover 
      from eval wt da conf_s0 wf
      have "s1\<Colon>\<preceq>(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 = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }\<close>
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Throw e. {Q} }"
  proof (rule valid_stmt_NormalI)
    fix n s0 L accC C s2 Y Z
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
    assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Throw e\<Colon>\<surd>"
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                    \<turnstile>dom (locals (store s0))\<guillemotright>\<langle>Throw e\<rangle>\<^sub>s\<guillemotright>C"
    assume eval: "G\<turnstile>s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> s2"
    assume P: "(Normal P) Y s0 Z"
    show "Q \<diamondsuit> s2 Z \<and> s2\<Colon>\<preceq>(G,L)"
    proof -
      from eval obtain s1 a where
        eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1" and
        s2: "s2 = abupd (throw a) s1"
        using normal_s0 by (auto elim: evaln_elim_cases)
      from wt obtain T where
        wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-T"
        by cases simp
      from da obtain E where
        da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
        by cases simp
      from valid_e P valid_A conf_s0 eval_e wt_e da_e 
      obtain "(\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>) \<lfloor>a\<rfloor>\<^sub>e s1 Z"
        by (rule validE)
      with s2 have "Q \<diamondsuit> s2 Z"
        by simp
      moreover 
      from eval wt da conf_s0 wf
      have "s2\<Colon>\<preceq>(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 = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }\<close>
  note valid_c2 = \<open>G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn} 
                           .c2. 
                          {R} }\<close>
  note Q_R = \<open>(Q \<and>. (\<lambda>s. \<not> G,s\<turnstile>catch C)) \<Rightarrow> R\<close>
  show "G,A|\<Turnstile>\<Colon>{ {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: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
    assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Try c1 Catch(C vn) c2\<Colon>\<surd>"
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                    \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<^sub>s\<guillemotright> E"
    assume eval: "G\<turnstile>s0 \<midarrow>Try c1 Catch(C vn) c2\<midarrow>n\<rightarrow> s3"
    assume P: "(Normal P) Y s0 Z"
    show "R \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
    proof -
      from eval obtain s1 s2 where
        eval_c1: "G\<turnstile>s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1" and
        sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" and
        s3: "if G,s2\<turnstile>catch C 
                then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 
                else s3 = s2"
        using normal_s0 by (fastforce elim: evaln_elim_cases)
      from wt obtain
        wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
        wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
        by cases simp
      from da obtain C1 C2 where
        da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and
        da_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class C)\<rparr>
                   \<turnstile> (dom (locals (store s0)) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2"
        by cases simp
      from valid_c1 P valid_A conf_s0 eval_c1 wt_c1 da_c1
      obtain sxQ: "(SXAlloc G Q) \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
        by (rule validE)
      from sxalloc sxQ
      have Q: "Q \<diamondsuit> s2 Z"
        by auto
      have "R \<diamondsuit> s3 Z"
      proof (cases "\<exists> x. abrupt s1 = Some (Xcpt x)")
        case False
        from sxalloc wf
        have "s2=s1"
          by (rule sxalloc_type_sound [elim_format])
             (use False in \<open>auto split: option.splits abrupt.splits\<close>)
        with False 
        have no_catch: "\<not>  G,s2\<turnstile>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\<turnstile>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\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3"
            by simp
          from conf_s1 sxalloc wf 
          have conf_s2: "s2\<Colon>\<preceq>(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\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class C"
            by (cases s2) simp
          with xcpt_s2 conf_s2 wf
          have conf_new_xcpt: "new_xcpt_var vn s2 \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class C))"
            by (auto dest: Try_lemma)
          obtain C2' where
            da_c2':
            "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class C)\<rparr>
              \<turnstile> (dom (locals (store (new_xcpt_var vn s2)))) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
          proof -
            have "(dom (locals (store s0)) \<union> {VName vn}) 
                    \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
            proof -
              from eval_c1 
              have "dom (locals (store s0)) 
                      \<subseteq> dom (locals (store s1))"
                by (rule dom_locals_evaln_mono_elim)
              also
              from sxalloc
              have "\<dots> \<subseteq> dom (locals (store s2))"
                by (rule dom_locals_sxalloc_mono)
              also 
              have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))" 
                by (cases s2) (simp add: new_xcpt_var_def, blast) 
              also
              have "{VName vn} \<subseteq> \<dots>"
                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 \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn) 
                   \<diamondsuit> (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 \<diamondsuit> s3 Z"
            by (rule validE)
        qed
      qed
      moreover 
      from eval wt da conf_s0 wf
      have "s3\<Colon>\<preceq>(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 = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }\<close>
  have valid_c2: "\<And> abr. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. abr = fst s) ;. abupd (\<lambda>x. None)} 
                                  .c2.
                                  {abupd (abrupt_if (abr \<noteq> None) abr) .; R} }"
    using Fin.hyps by simp
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1 Finally c2. {R} }"
  proof (rule valid_stmt_NormalI)
    fix n s0 L accC E s3 Y Z
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
    assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1 Finally c2\<Colon>\<surd>"
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                    \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> E"
    assume eval: "G\<turnstile>s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
    assume P: "(Normal P) Y s0 Z"
    show "R \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
    proof -
      from eval obtain s1 abr1 s2 where
        eval_c1: "G\<turnstile>s0 \<midarrow>c1\<midarrow>n\<rightarrow> (abr1, s1)" and
        eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2" and
        s3: "s3 = (if \<exists>err. abr1 = Some (Error err) 
                      then (abr1, s1)
                      else abupd (abrupt_if (abr1 \<noteq> None) abr1) s2)"
        using normal_s0 by (fastforce elim: evaln_elim_cases)
      from wt obtain
        wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
        wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
        by cases simp
      from da obtain C1 C2 where
        da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and
        da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2"
        by cases simp
      from valid_c1 P valid_A conf_s0 eval_c1 wt_c1 da_c1
      obtain Q: "Q \<diamondsuit> (abr1,s1) Z" and conf_s1: "(abr1,s1)\<Colon>\<preceq>(G,L)" 
        by (rule validE)
      from Q 
      have Q': "(Q \<and>. (\<lambda>s. abr1 = fst s) ;. abupd (\<lambda>x. None)) \<diamondsuit> (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]) (use normal_s0 in simp)
      with s3 have s3': "s3 = abupd (abrupt_if (abr1 \<noteq> None) abr1) s2"
        by (simp add: error_free_def)
      from conf_s1 
      have conf_Norm_s1: "Norm s1\<Colon>\<preceq>(G,L)"
        by (rule conforms_NormI)
      obtain C2' where 
        da_c2': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile> dom (locals (store ((Norm s1)::state))) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
      proof -
        from eval_c1 
        have "dom (locals (store s0)) \<subseteq> dom (locals (store (abr1,s1)))"
          by (rule dom_locals_evaln_mono_elim)
        hence "dom (locals (store s0)) 
                 \<subseteq> 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 \<noteq> None) abr1) .; R) \<diamondsuit> s2 Z"
        by (rule validE)
      with s3' have "R \<diamondsuit> s3 Z"
        by simp
      moreover
      from eval wt da conf_s0 wf
      have "s3\<Colon>\<preceq>(G,L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Done A P C)
  show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P} }" 
  proof (rule valid_stmt_NormalI)
    fix n s0 L accC E s3 Y Z
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
    assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>"
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                    \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Init C\<rangle>\<^sub>s\<guillemotright> E"
    assume eval: "G\<turnstile>s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
    assume P: "(Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)) Y s0 Z"
    show "P \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(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 = \<open>the (class G C) = c\<close>
  note valid_super =
        \<open>G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
                 .(if C = Object then Skip else Init (super c)). 
                 {Q} }\<close>
  have valid_init: 
        "\<And> l.  G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars Map.empty} 
                        .init c.
                        {set_lvars l .; R} }"
    using Init.hyps by simp
  show "G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C)} .Init C. {R} }"
  proof (rule valid_stmt_NormalI)
    fix n s0 L accC E s3 Y Z
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
    assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>"
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                    \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Init C\<rangle>\<^sub>s\<guillemotright> E"
    assume eval: "G\<turnstile>s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
    assume P: "(Normal (P \<and>. Not \<circ> initd C)) Y s0 Z"
    show "R \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
    proof -
      from P have not_inited: "\<not> inited C (globs (store s0))" by simp
      with eval c obtain s1 s2 where
        eval_super: 
        "G\<turnstile>Norm ((init_class_obj G C) (store s0)) 
           \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1" and
        eval_init: "G\<turnstile>(set_lvars Map.empty) s1 \<midarrow>init c\<midarrow>n\<rightarrow> 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: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                         \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
        by (cases "C=Object")
           (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
      obtain S where
        da_super:
        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
          \<turnstile> dom (locals (store ((Norm 
                            ((init_class_obj G C) (store s0)))::state))) 
               \<guillemotright>\<langle>if C = Object then Skip else Init (super c)\<rangle>\<^sub>s\<guillemotright> S"
      proof (cases "C=Object")
        case True 
        with da_Skip show ?thesis
          using that by (auto intro: assigned.select_convs)
      next
        case False 
        show ?thesis
          by (rule that) (use da_Init False in \<open>auto intro: assigned.select_convs\<close>)
      qed
      from normal_s0 conf_s0 wf cls_C not_inited
      have conf_init_cls: "(Norm ((init_class_obj G C) (store s0)))\<Colon>\<preceq>(G, L)"
        by (auto intro: conforms_init_class_obj)        
      from P 
      have P': "(Normal (P \<and>. Not \<circ> 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 \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
        by (rule validE)
      
      from cls_C wf have wt_init: "\<lparr>prg=G, cls=C,lcl=Map.empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
        by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
      from cls_C wf obtain I where 
        "\<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<^sub>s\<guillemotright> I"
        by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
       (*  simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *) 
      then obtain I' where
        da_init:
        "\<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>dom (locals (store ((set_lvars Map.empty) s1))) 
            \<guillemotright>\<langle>init c\<rangle>\<^sub>s\<guillemotright> I'"
        by (rule da_weakenE) simp
      have conf_s1_empty: "(set_lvars Map.empty) s1\<Colon>\<preceq>(G, Map.empty)"
      proof -
        from eval_super have
          "G\<turnstile>Norm ((init_class_obj G C) (store s0)) 
             \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
          by (rule evaln_eval)
        from this wt_super wf
        have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
          by - (rule eval_statement_no_jump 
                 [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"], 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 \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars Map.empty)
                  \<diamondsuit> ((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) \<diamondsuit> s2 Z"
        by (rule validE)
      with s3 l have "R \<diamondsuit> s3 Z"
        by simp
      moreover 
      from eval wt da conf_s0 wf
      have "s3\<Colon>\<preceq>(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|\<Turnstile>\<Colon>{ {Normal P} InsInitV c v=\<succ> {Q} }"
  proof (rule valid_var_NormalI)
    fix s0 vf n s1 L Z
    assume "normal s0"
    moreover
    assume "G\<turnstile>s0 \<midarrow>InsInitV c v=\<succ>vf\<midarrow>n\<rightarrow> s1"
    ultimately have "False" 
      by (cases s0) (simp add: evaln_InsInitV) 
    thus "Q \<lfloor>vf\<rfloor>\<^sub>v s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
  qed
next
  case (InsInitE A P c e Q)
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} InsInitE c e-\<succ> {Q} }"
  proof (rule valid_expr_NormalI)
    fix s0 v n s1 L Z
    assume "normal s0"
    moreover
    assume "G\<turnstile>s0 \<midarrow>InsInitE c e-\<succ>v\<midarrow>n\<rightarrow> s1"
    ultimately have "False" 
      by (cases s0) (simp add: evaln_InsInitE) 
    thus "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
  qed
next
  case (Callee A P l e Q)
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} Callee l e-\<succ> {Q} }"
  proof (rule valid_expr_NormalI)
    fix s0 v n s1 L Z
    assume "normal s0"
    moreover
    assume "G\<turnstile>s0 \<midarrow>Callee l e-\<succ>v\<midarrow>n\<rightarrow> s1"
    ultimately have "False" 
      by (cases s0) (simp add: evaln_Callee) 
    thus "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
  qed
next
  case (FinA A P a c Q)
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} .FinA a c. {Q} }"
  proof (rule valid_stmt_NormalI)
    fix s0 v n s1 L Z
    assume "normal s0"
    moreover
    assume "G\<turnstile>s0 \<midarrow>FinA a c\<midarrow>n\<rightarrow> s1"
    ultimately have "False" 
      by (cases s0) (simp add: evaln_FinA) 
    thus "Q \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
  qed
qed
declare inj_term_simps [simp del]
    
theorem ax_sound: 
 "wf_prog G \<Longrightarrow> G,(A::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> G,A|\<Turnstile>ts"
apply (subst ax_valids2_eq [symmetric])
apply  assumption
apply (erule (1) ax_sound2)
done

lemma sound_valid2_lemma: 
"\<lbrakk>\<forall>v n. Ball A (triple_valid2 G n) \<longrightarrow> P v n; Ball A (triple_valid2 G n)\<rbrakk>
 \<Longrightarrow>P v n"
by blast

end