Theory Progress

(*  Title:      JinjaThreads/J/SmallProgress.thy
    Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Progress of Small Step Semantics›

theory Progress
imports
  WellTypeRT
  DefAss
  SmallStep
  "../Common/ExternalCallWF"
  WWellForm
begin

context J_heap begin

lemma final_addrE [consumes 3, case_names addr Throw]:
  "⟦ P,E,h ⊢ e : T; class_type_of' T = ⌊U⌋; final e;
    ⋀a. e = addr a ⟹ R;
    ⋀a. e = Throw a ⟹ R ⟧ ⟹ R"
apply(auto elim!: final.cases)
apply(case_tac v)
apply auto
done

lemma finalRefE [consumes 3, case_names null Class Array Throw]:
 "⟦ P,E,h ⊢ e : T; is_refT T; final e;
   e = null ⟹ R;
   ⋀a C. ⟦ e = addr a; T = Class C ⟧ ⟹ R;
   ⋀a U. ⟦ e = addr a; T = U⌊⌉ ⟧ ⟹ R;
   ⋀a. e = Throw a ⟹ R ⟧ ⟹ R"
apply(auto simp:final_iff)
apply(case_tac v)
apply(auto elim!: is_refT.cases)
done

end

theorem (in J_progress) red_progress:
  assumes wf: "wwf_J_prog P" and hconf: "hconf h"
  shows progress: "⟦ P,E,h ⊢ e : T; 𝒟 e ⌊dom l⌋; ¬ final e ⟧ ⟹ ∃e' s' ta. extTA,P,t ⊢ ⟨e,(h,l)⟩ -ta→ ⟨e',s'⟩"
  and progresss: "⟦ P,E,h ⊢ es [:] Ts; 𝒟s es ⌊dom l⌋; ¬ finals es ⟧ ⟹ ∃es' s' ta. extTA,P,t ⊢ ⟨es,(h,l)⟩ [-ta→] ⟨es',s'⟩"
proof (induct arbitrary: l and l rule:WTrt_WTrts.inducts)
  case (WTrtNew C)
  thus ?case using WTrtNew
    by(cases "allocate h (Class_type C) = {}")(fastforce intro: RedNewFail RedNew)+
next
  case (WTrtNewArray E e T l)
  have IH: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h,l)⟩ -tas→ ⟨e', s'⟩"
   and D: "𝒟 (newA T⌊e⌉) ⌊dom l⌋"
   and ei: "P,E,h ⊢ e : Integer" by fact+
  from D have De: "𝒟 e ⌊dom l⌋" by auto
  show ?case
  proof cases 
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v
      assume e [simp]: "e = Val v"
      with ei have "typeof⇘h⇙ v = Some Integer" by fastforce
      hence exei: "∃i. v = Intg i" by fastforce
      then obtain i where v: "v = Intg i" by blast
      thus ?thesis
      proof (cases "0 <=s i")
        case True
        thus ?thesis using True ‹v = Intg i› WTrtNewArray.prems
          by(cases "allocate h (Array_type T (nat (sint i))) = {}")(auto simp del: split_paired_Ex intro: RedNewArrayFail RedNewArray)
      next
        assume "¬ 0 <=s i"
        hence "i <s 0" by simp
        then have "extTA,P,t ⊢ ⟨newA T⌊Val(Intg i)⌉,(h, l)⟩ -ε→ ⟨THROW NegativeArraySize,(h, l)⟩"
          by - (rule RedNewArrayNegative, auto)
        with e v show ?thesis by blast
      qed
    next
      fix exa
      assume e: "e = Throw exa"
      then have "extTA,P,t ⊢ ⟨newA T⌊Throw exa⌉,(h, l)⟩ -ε→ ⟨Throw exa,(h, l)⟩"
        by - (rule NewArrayThrow)
      with e show ?thesis by blast
    qed
  next
    assume "¬ final e"
    with IH De have exes: "∃e' s' ta. extTA,P,t ⊢ ⟨e,(h, l)⟩ -ta→ ⟨e',s'⟩" by simp
    then obtain e' s' ta where "extTA,P,t ⊢ ⟨e,(h, l)⟩ -ta→ ⟨e',s'⟩" by blast
    hence "extTA,P,t ⊢ ⟨newA T⌊e⌉,(h, l)⟩ -ta→ ⟨newA T⌊e'⌉,s'⟩" by - (rule NewArrayRed)
    thus ?thesis by blast
  qed
next
  case (WTrtCast E e T U l)
  have wte: "P,E,h ⊢ e : T"
   and IH: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧
                ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h,l)⟩ -tas→ ⟨e',s'⟩"
   and D: "𝒟 (Cast U e) ⌊dom l⌋" by fact+
  from D have De: "𝒟 e ⌊dom l⌋" by auto
  show ?case
  proof (cases "final e")
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v
      assume ev: "e = Val v"
      with WTrtCast obtain V where thvU: "typeof⇘h⇙ v = ⌊V⌋" by fastforce
      thus ?thesis
      proof (cases "P ⊢ V ≤ U")
        assume "P ⊢ V ≤ U"
        with thvU have "extTA,P,t ⊢ ⟨Cast U (Val v),(h, l)⟩ -ε→ ⟨Val v,(h,l)⟩"
          by - (rule RedCast, auto)
        with ev show ?thesis by blast
      next
        assume "¬ P ⊢ V ≤ U"
        with thvU have "extTA,P,t ⊢ ⟨Cast U (Val v),(h, l)⟩ -ε→ ⟨THROW ClassCast,(h,l)⟩"
          by - (rule RedCastFail, auto)
        with ev show ?thesis by blast
      qed
    next
      fix a
      assume "e = Throw a"
      thus ?thesis by(blast intro!:CastThrow)
    qed
  next
    assume nf: "¬ final e"
    from IH[OF De nf] show ?thesis by (blast intro:CastRed)
  qed
next
  case (WTrtInstanceOf E e T U l)
  have wte: "P,E,h ⊢ e : T"
   and IH: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧
                ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h,l)⟩ -tas→ ⟨e',s'⟩"
   and D: "𝒟 (e instanceof U) ⌊dom l⌋" by fact+
  from D have De: "𝒟 e ⌊dom l⌋" by auto
  show ?case
  proof (cases "final e")
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v
      assume ev: "e = Val v"
      with WTrtInstanceOf obtain V where thvU: "typeof⇘h⇙ v = ⌊V⌋" by fastforce
      hence "extTA,P,t ⊢ ⟨(Val v) instanceof U,(h, l)⟩ -ε→ ⟨Val (Bool (v ≠ Null ∧ P ⊢ V ≤ U)),(h,l)⟩"
        by -(rule RedInstanceOf, auto)
      with ev show ?thesis by blast
    next
      fix a
      assume "e = Throw a"
      thus ?thesis by(blast intro!:InstanceOfThrow)
    qed
  next
    assume nf: "¬ final e"
    from IH[OF De nf] show ?thesis by (blast intro:InstanceOfRed)
  qed
next
  case WTrtVal thus ?case by(simp add:final_iff)
next
  case WTrtVar thus ?case by(fastforce intro:RedVar simp:hyper_isin_def)
next
  case (WTrtBinOp E e1 T1 e2 T2 bop T)
  show ?case
  proof cases
    assume "final e1"
    thus ?thesis
    proof (rule finalE)
      fix v1 assume [simp]: "e1 = Val v1"
      show ?thesis
      proof cases
        assume "final e2"
        thus ?thesis
        proof (rule finalE)
          fix v2 assume [simp]: "e2 = Val v2"
          with WTrtBinOp have type: "typeof⇘h⇙ v1 = ⌊T1⌋" "typeof⇘h⇙ v2 = ⌊T2⌋" by auto
          from binop_progress[OF this ‹P ⊢ T1«bop»T2 : T›] obtain va
            where "binop bop v1 v2 = ⌊va⌋" by blast
          thus ?thesis by(cases va)(fastforce intro: RedBinOp RedBinOpFail)+
        next
          fix a assume "e2 = Throw a"
          thus ?thesis by(fastforce intro:BinOpThrow2)
        qed
      next
        assume "¬ final e2" with WTrtBinOp show ?thesis
          by simp (fast intro!:BinOpRed2)
      qed
    next
      fix a assume "e1 = Throw a"
      thus ?thesis by simp (fast intro:BinOpThrow1)
    qed
  next
    assume "¬ final e1" with WTrtBinOp show ?thesis
      by simp (fast intro:BinOpRed1)
  qed
next
  case (WTrtLAss E V T e T')
  show ?case
  proof cases
    assume "final e" with WTrtLAss show ?thesis
      by(fastforce simp:final_iff intro!:RedLAss LAssThrow)
  next
    assume "¬ final e" with WTrtLAss show ?thesis
      by simp (fast intro:LAssRed)
  qed
next
  case (WTrtAAcc E a T i l)
  have wte: "P,E,h ⊢ a : T⌊⌉"
   and wtei: "P,E,h ⊢ i : Integer"
   and IHa: "⋀l. ⟦𝒟 a ⌊dom l⌋; ¬ final a⟧
                 ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨a,(h,l)⟩ -tas→ ⟨e',s'⟩"
   and IHi: "⋀l. ⟦𝒟 i ⌊dom l⌋; ¬ final i⟧
                 ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨i,(h,l)⟩ -tas→ ⟨e',s'⟩"
   and D: "𝒟 (a⌊i⌉) ⌊dom l⌋" by fact+
  have ref: "is_refT (T⌊⌉)" by simp
  from D have Da: "𝒟 a ⌊dom l⌋" by simp
  show ?case
  proof (cases "final a")
    assume "final a"
    with wte ref show ?case
    proof (cases rule: finalRefE)
      case null
      thus ?thesis
      proof (cases "final i")
        assume "final i"
        thus ?thesis
        proof (rule finalE)
          fix v
          assume i: "i = Val v"
          have "extTA,P,t ⊢ ⟨null⌊Val v⌉, (h, l)⟩ -ε→ ⟨THROW NullPointer, (h,l)⟩"
            by(rule RedAAccNull)
          with i null show ?thesis by blast
        next
          fix ex
          assume i: "i = Throw ex"
          have "extTA,P,t ⊢ ⟨null⌊Throw ex⌉, (h, l)⟩ -ε→ ⟨Throw ex, (h,l)⟩"
            by(rule AAccThrow2)
          with i null show ?thesis by blast
        qed
      next
        assume "¬ final i"
        from WTrtAAcc null show ?thesis
          by simp
      qed
    next
      case (Array ad U)
      with wte obtain n where ty: "typeof_addr h ad = ⌊Array_type U n⌋" by auto
      thus ?thesis
      proof (cases "final i")
        assume "final i"
        thus ?thesis
        proof(rule finalE)
          fix v
          assume [simp]: "i = Val v"
          with wtei have "typeof⇘h⇙ v = Some Integer" by fastforce
          hence "∃i. v = Intg i" by fastforce
          then obtain i where [simp]: "v = Intg i" by blast
          thus ?thesis
          proof (cases "i <s 0 ∨ sint i ≥ int n")
            case True
            with WTrtAAcc Array ty show ?thesis by (fastforce intro: RedAAccBounds)
          next
            case False
            then have "nat (sint i) < n"
              by (simp add: not_le word_sless_alt nat_less_iff)
            with ty have "P,h ⊢ ad@ACell (nat (sint i)) : U" by(auto intro!: addr_loc_type.intros)
            from heap_read_total[OF hconf this]
            obtain v where "heap_read h ad (ACell (nat (sint i))) v" by blast
            with False Array ty show ?thesis by(fastforce intro: RedAAcc)
          qed
        next
          fix ex
          assume "i = Throw ex"
          with WTrtAAcc Array show ?thesis by (fastforce intro: AAccThrow2)
        qed
      next
        assume "¬ final i"
        with WTrtAAcc Array show ?thesis by (fastforce intro: AAccRed2)
      qed
    next
      fix ex
      assume "a = Throw ex"
      with WTrtAAcc show ?thesis by (fastforce intro: AAccThrow1)
    qed simp
  next
    assume "¬ final a"
    with WTrtAAcc show ?thesis by (fastforce intro: AAccRed1)
  qed
next
  case (WTrtAAccNT E a i T l)
  have wte: "P,E,h ⊢ a : NT"
   and wtei: "P,E,h ⊢ i : Integer"
   and IHa: "⋀l. ⟦𝒟 a ⌊dom l⌋; ¬ final a⟧
                 ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨a,(h,l)⟩ -tas→ ⟨e',s'⟩"
   and IHi: "⋀l. ⟦𝒟 i ⌊dom l⌋; ¬ final i⟧
                 ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨i,(h,l)⟩ -tas→ ⟨e',s'⟩" by fact+
  have ref: "is_refT NT" by simp
  with WTrtAAccNT have Da: "𝒟 a ⌊dom l⌋" by simp
  thus ?case
  proof (cases "final a")
    case True
    with wte ref show ?thesis
    proof (cases rule: finalRefE)
      case null
      thus ?thesis
      proof (cases "final i")
        assume "final i"
        thus ?thesis
        proof (rule finalE)
          fix v
          assume i: "i = Val v"
          have "extTA,P,t ⊢ ⟨null⌊Val v⌉, (h, l)⟩ -ε→ ⟨THROW NullPointer, (h,l)⟩"
            by (rule RedAAccNull)
          with WTrtAAccNT ‹final a› null ‹final i› i show ?thesis by blast
        next
          fix ex
          assume i: "i = Throw ex"
          have "extTA,P,t ⊢ ⟨null⌊Throw ex⌉, (h, l)⟩ -ε→ ⟨Throw ex, (h,l)⟩"
            by(rule AAccThrow2)
          with WTrtAAccNT ‹final a› null ‹final i› i show ?thesis by blast
        qed
      next
        assume "¬ final i"
        with WTrtAAccNT null show ?thesis
          by(fastforce intro: AAccRed2)
      qed
    next
      case Throw thus ?thesis by (fastforce intro: AAccThrow1)
    qed simp_all
  next
    case False
    with WTrtAAccNT Da show ?thesis by (fastforce intro:AAccRed1)
  qed
next
  case (WTrtAAss E a T i e T' l)
  have wta: "P,E,h ⊢ a : T⌊⌉"
    and wti: "P,E,h ⊢ i : Integer"
    and wte: "P,E,h ⊢ e : T'"
    and D: "𝒟 (a⌊i⌉ := e) ⌊dom l⌋"
    and IH1: "⋀l. ⟦𝒟 a ⌊dom l⌋; ¬ final a⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨a,(h, l)⟩ -tas→ ⟨e',s'⟩"
    and IH2: "⋀l. ⟦𝒟 i ⌊dom l⌋; ¬ final i⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨i,(h, l)⟩ -tas→ ⟨e',s'⟩"
    and IH3: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h, l)⟩ -tas→ ⟨e',s'⟩" by fact+
  have ref: "is_refT (T⌊⌉)" by simp
  show ?case
  proof (cases "final a")
    assume fa: "final a"
    with wta ref show ?thesis
    proof(cases rule: finalRefE)
      case null
      show ?thesis
      proof(cases "final i")
        assume "final i"
        thus ?thesis
        proof (rule finalE)
          fix v
          assume i: "i = Val v"
          with wti have "typeof⇘h⇙ v = Some Integer" by fastforce
          then obtain idx where "v = Intg idx" by fastforce
          thus ?thesis
          proof (cases "final e")
            assume "final e"
            thus ?thesis
            proof (rule finalE)
              fix w
              assume "e = Val w"
              with WTrtAAss null show ?thesis by (fastforce intro: RedAAssNull)
            next
              fix ex
              assume "e = Throw ex"
              with WTrtAAss null show ?thesis by (fastforce intro: AAssThrow3)
            qed
          next
            assume "¬ final e"
            with WTrtAAss null show ?thesis by (fastforce intro: AAssRed3)
          qed
        next
          fix ex
          assume "i = Throw ex"
          with WTrtAAss null show ?thesis by (fastforce intro: AAssThrow2)
        qed
      next
        assume "¬ final i"
        with WTrtAAss null show ?thesis by (fastforce intro: AAssRed2)
      qed
    next
      case (Array ad U)
      with wta obtain n where ty: "typeof_addr h ad = ⌊Array_type U n⌋" by auto
      thus ?thesis
      proof (cases "final i")
        assume fi: "final i"
        thus ?thesis
        proof (rule finalE)
          fix v
          assume ivalv: "i = Val v"
          with wti have "typeof⇘h⇙ v = Some Integer" by fastforce
          then obtain idx where vidx: "v = Intg idx" by fastforce
          thus ?thesis
          proof (cases "final e")
            assume fe: "final e"
            thus ?thesis
            proof(rule finalE)
              fix w
              assume evalw: "e = Val w"
              show ?thesis
              proof(cases "idx <s 0 ∨ sint idx ≥ int n")
                case True
                with ty evalw Array ivalv vidx show ?thesis by(fastforce intro: RedAAssBounds)
              next
                case False
                then have "nat (sint idx) < n"
                  by (simp add: not_le word_sless_alt nat_less_iff)
                with ty have adal: "P,h ⊢ ad@ACell (nat (sint idx)) : U"
                  by(auto intro!: addr_loc_type.intros)
                show ?thesis
                proof(cases "P ⊢ T' ≤ U")
                  case True
                  with wte evalw have "P,h ⊢ w :≤ U"
                    by(auto simp add: conf_def)
                  from heap_write_total[OF hconf adal this]
                  obtain h' where h': "heap_write h ad (ACell (nat (sint idx))) w h'" ..
                  with ty False vidx ivalv evalw Array wte True
                  show ?thesis by(fastforce intro: RedAAss)
                next
                  case False
                  with ty vidx ivalv evalw Array wte ‹¬ (idx <s 0 ∨ sint idx ≥ int n)›
                  show ?thesis by(fastforce intro: RedAAssStore)
                qed
              qed
            next
              fix ex
              assume "e = Throw ex"
              with Array ivalv show ?thesis by (fastforce intro: AAssThrow3)
            qed
          next
            assume "¬ final e"
            with WTrtAAss Array fi ivalv vidx show ?thesis by (fastforce intro: AAssRed3)
          qed
        next
          fix ex
          assume "i = Throw ex"
          with WTrtAAss Array show ?thesis by (fastforce intro: AAssThrow2)
        qed
      next
        assume "¬ final i"
        with WTrtAAss Array show ?thesis by (fastforce intro: AAssRed2)
      qed
    next
      fix ex
      assume "a = Throw ex"
      with WTrtAAss show ?thesis by (fastforce intro:AAssThrow1)
    qed simp_all
  next
    assume "¬ final a"
    with WTrtAAss show ?thesis by (fastforce intro: AAssRed1)
  qed
next
  case (WTrtAAssNT E a i e T' l)
  have wta: "P,E,h ⊢ a : NT"
    and wti: "P,E,h ⊢ i : Integer"
    and wte: "P,E,h ⊢ e : T'"
    and D: "𝒟 (a⌊i⌉ := e) ⌊dom l⌋"
    and IH1: "⋀l. ⟦𝒟 a ⌊dom l⌋; ¬ final a⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨a,(h, l)⟩ -tas→ ⟨e',s'⟩"
    and IH2: "⋀l. ⟦𝒟 i ⌊dom l⌋; ¬ final i⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨i,(h, l)⟩ -tas→ ⟨e',s'⟩"
    and IH3: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h, l)⟩ -tas→ ⟨e',s'⟩" by fact+
  have ref: "is_refT NT" by simp
  show ?case
  proof (cases "final a")
    assume fa: "final a"
    show ?case
    proof (cases "final i")
      assume fi: "final i"
      show ?case
      proof (cases "final e")
        assume fe: "final e"
        with WTrtAAssNT fa fi show ?thesis
          by (fastforce simp:final_iff intro: RedAAssNull AAssThrow1 AAssThrow2 AAssThrow3)
      next
        assume "¬ final e"
        with WTrtAAssNT fa fi show ?thesis
          by (fastforce simp: final_iff intro!:AAssRed3 AAssThrow1 AAssThrow2)
      qed
    next
      assume "¬ final i"
      with WTrtAAssNT fa show ?thesis
        by (fastforce simp: final_iff intro!:AAssRed2 AAssThrow1)
    qed
  next
    assume "¬ final a"
    with WTrtAAssNT show ?thesis by (fastforce simp: final_iff intro!:AAssRed1)
  qed
next
  case (WTrtALength E a T l)
  show ?case
  proof(cases "final a")
    case True
    note wta = ‹P,E,h ⊢ a : T⌊⌉›
    thus ?thesis 
    proof(rule finalRefE[OF _ _ True])
      show "is_refT (T⌊⌉)" by simp
    next
      assume "a = null"
      thus ?thesis by(fastforce intro: RedALengthNull)
    next
      fix ad U
      assume "a = addr ad" and "T⌊⌉ = U⌊⌉"
      with wta show ?thesis by(fastforce intro: RedALength)
    next
      fix ad
      assume "a = Throw ad"
      thus ?thesis by (fastforce intro: ALengthThrow)
    qed simp
  next
    case False
    from ‹𝒟 (a∙length) ⌊dom l⌋› have "𝒟 a ⌊dom l⌋" by simp
    with False ‹⟦𝒟 a ⌊dom l⌋; ¬ final a⟧ ⟹ ∃e' s' ta. extTA,P,t ⊢ ⟨a,(h, l)⟩ -ta→ ⟨e',s'⟩›
    obtain e' s' ta where "extTA,P,t ⊢ ⟨a,(h, l)⟩ -ta→ ⟨e',s'⟩" by blast
    thus ?thesis by(blast intro: ALengthRed)
  qed
next
  case (WTrtALengthNT E a T l)
  show ?case
  proof(cases "final a")
    case True
    note wta = ‹P,E,h ⊢ a : NT›
    thus ?thesis
    proof(rule finalRefE[OF _ _ True])
      show "is_refT NT" by simp
    next
      assume "a = null"
      thus ?thesis by(blast intro: RedALengthNull)
    next
      fix ad
      assume "a = Throw ad"
      thus ?thesis by(blast intro: ALengthThrow)
    qed simp_all
  next
    case False
    from ‹𝒟 (a∙length) ⌊dom l⌋› have "𝒟 a ⌊dom l⌋" by simp
    with False ‹⟦𝒟 a ⌊dom l⌋; ¬ final a⟧ ⟹ ∃e' s' ta. extTA,P,t ⊢ ⟨a,(h, l)⟩ -ta→ ⟨e',s'⟩›
    obtain e' s' ta where "extTA,P,t ⊢ ⟨a,(h, l)⟩ -ta→ ⟨e',s'⟩" by blast
    thus ?thesis by(blast intro: ALengthRed)
  qed
next
  case (WTrtFAcc E e U C F T fm D l)
  have wte: "P,E,h ⊢ e : U"
    and icto: "class_type_of' U = ⌊C⌋"
   and field: "P ⊢ C has F:T (fm) in D" by fact+
  show ?case
  proof cases
    assume "final e"
    with wte icto show ?thesis
    proof (cases rule: final_addrE)
      case (addr a)
      with wte obtain hU where ty: "typeof_addr h a = ⌊hU⌋" "U = ty_of_htype hU" by auto
      with icto field have "P,h ⊢ a@CField D F : T" by(auto intro: addr_loc_type.intros)
      from heap_read_total[OF hconf this]
      obtain v where "heap_read h a (CField D F) v" by blast
      with addr ty show ?thesis by(fastforce intro: RedFAcc)
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fastforce intro:FAccThrow)
    qed
  next
    assume "¬ final e" with WTrtFAcc show ?thesis
      by(fastforce intro!:FAccRed)
  qed
next
  case (WTrtFAccNT E e F D T l)
  show ?case
  proof cases
    assume "final e"  ― ‹@{term e} is @{term null} or @{term throw}›
    with WTrtFAccNT show ?thesis
      by(fastforce simp:final_iff intro: RedFAccNull FAccThrow)
  next
    assume "¬ final e" ― ‹@{term e} reduces by IH›
    with WTrtFAccNT show ?thesis by simp (fast intro:FAccRed)
  qed
next
  case (WTrtFAss E e1 U C F T fm D e2 T2 l)
  have wte1: "P,E,h ⊢ e1 : U"
    and icto: "class_type_of' U = ⌊C⌋"
    and field: "P ⊢ C has F:T (fm) in D" by fact+
  show ?case
  proof cases
    assume "final e1"
    with wte1 icto 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: "e2 = Val v"
          from wte1 field icto e1 have adal: "P,h ⊢ a@CField D F : T"
            by(auto intro: addr_loc_type.intros)
          from e2 ‹P ⊢ T2 ≤ T› ‹P,E,h ⊢ e2 : T2›
          have "P,h ⊢ v :≤ T" by(auto simp add: conf_def)
          from heap_write_total[OF hconf adal this] obtain h' 
            where "heap_write h a (CField D F) v h'" ..
          with wte1 field e1 e2 show ?thesis
            by(fastforce intro: RedFAss)
        next
          fix a assume "e2 = Throw a"
          thus ?thesis using e1 by(fastforce intro:FAssThrow2)
        qed
      next
        assume "¬ final e2" with WTrtFAss ‹final e1› e1 show ?thesis
          by simp (fast intro!:FAssRed2)
      qed
    next
      fix a assume "e1 = Throw a"
      thus ?thesis by(fastforce intro:FAssThrow1)
    qed
  next
    assume "¬ final e1" with WTrtFAss show ?thesis
      by(simp del: split_paired_Ex)(blast intro!:FAssRed1)
  qed
next
  case (WTrtFAssNT E e⇩1 e⇩2 T⇩2 F D l)
  show ?case
  proof cases
    assume "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 ‹final e⇩1› show ?thesis
        by(fastforce simp:final_iff intro: RedFAssNull FAssThrow1 FAssThrow2)
    next
      assume "¬ final e⇩2" ― ‹@{term e⇩2} reduces by IH›
      with WTrtFAssNT ‹final e⇩1› show ?thesis
        by (fastforce  simp:final_iff intro!:FAssRed2 FAssThrow1)
    qed
  next
    assume "¬ final e⇩1" ― ‹@{term e⇩1} reduces by IH›
    with WTrtFAssNT show ?thesis by (fastforce intro:FAssRed1)
  qed
next
  case (WTrtCAS E e1 U C F T fm D e2 T2 e3 T3)
  show ?case
  proof(cases "final e1")
    case e1: True
    with WTrtCAS.hyps(1,3) show ?thesis
    proof(rule final_addrE)
      fix a
      assume e1: "e1 = addr a"
      with WTrtCAS.hyps(1) obtain hU
        where ty: "typeof_addr h a = ⌊hU⌋" "U = ty_of_htype hU" by auto
      with WTrtCAS.hyps(3,4) have adal: "P,h ⊢ a@CField D F : T" by(auto intro: addr_loc_type.intros)
      from heap_read_total[OF hconf this]
      obtain v where v: "heap_read h a (CField D F) v" by blast
      show ?thesis
      proof(cases "final e2")
        case e2: True
        show ?thesis
        proof(cases "final e3")
          case e3: True
          consider (Val2) v2 where "e2 = Val v2" | (Throw2) a2 where "e2 = Throw a2"
            using e2 by(auto simp add: final_iff)
          then show ?thesis
          proof(cases)
            case Val2
            consider (Succeed) v3 where "e3 = Val v3" "v2 = v" 
              | (Fail) v3 where "e3 = Val v3" "v2 ≠ v" 
              | (Throw3) a3 where "e3 = Throw a3"
              using e3 by(auto simp add: final_iff)
            then show ?thesis
            proof cases
              case Succeed
              with WTrtCAS.hyps(9,11) adal have "P,h ⊢ v3 :≤ T" by(auto simp add: conf_def)
              from heap_write_total[OF hconf adal this] obtain h' 
                where "heap_write h a (CField D F) v3 h'" ..
              with Val2 e1 v Succeed show ?thesis
                by(auto intro: RedCASSucceed simp del: split_paired_Ex)
            next
              case Fail
              with Val2 e1 v show ?thesis 
                by(auto intro: RedCASFail simp del: split_paired_Ex)
            next
              case Throw3
              then show ?thesis using e1 Val2 by(auto intro: CASThrow3 simp del: split_paired_Ex)
            qed
          next
            case Throw2
            then show ?thesis using e1 by(auto intro: CASThrow2 simp del: split_paired_Ex)
          qed
        next
          case False
          with WTrtCAS e1 e2 show ?thesis 
            by(fastforce simp del: split_paired_Ex simp add: final_iff intro: CASRed3 CASThrow2)
        qed
      next
        case False
        with WTrtCAS e1 show ?thesis 
          by(fastforce intro: CASRed2 CASThrow2 simp del: split_paired_Ex)
      qed
    qed(fastforce intro: CASThrow)
  next
    case False
    then show ?thesis using WTrtCAS by(fastforce intro: CASRed1)
  qed
next
  case (WTrtCASNT E e1 e2 T2 e3 T3 D F)
  note [simp del] = split_paired_Ex
  show ?case
  proof(cases "final e1")
    case e1: True
    show ?thesis
    proof(cases "final e2")
      case e2: True
      show ?thesis
      proof(cases "final e3")
        case True
        with e1 e2 WTrtCASNT show ?thesis
          by(fastforce simp add: final_iff intro: CASNull CASThrow CASThrow2 CASThrow3) 
      next
        case False
        with e1 e2 WTrtCASNT show ?thesis
          by(fastforce simp add: final_iff intro: CASRed3 CASThrow CASThrow2) 
      qed
    next
      case False
      with e1 WTrtCASNT show ?thesis
        by(fastforce simp add: final_iff intro: CASRed2 CASThrow) 
    qed
  next
    case False
    with WTrtCASNT show ?thesis
      by(fastforce simp add: final_iff intro: CASRed1) 
  qed
next
  case (WTrtCall E e U C M Ts T meth D es Ts' l)
  have wte: "P,E,h ⊢ e : U" 
    and icto: "class_type_of' U = ⌊C⌋" by fact+
  have IHe: "⋀l. ⟦ 𝒟 e ⌊dom l⌋; ¬ final e ⟧
             ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h, l)⟩ -tas→ ⟨e',s'⟩" by fact
  have sees: "P ⊢ C sees M: Ts→T = meth in D" by fact
  have wtes: "P,E,h ⊢ es [:] Ts'" by fact
  have IHes: "⋀l. ⟦𝒟s es ⌊dom l⌋; ¬ finals es⟧ ⟹ ∃es' s' ta. extTA,P,t ⊢ ⟨es,(h, l)⟩ [-ta→] ⟨es',s'⟩" by fact
  have subtype: "P ⊢ Ts' [≤] Ts" by fact
  have dae: "𝒟 (e∙M(es)) ⌊dom l⌋" by fact
  show ?case
  proof(cases "final e")
    assume fine: "final e"
    with wte icto show ?thesis
    proof (rule final_addrE)
      fix a assume e_addr: "e = addr a"
      show ?thesis
      proof(cases "∃vs. es = map Val vs")
        assume es: "∃vs. es = map Val vs"
        from wte e_addr obtain hU where ha: "typeof_addr h a = ⌊hU⌋" "U = ty_of_htype hU"  by(auto)
        have "length es = length Ts'" using wtes by(auto simp add: WTrts_conv_list_all2 dest: list_all2_lengthD)
        moreover from subtype have "length Ts' = length Ts" by(auto dest: list_all2_lengthD)
        ultimately have esTs: "length es = length Ts" by(auto)
        show ?thesis
        proof(cases meth)
          case (Some pnsbody)
          with esTs e_addr ha sees subtype es sees_wf_mdecl[OF wf sees] icto
          show ?thesis by(cases pnsbody) (fastforce intro!: RedCall simp:list_all2_iff wf_mdecl_def)
        next
          case None
          with sees wf have "D∙M(Ts) :: T" by(auto intro: sees_wf_native)
          moreover from es obtain vs where vs: "es = map Val vs" ..
          with wtes have tyes: "map typeof⇘h⇙ vs = map Some Ts'" by simp
          with ha ‹D∙M(Ts) :: T› icto sees None
          have "P,h ⊢ a∙M(vs) : T" using subtype by(auto simp add: external_WT'_iff)
          from external_call_progress[OF wf this hconf, of t] obtain ta va h'
            where "P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩" by blast
          thus ?thesis using ha icto None sees vs e_addr
            by(fastforce intro: RedCallExternal simp del: split_paired_Ex)
        qed
      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 "¬ finals es" using not_finals_ConsI[OF not_fin] by blast
          thus ?thesis using e_addr dae IHes  by(fastforce intro!:CallParams)
        qed
      qed
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fast intro!:CallThrowObj)
    qed
  next
    assume "¬ final e"
    with WTrtCall show ?thesis by(simp del: split_paired_Ex)(blast intro!:CallObj)
  qed
next
  case (WTrtCallNT E e es Ts M T l)
  have wte: "P,E,h ⊢ e : NT" by fact
  have IHe: "⋀l. ⟦ 𝒟 e ⌊dom l⌋; ¬ final e ⟧
             ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h, l)⟩ -tas→ ⟨e',s'⟩"  by fact
  have IHes: "⋀l. ⟦𝒟s es ⌊dom l⌋; ¬ finals es⟧ ⟹ ∃es' s' ta. extTA,P,t ⊢ ⟨es,(h, l)⟩ [-ta→] ⟨es',s'⟩" by fact
  have wtes: "P,E,h ⊢ es [:] Ts" by fact
  have dae: "𝒟 (e∙M(es)) ⌊dom l⌋" by fact
  show ?case
  proof(cases "final e")
    assume "final e"
    moreover
    { fix v assume "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 = null› ‹finals es› have ?thesis by(fastforce intro: RedCallNull) }
        moreover
        { fix vs a es' assume "es = map Val vs @ Throw a # es'"
          with WTrtCallNT ‹e = null› ‹finals es› have ?thesis by(fastforce intro: CallThrowParams) }
        ultimately show ?thesis by(fastforce simp:finals_iff)
      next
        assume "¬ finals es" ― ‹@{term es} reduces by IH›
        with WTrtCallNT ‹e = null› 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_iff)
  next
    assume "¬ final e" ― ‹@{term e} reduces by IH›
    with WTrtCallNT show ?thesis by (fastforce intro:CallObj)
  qed
next
  case (WTrtBlock E V T e T' vo l)
  have IH: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧
                 ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h,l)⟩ -tas→ ⟨e',s'⟩"
   and D: "𝒟 {V:T=vo; 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:BlockThrow)
    qed
  next
    assume not_fin: "¬ final e"
    from D have De: "𝒟 e ⌊dom(l(V:=vo))⌋" by(auto simp add:hyperset_defs)
    from IH[OF De not_fin]
    obtain h' l' e' tas where red: "extTA,P,t ⊢ ⟨e,(h,l(V:=vo))⟩ -tas→ ⟨e',(h',l')⟩"
      by auto
    thus ?thesis by(blast intro: BlockRed)
  qed
next
  case (WTrtSynchronized E o' T e T' l)
  note wto = ‹P,E,h ⊢ o' : T›
  note IHe = ‹⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e ⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h, l)⟩ -tas→ ⟨e',s'⟩›
  note wte = ‹P,E,h ⊢ e : T'›
  note IHo = ‹⋀l. ⟦𝒟 o' ⌊dom l⌋; ¬ final o' ⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨o',(h, l)⟩ -tas→ ⟨e',s'⟩›
  note refT = ‹is_refT T›
  note dae = ‹𝒟 (sync(o') e) ⌊dom l⌋›
  show ?case
  proof(cases "final o'")
    assume fino: "final o'" 
    thus ?thesis
    proof (rule finalE)
      fix v
      assume oval: "o' = Val v"
      with wto refT show ?thesis
      proof(cases "v")
        assume vnull: "v = Null"
        with oval vnull show ?thesis
          by(fastforce intro: SynchronizedNull)
      next
        fix ad
        assume vaddr: "v = Addr ad"
        thus ?thesis using oval 
          by(fastforce intro: LockSynchronized)
      qed(auto elim: refTE)
    next
      fix a
      assume othrow: "o' = Throw a"
      thus ?thesis by(fastforce intro: SynchronizedThrow1)
    qed
  next
    assume nfino: "¬ final o'"
    with dae IHo show ?case by(fastforce intro: SynchronizedRed1)
  qed
next
  case (WTrtInSynchronized E a T e T' l)
  show ?case
  proof(cases "final e")
    case True thus ?thesis
      by(fastforce elim!: finalE intro: UnlockSynchronized SynchronizedThrow2)
  next
    case False 
    moreover from ‹𝒟 (insync(a) e) ⌊dom l⌋› have "𝒟 e ⌊dom l⌋" by simp
    moreover note IHe = ‹⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧ ⟹ ∃e' s' tas. extTA,P,t ⊢ ⟨e,(h, l)⟩ -tas→ ⟨e',s'⟩›
    ultimately show ?thesis by(fastforce intro: SynchronizedRed2)
  qed
next
  case (WTrtSeq E e1 T1 e2 T2 l)
  show ?case
  proof cases
    assume "final e1"
    thus ?thesis
      by(fast elim:finalE intro:intro:RedSeq SeqThrow)
  next
    assume "¬ final e1" with WTrtSeq show ?thesis
      by(simp del: split_paired_Ex)(blast intro!:SeqRed)
  qed
next
  case (WTrtCond E e e1 T1 e2 T2 T l)
  have wt: "P,E,h ⊢ 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)
      next
        case False with val v show ?thesis by(fastforce intro:RedCondF)
      qed
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fast intro:CondThrow)
    qed
  next
    assume "¬ final e" with WTrtCond show ?thesis
      by simp (fast intro:CondRed)
  qed
next
  case WTrtWhile show ?case by(fast intro:RedWhile)
next
  case (WTrtThrow E e T T' l)
  show ?case
  proof cases
    assume "final e" ― ‹Then @{term e} must be @{term throw} or @{term null}›
    thus ?thesis
    proof(induct rule: finalE)
      case (Val v)
      with ‹P ⊢ T ≤ Class Throwable› ‹¬ final (throw e)› ‹P,E,h ⊢ e : T›
      have "v = Null" by(cases v)(auto simp add: final_iff widen_Class)
      thus ?thesis using Val by(fastforce intro: RedThrowNull)
    next
      case (Throw a)
      thus ?thesis by(fastforce intro: ThrowThrow)
    qed
  next
    assume "¬ final e" ― ‹Then @{term e} must reduce›
    with WTrtThrow show ?thesis by simp (blast intro:ThrowRed)
  qed
next
  case (WTrtTry E e1 T1 V C e2 T2 l)
  have wt1: "P,E,h ⊢ 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 where ha: "typeof_addr h a = ⌊Class_type D⌋"
        by(auto simp add: widen_Class)
      thus ?thesis using e1_Throw
        by(cases "P ⊢ D ≼⇧* C")(fastforce intro:RedTryCatch RedTryFail)+
    qed
  next
    assume "¬ final e1"
    with WTrtTry show ?thesis by simp (fast intro:TryRed)
  qed
next
  case WTrtNil thus ?case by simp
next
  case (WTrtCons E e T es Ts)
  have IHe: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧
                ⟹ ∃e' s' ta. extTA,P,t ⊢ ⟨e,(h,l)⟩ -ta→ ⟨e',s'⟩"
   and IHes: "⋀l. ⟦𝒟s es ⌊dom l⌋; ¬ finals es⟧
             ⟹ ∃es' s' ta. extTA,P,t ⊢ ⟨es,(h,l)⟩ [-ta→] ⟨es',s'⟩"
   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 not_fins_tl: "¬ finals es" using not_fins e by simp
      show ?thesis using e IHes[OF Des' 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 "¬ final e"
    with IHe[OF De] show ?thesis by(fast intro!:ListRed1)
  qed
qed

end