Theory Progress

(*  Title:      JinjaDCI/J/Progress.thy

    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory J/Progress.thy by Tobias Nipkow
*)

section ‹ Progress of Small Step Semantics ›

theory Progress
imports WellTypeRT DefAss "../Common/Conform" EConform
begin

lemma final_addrE:
  "⟦ P,E,h,sh ⊢ e : Class C; final e;
    ⋀a. e = addr a ⟹ R;
    ⋀a. e = Throw a ⟹ R ⟧ ⟹ R"
(*<*)by(auto simp:final_def)(*>*)


lemma finalRefE:
 "⟦ P,E,h,sh ⊢ e : T; is_refT T; final e;
   e = null ⟹ R;
   ⋀a C. ⟦ e = addr a; T = Class C ⟧ ⟹ R;
   ⋀a. e = Throw a ⟹ R ⟧ ⟹ R"
(*<*)by(auto simp:final_def is_refT_def)(*>*)


text‹ Derivation of new induction scheme for well typing: ›

inductive
  WTrt' :: "[J_prog,heap,sheap,env,expr,ty] ⇒ bool"
  and WTrts' :: "[J_prog,heap,sheap,env,expr list, ty list] ⇒ bool"
  and WTrt2' :: "[J_prog,env,heap,sheap,expr,ty] ⇒ bool"
        ("_,_,_,_ ⊢ _ :'' _"   [51,51,51,51]50)
  and WTrts2' :: "[J_prog,env,heap,sheap,expr list, ty list] ⇒ bool"
        ("_,_,_,_ ⊢ _ [:''] _" [51,51,51,51]50)
  for P :: J_prog and h :: heap and sh :: sheap
where
  "P,E,h,sh ⊢ e :' T ≡ WTrt' P h sh E e T"
| "P,E,h,sh ⊢ es [:'] Ts ≡ WTrts' P h sh E es Ts"

| "is_class P C  ⟹  P,E,h,sh ⊢ new C :' Class C"
| "⟦ P,E,h,sh ⊢ e :' T; is_refT T; is_class P C ⟧
  ⟹ P,E,h,sh ⊢ Cast C e :' Class C"
| "typeof⇘h⇙ v = Some T ⟹ P,E,h,sh ⊢ Val v :' T"
| "E v = Some T  ⟹  P,E,h,sh ⊢ Var v :' T"
| "⟦ P,E,h,sh ⊢ e⇩1 :' T⇩1;  P,E,h,sh ⊢ e⇩2 :' T⇩2 ⟧
  ⟹ P,E,h,sh ⊢ e⇩1 «Eq» e⇩2 :' Boolean"
| "⟦ P,E,h,sh ⊢ e⇩1 :' Integer;  P,E,h,sh ⊢ e⇩2 :' Integer ⟧
  ⟹ P,E,h,sh ⊢ e⇩1 «Add» e⇩2 :' Integer"
| "⟦ P,E,h,sh ⊢ Var V :' T;  P,E,h,sh ⊢ e :' T';  P ⊢ T' ≤ T ⟧
  ⟹ P,E,h,sh ⊢ V:=e :' Void"
| "⟦ P,E,h,sh ⊢ e :' Class C; P ⊢ C has F,NonStatic:T in D ⟧ ⟹ P,E,h,sh ⊢ e∙F{D} :' T"
| "P,E,h,sh ⊢ e :' NT ⟹ P,E,h,sh ⊢ e∙F{D} :' T"
| "⟦ P ⊢ C has F,Static:T in D ⟧ ⟹ P,E,h,sh ⊢ C∙⇩sF{D} :' T"
| "⟦ P,E,h,sh ⊢ e⇩1 :' Class C;  P ⊢ C has F,NonStatic:T in D;
    P,E,h,sh ⊢ e⇩2 :' T⇩2;  P ⊢ T⇩2 ≤ T ⟧
  ⟹ P,E,h,sh ⊢ e⇩1∙F{D}:=e⇩2 :' Void"
| "⟦ P,E,h,sh ⊢ e⇩1:'NT; P,E,h,sh ⊢ e⇩2 :' T⇩2 ⟧ ⟹ P,E,h,sh ⊢ e⇩1∙F{D}:=e⇩2 :' Void"
| "⟦ P ⊢ C has F,Static:T in D;
    P,E,h,sh ⊢ e⇩2 :' T⇩2;  P ⊢ T⇩2 ≤ T ⟧
  ⟹ P,E,h,sh ⊢ C∙⇩sF{D}:=e⇩2 :' Void"
| "⟦ P,E,h,sh ⊢ e :' Class C; P ⊢ C sees M,NonStatic:Ts → T = (pns,body) in D;
    P,E,h,sh ⊢ es [:'] Ts'; P ⊢ Ts' [≤] Ts ⟧
  ⟹ P,E,h,sh ⊢ e∙M(es) :' T"
| "⟦ P,E,h,sh ⊢ e :' NT; P,E,h,sh ⊢ es [:'] Ts ⟧ ⟹ P,E,h,sh ⊢ e∙M(es) :' T"
| "⟦ P ⊢ C sees M,Static:Ts → T = (pns,body) in D;
    P,E,h,sh ⊢ es [:'] Ts'; P ⊢ Ts' [≤] Ts;
    M = clinit ⟶ sh D = ⌊(sfs,Processing)⌋ ∧ es = map Val vs ⟧
  ⟹ P,E,h,sh ⊢ C∙⇩sM(es) :' T"
| "P,E,h,sh ⊢ [] [:'] []"
| "⟦ P,E,h,sh ⊢ e :' T;  P,E,h,sh ⊢ es [:'] Ts ⟧ ⟹  P,E,h,sh ⊢ e#es [:'] T#Ts"
| "⟦ typeof⇘h⇙ v = Some T⇩1; P ⊢ T⇩1 ≤ T; P,E(V↦T),h,sh ⊢ e⇩2 :' T⇩2 ⟧
  ⟹  P,E,h,sh ⊢ {V:T := Val v; e⇩2} :' T⇩2"
| "⟦ P,E(V↦T),h,sh ⊢ e :' T'; ¬ assigned V e ⟧ ⟹  P,E,h,sh ⊢ {V:T; e} :' T'"
| "⟦ P,E,h,sh ⊢ e⇩1:' T⇩1;  P,E,h,sh ⊢ e⇩2:'T⇩2 ⟧  ⟹  P,E,h,sh ⊢ e⇩1;;e⇩2 :' T⇩2"
| "⟦ P,E,h,sh ⊢ e :' Boolean;  P,E,h,sh ⊢ e⇩1:' T⇩1;  P,E,h,sh ⊢ e⇩2:' T⇩2;
    P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1;
    P ⊢ T⇩1 ≤ T⇩2 ⟶ T = T⇩2; P ⊢ T⇩2 ≤ T⇩1 ⟶ T = T⇩1 ⟧
  ⟹ P,E,h,sh ⊢ if (e) e⇩1 else e⇩2 :' T"
| "⟦ P,E,h,sh ⊢ e :' Boolean;  P,E,h,sh ⊢ c:' T ⟧
  ⟹  P,E,h,sh ⊢ while(e) c :' Void"
| "⟦ P,E,h,sh ⊢ e :' T⇩r; is_refT T⇩r ⟧  ⟹  P,E,h,sh ⊢ throw e :' T"
| "⟦ P,E,h,sh ⊢ e⇩1 :' T⇩1;  P,E(V ↦ Class C),h,sh ⊢ e⇩2 :' T⇩2; P ⊢ T⇩1 ≤ T⇩2 ⟧
  ⟹ P,E,h,sh ⊢ try e⇩1 catch(C V) e⇩2 :' T⇩2"
| "⟦ P,E,h,sh ⊢ e :' T; ∀C' ∈ set (C#Cs). is_class P C'; ¬sub_RI e;
     ∀C' ∈ set (tl Cs). ∃sfs. sh C' = ⌊(sfs,Processing)⌋;
     b ⟶ (∀C' ∈ set Cs. ∃sfs. sh C' = ⌊(sfs,Processing)⌋);
     distinct Cs; supercls_lst P Cs ⟧ ⟹ P,E,h,sh ⊢ INIT C (Cs, b) ← e :' T"
| "⟦ P,E,h,sh ⊢ e :' T; P,E,h,sh ⊢ e' :' T'; ∀C' ∈ set (C#Cs). is_class P C'; ¬sub_RI e';
     ∀C' ∈ set (C#Cs). not_init C' e;
     ∀C' ∈ set Cs. ∃sfs. sh C' = ⌊(sfs,Processing)⌋;
     ∃sfs. sh C = ⌊(sfs, Processing)⌋ ∨ (sh C = ⌊(sfs, Error)⌋ ∧ e = THROW NoClassDefFoundError);
     distinct (C#Cs); supercls_lst P (C#Cs) ⟧
  ⟹ P,E,h,sh ⊢ RI(C, e);Cs ← e' :' T'"

(*<*)
lemmas WTrt'_induct = WTrt'_WTrts'.induct [split_format (complete)]
  and WTrt'_inducts = WTrt'_WTrts'.inducts [split_format (complete)]

inductive_cases WTrt'_elim_cases[elim!]:
  "P,E,h,sh ⊢ V :=e :' T"
(*>*)

lemma [iff]: "P,E,h,sh ⊢ e⇩1;;e⇩2 :' T⇩2 = (∃T⇩1. P,E,h,sh ⊢ e⇩1:' T⇩1 ∧ P,E,h,sh ⊢ e⇩2:' T⇩2)"
(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)

lemma [iff]: "P,E,h,sh ⊢ Val v :' T = (typeof⇘h⇙ v = Some T)"
(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)

lemma [iff]: "P,E,h,sh ⊢ Var v :' T = (E v = Some T)"
(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)


lemma wt_wt': "P,E,h,sh ⊢ e : T ⟹ P,E,h,sh ⊢ e :' T"
and wts_wts': "P,E,h,sh ⊢ es [:] Ts ⟹ P,E,h,sh ⊢ es [:'] Ts"
(*<*)
proof(induct rule:WTrt_inducts)
  case (WTrtBlock E V T e T')
  then show ?case
  proof(cases "assigned V e")
    case True then show ?thesis using WTrtBlock.hyps(2)
      by(clarsimp simp add:fun_upd_same assigned_def WTrt'_WTrts'.intros
                  simp del:fun_upd_apply)
  next
    case False then show ?thesis
      by (simp add: WTrtBlock.hyps(2) WTrt'_WTrts'.intros)
  qed
qed (blast intro:WTrt'_WTrts'.intros)+
(*>*)


lemma wt'_wt: "P,E,h,sh ⊢ e :' T ⟹ P,E,h,sh ⊢ e : T"
and wts'_wts: "P,E,h,sh ⊢ es [:'] Ts ⟹ P,E,h,sh ⊢ es [:] Ts"
(*<*)
proof(induct rule:WTrt'_inducts)
  case Block: (19 v T⇩1 T E V e⇩2 T⇩2)
  let ?E = "E(V ↦ T)"
  have "P,?E,h,sh ⊢ Val v : T⇩1" using Block.hyps(1) by simp
  moreover have "P ⊢ T⇩1 ≤ T" by(rule Block.hyps(2))
  ultimately have "P,?E,h,sh ⊢ V:=Val v : Void" using WTrtLAss by simp
  moreover have "P,?E,h,sh ⊢ e⇩2 : T⇩2" by(rule Block.hyps(4))
  ultimately have "P,?E,h,sh ⊢ V:=Val v;; e⇩2 : T⇩2" by blast
  then show ?case by simp
qed (blast intro:WTrt_WTrts.intros)+
(*>*)


corollary wt'_iff_wt: "(P,E,h,sh ⊢ e :' T) = (P,E,h,sh ⊢ e : T)"
(*<*)by(blast intro:wt_wt' wt'_wt)(*>*)


corollary wts'_iff_wts: "(P,E,h,sh ⊢ es [:'] Ts) = (P,E,h,sh ⊢ es [:] Ts)"
(*<*)by(blast intro:wts_wts' wts'_wts)(*>*)

(*<*)
lemmas WTrt_inducts2 = WTrt'_inducts [unfolded wt'_iff_wt wts'_iff_wts,
 case_names WTrtNew WTrtCast WTrtVal WTrtVar WTrtBinOpEq WTrtBinOpAdd WTrtLAss
 WTrtFAcc WTrtFAccNT WTrtSFAcc WTrtFAss WTrtFAssNT WTrtSFAss WTrtCall WTrtCallNT WTrtSCall
 WTrtNil WTrtCons WTrtInitBlock WTrtBlock WTrtSeq WTrtCond WTrtWhile WTrtThrow WTrtTry
 WTrtInit WTrtRI, consumes 1]
(*>*)

theorem assumes wf: "wwf_J_prog P" and hconf: "P ⊢ h √" and shconf: "P,h ⊢⇩s sh √"
shows progress: "P,E,h,sh ⊢ e : T ⟹
 (⋀l. ⟦ 𝒟 e ⌊dom l⌋; P,sh ⊢⇩b (e,b) √; ¬ final e ⟧ ⟹ ∃e' s' b'. P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',s',b'⟩)"
and "P,E,h,sh ⊢ es [:] Ts ⟹
 (⋀l. ⟦ 𝒟s es ⌊dom l⌋; P,sh ⊢⇩b (es,b) √; ¬ finals es ⟧ ⟹ ∃es' s' b'. P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',s',b'⟩)"
(*<*)
proof (induct rule:WTrt_inducts2)
  case (WTrtNew C) show ?case
  proof (cases b)
    case True then show ?thesis
    proof cases
      assume "∃a. h a = None"
      with assms WTrtNew True show ?thesis
        by (fastforce del:exE intro!:RedNew simp add:new_Addr_def
                     elim!:wf_Fields_Ex[THEN exE])
    next
      assume "¬(∃a. h a = None)"
      with assms WTrtNew True show ?thesis
        by(fastforce intro:RedNewFail simp:new_Addr_def)
    qed
  next
    case False then show ?thesis
    proof cases
      assume "∃sfs. sh C = Some (sfs, Done)"
      with assms WTrtNew False show ?thesis
        by(fastforce intro:NewInitDoneRed simp:new_Addr_def)
    next
      assume "∄sfs. sh C = Some (sfs, Done)"
      with assms WTrtNew False show ?thesis
        by(fastforce intro:NewInitRed simp:new_Addr_def)
    qed
  qed
next
  case (WTrtCast E e T C)
  have wte: "P,E,h,sh ⊢ e : T" and ref: "is_refT T"
   and IH: "⋀l. ⟦𝒟 e ⌊dom l⌋; P,sh ⊢⇩b (e,b) √; ¬ final e⟧
                ⟹ ∃e' s' b'. P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',s',b'⟩"
   and D: "𝒟 (Cast C e) ⌊dom l⌋"
   and castconf: "P,sh ⊢⇩b (Cast C e,b) √" by fact+
  from D have De: "𝒟 e ⌊dom l⌋" by auto
  have bconf: "P,sh ⊢⇩b (e,b) √" using castconf bconf_Cast by fast
  show ?case
  proof cases
    assume "final e"
    with wte ref show ?thesis
    proof (rule finalRefE)
      assume "e = null" thus ?case by(fastforce intro:RedCastNull)
    next
      fix D a assume A: "T = Class D" "e = addr a"
      show ?thesis
      proof cases
        assume "P ⊢ D ≼⇧* C"
        thus ?thesis using A wte by(fastforce intro:RedCast)
      next
        assume "¬ P ⊢ D ≼⇧* C"
        thus ?thesis using A wte by(fastforce elim!:RedCastFail)
      qed
    next
      fix a assume "e = Throw a"
      thus ?thesis by(blast intro!:red_reds.CastThrow)
    qed
  next
    assume nf: "¬ final e"
    from IH[OF De bconf nf] show ?thesis by (blast intro:CastRed)
  qed
next
  case WTrtVal thus ?case by(simp add:final_def)
next
  case WTrtVar thus ?case by(fastforce intro:RedVar simp:hyper_isin_def)
next
  case (WTrtBinOpEq E e1 T1 e2 T2) show ?case
  proof cases
    assume "final e1"
    thus ?thesis
    proof (rule finalE)
      fix v1 assume eV[simp]: "e1 = Val v1"
      show ?thesis
      proof cases
        assume "final e2"
        thus ?thesis
        proof (rule finalE)
          fix v2 assume "e2 = Val v2"
          thus ?thesis using WTrtBinOpEq by(fastforce intro:RedBinOp)
        next
          fix a assume "e2 = Throw a"
          thus ?thesis using eV by(blast intro:red_reds.BinOpThrow2)
        qed
      next
        assume nf: "¬ final e2"
        then have "P,sh ⊢⇩b (e2,b) √" using WTrtBinOpEq.prems(2) by(simp add:bconf_BinOp)
        with WTrtBinOpEq nf show ?thesis
          by simp (fast intro!:BinOpRed2)
      qed
    next
      fix a assume "e1 = Throw a"
      thus ?thesis by (fast intro:red_reds.BinOpThrow1)
    qed
  next
    assume nf: "¬ final e1"
    then have e1: "val_of e1 = None" proof(cases e1)qed(auto)
    then have "P,sh ⊢⇩b (e1,b) √" using WTrtBinOpEq.prems(2) by(simp add:bconf_BinOp)
    with WTrtBinOpEq nf e1 show ?thesis
      by simp (fast intro:BinOpRed1)
  qed
next
  case (WTrtBinOpAdd E e1 e2) show ?case
  proof cases
    assume "final e1"
    thus ?thesis
    proof (rule finalE)
      fix v1 assume eV[simp]: "e1 = Val v1"
      show ?thesis
      proof cases
        assume "final e2"
        thus ?thesis
        proof (rule finalE)
          fix v2 assume eV2:"e2 = Val v2"
          then obtain i1 i2 where "v1 = Intg i1 ∧ v2 = Intg i2" using WTrtBinOpAdd by clarsimp
          thus ?thesis using WTrtBinOpAdd eV eV2 by(fastforce intro:RedBinOp)
        next
          fix a assume "e2 = Throw a"
          thus ?thesis using eV by(blast intro:red_reds.BinOpThrow2)
        qed
      next
        assume nf:"¬ final e2"
        then have "P,sh ⊢⇩b (e2,b) √" using WTrtBinOpAdd.prems(2) by(simp add:bconf_BinOp)
        with WTrtBinOpAdd nf show ?thesis
          by simp (fast intro!:BinOpRed2)
      qed
    next
      fix a assume "e1 = Throw a"
      thus ?thesis by(fast intro:red_reds.BinOpThrow1)
    qed
  next
    assume nf: "¬ final e1"
    then have e1: "val_of e1 = None" proof(cases e1)qed(auto)
    then have "P,sh ⊢⇩b (e1,b) √" using WTrtBinOpAdd.prems(2) by(simp add:bconf_BinOp)
    with WTrtBinOpAdd nf e1 show ?thesis
      by simp (fast intro:BinOpRed1)
  qed
next
  case (WTrtLAss E V T e T')
  then have bconf: "P,sh ⊢⇩b (e,b) √" using bconf_LAss by fast
  show ?case
  proof cases
    assume "final e" with WTrtLAss show ?thesis
      by(fastforce simp:final_def intro: red_reds.RedLAss red_reds.LAssThrow)
  next
    assume "¬ final e" with WTrtLAss bconf show ?thesis
      by simp (fast intro:LAssRed)
  qed
next
  case (WTrtFAcc E e C F T D)
  then have bconf: "P,sh ⊢⇩b (e,b) √" using bconf_FAcc by fast
  have wte: "P,E,h,sh ⊢ e : Class C"
   and field: "P ⊢ C has F,NonStatic:T in D" by fact+
  show ?case
  proof cases
    assume "final e"
    with wte show ?thesis
    proof (rule final_addrE)
      fix a assume e: "e = addr a"
      with wte obtain fs where hp: "h a = Some(C,fs)" by auto
      with hconf have "P,h ⊢ (C,fs) √" using hconf_def by fastforce
      then obtain v where "fs(F,D) = Some v" using field
        by(fastforce dest:has_fields_fun simp:oconf_def has_field_def)
      with hp e show ?thesis by (meson field red_reds.RedFAcc)
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fastforce intro:red_reds.FAccThrow)
    qed
  next
    assume "¬ final e" with WTrtFAcc bconf show ?thesis
      by(fastforce intro!:FAccRed)
  qed
next
  case (WTrtFAccNT E e F D T)
  then have bconf: "P,sh ⊢⇩b (e,b) √" using bconf_FAcc by fast
  show ?case
  proof cases
    assume "final e"  ― ‹@{term e} is @{term null} or @{term throw}›
    with WTrtFAccNT show ?thesis
      by(fastforce simp:final_def intro: red_reds.RedFAccNull red_reds.FAccThrow)
  next
    assume "¬ final e" ― ‹@{term e} reduces by IH›
    with WTrtFAccNT bconf show ?thesis by simp (fast intro:FAccRed)
  qed
next
case (WTrtSFAcc C F T D E) then show ?case
  proof (cases b)
    case True
    then obtain sfs i where shD: "sh D = ⌊(sfs,i)⌋"
      using bconf_def[of P sh "C∙⇩sF{D}" b] WTrtSFAcc.prems(2) initPD_def by auto
    with shconf have "P,h,D ⊢⇩s sfs √" using shconf_def[of P h sh] by auto
    then obtain v where sfsF: "sfs F = Some v" using WTrtSFAcc.hyps
      by(unfold soconf_def) (auto dest:has_field_idemp)
    then show ?thesis using WTrtSFAcc.hyps shD sfsF True
      by(fastforce elim:RedSFAcc)
  next
    case False
    with assms WTrtSFAcc show ?thesis
      by(metis (full_types) SFAccInitDoneRed SFAccInitRed)
  qed
next
  case (WTrtFAss E e1 C F T D e2 T2)
  have wte1: "P,E,h,sh ⊢ e1 : Class C" and field: "P ⊢ C has F,NonStatic:T in D" by fact+
  show ?case
  proof cases
    assume "final e1"
    with wte1 show ?thesis
    proof (rule final_addrE)
      fix a assume e1: "e1 = addr a"
      show ?thesis
      proof cases
        assume "final e2"
        thus ?thesis
        proof (rule finalE)
          fix v assume "e2 = Val v"
          thus ?thesis using e1 wte1 by(fastforce intro: RedFAss[OF field])
        next
          fix a assume "e2 = Throw a"
          thus ?thesis using e1 by(fastforce intro:red_reds.FAssThrow2)
        qed
      next
        assume nf: "¬ final e2"
        then have "P,sh ⊢⇩b (e2,b) √" using WTrtFAss.prems(2) e1 by(simp add:bconf_FAss)
        with WTrtFAss e1 nf show ?thesis
          by simp (fast intro!:FAssRed2)
      qed
    next
      fix a assume "e1 = Throw a"
      thus ?thesis by(fastforce intro:red_reds.FAssThrow1)
    qed
  next
    assume nf: "¬ final e1"
    then have e1: "val_of e1 = None" proof(cases e1)qed(auto)
    then have "P,sh ⊢⇩b (e1,b) √" using WTrtFAss.prems(2) by(simp add:bconf_FAss)
    with WTrtFAss nf e1 show ?thesis
      by simp (blast intro!:FAssRed1)
  qed
next
  case (WTrtFAssNT E e⇩1 e⇩2 T⇩2 F D)
  show ?case
  proof cases
    assume e1: "final e⇩1"  ― ‹@{term e⇩1} is @{term null} or @{term throw}›
    show ?thesis
    proof cases
      assume "final e⇩2"  ― ‹@{term e⇩2} is @{term Val} or @{term throw}›
      with WTrtFAssNT e1 show ?thesis
        by(fastforce simp:final_def
                    intro: red_reds.RedFAssNull red_reds.FAssThrow1 red_reds.FAssThrow2)
    next
      assume nf: "¬ final e⇩2" ― ‹@{term e⇩2} reduces by IH›
      show ?thesis
      proof (rule finalE[OF e1])
        fix v assume ev: "e⇩1 = Val v"
        then have "P,sh ⊢⇩b (e⇩2,b) √" using WTrtFAssNT.prems(2) nf by(simp add:bconf_FAss)
        with WTrtFAssNT ev nf show ?thesis by auto (meson red_reds.FAssRed2)
      next
        fix a assume et: "e⇩1 = Throw a"
        then have "P,sh ⊢⇩b (e⇩1,b) √" using WTrtFAssNT.prems(2) nf by(simp add:bconf_FAss)
        with WTrtFAssNT et nf show ?thesis by(fastforce intro: red_reds.FAssThrow1)
      qed
    qed
  next
    assume nf: "¬ final e⇩1" ― ‹@{term e⇩1} reduces by IH›
    then have e1: "val_of e⇩1 = None" proof(cases e⇩1)qed(auto)
    then have "P,sh ⊢⇩b (e⇩1,b) √" using WTrtFAssNT.prems(2) by(simp add:bconf_FAss)
    with WTrtFAssNT nf e1 show ?thesis
      by simp (blast intro!:FAssRed1)
  qed
next
  case (WTrtSFAss C F T D E e2 T⇩2)
  have field: "P ⊢ C has F,Static:T in D" by fact+
  show ?case
  proof cases
    assume "final e2"
    thus ?thesis
    proof (rule finalE)
      fix v assume ev: "e2 = Val v"
      then show ?case
      proof (cases b)
        case True
        then obtain sfs i where shD: "sh D = ⌊(sfs,i)⌋"
          using bconf_def[of P _ "C∙⇩sF{D} := e2"] WTrtSFAss.prems(2) initPD_def ev by auto
        with shconf have "P,h,D ⊢⇩s sfs √" using shconf_def[of P] by auto
        then obtain v where sfsF: "sfs F = Some v" using field
          by(unfold soconf_def) (auto dest:has_field_idemp)
        then show ?thesis using WTrtSFAss.hyps shD sfsF True ev
          by(fastforce elim:RedSFAss)
      next
        case False
        with assms WTrtSFAss ev show ?thesis
          by(metis (full_types) SFAssInitDoneRed SFAssInitRed)
      qed
    next
      fix a assume "e2 = Throw a"
      thus ?thesis by(fastforce intro:red_reds.SFAssThrow)
    qed
  next
    assume nf: "¬ final e2"
    then have "val_of e2 = None" using final_def val_of_spec by fastforce
    then have "P,sh ⊢⇩b (e2,b) √" using WTrtSFAss.prems(2) by(simp add:bconf_SFAss)
    with WTrtSFAss nf show ?thesis
      by simp (fast intro!:SFAssRed)
  qed
next
  case (WTrtCall E e C M Ts T pns body D es Ts')
  have wte: "P,E,h,sh ⊢ e : Class C"
   and "method": "P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D"
   and wtes: "P,E,h,sh ⊢ es [:] Ts'"and sub: "P ⊢ Ts' [≤] Ts"
   and IHes: "⋀l.
             ⟦𝒟s es ⌊dom l⌋; P,sh ⊢⇩b (es,b) √; ¬ finals es⟧
             ⟹ ∃es' s' b'. P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',s',b'⟩"
   and D: "𝒟 (e∙M(es)) ⌊dom l⌋" by fact+
  show ?case
  proof cases
    assume "final e"
    with wte show ?thesis
    proof (rule final_addrE)
      fix a assume e_addr: "e = addr a"
      show ?thesis
      proof cases
        assume es: "∃vs. es = map Val vs"
        from wte e_addr obtain fs where ha: "h a = Some(C,fs)" by auto
        show ?thesis
          using e_addr ha "method" WTrts_same_length[OF wtes] sub es sees_wf_mdecl[OF wf "method"]
          by(fastforce intro!: RedCall simp:list_all2_iff wf_mdecl_def)
      next
        assume "¬(∃vs. es = map Val vs)"
        hence not_all_Val: "¬(∀e ∈ set es. ∃v. e = Val v)"
          by(simp add:ex_map_conv)
        let ?ves = "takeWhile (λe. ∃v. e = Val v) es"
        let ?rest = "dropWhile (λe. ∃v. e = Val v) es"
        let ?ex = "hd ?rest" let ?rst = "tl ?rest"
        from not_all_Val have nonempty: "?rest ≠ []" by auto
        hence es: "es = ?ves @ ?ex # ?rst" by simp
        have "∀e ∈ set ?ves. ∃v. e = Val v" by(fastforce dest:set_takeWhileD)
        then obtain vs where ves: "?ves = map Val vs"
          using ex_map_conv by blast
        show ?thesis
        proof cases
          assume "final ?ex"
          moreover from nonempty have "¬(∃v. ?ex = Val v)"
            by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv)
              (simp add:dropWhile_eq_Cons_conv)
          ultimately obtain b where ex_Throw: "?ex = Throw b"
            by(fast elim!:finalE)
          show ?thesis using e_addr es ex_Throw ves
            by(fastforce intro:CallThrowParams)
        next
          assume not_fin: "¬ final ?ex"
          have "finals es = finals(?ves @ ?ex # ?rst)" using es
            by(rule arg_cong)
          also have "… = finals(?ex # ?rst)" using ves by simp
          finally have "finals es = finals(?ex # ?rst)" .
          hence fes: "¬ finals es" using not_finals_ConsI[OF not_fin] by blast
          have "P,sh ⊢⇩b (es,b) √" using bconf_Call WTrtCall.prems(2)
            by (metis e_addr option.simps(5) val_of.simps(1))
          thus ?thesis using fes e_addr D IHes by(fastforce intro!:CallParams)
        qed
      qed
    next
      fix a assume "e = Throw a"
      with WTrtCall.prems show ?thesis by(fast intro!:CallThrowObj)
    qed
  next
    assume nf: "¬ final e"
    then have e1: "val_of e = None" proof(cases e)qed(auto)
    then have "P,sh ⊢⇩b (e,b) √" using WTrtCall.prems(2) by(simp add:bconf_Call)
    with WTrtCall nf e1 show ?thesis by simp (blast intro!:CallObj)
  qed
next
  case (WTrtCallNT E e es Ts M T) show ?case
  proof cases
    assume "final e"
    moreover
    { fix v assume e: "e = Val v"
      hence "e = null" using WTrtCallNT by simp
      have ?case
      proof cases
        assume "finals es"
        moreover
        { fix vs assume "es = map Val vs"
          with WTrtCallNT e have ?thesis by(fastforce intro: RedCallNull) }
        moreover
        { fix vs a es' assume "es = map Val vs @ Throw a # es'"
          with WTrtCallNT e have ?thesis by(fastforce intro: CallThrowParams) }
        ultimately show ?thesis by(fastforce simp:finals_def)
      next
        assume nf: "¬ finals es" ― ‹@{term es} reduces by IH›
        have "P,sh ⊢⇩b (es,b) √" using WTrtCallNT.prems(2) e by (simp add: bconf_Call)
        with WTrtCallNT e nf show ?thesis by(fastforce intro: CallParams)
      qed
    }
    moreover
    { fix a assume "e = Throw a"
      with WTrtCallNT have ?case by(fastforce intro: CallThrowObj) }
    ultimately show ?thesis by(fastforce simp:final_def)
  next
    assume nf: "¬ final e" ― ‹@{term e} reduces by IH›
    then have "val_of e = None" proof(cases e)qed(auto)
    then have "P,sh ⊢⇩b (e,b) √" using WTrtCallNT.prems(2) by(simp add:bconf_Call)
    with WTrtCallNT nf show ?thesis by (fastforce intro:CallObj)
  qed
next
  case (WTrtSCall C M Ts T pns body D E es Ts' sfs vs)
  have "method": "P ⊢ C sees M,Static:Ts→T = (pns,body) in D"
   and wtes: "P,E,h,sh ⊢ es [:] Ts'"and sub: "P ⊢ Ts' [≤] Ts"
   and IHes: "⋀l.
             ⟦𝒟s es ⌊dom l⌋; P,sh ⊢⇩b (es,b) √; ¬ finals es⟧
             ⟹ ∃es' s' b'. P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',s',b'⟩"
   and clinit: "M = clinit ⟶ sh D = ⌊(sfs, Processing)⌋ ∧ es = map Val vs"
   and D: "𝒟 (C∙⇩sM(es)) ⌊dom l⌋" by fact+
  show ?case
  proof cases
    assume es: "∃vs. es = map Val vs"
    show ?thesis
    proof (cases b)
      case True
      then show ?thesis
      using "method" WTrts_same_length[OF wtes] sub es sees_wf_mdecl[OF wf "method"] True
      by(fastforce intro!: RedSCall simp:list_all2_iff wf_mdecl_def)
    next
      case False
      show ?thesis
      using "method" clinit WTrts_same_length[OF wtes] sub es False
        by (metis (full_types) red_reds.SCallInitDoneRed red_reds.SCallInitRed)
    qed
  next
    assume nmap: "¬(∃vs. es = map Val vs)"
    hence not_all_Val: "¬(∀e ∈ set es. ∃v. e = Val v)"
      by(simp add:ex_map_conv)
    let ?ves = "takeWhile (λe. ∃v. e = Val v) es"
    let ?rest = "dropWhile (λe. ∃v. e = Val v) es"
    let ?ex = "hd ?rest" let ?rst = "tl ?rest"
    from not_all_Val have nonempty: "?rest ≠ []" by auto
    hence es: "es = ?ves @ ?ex # ?rst" by simp
    have "∀e ∈ set ?ves. ∃v. e = Val v" by(fastforce dest:set_takeWhileD)
    then obtain vs where ves: "?ves = map Val vs"
      using ex_map_conv by blast
    show ?thesis
    proof cases
      assume "final ?ex"
      moreover from nonempty have "¬(∃v. ?ex = Val v)"
        by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv)
          (simp add:dropWhile_eq_Cons_conv)
      ultimately obtain b where ex_Throw: "?ex = Throw b"
        by(fast elim!:finalE)
      show ?thesis using es ex_Throw ves
        by(fastforce intro:SCallThrowParams)
    next
      assume not_fin: "¬ final ?ex"
      have "finals es = finals(?ves @ ?ex # ?rst)" using es
        by(rule arg_cong)
      also have "… = finals(?ex # ?rst)" using ves by simp
      finally have "finals es = finals(?ex # ?rst)" .
      hence fes: "¬ finals es" using not_finals_ConsI[OF not_fin] by blast
      have "P,sh ⊢⇩b (es,b) √"
        by (meson WTrtSCall.prems(2) nmap bconf_SCall map_vals_of_spec not_None_eq)
      thus ?thesis using fes D IHes by(fastforce intro!:SCallParams)
    qed
  qed
next
  case WTrtNil thus ?case by simp
next
  case (WTrtCons E e T es Ts)
  have IHe: "⋀l. ⟦𝒟 e ⌊dom l⌋; P,sh ⊢⇩b (e,b) √; ¬ final e⟧
                ⟹ ∃e' s' b'. P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',s',b'⟩"
   and IHes: "⋀l. ⟦𝒟s es ⌊dom l⌋; P,sh ⊢⇩b (es,b) √; ¬ finals es⟧
             ⟹ ∃es' s' b'. P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',s',b'⟩"
   and D: "𝒟s (e#es) ⌊dom l⌋" and not_fins: "¬ finals(e # es)" by fact+
  have De: "𝒟 e ⌊dom l⌋" and Des: "𝒟s es (⌊dom l⌋ ⊔ 𝒜 e)"
    using D by auto
  show ?case
  proof cases
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v assume e: "e = Val v"
      hence Des': "𝒟s es ⌊dom l⌋" using De Des by auto
      have bconfs: "P,sh ⊢⇩b (es,b) √" using WTrtCons.prems(2) e by(simp add: bconf_Cons)
      have not_fins_tl: "¬ finals es" using not_fins e by simp
      show ?thesis using e IHes[OF Des' bconfs not_fins_tl]
        by (blast intro!:ListRed2)
    next
      fix a assume "e = Throw a"
      hence False using not_fins by simp
      thus ?thesis ..
    qed
  next
    assume nf:"¬ final e"
    then have "val_of e = None" proof(cases e)qed(auto)
    then have bconf: "P,sh ⊢⇩b (e,b) √" using WTrtCons.prems(2) by(simp add: bconf_Cons)
    with IHe[OF De bconf nf] show ?thesis by(fast intro!:ListRed1)
  qed
next
  case (WTrtInitBlock v T⇩1 T E V e⇩2 T⇩2)
  have IH2: "⋀l. ⟦𝒟 e⇩2 ⌊dom l⌋; P,sh ⊢⇩b (e⇩2,b) √; ¬ final e⇩2⟧
                  ⟹ ∃e' s' b'. P ⊢ ⟨e⇩2,(h,l,sh),b⟩ → ⟨e',s',b'⟩"
   and D: "𝒟 {V:T := Val v; e⇩2} ⌊dom l⌋" by fact+
  show ?case
  proof cases
    assume "final e⇩2"
    then show ?thesis
    proof (rule finalE)
      fix v⇩2 assume "e⇩2 = Val v⇩2"
      thus ?thesis by(fast intro:RedInitBlock)
    next
      fix a assume "e⇩2 = Throw a"
      thus ?thesis by(fast intro:red_reds.InitBlockThrow)
    qed
  next
    assume not_fin2: "¬ final e⇩2"
    then have "val_of e⇩2 = None" proof(cases e⇩2)qed(auto)
    from D have D2: "𝒟 e⇩2 ⌊dom(l(V↦v))⌋" by (auto simp:hyperset_defs)
    have e2conf: "P,sh ⊢⇩b (e⇩2,b) √" using WTrtInitBlock.prems(2) by(simp add: bconf_InitBlock)
    from IH2[OF D2 e2conf not_fin2]
    obtain h' l' sh' e' b' where red2: "P ⊢ ⟨e⇩2,(h, l(V↦v),sh),b⟩ → ⟨e',(h', l',sh'),b'⟩"
      by auto
    from red_lcl_incr[OF red2] have "V ∈ dom l'" by auto
    with red2 show ?thesis by(fastforce intro:InitBlockRed)
  qed
next
  case (WTrtBlock E V T e T')
  have IH: "⋀l. ⟦𝒟 e ⌊dom l⌋; P,sh ⊢⇩b (e,b) √; ¬ final e⟧
                 ⟹ ∃e' s' b'. P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',s',b'⟩"
   and unass: "¬ assigned V e" and D: "𝒟 {V:T; e} ⌊dom l⌋" by fact+
  show ?case
  proof cases
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v assume "e = Val v" thus ?thesis by(fast intro:RedBlock)
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fast intro:red_reds.BlockThrow)
    qed
  next
    assume not_fin: "¬ final e"
    then have "val_of e = None" proof(cases e)qed(auto)
    from D have De: "𝒟 e ⌊dom(l(V:=None))⌋" by(simp add:hyperset_defs)
    have bconf: "P,sh ⊢⇩b (e,b) √" using WTrtBlock by(simp add: bconf_Block)
    from IH[OF De bconf not_fin]
    obtain h' l' sh' e' b' where red: "P ⊢ ⟨e,(h,l(V:=None),sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
      by auto
    show ?thesis
    proof (cases "l' V")
      assume "l' V = None"
      with red unass show ?thesis by(blast intro: BlockRedNone)
    next
      fix v assume "l' V = Some v"
      with red unass show ?thesis by(blast intro: BlockRedSome)
    qed
  qed
next
  case (WTrtSeq E e1 T1 e2 T2) show ?case
  proof cases
    assume "final e1"
    thus ?thesis
      by(fast elim:finalE intro:RedSeq red_reds.SeqThrow)
  next
    assume nf: "¬ final e1"
    then have e1: "val_of e1 = None" proof(cases e1)qed(auto)
    then show ?thesis
    proof(cases "lass_val_of e1")
      case None
      then have "P,sh ⊢⇩b (e1,b) √" using WTrtSeq.prems(2) e1 by(simp add: bconf_Seq)
      with WTrtSeq nf e1 None show ?thesis by simp (blast intro:SeqRed)
    next
      case (Some p)
      obtain V v where "e1 = V:=Val v" using lass_val_of_spec[OF Some] by simp
      then show ?thesis using SeqRed[OF RedLAss] by blast
    qed
  qed
next
  case (WTrtCond E e e⇩1 T⇩1 e⇩2 T⇩2 T)
  have wt: "P,E,h,sh ⊢ e : Boolean" by fact
  show ?case
  proof cases
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v assume val: "e = Val v"
      then obtain b where v: "v = Bool b" using wt by auto
      show ?thesis
      proof (cases b)
        case True with val v show ?thesis by(fastforce intro:RedCondT simp: prod_cases3)
      next
        case False with val v show ?thesis by(fastforce intro:RedCondF simp: prod_cases3)
      qed
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fast intro:red_reds.CondThrow)
    qed
  next
    assume nf: "¬ final e"
    then have "bool_of e = None" proof(cases e)qed(auto)
    then have "P,sh ⊢⇩b (e,b) √" using WTrtCond.prems(2) by(simp add: bconf_Cond)
    with WTrtCond nf show ?thesis by simp (blast intro:CondRed)
  qed
next
  case WTrtWhile show ?case by(fast intro:RedWhile)
next
  case (WTrtThrow E e T⇩r T) show ?case
  proof cases
    assume "final e" ― ‹Then @{term e} must be @{term throw} or @{term null}›
    with WTrtThrow show ?thesis
      by(fastforce simp:final_def is_refT_def
                  intro:red_reds.ThrowThrow red_reds.RedThrowNull)
  next
    assume nf: "¬ final e" ― ‹Then @{term e} must reduce›
    then have "val_of e = None" proof(cases e)qed(auto)
    then have "P,sh ⊢⇩b (e,b) √" using WTrtThrow.prems(2) by(simp add: bconf_Throw)
    with WTrtThrow nf show ?thesis by simp (blast intro:ThrowRed)
  qed
next
  case (WTrtTry E e1 T1 V C e2 T2)
  have wt1: "P,E,h,sh ⊢ e1 : T1" by fact
  show ?case
  proof cases
    assume "final e1"
    thus ?thesis
    proof (rule finalE)
      fix v assume "e1 = Val v"
      thus ?thesis by(fast intro:RedTry)
    next
      fix a assume e1_Throw: "e1 = Throw a"
      with wt1 obtain D fs where ha: "h a = Some(D,fs)" by fastforce
      show ?thesis
      proof cases
        assume "P ⊢ D ≼⇧* C"
        with e1_Throw ha show ?thesis by(fastforce intro!:RedTryCatch)
      next
        assume "¬ P ⊢ D ≼⇧* C"
        with e1_Throw ha show ?thesis by(fastforce intro!:RedTryFail)
      qed
    qed
  next
    assume nf: "¬ final e1"
    then have "val_of e1 = None" proof(cases e1)qed(auto)
    then have "P,sh ⊢⇩b (e1,b) √" using WTrtTry.prems(2) by(simp add: bconf_Try)
    with WTrtTry nf show ?thesis by simp (fast intro:TryRed)
  qed
next
  case (WTrtInit E e T⇩r C Cs b) show ?case
  proof(cases Cs)
    case Nil then show ?thesis using WTrtInit by(fastforce intro!: RedInit)
  next
    case (Cons C' Cs')
    show ?thesis
    proof(cases b)
      case True then show ?thesis using Cons by(fastforce intro!: RedInitRInit)
    next
      case False
      show ?thesis
      proof(cases "sh C'")
        case None
        then show ?thesis using False Cons by(fastforce intro!: InitNoneRed)
      next
        case (Some sfsi)
        then obtain sfs i where sfsi:"sfsi = (sfs,i)" by(cases sfsi)
        show ?thesis
        proof(cases i)
          case Done
          then show ?thesis using False Some sfsi Cons by(fastforce intro!: RedInitDone)
        next
          case Processing
          then show ?thesis using False Some sfsi Cons by(fastforce intro!: RedInitProcessing)
        next
          case Error
          then show ?thesis using False Some sfsi Cons by(fastforce intro!: RedInitError)
        next
          case Prepared
          show ?thesis
          proof cases
            assume "C' = Object"
            then show ?thesis using False Some sfsi Prepared Cons by(fastforce intro: InitObjectRed)
          next
            assume "C' ≠ Object"
            then show ?thesis using False Some sfsi Prepared WTrtInit.hyps(3) Cons
              by(simp only: is_class_def)(fastforce intro!: InitNonObjectSuperRed)
          qed
        qed
      qed
    qed
  qed
next
  case (WTrtRI E e T⇩r e' T⇩r' C Cs)
  obtain sfs i where shC: "sh C = ⌊(sfs, i)⌋" using WTrtRI.hyps(9) by blast
  show ?case
  proof cases
    assume fin: "final e" then show ?thesis
    proof (rule finalE)
      fix v assume e: "e = Val v"
      then show ?thesis using shC e by(fast intro:RedRInit)
    next
      fix a assume eThrow: "e = Throw a"
      show ?thesis
      proof(cases Cs)
        case Nil then show ?thesis using eThrow shC by(fastforce intro!: RInitThrow)
      next
        case Cons then show ?thesis using eThrow shC by(fastforce intro!: RInitInitThrow)
      qed
    qed
  next
    assume nf: "¬ final e"
    then have "val_of e = None" proof(cases e)qed(auto)
    then have "P,sh ⊢⇩b (e,b) √" using WTrtRI.prems(2) by(simp add: bconf_RI)
    with WTrtRI nf show ?thesis by simp (meson red_reds.RInitRed)
  qed
qed
(*>*)

end