Theory AxSound

(*  Title:      HOL/Bali/AxSound.thy
    Author:     David von Oheimb and Norbert Schirmer
*)
subsection ‹Soundness proof for Axiomatic semantics of Java expressions and 
          statements
›

theory AxSound imports AxSem begin

subsubsection "validity"

definition
  triple_valid2 :: "prog  nat  'a triple  bool"  ("___"[61,0, 58] 57)
  where
    "Gnt =
      (case t of {P} t {Q} 
        Y s Z. P Y s Z  (L. s∷≼(G,L)
           (T C A. (normal s  (prg=G,cls=C,lcl=LtT 
            prg=G,cls=C,lcl=Ldom (locals (store s))»t»A)) 
             (Y' s'. Gs t≻─n (Y',s')  Q Y' s' Z  s'∷≼(G,L)))))"

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

definition
  ax_valids2 :: "prog  'a triples  'a triples  bool"  ("_,_|⊨∷_" [61,58,58] 57)
  where "G,A|⊨∷ts = (n. (tA. Gnt)  (tts. Gnt))"

lemma triple_valid2_def2: "Gn{P} t {Q} =  
 (Y s Z. P Y s Z  (Y' s'. Gs t≻─n (Y',s')  
  (L. s∷≼(G,L)  (T C A. (normal s  (prg=G,cls=C,lcl=LtT  
                            prg=G,cls=C,lcl=Ldom (locals (store s))»t»A)) 
  Q Y' s' Z  s'∷≼(G,L)))))"
apply (unfold triple_valid2_def)
apply (simp (no_asm) add: split_paired_All)
apply blast
done

lemma triple_valid2_eq [rule_format (no_asm)]: 
  "wf_prog G ==> triple_valid2 G = triple_valid G"
apply (rule ext)
apply (rule ext)
apply (rule triple.induct)
apply (simp (no_asm) add: triple_valid_def2 triple_valid2_def2)
apply (rule iffI)
apply  fast
apply clarify
apply (tactic "smp_tac context 3 1")
apply (case_tac "normal s")
apply  clarsimp
apply  (elim conjE impE)
apply    blast

apply    (tactic "smp_tac context 2 1")
apply    (drule evaln_eval)
apply    (drule (1) eval_type_sound [THEN conjunct1],simp, assumption+)
apply    simp

apply    clarsimp
done


lemma ax_valids2_eq: "wf_prog G  G,A|⊨∷ts = G,A|⊨ts"
apply (unfold ax_valids_def ax_valids2_def)
apply (force simp add: triple_valid2_eq)
done

lemma triple_valid2_Suc [rule_format (no_asm)]: "GSuc nt  Gnt"
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: "G0{Normal P} Methd C sig-≻ {Q}"
by (auto elim!: evaln_elim_cases simp add: triple_valid2_def2)

lemma Methd_triple_valid2_SucI: 
"Gn{Normal P} body G C sig-≻{Q} 
   GSuc n{Normal P} Methd C sig-≻ {Q}"
apply (simp (no_asm_use) add: triple_valid2_def2)
apply (intro strip, tactic "smp_tac context 3 1", clarify)
apply (erule wt_elim_cases, erule da_elim_cases, erule evaln_elim_cases)
apply (unfold body_def Let_def)
apply (clarsimp simp add: inj_term_simps)
apply blast
done

lemma triples_valid2_Suc: 
 "Ball ts (triple_valid2 G (Suc n))  Ball ts (triple_valid2 G n)"
apply (fast intro: triple_valid2_Suc)
done

lemma "G|⊨n:insert t A = (Gn:t  G|⊨n:A)"
oops


subsubsection "soundness"

lemma Methd_sound: 
  assumes recursive: "G,A  {{P} Methd-≻ {Q} | ms}|⊨∷{{P} body G-≻ {Q} | ms}"
  shows "G,A|⊨∷{{P} Methd-≻ {Q} | ms}"
proof -
  {
    fix n
    assume recursive: " n. t(A  {{P} Methd-≻ {Q} | ms}). Gnt
                                t{{P} body G-≻ {Q} | ms}.  Gnt"
    have "tA. Gnt  t{{P} Methd-≻ {Q} | ms}.  Gnt"
    proof (induct n)
      case 0
      show "t{{P} Methd-≻ {Q} | ms}.  G0t"
      proof -
        {
          fix C sig
          assume "(C,sig)  ms" 
          have "G0{Normal (P C sig)} Methd C sig-≻ {Q C sig}"
            by (rule Methd_triple_valid2_0)
        }
        thus ?thesis
          by (simp add: mtriples_def split_def)
      qed
    next
      case (Suc m)
      note hyp = tA. Gmt  t{{P} Methd-≻ {Q} | ms}.  Gmt
      note prem = tA. GSuc mt
      show "t{{P} Methd-≻ {Q} | ms}.  GSuc mt"
      proof -
        {
          fix C sig
          assume m: "(C,sig)  ms" 
          have "GSuc m{Normal (P C sig)} Methd C sig-≻ {Q C sig}"
          proof -
            from prem have prem_m: "tA. Gmt"
              by (rule triples_valid2_Suc)
            hence "t{{P} Methd-≻ {Q} | ms}.  Gmt"
              by (rule hyp)
            with prem_m
            have "t(A  {{P} Methd-≻ {Q} | ms}). Gmt"
              by (simp add: ball_Un)
            hence "t{{P} body G-≻ {Q} | ms}.  Gmt"
              by (rule recursive)
            with m have "Gm{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'. Gst≻─n (Y',s')  t = c     
  Ball A (triple_valid2 G n)  (Y Z. P Y s Z   
  (L. s∷≼(G,L)  
    (T C A. (normal s  (prg=G,cls=C,lcl=LtT)  
                            prg=G,cls=C,lcl=Ldom (locals (store s))»t»A) 
    Q Y' s' Z  s'∷≼(G, L))))   
  G,A|⊨∷{ {P} c {Q}}"
apply (simp (no_asm) add: ax_valids2_def triple_valid2_def2)
apply clarsimp
done

lemma da_good_approx_evalnE [consumes 4]:
  assumes evaln: "Gs0 t≻─n (v, s1)"
     and     wt: "prg=G,cls=C,lcl=LtT"
     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 "Gs0 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.
               tA. Gnt; s0∷≼(G,L); 
               normal s0  prg=G,cls=accC,lcl=LtT;
               normal s0  prg=G,cls=accC,lcl=Ldom (locals (store s0))»t»C;
               Gs0 t≻─n (v,s1); P Y s0 Z  Q v s1 Z  s1∷≼(G,L)" 
  shows "G,A|⊨∷{ {P} t {Q} }"
apply (simp add: ax_valids2_def triple_valid2_def2)
apply (intro allI impI)
apply (case_tac "normal s")
apply   clarsimp 
apply   (rule I,(assumption|simp)+)

apply   (rule I,auto)
done
  

declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]

lemma valid_stmtI: 
   assumes I: " n s0 L accC C s1 Y Z.
             tA. Gnt; s0∷≼(G,L); 
              normal s0 prg=G,cls=accC,lcl=Lc∷√;
              normal s0prg=G,cls=accC,lcl=Ldom (locals (store s0))»cs»C;
              Gs0 cn s1; P Y s0 Z  Q  s1 Z  s1∷≼(G,L)" 
  shows "G,A|⊨∷{ {P} cs {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.
               tA. Gnt; s0∷≼(G,L); normal s0; prg=G,cls=accC,lcl=Lc∷√;
               prg=G,cls=accC,lcl=Ldom (locals (store s0))»cs»C;
               Gs0 cn s1; (Normal P) Y s0 Z  Q  s1 Z  s1∷≼(G,L)" 
  shows "G,A|⊨∷{ {Normal P} cs {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.
               tA. Gnt; s0∷≼(G,L); normal s0; 
                prg=G,cls=accC,lcl=Lt∷=T;
                prg=G,cls=accC,lcl=Ldom (locals (store s0))»tv»C;
                Gs0 t=≻vfn s1; (Normal P) Y s0 Z 
                Q (In2 vf) s1 Z  s1∷≼(G,L)"
   shows "G,A|⊨∷{ {Normal P} tv {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.
               tA. Gnt; s0∷≼(G,L); normal s0; 
                prg=G,cls=accC,lcl=Lt∷-T;
                prg=G,cls=accC,lcl=Ldom (locals (store s0))»te»C;
                Gs0 t-≻vn s1; (Normal P) Y s0 Z 
                Q (In1 v) s1 Z  s1∷≼(G,L)"
   shows "G,A|⊨∷{ {Normal P} te {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.
               tA. Gnt; s0∷≼(G,L); normal s0; 
                prg=G,cls=accC,lcl=Lt∷≐T;
                prg=G,cls=accC,lcl=Ldom (locals (store s0))»tl»C;
                Gs0 t≐≻vsn s1; (Normal P) Y s0 Z 
                 Q (In3 vs) s1 Z  s1∷≼(G,L)"
   shows "G,A|⊨∷{ {Normal P} tl {Q} }"
apply (simp add: ax_valids2_def triple_valid2_def2)
apply (intro allI impI)
apply (elim exE conjE)
apply simp
apply (rule I)
by auto

lemma validE [consumes 5]: 
  assumes valid: "G,A|⊨∷{ {P} t {Q} }"
   and    P: "P Y s0 Z"
   and    valid_A: "tA. Gnt"
   and    conf: "s0∷≼(G,L)"
   and    eval: "Gs0 t≻─n (v,s1)"
   and    wt: "normal s0  prg=G,cls=accC,lcl=LtT"
   and    da: "normal s0  prg=G,cls=accC,lcl=Ldom (locals (store s0))»t»C"
   and    elim: "Q v s1 Z; s1∷≼(G,L)  concl" 
  shows concl
using assms
by (simp add: ax_valids2_def triple_valid2_def2) fast
(* why consumes 5?. If I want to apply this lemma in a context wgere
   ¬ normal s0 holds,
   I can chain "¬ normal s0" as fact number 6 and apply the rule with
   cases. Auto will then solve premise 6 and 7.
*)

lemma all_empty: "(x. P) = P"
by simp

corollary evaln_type_sound:
  assumes evaln: "Gs0 t≻─n (v,s1)" and
             wt: "prg=G,cls=accC,lcl=LtT" and
             da: "prg=G,cls=accC,lcl=Ldom (locals (store s0)) »t» A" and
        conf_s0: "s0∷≼(G,L)" and
             wf: "wf_prog G"                         
  shows "s1∷≼(G,L)   (normal s1  G,L,store s1tv∷≼T)  
         (error_free s0 = error_free s1)"
proof -
  from evaln have "Gs0 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'. Gs t≻─n (w,s'); normal s'  normal s"
by (erule evaln_cases,auto)

declare inj_term_simps [simp]
lemma ax_sound2: 
  assumes    wf: "wf_prog G" 
    and   deriv: "G,A|⊢ts"
  shows "G,A|⊨∷ts"
using deriv
proof (induct)
  case (empty A)
  show ?case
    by (simp add: ax_valids2_def triple_valid2_def2)
next
  case (insert A t ts)
  note valid_t = G,A|⊨∷{t}
  moreover
  note valid_ts = G,A|⊨∷ts
  {
    fix n assume valid_A: "tA. Gnt"
    have "Gnt" and "tts. Gnt"
    proof -
      from valid_A valid_t show "Gnt"
        by (simp add: ax_valids2_def)
    next
      from valid_A valid_ts show "tts. Gnt"
        by (unfold ax_valids2_def) blast
    qed
    hence "t'insert t ts. Gnt'"
      by simp
  }
  thus ?case
    by (unfold ax_valids2_def) blast
next
  case (asm ts A)
  from ts  A
  show "G,A|⊨∷ts"
    by (auto simp add: ax_valids2_def triple_valid2_def)
next
  case (weaken A ts' ts)
  note G,A|⊨∷ts'
  moreover note ts  ts'
  ultimately show "G,A|⊨∷ts"
    by (unfold ax_valids2_def triple_valid2_def) blast
next
  case (conseq P A t Q)
  note con = Y s Z. P Y s Z  
              (P' Q'.
                  (G,A{P'} t {Q'}  G,A|⊨∷{ {P'} t {Q'} }) 
                  (Y' s'. (Y Z'. P' Y s Z'  Q' Y' s' Z')  Q Y' s' Z))
  show "G,A|⊨∷{ {P} t {Q} }"
  proof (rule validI)
    fix n s0 L accC T C v s1 Y Z
    assume valid_A: "tA. Gnt" 
    assume conf: "s0∷≼(G,L)"
    assume wt: "normal s0  prg=G,cls=accC,lcl=LtT"
    assume da: "normal s0 
                  prg=G,cls=accC,lcl=Ldom (locals (store s0)) »t» C"
    assume eval: "Gs0 t≻─n (v, s1)"
    assume P: "P Y s0 Z"
    show "Q v s1 Z  s1∷≼(G, L)"
    proof -
      from valid_A conf wt da eval P con
      have "Q v s1 Z"
        apply (simp add: ax_valids2_def triple_valid2_def2)
        apply (tactic "smp_tac context 3 1")
        apply clarify
        apply (tactic "smp_tac context 1 1")
        apply (erule allE,erule allE, erule mp)
        apply (intro strip)
        apply (tactic "smp_tac context 3 1")
        apply (tactic "smp_tac context 2 1")
        apply (tactic "smp_tac context 1 1")
        by blast
      moreover have "s1∷≼(G, L)"
      proof (cases "normal s0")
        case True
        from eval wt [OF True] da [OF True] conf wf 
        show ?thesis
          by (rule evaln_type_sound [elim_format]) simp
      next
        case False
        with eval have "s1=s0"
          by auto
        with conf show ?thesis by simp
      qed
      ultimately show ?thesis ..
    qed
  qed
next
  case (hazard A P t Q)
  show "G,A|⊨∷{ {P ∧. Not  type_ok G t} t {Q} }"
    by (simp add: ax_valids2_def triple_valid2_def2 type_ok_def) fast
next
  case (Abrupt A P t)
  show "G,A|⊨∷{ {Pundefined3 t ∧. Not  normal} t {P} }"
  proof (rule validI)
    fix n s0 L accC T C v s1 Y Z 
    assume conf_s0: "s0∷≼(G, L)"
    assume eval: "Gs0 t≻─n (v, s1)"
    assume "(Pundefined3 t ∧. Not  normal) Y s0 Z"
    then obtain P: "P (undefined3 t) s0 Z" and abrupt_s0: "¬ normal s0"
      by simp
    from eval abrupt_s0 obtain "s1=s0" and "v=undefined3 t"
      by auto
    with P conf_s0
    show "P v s1 Z  s1∷≼(G, L)"
      by simp
  qed
next
  case (LVar A P vn)
  show "G,A|⊨∷{ {Normal (λs.. PIn2 (lvar vn s))} LVar vn=≻ {P} }"
  proof (rule valid_var_NormalI)
    fix n s0 L accC T C vf s1 Y Z
    assume conf_s0: "s0∷≼(G, L)"
    assume normal_s0: "normal s0"
    assume wt: "prg = G, cls = accC, lcl = LLVar vn∷=T"
    assume da: "prg=G,cls=accC,lcl=L dom (locals (store s0)) »LVar vnv» C"
    assume eval: "Gs0 LVar vn=≻vfn s1" 
    assume P: "(Normal (λs.. PIn2 (lvar vn s))) Y s0 Z"
    show "P (In2 vf) s1 Z  s1∷≼(G, L)"
    proof 
      from eval normal_s0 obtain "s1=s0" "vf=lvar vn (store s0)"
        by (fastforce elim: evaln_elim_cases)
      with P show "P (In2 vf) s1 Z"
        by simp
    next
      from eval wt da conf_s0 wf
      show "s1∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
    qed
  qed
next
  case (FVar A P statDeclC Q e stat fn R accC)
  note valid_init = G,A|⊨∷{ {Normal P} .Init statDeclC. {Q} }
  note valid_e = G,A|⊨∷{ {Q} e-≻ {λVal:a:. fvar statDeclC stat fn a ..; R} }
  show "G,A|⊨∷{ {Normal P} {accC,statDeclC,stat}e..fn=≻ {R} }"
  proof (rule valid_var_NormalI)
    fix n s0 L accC' T V vf s3 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0:  "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC',lcl=L{accC,statDeclC,stat}e..fn∷=T"
    assume da: "prg=G,cls=accC',lcl=L
                   dom (locals (store s0)) »{accC,statDeclC,stat}e..fnv» V"
    assume eval: "Gs0 {accC,statDeclC,stat}e..fn=≻vfn s3"
    assume P: "(Normal P) Y s0 Z"
    show "R vfv s3 Z  s3∷≼(G, L)"
    proof -
      from wt obtain statC f where
        wt_e: "prg=G, cls=accC, lcl=Le∷-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=Ldom (locals (store s0))»ee» V"
        by cases simp
      from eval obtain a s1 s2 s2' where
        eval_init: "Gs0 Init statDeclCn s1" and 
        eval_e: "Gs1 e-≻an s2" and 
        fvar: "(vf,s2')=fvar statDeclC stat fn a s2" and
        s3: "s3 = check_field_access G accC statDeclC fn stat a s2'"
        using normal_s0 by (fastforce elim: evaln_elim_cases) 
      have wt_init: "prg=G, cls=accC, lcl=L(Init statDeclC)∷√"
      proof -
        from wf wt_e 
        have iscls_statC: "is_class G statC"
          by (auto dest: ty_expr_is_type type_is_class)
        with wf accfield 
        have iscls_statDeclC: "is_class G statDeclC"
          by (auto dest!: accfield_fields dest: fields_declC)
        thus ?thesis by simp
      qed
      obtain I where 
        da_init: "prg=G,cls=accC,lcl=L
                     dom (locals (store s0)) »Init statDeclCs» I"
        by (auto intro: da_Init [simplified] assigned.select_convs)
      from valid_init P valid_A conf_s0 eval_init wt_init da_init
      obtain Q: "Q  s1 Z" and conf_s1: "s1∷≼(G, L)"
        by (rule validE)
      obtain 
        R: "R vfv s2' Z" and 
        conf_s2: "s2∷≼(G, L)" and
        conf_a: "normal s2  G,store s2a∷≼Class statC"
      proof (cases "normal s1")
        case True
        obtain V' where 
          da_e':
          "prg=G,cls=accC,lcl=L dom (locals (store s1))»ee» 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 vfv s2' Z" and "s2∷≼(G, L)"
          by (rule validE) (simp add: fvar [symmetric])
        moreover
        from eval_e wt_e da_e' conf_s1 wf
        have "normal s2  G,store s2a∷≼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 vfv s2' Z" and "s2∷≼(G, L)"
          by (cases rule: validE) (simp add: fvar [symmetric])+
        moreover from False eval_e have "¬ normal s2"
          by auto
        hence "normal s2  G,store s2a∷≼Class statC"
          by auto
        ultimately show ?thesis ..
      qed
      from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat s3 wf
      have eq_s3_s2': "s3=s2'"  
        using normal_s0 by (auto dest!: error_free_field_access evaln_eval)
      moreover
      from eval wt da conf_s0 wf
      have "s3∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis using Q R by simp
    qed
  qed
next
  case (AVar A P e1 Q e2 R)
  note valid_e1 = G,A|⊨∷{ {Normal P} e1-≻ {Q} }
  have valid_e2: " a. G,A|⊨∷{ {QIn1 a} e2-≻ {λVal:i:. avar G i a ..; R} }"
    using AVar.hyps by simp
  show "G,A|⊨∷{ {Normal P} e1.[e2]=≻ {R} }"
  proof (rule valid_var_NormalI)
    fix n s0 L accC T V vf s2' Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=Le1.[e2]∷=T"
    assume da: "prg=G,cls=accC,lcl=L
                   dom (locals (store s0)) »e1.[e2]v» V"
    assume eval: "Gs0 e1.[e2]=≻vfn s2'"
    assume P: "(Normal P) Y s0 Z"
    show "R vfv s2' Z  s2'∷≼(G, L)"
    proof -
      from wt obtain 
        wt_e1: "prg=G,cls=accC,lcl=Le1∷-T.[]" and
        wt_e2: "prg=G,cls=accC,lcl=Le2∷-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))»e1e» E1" and
        da_e2: "prg=G,cls=accC,lcl=L nrm E1 »e2e» V"
        by (rule da_elim_cases) simp
      from eval obtain s1 a i s2 where
        eval_e1: "Gs0 e1-≻an s1" and
        eval_e2: "Gs1 e2-≻in 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 ae s1 Z" and conf_s1: "s1∷≼(G, L)"
        by (rule validE)
      from Q have Q': " v. (QIn1 a) v s1 Z"
        by simp
      have "R vfv s2' Z"
      proof (cases "normal s1")
        case True
        obtain V' where 
          "prg=G,cls=accC,lcl=L dom (locals (store s1))»e2e» V'"
        proof -
          from eval_e1  wt_e1 da_e1 wf True
          have "nrm E1  dom (locals (store s1))"
            by (cases rule: da_good_approx_evalnE) iprover
          with da_e2 show thesis
            by (rule da_weakenE) (rule that)
        qed
        with valid_e2 Q' valid_A conf_s1 eval_e2 wt_e2 
        show ?thesis
          by (rule validE) (simp add: avar)
      next
        case False
        with valid_e2 Q' valid_A conf_s1 eval_e2
        show ?thesis
          by (cases rule: validE) (simp add: avar)+
      qed
      moreover
      from eval wt da conf_s0 wf
      have "s2'∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (NewC A P C Q)
  note valid_init = G,A|⊨∷{ {Normal P} .Init C. {Alloc G (CInst C) Q} }
  show "G,A|⊨∷{ {Normal P} NewC C-≻ {Q} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC T E v s2 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=LNewC C∷-T"
    assume da: "prg=G,cls=accC,lcl=L
                   dom (locals (store s0)) »NewC Ce» E"
    assume eval: "Gs0 NewC C-≻vn s2"
    assume P: "(Normal P) Y s0 Z"
    show "Q ve s2 Z  s2∷≼(G, L)"
    proof -
      from wt obtain is_cls_C: "is_class G C" 
        by (rule wt_elim_cases) (auto dest: is_acc_classD)
      hence wt_init: "prg=G, cls=accC, lcl=LInit C∷√" 
        by auto
      obtain I where 
        da_init: "prg=G,cls=accC,lcl=L dom (locals (store s0)) »Init Cs» I"
        by (auto intro: da_Init [simplified] assigned.select_convs)
      from eval obtain s1 a where
        eval_init: "Gs0 Init Cn s1" and 
        alloc: "Gs1 ─halloc CInst Ca 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 ve s2 Z"
        by simp
      moreover
      from eval wt da conf_s0 wf
      have "s2∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (NewA A P T Q e R)
  note valid_init = G,A|⊨∷{ {Normal P} .init_comp_ty T. {Q} }
  note valid_e = G,A|⊨∷{ {Q} e-≻ {λVal:i:. abupd (check_neg i) .; 
                                            Alloc G (Arr T (the_Intg i)) R}}
  show "G,A|⊨∷{ {Normal P} New T[e]-≻ {R} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC arrT E v s3 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=LNew T[e]∷-arrT"
    assume da: "prg=G,cls=accC,lcl=Ldom (locals (store s0)) »New T[e]e» E"
    assume eval: "Gs0 New T[e]-≻vn s3"
    assume P: "(Normal P) Y s0 Z"
    show "R ve s3 Z  s3∷≼(G, L)"
    proof -
      from wt obtain
        wt_init: "prg=G,cls=accC,lcl=Linit_comp_ty T∷√" and 
        wt_e: "prg=G,cls=accC,lcl=Le∷-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)) »ee» E"
        by cases simp
      from eval obtain s1 i s2 a where
        eval_init: "Gs0 init_comp_ty Tn s1" and 
        eval_e: "Gs1 e-≻in s2" and
        alloc: "Gabupd (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=Ldom (locals (store s0)) »init_comp_ty Ts» I"
      proof (cases "C. T = Class C")
        case True
        thus ?thesis
          by - (rule that, (auto intro: da_Init [simplified] 
                                        assigned.select_convs
                              simp add: init_comp_ty_def))
         (* simplified: to rewrite ⟨Init C⟩ to In1r (Init C) *)
      next
        case False
        thus ?thesis
          by - (rule that, (auto intro: da_Skip [simplified] 
                                      assigned.select_convs
                           simp add: init_comp_ty_def))
         (* simplified: to rewrite ⟨Skip⟩ to In1r (Skip) *)
      qed
      with valid_init P valid_A conf_s0 eval_init wt_init 
      obtain Q: "Q  s1 Z" and conf_s1: "s1∷≼(G, L)"
        by (rule validE)
      obtain E' where
       "prg=G,cls=accC,lcl=L dom (locals (store s1)) »ee» 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) ie s2 Z"
        by (rule validE)
      with alloc v have "R ve s3 Z"
        by simp
      moreover 
      from eval wt da conf_s0 wf
      have "s3∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Cast A P e T Q)
  note valid_e = G,A|⊨∷{ {Normal P} e-≻ 
                 {λVal:v:. λs.. abupd (raise_if (¬ G,sv fits T) ClassCast) .;
                  QIn1 v} }
  show "G,A|⊨∷{ {Normal P} Cast T e-≻ {Q} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC castT E v s2 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=LCast T e∷-castT"
    assume da: "prg=G,cls=accC,lcl=Ldom (locals (store s0)) »Cast T ee» E"
    assume eval: "Gs0 Cast T e-≻vn s2"
    assume P: "(Normal P) Y s0 Z"
    show "Q ve s2 Z  s2∷≼(G, L)"
    proof -
      from wt obtain eT where 
        wt_e: "prg = G, cls = accC, lcl = Le∷-eT" 
        by cases simp
      from da obtain
        da_e: "prg=G,cls=accC,lcl=L dom (locals (store s0)) »ee» E"
        by cases simp
      from eval obtain s1 where
        eval_e: "Gs0 e-≻vn s1" and
        s2: "s2 = abupd (raise_if (¬ G,snd s1v 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,sv fits T) ClassCast) .;
                  QIn1 v) ve s1 Z"
        by (rule validE)
      with s2 have "Q ve s2 Z"
        by simp
      moreover
      from eval wt da conf_s0 wf
      have "s2∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Inst A P e Q T)
  assume valid_e: "G,A|⊨∷{ {Normal P} e-≻
               {λVal:v:. λs.. QIn1 (Bool (v  Null  G,sv fits RefT T))} }"
  show "G,A|⊨∷{ {Normal P} e InstOf T-≻ {Q} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC instT E v s1 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=Le InstOf T∷-instT"
    assume da: "prg=G,cls=accC,lcl=Ldom (locals (store s0))»e InstOf Te» E"
    assume eval: "Gs0 e InstOf T-≻vn s1"
    assume P: "(Normal P) Y s0 Z"
    show "Q ve s1 Z  s1∷≼(G, L)"
    proof -
      from wt obtain eT where 
        wt_e: "prg = G, cls = accC, lcl = Le∷-eT" 
        by cases simp
      from da obtain
        da_e: "prg=G,cls=accC,lcl=L dom (locals (store s0)) »ee» E"
        by cases simp
      from eval obtain a where
        eval_e: "Gs0 e-≻an s1" and
        v: "v = Bool (a  Null  G,store s1a 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.. QIn1 (Bool (v  Null  G,sv fits RefT T))) 
              ae s1 Z"
        by (rule validE)
      with v have "Q ve s1 Z"
        by simp
      moreover
      from eval wt da conf_s0 wf
      have "s1∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Lit A P v)
  show "G,A|⊨∷{ {Normal (PIn1 v)} Lit v-≻ {P} }"
  proof (rule valid_expr_NormalI)
    fix n L s0 s1 v'  Y Z
    assume conf_s0: "s0∷≼(G, L)"
    assume normal_s0: " normal s0"
    assume eval: "Gs0 Lit v-≻v'n s1"
    assume P: "(Normal (PIn1 v)) Y s0 Z"
    show "P v'e s1 Z  s1∷≼(G, L)"
    proof -
      from eval have "s1=s0" and  "v'=v"
        using normal_s0 by (auto elim: evaln_elim_cases)
      with P conf_s0 show ?thesis by simp
    qed
  qed
next
  case (UnOp A P e Q unop)
  assume valid_e: "G,A|⊨∷{ {Normal P}e-≻{λVal:v:. QIn1 (eval_unop unop v)} }"
  show "G,A|⊨∷{ {Normal P} UnOp unop e-≻ {Q} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC T E v s1 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=LUnOp unop e∷-T"
    assume da: "prg=G,cls=accC,lcl=Ldom (locals (store s0))»UnOp unop ee»E"
    assume eval: "Gs0 UnOp unop e-≻vn s1"
    assume P: "(Normal P) Y s0 Z"
    show "Q ve s1 Z  s1∷≼(G, L)"
    proof -
      from wt obtain eT where 
        wt_e: "prg = G, cls = accC, lcl = Le∷-eT" 
        by cases simp
      from da obtain
        da_e: "prg=G,cls=accC,lcl=L dom (locals (store s0)) »ee» E"
        by cases simp
      from eval obtain ve where
        eval_e: "Gs0 e-≻ven 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:. QIn1 (eval_unop unop v)) vee s1 Z"
        by (rule validE)
      with v have "Q ve s1 Z"
        by simp
      moreover
      from eval wt da conf_s0 wf
      have "s1∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (BinOp A P e1 Q binop e2 R)
  assume valid_e1: "G,A|⊨∷{ {Normal P} e1-≻ {Q} }" 
  have valid_e2: " v1.  G,A|⊨∷{ {QIn1 v1}
              (if need_second_arg binop v1 then In1l e2 else In1r Skip)
              {λVal:v2:. RIn1 (eval_binop binop v1 v2)} }"
    using BinOp.hyps by simp
  show "G,A|⊨∷{ {Normal P} BinOp binop e1 e2-≻ {R} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC T E v s2 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=LBinOp binop e1 e2∷-T"
    assume da: "prg=G,cls=accC,lcl=L
                  dom (locals (store s0)) »BinOp binop e1 e2e» E"
    assume eval: "Gs0 BinOp binop e1 e2-≻vn s2"
    assume P: "(Normal P) Y s0 Z"
    show "R ve s2 Z  s2∷≼(G, L)"
    proof -
      from wt obtain e1T e2T where
        wt_e1: "prg=G,cls=accC,lcl=Le1∷-e1T" and
        wt_e2: "prg=G,cls=accC,lcl=Le2∷-e2T" and
        wt_binop: "wt_binop G binop e1T e2T" 
        by cases simp
      have wt_Skip: "prg = G, cls = accC, lcl = LSkip∷√"
        by simp
      (*
      obtain S where
        daSkip: "⦇prg=G,cls=accC,lcl=L⦈
                   ⊢ dom (locals (store s1)) »In1r Skip» S"
        by (auto intro: da_Skip [simplified] assigned.select_convs) *)
      from da obtain E1 where
        da_e1: "prg=G,cls=accC,lcl=L  dom (locals (store s0)) »e1e» E1"
        by cases simp+
      from eval obtain v1 s1 v2 where
        eval_e1: "Gs0 e1-≻v1n s1" and
        eval_e2: "Gs1 (if need_second_arg binop v1 then e2e else Skips)
                        ≻─n (v2e, 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 v1e s1 Z" and conf_s1: "s1∷≼(G,L)"
        by (rule validE)
      from Q have Q': " v. (QIn1 v1) v s1 Z"
        by simp
      have "(λVal:v2:. RIn1 (eval_binop binop v1 v2)) v2e s2 Z"
      proof (cases "normal s1")
        case True
        from eval_e1 wt_e1 da_e1 conf_s0 wf
        have conf_v1: "G,store s1v1∷≼e1T" 
          by (rule evaln_type_sound [elim_format]) (insert True,simp)
        from eval_e1 
        have "Gs0 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 e2e else Skips)» 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 e2e else Skips)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 ve s2 Z"
        by simp
      moreover
      from eval wt da conf_s0 wf
      have "s2∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Super A P)
  show "G,A|⊨∷{ {Normal (λs.. PIn1 (val_this s))} Super-≻ {P} }"
  proof (rule valid_expr_NormalI)
    fix n L s0 s1 v  Y Z
    assume conf_s0: "s0∷≼(G, L)"
    assume normal_s0: " normal s0"
    assume eval: "Gs0 Super-≻vn s1"
    assume P: "(Normal (λs.. PIn1 (val_this s))) Y s0 Z"
    show "P ve s1 Z  s1∷≼(G, L)"
    proof -
      from eval have "s1=s0" and  "v=val_this (store s0)"
        using normal_s0 by (auto elim: evaln_elim_cases)
      with P conf_s0 show ?thesis by simp
    qed
  qed
next
  case (Acc A P var Q)
  note valid_var = G,A|⊨∷{ {Normal P} var=≻ {λVar:(v, f):. QIn1 v} }
  show "G,A|⊨∷{ {Normal P} Acc var-≻ {Q} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC T E v s1 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=LAcc var∷-T"
    assume da: "prg=G,cls=accC,lcl=Ldom (locals (store s0))»Acc vare»E"
    assume eval: "Gs0 Acc var-≻vn s1"
    assume P: "(Normal P) Y s0 Z"
    show "Q ve s1 Z  s1∷≼(G, L)"
    proof -
      from wt obtain 
        wt_var: "prg=G,cls=accC,lcl=Lvar∷=T" 
        by cases simp
      from da obtain V where 
        da_var: "prg=G,cls=accC,lcl=L  dom (locals (store s0)) »varv» V"
        by (cases " n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
      from eval obtain upd where
        eval_var: "Gs0 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):. QIn1 v) (v, upd)v s1 Z"
        by (rule validE)
      then have "Q ve s1 Z"
        by simp
      moreover
      from eval wt da conf_s0 wf
      have "s1∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Ass A P var Q e R)
  note valid_var = G,A|⊨∷{ {Normal P} var=≻ {Q} }
  have valid_e: " vf. 
                  G,A|⊨∷{ {QIn2 vf} e-≻ {λVal:v:. assign (snd vf) v .; R} }"
    using Ass.hyps by simp
  show "G,A|⊨∷{ {Normal P} var:=e-≻ {R} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC T E v s3 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=Lvar:=e∷-T"
    assume da: "prg=G,cls=accC,lcl=Ldom (locals (store s0))»var:=ee»E"
    assume eval: "Gs0 var:=e-≻vn s3"
    assume P: "(Normal P) Y s0 Z"
    show "R ve s3 Z  s3∷≼(G, L)"
    proof -
      from wt obtain varT  where
        wt_var: "prg=G,cls=accC,lcl=Lvar∷=varT" and
        wt_e: "prg=G,cls=accC,lcl=Le∷-T" 
        by cases simp
      from eval obtain w upd s1 s2 where
        eval_var: "Gs0 var=≻(w, upd)n s1" and
        eval_e: "Gs1 e-≻vn s2" and
        s3: "s3=assign upd v s2"
        using normal_s0 by (auto elim: evaln_elim_cases)
      have "R ve 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)) »varv» V" and
          da_e:   "prg=G,cls=accC,lcl=L  nrm V »ee» E"
          by cases simp+
        from valid_var P valid_A conf_s0 eval_var wt_var da_var
        obtain Q: "Q (w,upd)v s1 Z" and conf_s1: "s1∷≼(G,L)"  
          by (rule validE) 
        hence Q': " v. (QIn2 (w,upd)) v s1 Z"
          by simp
        have "(λVal:v:. assign (snd (w,upd)) v .; R) ve s2 Z"
        proof (cases "normal s1")
          case True
          obtain E' where 
            da_e': "prg=G,cls=accC,lcl=L dom (locals (store s1)) »ee» 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 ve 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)) »ee» E"
          by cases simp+
        from da.LVar vn obtain  V where
          da_var: "prg=G,cls=accC,lcl=L
                       dom (locals (store s0)) »varv» V"
          by auto
        from valid_var P valid_A conf_s0 eval_var wt_var da_var
        obtain Q: "Q (w,upd)v s1 Z" and conf_s1: "s1∷≼(G,L)"  
          by (rule validE) 
        hence Q': " v. (QIn2 (w,upd)) v s1 Z"
          by simp
        have "(λVal:v:. assign (snd (w,upd)) v .; R) ve s2 Z"
        proof (cases "normal s1")
          case True
          obtain E' where
            da_e': "prg=G,cls=accC,lcl=L
                        dom (locals (store s1)) »ee» 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 ve s3 Z"
          by simp
      qed
      moreover
      from eval wt da conf_s0 wf
      have "s3∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Cond A P e0 P' e1 e2 Q)
  note valid_e0 = G,A|⊨∷{ {Normal P} e0-≻ {P'} }
  have valid_then_else:" b.  G,A|⊨∷{ {P'←=b} (if b then e1 else e2)-≻ {Q} }"
    using Cond.hyps by simp
  show "G,A|⊨∷{ {Normal P} e0 ? e1 : e2-≻ {Q} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC T E v s2 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=Le0 ? e1 : e2∷-T"
    assume da: "prg=G,cls=accC,lcl=Ldom (locals (store s0))»e0 ? e1:e2e»E"
    assume eval: "Gs0 e0 ? e1 : e2-≻vn s2"
    assume P: "(Normal P) Y s0 Z"
    show "Q ve s2 Z  s2∷≼(G, L)"
    proof -
      from wt obtain T1 T2 where
        wt_e0: "prg=G,cls=accC,lcl=Le0∷-PrimT Boolean" and
        wt_e1: "prg=G,cls=accC,lcl=Le1∷-T1" and
        wt_e2: "prg=G,cls=accC,lcl=Le2∷-T2" 
        by cases simp
      from da obtain E0 E1 E2 where
        da_e0: "prg=G,cls=accC,lcl=L dom (locals (store s0)) »e0e» E0" and
        da_e1: "prg=G,cls=accC,lcl=L
                 (dom (locals (store s0))  assigns_if True e0)»e1e» E1" and
        da_e2: "prg=G,cls=accC,lcl=L
                 (dom (locals (store s0))  assigns_if False e0)»e2e» E2"
        by cases simp+
      from eval obtain b s1 where
        eval_e0: "Gs0 e0-≻bn s1" and
        eval_then_else: "Gs1 (if the_Bool b then e1 else e2)-≻vn 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' be s1 Z" and conf_s1: "s1∷≼(G,L)"  
        by (rule validE)
      hence P': " v. (P'←=(the_Bool b)) v s1 Z"
        by (cases "normal s1") auto
      have "Q ve s2 Z"
      proof (cases "normal s1")
        case True
        note normal_s1=this
        from wt_e1 wt_e2 obtain T' where
          wt_then_else: 
          "prg=G,cls=accC,lcl=L(if the_Bool b then e1 else e2)∷-T'"
          by (cases "the_Bool b") simp+
        have s0_s1: "dom (locals (store s0)) 
                       assigns_if (the_Bool b) e0  dom (locals (store s1))"
        proof -
          from eval_e0 
          have eval_e0': "Gs0 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 e2e» E'"
        proof (cases "the_Bool b")
          case True
          with that da_e1 s0_s1 show ?thesis
            by simp (erule da_weakenE,auto)
        next
          case False
          with that da_e2 s0_s1 show ?thesis
            by simp (erule da_weakenE,auto)
        qed
        with valid_then_else P' valid_A conf_s1 eval_then_else wt_then_else
        show ?thesis
          by (rule validE)
      next
        case False
        with valid_then_else P' valid_A conf_s1 eval_then_else
        show ?thesis
          by (cases rule: validE) iprover+
      qed
      moreover
      from eval wt da conf_s0 wf
      have "s2∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      ultimately show ?thesis ..
    qed
  qed
next
  case (Call A P e Q args R mode statT mn pTs' S accC')
  note valid_e = G,A|⊨∷{ {Normal P} e-≻ {Q} }
  have valid_args: " a. G,A|⊨∷{ {QIn1 a} args≐≻ {R a} }"
    using Call.hyps by simp
  have valid_methd: " a vs invC declC l.
        G,A|⊨∷{ {R aIn3 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  GmodeinvCstatT)}
            Methd declC name=mn,parTs=pTs'-≻ {set_lvars l .; S} }"
    using Call.hyps by simp
  show "G,A|⊨∷{ {Normal P} {accC',statT,mode}emn( {pTs'}args)-≻ {S} }"
  proof (rule valid_expr_NormalI)
    fix n s0 L accC T E v s5 Y Z
    assume valid_A: "tA. Gnt"
    assume conf_s0: "s0∷≼(G,L)"  
    assume normal_s0: "normal s0"
    assume wt: "prg=G,cls=accC,lcl=L{accC',statT,mode}emn( {pTs'}args)∷-T"
    assume da: "prg=G,cls=accC,lcl=Ldom (locals (store s0))
                   »{accC',statT,mode}emn( {pTs'}args)e» E"
    assume eval: "Gs0 {accC',statT,mode}emn( {pTs'}args)-≻vn s5"
    assume P: "(Normal P) Y s0 Z"
    show "S ve s5 Z  s5∷≼(G, L)"
    proof -
      from wt obtain pTs statDeclT statM where
                 wt_e: "prg=G,cls=accC,lcl=Le∷-RefT statT" and
              wt_args: "prg=G,cls=accC,lcl=Largs∷≐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)))»ee» C" and
        da_args: "prg=G,cls=accC,lcl=L nrm C »argsl» E" 
        by cases simp
      from eval eq_accC_accC' obtain a s1 vs s2 s3 s3' s4 invDeclC where
        evaln_e: "Gs0 e-≻an s1" and
        evaln_args: "Gs1 args≐≻vsn 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:
           "Gs3' Methd invDeclC  name=mn,parTs=pTs'-≻vn 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: "Gs0 e-≻a s1"
        by (rule evaln_eval)
      
      from eval_e _ wt_e wf
      have s1_no_return: "abrupt s1  Some (Jump Ret)"
        by (rule eval_expression_no_jump 
                 [where ?Env="prg=G,cls=accC,lcl=L",simplified])
           (insert normal_s0,auto)

      from valid_e P valid_A conf_s0 evaln_e wt_e da_e
      obtain "Q ae s1 Z" and conf_s1: "s1∷≼(G,L)"
        by (rule validE)
      hence Q: " v. (QIn1 a) v s1 Z"
        by simp
      obtain 
        R: "(R a) vsl s2 Z" and 
        conf_s2: "s2∷≼(G,L)" and 
        s2_no_return: "abrupt s2  Some (Jump Ret)"
      proof (cases "normal s1")
        case True
        obtain E' where 
          da_args':
          "prg=G,cls=accC,lcl=L dom (locals (store s1)) »argsl» 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) vsl s2 Z" "s2∷≼(G,L)" 
          by (rule validE)
        moreover
        from evaln_args
        have e: "Gs1 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) vsl s2 Z" "s2∷≼(G,L)" 
          by (cases rule: validE) iprover+
        moreover
        from False evaln_args have "s2=s1"
          by auto
        with s1_no_return have "abrupt s2  Some (Jump Ret)"
          by simp
        ultimately show ?thesis ..
      qed

      obtain invC where
        invC: "invC = invocation_class mode (store s2) a statT"
        by simp
      with s3
      have invC': "invC = (invocation_class mode (store s3) a statT)"
        by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
      obtain l where
        l: "l = locals (store s2)"
        by simp

      from eval wt da conf_s0 wf
      have conf_s5: "s5∷≼(G, L)"
        by (rule evaln_type_sound [elim_format]) simp
      let "PROP ?R" = " v.
             (R aIn3 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  GmodeinvCstatT)
               ) v s3' Z"
      {
        assume abrupt_s3: "¬ normal s3"
        have "S ve s5 Z"
        proof -
          from abrupt_s3 check have eq_s3'_s3: "s3'=s3"
            by (auto simp add: check_method_access_def Let_def)
          with R s3 invDeclC invC l abrupt_s3
          have R': "PROP ?R"
            by auto
          have conf_s3': "s3'∷≼(G, Map.empty)"
           (* we need an arbirary environment (here empty) that s2' conforms to
              to apply validE *)
          proof -
            from s2_no_return s3
            have "abrupt s3  Some (Jump Ret)"
              by (cases s2) (auto simp add: init_lvars_def2 split: if_split_asm)
            moreover
            obtain abr2 str2 where s2: "s2=(abr2,str2)"
              by (cases s2)
            from s3 s2 conf_s2 have "(abrupt s3,str2)∷≼(G, L)"
              by (auto simp add: init_lvars_def2 split: if_split_asm)
            ultimately show ?thesis
              using s3 s2 eq_s3'_s3
              apply (simp add: init_lvars_def2)
              apply (rule conforms_set_locals [OF _ wlconf_empty])
              by auto
          qed
          from valid_methd R' valid_A conf_s3' evaln_methd abrupt_s3 eq_s3'_s3
          have "(set_lvars l .; S) ve s4 Z"
            by (cases rule: validE) simp+
          with s5 l show ?thesis
            by simp
        qed
      } note abrupt_s3_lemma = this

      have "S ve 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)) »argsl» 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: "Gs1 args≐≻vs s2"
          by (rule evaln_eval)
        from evaln_e wt_e da_e conf_s0 wf
        have conf_a: "G, store s1a∷≼RefT statT"
          by (rule evaln_type_sound [elim_format]) (insert normal_s1,simp)
        with normal_s1 normal_s2 eval_args 
        have conf_a_s2: "G, store s2a∷≼RefT statT"
          by (auto dest: eval_gext)
        from evaln_args wt_args da_args' conf_s1 wf
        have conf_args: "list_all2 (conf G (store s2)) vs pTs"
          by (rule evaln_type_sound [elim_format]) (insert normal_s2,simp)
        from statM 
        obtain
          statM': "(statDeclT,statM)mheads G accC statT name=mn,parTs=pTs'" 
          and
          pTs_widen: "GpTs[≼]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: "GmodeinvCstatT"
            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: "GinvCC invDeclC" and
             resTy_widen: "GresTy dynMresTy 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  GinvCC statC
               else ((statC. statT = ClassT statC  GstatCC invDeclC) 
                     (statC. statT  ClassT statC  invDeclC = Object)) 
                      statDeclT = ClassT invDeclC)"
            by (cases rule: DynT_mheadsE) simp
          obtain L' where 
            L':"L'=(λ k. 
                    (case k of
                       EName e
                        (case e of 
                             VNam v 
                             ((table_of (lcls (mbody (mthd dynM))))
                                (pars (mthd dynM)[↦]pTs')) v
                           | Res  Some (resTy dynM))
                     | This  if is_static statM 
                               then None else Some (Class invDeclC)))"
            by simp
          from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
            wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
          have conf_s3: "s3∷≼(G,L')"
            apply - 
               (* FIXME confomrs_init_lvars should be 
                  adjusted to be more directy applicable *)
            apply (drule conforms_init_lvars [of G invDeclC 
                    "name=mn,parTs=pTs'" dynM "store s2" vs pTs "abrupt s2" 
                    L statT invC a "(statDeclT,statM)" e])
            apply (rule wf)
            apply (rule conf_args)
            apply (simp add: pTs_widen)
            apply (cases s2,simp)
            apply (rule dynM')
            apply (force dest: ty_expr_is_type)
            apply (rule invC_widen)
            apply (force dest: eval_gext)
            apply simp
            apply simp
            apply (simp add: invC)
            apply (simp add: invDeclC)
            apply (simp add: normal_s2)
            apply (cases s2, simp add: L' init_lvars_def2 s3
                             cong add: lname.case_cong ename.case_cong)
            done
          with eq_s3'_s3 have conf_s3': "s3'∷≼(G,L')" by simp
          from is_static_eq wf_dynM L'
          obtain mthdT where
            "prg=G,cls=invDeclC,lcl=L'
               Body invDeclC (stmt (mbody (mthd dynM)))∷-mthdT" and
            mthdT_widen: "GmthdTresTy dynM"
            by - (drule wf_mdecl_bodyD,
                  auto simp add: callee_lcl_def  
                       cong add: lname.case_cong ename.case_cong)
          with dynM' iscls_invDeclC invDeclC'
          have
            wt_methd:
            "prg=G,cls=invDeclC,lcl=L'
               (Methd invDeclC name = mn, parTs = pTs')∷-mthdT"
            by (auto intro: wt.Methd)
          obtain M where 
            da_methd:
            "prg=G,cls=invDeclC,lcl=L' 
                dom (locals (store s3')) 
                   »Methd invDeclC name=mn,parTs=pTs'e» M"
          proof -
            from wf_dynM
            obtain M' where
              da_body: 
              "prg=G, cls=invDeclC
               ,lcl=callee_lcl invDeclC name = mn, parTs = pTs' (mthd dynM)
                 parameters (mthd dynM) »stmt (mbody (mthd dynM))» M'" and
              res: "Result  nrm M'"
              by (rule wf_mdeclE) iprover
            from da_body is_static_eq L' have
              "prg=G, cls=invDeclC,lcl=L' 
                  parameters (mthd dynM) »stmt (mbody (mthd dynM))» M'"
              by (simp add