Theory Progress

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

header {* \isaheader{Progress of Small Step Semantics} *}
theory Progress
imports WellTypeRT DefAss SmallStep "../Common/Conform" WWellForm
begin

lemma final_addrE:
  "[| P,E,h \<turnstile> e : Class C; final e;
    !!a. e = addr a ==> R;
    !!a. e = Throw a ==> R |] ==> R"
by(auto elim!: final.cases)

lemma finalRefE:
 "[| P,E,h \<turnstile> 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"
by(auto simp:final_iff elim!: refTE)


inductive WTrt' :: "J_prog => heap => env => expr => ty => bool"
  and WTrts' :: "J_prog => heap => env => expr list => ty list => bool"
  for P :: "J_prog" and h :: "heap" where
  "is_class P C  ==> WTrt' P h E (new C) (Class C)"

| "[| WTrt' P h E e Integer; is_type P T |] ==> WTrt' P h E (newA T⌊e⌉) (T⌊⌉)"

| "[| WTrt' P h E e T; is_type P U |] ==> WTrt' P h E (Cast U e) U"

| "typeofh v = Some T ==> WTrt' P h E (Val v) T"

| "E V = Some T  ==> WTrt' P h E (Var V) T"

| "[| WTrt' P h E e1 T1; WTrt' P h E e2 T2; P \<turnstile> T1«bop»T2 : T |] ==> WTrt' P h E (e1«bop»e2) T"

| "[| WTrt' P h E (Var V) T; WTrt' P h E e T'; P \<turnstile> T' ≤ T |] ==> WTrt' P h E (V:=e) Void"

| "[| WTrt' P h E a (T⌊⌉); WTrt' P h E i Integer |] ==> WTrt' P h E (a⌊i⌉) T"

| "[| WTrt' P h E a NT; WTrt' P h E i Integer |] ==> WTrt' P h E (a⌊i⌉) T"

| "[| WTrt' P h E a (T⌊⌉); WTrt' P h E i Integer; WTrt' P h E e T' |] ==> WTrt' P h E (a⌊i⌉ := e) Void"

| "[| WTrt' P h E a NT; WTrt' P h E i Integer; WTrt' P h E e T' |] ==> WTrt' P h E (a⌊i⌉ := e) Void"

| "WTrt' P h E a (T⌊⌉) ==> WTrt' P h E (a•length) Integer"

| "WTrt' P h E a NT ==> WTrt' P h E (a•length) T"

| "[| WTrt' P h E e (Class C); P \<turnstile> C has F:T in D |] ==> WTrt' P h E (e•F{D}) T"

| "WTrt' P h E e NT ==> WTrt' P h E (e•F{D}) T"

| "[| WTrt' P h E e1 (Class C); P \<turnstile> C has F:T in D; WTrt' P h E e2 T2; P \<turnstile> T2 ≤ T |] ==> WTrt' P h E (e1•F{D}:=e2) Void"

| "[| WTrt' P h E e1 NT; WTrt' P h E e2 T2 |] ==> WTrt' P h E (e1•F{D}:=e2) Void"

| "[| WTrt' P h E e (Class C); ¬ is_external_call P (Class C) M; P \<turnstile> C sees M:Ts -> T = (pns,body) in D;
     WTrts' P h E es Ts'; P \<turnstile> Ts' [≤] Ts |] ==> WTrt' P h E (e•M(es)) T"

| "[| WTrt' P h E e NT; WTrts' P h E es Ts |] ==> WTrt' P h E (e•M(es)) T"

| "[| WTrt' P h E e T; WTrts' P h E es Ts; P \<turnstile> T•M(Ts) :: U |] ==> WTrt' P h E (e•M(es)) U"

| "[| typeofh v = Some T1; P \<turnstile> T1 ≤ T; WTrt' P h (E(V\<mapsto>T)) e2 T2 |] ==> WTrt' P h E {V:T=⌊v⌋; e2} T2"

| "[| WTrt' P h (E(V\<mapsto>T)) e T' |] ==> WTrt' P h E {V:T=None; e} T'"

| "[| WTrt' P h E o' T; is_refT T; T ≠ NT; WTrt' P h E e T' |] ==> WTrt' P h E (sync(o') e) T'"

| "[| WTrt' P h E o' NT; WTrt' P h E e T |] ==> WTrt' P h E (sync(o') e) T'"

| "[| WTrt' P h E (addr a) T; WTrt' P h E e T' |] ==> WTrt' P h E (insync(a) e) T'"

| "[| WTrt' P h E e1 T1; WTrt' P h E e2 T2 |] ==> WTrt' P h E (e1;;e2) T2"

| "[| WTrt' P h E e Boolean; WTrt' P h E e1 T1; WTrt' P h E e2 T2; 
       P \<turnstile> T1 ≤ T2 ∨ P \<turnstile> T2 ≤ T1; P \<turnstile> T1 ≤ T2 --> T = T2; P \<turnstile> T2 ≤ T1 ==> T = T1 |]
    ==> WTrt' P h E (if (e) e1 else e2) T"

| "[| WTrt' P h E e Boolean; WTrt' P h E c T |] ==> WTrt' P h E (while(e) c) Void"

| "[| WTrt' P h E e T; P \<turnstile> T ≤ Class Throwable |] ==> WTrt' P h E (throw e) T'"

| "[| WTrt' P h E e1 T1; WTrt' P h (E(V \<mapsto> Class C)) e2 T2; P \<turnstile> T1 ≤ T2 |] ==> WTrt' P h E (try e1 catch(C V) e2) T2"

| "WTrts' P h E [] []"

| "[| WTrt' P h E e T; WTrts' P h E es Ts |] ==> WTrts' P h E (e # es) (T # Ts)"

abbreviation
  WTrt'_syntax :: "J_prog => env => heap => expr => ty => bool" ("_,_,_ \<turnstile> _ :' _"   [51,51,51]50)
where
  "P,E,h \<turnstile> e :' T ≡ WTrt' P h E e T"

abbreviation
  WTrts'_syntax :: "J_prog => env => heap => expr list => ty list => bool" ("_,_,_ \<turnstile> _ [:''] _"   [51,51,51]50)
where
  "P,E,h \<turnstile> e [:'] T ≡ WTrts' P h E e T"

inductive_cases WTrt'_elim_cases[elim!]:
  "P,E,h \<turnstile> V :=e :' T"

lemma [iff]: "P,E,h \<turnstile> e1;;e2 :' T2 = (∃T1. P,E,h \<turnstile> e1:' T1 ∧ P,E,h \<turnstile> e2:' T2)"
by (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)

lemma [iff]: "P,E,h \<turnstile> Val v :' T = (typeofh v = Some T)"
by (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)

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


lemma wt_wt': "P,E,h \<turnstile> e : T ==> P,E,h \<turnstile> e :' T"
  and wts_wts': "P,E,h \<turnstile> es [:] Ts ==> P,E,h \<turnstile> es [:'] Ts"
apply (induct rule:WTrt_WTrts.inducts)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)
apply(clarsimp split: option.split_asm simp del: fun_upd_apply)
 apply(erule WTrt'_WTrts'.intros)
apply(blast intro: WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)+
done



lemma wt'_wt: "P,E,h \<turnstile> e :' T ==> P,E,h \<turnstile> e : T"
  and wts'_wts: "P,E,h \<turnstile> es [:'] Ts ==> P,E,h \<turnstile> es [:] Ts"
apply (induct rule:WTrt'_WTrts'.inducts)
apply(blast intro:WTrt_WTrts.intros)+
apply(erule WTrt_WTrts.intros, simp)
apply(erule WTrt_WTrts.intros, simp)
apply(erule WTrt_WTrts.intros, assumption+)
apply(erule WTrtSynchronizedNT, assumption)
apply(blast intro: WTrt_WTrts.intros)+
done


corollary wt'_iff_wt: "(P,E,h \<turnstile> e :' T) = (P,E,h \<turnstile> e : T)"
  and  wts'_iff_wts: "(P,E,h \<turnstile> es [:'] Ts) = (P,E,h \<turnstile> es [:] Ts)"
by(blast intro:wt_wt' wt'_wt wts_wts' wts'_wts)+


(*<*)
lemmas WTrt_induct2 = WTrt'_WTrts'.inducts[unfolded wt'_iff_wt wts'_iff_wts,
 case_names WTrtNew WTrtNewArray WTrtCast WTrtVal WTrtVar WTrtBinOp WTrtLAss
 WTrtAAcc WTrtAAccNT WTrtAAss WTrtAAssNT WTrtALength WTrtALengthNT WTrtFAcc WTrtFAccNT WTrtFAss
 WTrtFAssNT WTrtCall WTrtCallNT WTrtCallExternal
 WTrtInitBlock WTrtBlock WTrtSynchronized WTrtSynchronizedNT WTrtInSynchronized WTrtSeq WTrtCond
 WTrtWhile WTrtThrow WTrtTry WTrtNil WTrtCons, consumes 1]
(*>*)

theorem red_progress:
  assumes wf: "wwf_J_prog P" and hconf: "P \<turnstile> h \<surd>"
  shows progress: "[| P,E,h \<turnstile> e : T; \<D> e ⌊dom l⌋; ¬ final e |] ==> ∃e' s' ta. extTA,P \<turnstile> ⟨e,(h,l)⟩ -ta-> ⟨e',s'⟩"
  and progresss: "[| P,E,h \<turnstile> es [:] Ts; \<D>s es ⌊dom l⌋; ¬ finals es |] ==> ∃es' s' ta. extTA,P \<turnstile> ⟨es,(h,l)⟩ [-ta->] ⟨es',s'⟩"
proof (induct arbitrary: l and l rule:WTrt_induct2)
  case WTrtNew
  show ?case
  proof cases
    assume "∃a. h a = None"
    from prems show ?thesis
      by (fastsimp del:exE intro!:RedNew simp add:new_Addr_def
                   elim!:wf_Fields_Ex[THEN exE])
  next
    assume "¬(∃a. h a = None)"
    from prems show ?thesis
      by(fastsimp intro:RedNewFail simp add:new_Addr_def)
  qed
next
  case (WTrtNewArray E e T l)
  have IH: "!!l. [|\<D> e ⌊dom l⌋; ¬ final e|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e,(h,l)⟩ -tas-> ⟨e', s'⟩"
   and D: "\<D> (newA T⌊e⌉) ⌊dom l⌋"
   and ei: "P,E,h \<turnstile> e : Integer" by fact+
  from D have De: "\<D> e ⌊dom l⌋" by auto
  show ?case
  proof cases 
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v
      assume [simp]: "e = Val v"
      with ei have "typeofh v = Some Integer" by fastsimp
      hence exei: "∃i. v = Intg i" by fastsimp
      then obtain i where "v = Intg i" by blast
      thus ?thesis
      proof (cases "i ≥ 0")
        assume "0 ≤ i"
        thus ?thesis
        proof (cases "new_Addr h")
          assume "new_Addr h = None"
          from prems have "extTA,P \<turnstile> ⟨newA T⌊Val(Intg i)⌉,(h, l)⟩ -ε-> ⟨THROW OutOfMemory,(h, l)⟩"
            by - (rule RedNewArrayFail, auto)
          with prems show ?thesis by blast
        next
          fix a
          assume "new_Addr h = ⌊a⌋"
          from prems have "extTA,P \<turnstile> ⟨newA T⌊Val(Intg i)⌉,(h, l)⟩ -ε-> ⟨addr a,(h(a\<mapsto>(Arr T (replicate (nat i) (default_val T)))), l)⟩"
            by - (rule RedNewArray, auto)
          with prems show ?thesis by blast
        qed
      next
        assume "¬ i ≥ 0"
        hence "i < 0" by arith
        with prems have "extTA,P \<turnstile> ⟨newA T⌊Val(Intg i)⌉,(h, l)⟩ -ε-> ⟨THROW NegativeArraySize,(h, l)⟩"
          by - (rule RedNewArrayNegative, auto)
        with prems show ?thesis by blast
      qed
    next
      fix exa
      assume "e = Throw exa"
      with prems have "extTA,P \<turnstile> ⟨newA T⌊Throw exa⌉,(h, l)⟩ -ε-> ⟨Throw exa,(h, l)⟩"
        by - (rule NewArrayThrow)
      with prems show ?thesis by blast
    qed
  next
    assume "¬ final e"
    with IH De have exes: "∃e' s' ta. extTA,P \<turnstile> ⟨e,(h, l)⟩ -ta-> ⟨e',s'⟩" by simp
    then obtain e' s' ta where "extTA,P \<turnstile> ⟨e,(h, l)⟩ -ta-> ⟨e',s'⟩" by blast
    hence "extTA,P \<turnstile> ⟨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 \<turnstile> e : T"
   and IH: "!!l. [|\<D> e ⌊dom l⌋; ¬ final e|]
                ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e,(h,l)⟩ -tas-> ⟨e',s'⟩"
   and D: "\<D> (Cast U e) ⌊dom l⌋" by fact+
  from D have De: "\<D> 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 prems obtain V where thvU: "typeofh v = ⌊V⌋" by fastsimp
      thus ?thesis
      proof (cases "P \<turnstile> V ≤ U")
        assume "P \<turnstile> V ≤ U"
        with prems have "extTA,P \<turnstile> ⟨Cast U (Val v),(h, l)⟩ -ε-> ⟨Val v,(h,l)⟩"
          by - (rule RedCast, auto)
        with ev show ?thesis by blast
      next
        assume "¬ P \<turnstile> V ≤ U"
        with prems have "extTA,P \<turnstile> ⟨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 WTrtVal thus ?case by(simp add:final_iff)
next
  case WTrtVar thus ?case by(fastsimp 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 "typeofh v1 = ⌊T1⌋" "typeofh v2 = ⌊T2⌋" by auto
          from binop_progress[OF this `P \<turnstile> T1«bop»T2 : T`] obtain v
            where "binop bop v1 v2 = ⌊v⌋" by blast
          thus ?thesis by(fastsimp intro: RedBinOp)
        next
          fix a assume "e2 = Throw a"
          thus ?thesis by(fastsimp intro:BinOpThrow2)
        qed
      next
        assume "¬ final e2" from prems 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" from prems show ?thesis
      by simp (fast intro:BinOpRed1)
  qed
next
  case (WTrtLAss E V T e T')
  show ?case
  proof cases
    assume "final e" from prems show ?thesis
      by(fastsimp simp:final_iff intro!:RedLAss LAssThrow)
  next
    assume "¬ final e" from prems show ?thesis
      by simp (fast intro:LAssRed)
  qed
next
  case (WTrtAAcc E a T i l)
  have wte: "P,E,h \<turnstile> a : T⌊⌉"
   and wtei: "P,E,h \<turnstile> i : Integer"
   and IHa: "!!l. [|\<D> a ⌊dom l⌋; ¬ final a|]
                 ==> ∃e' s' tas. extTA,P \<turnstile> ⟨a,(h,l)⟩ -tas-> ⟨e',s'⟩"
   and IHi: "!!l. [|\<D> i ⌊dom l⌋; ¬ final i|]
                 ==> ∃e' s' tas. extTA,P \<turnstile> ⟨i,(h,l)⟩ -tas-> ⟨e',s'⟩"
   and D: "\<D> (a⌊i⌉) ⌊dom l⌋" by fact+
  have ref: "is_refT (T⌊⌉)" by simp
  from D have Da: "\<D> a ⌊dom l⌋" by simp
  show ?case
  proof (cases "final a")
    assume "final a"
    with wte ref show ?case
    proof (rule finalRefE)
      assume "a = null"
      thus ?case
      proof (cases "final i")
        assume "final i"
        thus ?thesis
        proof (rule finalE)
          fix v
          assume "i = Val v"
          with prems have "extTA,P \<turnstile> ⟨null⌊Val v⌉, (h, l)⟩ -ε-> ⟨THROW NullPointer, (h,l)⟩"
            by - (rule RedAAccNull)
          with prems show ?thesis by blast
        next
          fix ex
          assume "i = Throw ex"
          with prems have "extTA,P \<turnstile> ⟨null⌊Throw ex⌉, (h, l)⟩ -ε-> ⟨Throw ex, (h,l)⟩"
            by - (rule AAccThrow2)
          with prems show ?thesis by blast
        qed
      next
        assume "¬ final i"
        from prems show ?thesis
          by simp
      qed
    next
      fix ad C
      assume "a = addr ad" "T⌊⌉ = Class C"
      thus ?case by simp
    next
      fix ad U
      assume "a = addr ad" "T⌊⌉ = U⌊⌉"
      thus ?case
      proof (cases "final i")
        assume "final i"
        thus ?thesis
        proof(rule finalE)
          fix v
          assume "i = Val v"
          with wtei have "typeofh v = Some Integer" by fastsimp
          hence "∃i. v = Intg i" by fastsimp
          then obtain i where "v = Intg i" by blast
          thus ?thesis
          proof (cases "h ad")
            assume "h ad = None"
            from prems show ?thesis by fastsimp
          next
            fix arrobj
            assume had: "h ad = Some arrobj"
            with wte prems have "typeofh (Addr ad) = Some (T⌊⌉)" by fastsimp
            with had have "∃el. h ad = Some(Arr T el)" by(auto split: heapobj.split_asm)
            then obtain el where "h ad = Some(Arr T el)" ..
            thus ?thesis
            proof (cases "i < 0")
              assume "i < 0"
              from prems show ?thesis by (fastsimp intro: RedAAccBounds)
            next
              assume "¬ i < 0"
              hence "i ≥ 0" by arith
              thus ?thesis
              proof (cases "i ≥ int (length el)")
               case True
               from prems show ?thesis by (fastsimp intro: RedAAccBounds)
              next
               case False
               hence "i < int (length el)" by arith
               with prems show ?thesis by (fastsimp intro: RedAAcc)
              qed
            qed
          qed
        next
          fix ex
          assume "i = Throw ex"
          with prems show ?thesis by (fastsimp intro: AAccThrow2)
        qed
      next
        assume "¬ final i"
        with prems show ?thesis by (fastsimp intro: AAccRed2)
      qed
    next
      fix ex
      assume "a = Throw ex"
      with prems show ?thesis by (fastsimp intro: AAccThrow1)
    qed
  next
    assume "¬ final a"
    with prems Da show ?thesis by (fastsimp intro: AAccRed1)
  qed
next
  case (WTrtAAccNT E a i T l)
  have wte: "P,E,h \<turnstile> a : NT"
   and wtei: "P,E,h \<turnstile> i : Integer"
   and IHa: "!!l. [|\<D> a ⌊dom l⌋; ¬ final a|]
                 ==> ∃e' s' tas. extTA,P \<turnstile> ⟨a,(h,l)⟩ -tas-> ⟨e',s'⟩"
   and IHi: "!!l. [|\<D> i ⌊dom l⌋; ¬ final i|]
                 ==> ∃e' s' tas. extTA,P \<turnstile> ⟨i,(h,l)⟩ -tas-> ⟨e',s'⟩" by fact+
  have ref: "is_refT NT" by simp
  with prems have Da: "\<D> a ⌊dom l⌋" by simp
  thus ?case
  proof (cases "final a")
    assume "final a"
    with wte ref show ?thesis
    proof (rule finalRefE)
      assume "a = null"
      thus ?case
      proof (cases "final i")
        assume "final i"
        thus ?thesis
        proof (rule finalE)
          fix v
          assume "i = Val v"
          with prems have "extTA,P \<turnstile> ⟨null⌊Val v⌉, (h, l)⟩ -ε-> ⟨THROW NullPointer, (h,l)⟩"
            by - (rule RedAAccNull)
          with prems show ?thesis by blast
        next
          fix ex
          assume "i = Throw ex"
          with prems have "extTA,P \<turnstile> ⟨null⌊Throw ex⌉, (h, l)⟩ -ε-> ⟨Throw ex, (h,l)⟩"
            by - (rule AAccThrow2)
          with prems show ?thesis by blast
        qed
      next
        assume "¬ final i"
        from prems show ?thesis
          by(fastsimp intro: AAccRed2)
      qed
    next
      fix ad C
      assume "NT = Class C"
      thus ?thesis by simp
    next
      fix ad U
      assume "NT = U⌊⌉"
      thus ?thesis by simp
    next
      fix ex
      assume "a = Throw ex"
      thus ?thesis by (fastsimp intro: AAccThrow1)
    qed
  next
    assume "¬ final a"
    with prems Da show ?thesis by (fastsimp intro:AAccRed1)
  qed
next
  case (WTrtAAss E a T i e T' l)
  have wta: "P,E,h \<turnstile> a : T⌊⌉"
    and wti: "P,E,h \<turnstile> i : Integer"
    and wte: "P,E,h \<turnstile> e : T'"
    and D: "\<D> (a⌊i⌉ := e) ⌊dom l⌋"
    and IH1: "!!l. [|\<D> a ⌊dom l⌋; ¬ final a|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨a,(h, l)⟩ -tas-> ⟨e',s'⟩"
    and IH2: "!!l. [|\<D> i ⌊dom l⌋; ¬ final i|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨i,(h, l)⟩ -tas-> ⟨e',s'⟩"
    and IH3: "!!l. [|\<D> e ⌊dom l⌋; ¬ final e|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨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(rule finalRefE)
      assume "a = null"
      show ?case
      proof(cases "final i")
        assume "final i"
        thus ?case
        proof (rule finalE)
          fix v
          assume "i = Val v"
          with wti have "typeofh v = Some Integer" by fastsimp
          hence "∃idx. v = Intg idx" by fastsimp
          then obtain idx where "v = Intg idx" by blast
          thus ?thesis
          proof (cases "final e")
            assume "final e"
            thus ?case
            proof (rule finalE)
              fix w
              assume "e = Val w"
              with prems show ?thesis by (fastsimp intro: RedAAssNull)
            next
              fix ex
              assume "e = Throw ex"
              with prems show ?thesis by (fastsimp intro: AAssThrow3)
            qed
          next
            assume "¬ final e"
            with prems show ?thesis by (fastsimp intro: AAssRed3)
          qed
        next
          fix ex
          assume "i = Throw ex"
          with prems show ?thesis by (fastsimp intro: AAssThrow2)
        qed
      next
        assume "¬ final i"
        with prems show ?thesis by (fastsimp intro: AAssRed2)
      qed
    next
      fix ad C
      assume "T⌊⌉ = Class C"
      thus ?case by simp
    next
      fix ad U
      assume aad: "a = addr ad" "T⌊⌉ = U⌊⌉"
      thus ?case
      proof (cases "final i")
        assume fi: "final i"
        thus ?case
        proof (rule finalE)
          fix v
          assume ivalv: "i = Val v"
          with wti have "typeofh v = Some Integer" by fastsimp
          hence "∃idx. v = Intg idx" by fastsimp
          then obtain idx where vidx: "v = Intg idx" by blast
          thus ?thesis
          proof (cases "final e")
            assume fe: "final e"
            thus ?case
            proof(rule finalE)
              fix w
              assume evalw: "e = Val w"
              show ?case
              proof (cases "h ad")
               assume "h ad = None"
               from prems show ?thesis by fastsimp
              next
               fix arrobj
               assume had: "h ad = Some arrobj"
               with wta prems have "typeofh (Addr ad) = Some (T⌊⌉)" by fastsimp
               with had have "∃el. h ad = Some(Arr T el)" by(auto split: heapobj.split_asm)
               then obtain el where "h ad = Some(Arr T el)" ..
               thus ?thesis
               proof (cases "idx < 0")
                 assume "idx < 0"
                 from prems show ?case by (fastsimp intro:RedAAssBounds)
               next
                 assume "¬ idx < 0"
                 hence idxg0: "idx ≥ 0" by arith
                 thus ?case
                 proof (cases "idx ≥ int (length el)")
                   assume "idx ≥ int (length el)"
                   from prems show ?case by (fastsimp intro:RedAAssBounds)
                 next
                   assume "¬ idx ≥ int (length el)"
                   hence idxlsi: "idx < int (length el)" by arith
                   from wte evalw have "typeofh w = Some T'" by fastsimp
                   with prems idxlsi idxg0 show ?case
                   proof(cases "P \<turnstile> T' ≤ T")
                     assume "P \<turnstile> T' ≤ T"
                     with prems show ?thesis by(fastsimp intro: RedAAss)
                   next
                     assume "¬ P \<turnstile> T' ≤ T"
                     with prems show ?thesis by(fastsimp intro: RedAAssStore)
                   qed
                 qed
               qed
              qed
            next
              fix ex
              assume "e = Throw ex"
              with prems show ?case by (fastsimp intro: AAssThrow3)
            qed
          next
            assume "¬ final e"
            from prems show ?case by (fastsimp intro: AAssRed3)
          qed
        next
          fix ex
          assume "i = Throw ex"
          from prems show ?case by (fastsimp intro: AAssThrow2)
        qed
      next
        assume "¬ final i"
        from prems show ?case by (fastsimp intro: AAssRed2)
      qed
    next
      fix ex
      assume "a = Throw ex"
      from prems show ?case by (fastsimp intro:AAssThrow1)
    qed
  next
    assume "¬ final a"
    from prems show ?case by (fastsimp intro: AAssRed1)
  qed
next
  case (WTrtAAssNT E a i e T' l)
  have wta: "P,E,h \<turnstile> a : NT"
    and wti: "P,E,h \<turnstile> i : Integer"
    and wte: "P,E,h \<turnstile> e : T'"
    and D: "\<D> (a⌊i⌉ := e) ⌊dom l⌋"
    and IH1: "!!l. [|\<D> a ⌊dom l⌋; ¬ final a|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨a,(h, l)⟩ -tas-> ⟨e',s'⟩"
    and IH2: "!!l. [|\<D> i ⌊dom l⌋; ¬ final i|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨i,(h, l)⟩ -tas-> ⟨e',s'⟩"
    and IH3: "!!l. [|\<D> e ⌊dom l⌋; ¬ final e|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨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"
        from prems show ?thesis
          by(fastsimp simp:final_iff intro: RedAAssNull AAssThrow1 AAssThrow2 AAssThrow3)
      next
        assume "¬ final e"
        from prems show ?thesis by (fastsimp simp: final_iff intro!:AAssRed3 AAssThrow1 AAssThrow2)
      qed
    next
      assume "¬ final i"
      from prems show ?thesis by (fastsimp simp: final_iff intro!:AAssRed2 AAssThrow1)
    qed
  next
    assume "¬ final a"
    from prems show ?thesis by (fastsimp 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 \<turnstile> a : T⌊⌉`
    thus ?thesis
    proof(rule finalRefE[OF _ _ True])
      show "is_refT (T⌊⌉)" by simp
    next
      assume "a = null"
      thus ?thesis by(fastsimp intro: RedALengthNull)
    next
      fix ad U
      assume [simp]: "a = addr ad" and "T⌊⌉ = U⌊⌉"
      hence [simp]: "T = U" by(auto)
      show ?thesis
      proof(cases "h ad")
        case None 
        with wta show ?thesis by fastsimp
      next
        case (Some aa)
        with wta obtain elem where "h ad = ⌊Arr U elem⌋"
          by(cases aa, auto)
        thus ?thesis by(fastsimp intro: RedALength)
      qed
    next
      fix ad
      assume "a = Throw ad"
      thus ?thesis by (fastsimp intro: ALengthThrow)
    qed(fastsimp)
  next
    case False
    from `\<D> (a•length) ⌊dom l⌋` have "\<D> a ⌊dom l⌋" by simp
    with False `[|\<D> a ⌊dom l⌋; ¬ final a|] ==> ∃e' s' ta. extTA,P \<turnstile> ⟨a,(h, l)⟩ -ta-> ⟨e',s'⟩`
    obtain e' s' ta where "extTA,P \<turnstile> ⟨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 \<turnstile> 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(fastsimp+)
  next
    case False
    from `\<D> (a•length) ⌊dom l⌋` have "\<D> a ⌊dom l⌋" by simp
    with False `[|\<D> a ⌊dom l⌋; ¬ final a|] ==> ∃e' s' ta. extTA,P \<turnstile> ⟨a,(h, l)⟩ -ta-> ⟨e',s'⟩`
    obtain e' s' ta where "extTA,P \<turnstile> ⟨a,(h, l)⟩ -ta-> ⟨e',s'⟩" by blast
    thus ?thesis by(blast intro: ALengthRed)
  qed
next
  case (WTrtFAcc E e C F T D l)
  have wte: "P,E,h \<turnstile> e : Class C"
   and field: "P \<turnstile> C has F: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(Obj C fs)" apply (auto) apply(case_tac aa) by auto
      with hconf have "P,h \<turnstile> (Obj C fs) \<surd>" using hconf_def by fastsimp
      then obtain v where "fs(F,D) = Some v" using field
        by(fastsimp dest:has_fields_fun simp:oconf_def has_field_def)
      with hp e show ?thesis by(fastsimp intro:RedFAcc)
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fastsimp intro:FAccThrow)
    qed
  next
    assume "¬ final e" from prems show ?thesis
      by(fastsimp 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}"
    from prems show ?thesis
      by(fastsimp simp:final_iff intro: RedFAccNull FAccThrow)
  next
    assume "¬ final e" --"@{term e} reduces by IH"
    from prems show ?thesis by simp (fast intro:FAccRed)
  qed
next
  case (WTrtFAss E e1 C F T D e2 T2 l)
  have wte1: "P,E,h \<turnstile> e1 : Class C" 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(fastsimp split: heapobj.split_asm intro: RedFAss)
        next
          fix a assume "e2 = Throw a"
          thus ?thesis using e1 by(fastsimp intro:FAssThrow2)
        qed
      next
        assume "¬ final e2" from prems show ?thesis
          by simp (fast intro!:FAssRed2)
      qed
    next
      fix a assume "e1 = Throw a"
      thus ?thesis by(fastsimp intro:FAssThrow1)
    qed
  next
    assume "¬ final e1" from prems show ?thesis
      by simp (blast intro!:FAssRed1)
  qed
next
  case (WTrtFAssNT E e1 e2 T2 F D l)
  show ?case
  proof cases
    assume "final e1"  --"@{term e1} is @{term null} or @{term throw}"
    show ?thesis
    proof cases
      assume "final e2"  --"@{term e2} is @{term Val} or @{term throw}"
      from prems show ?thesis
        by(fastsimp simp:final_iff intro: RedFAssNull FAssThrow1 FAssThrow2)
    next
      assume  "¬ final e2" --"@{term e2} reduces by IH"
      from prems show ?thesis
        by (fastsimp  simp:final_iff intro!:FAssRed2 FAssThrow1)
    qed
  next
    assume "¬ final e1" --"@{term e1} reduces by IH"
    from prems show ?thesis by (fastsimp intro:FAssRed1)
  qed
next
  case (WTrtCall E e C M Ts T pns body D es Ts' l)
  have wte: "P,E,h \<turnstile> e : Class C" by fact
  have IHe: "!!l. [| \<D> e ⌊dom l⌋; ¬ final e |]
             ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e,(h, l)⟩ -tas-> ⟨e',s'⟩" by fact
  have sees: "P \<turnstile> C sees M: Ts->T = (pns, body) in D" by fact
  have nexc: "¬ is_external_call P (Class C) M" by fact
  have wtes: "P,E,h \<turnstile> es [:] Ts'" by fact
  have IHes: "!!l. [|\<D>s es ⌊dom l⌋; ¬ finals es|] ==> ∃es' s' ta. extTA,P \<turnstile> ⟨es,(h, l)⟩ [-ta->] ⟨es',s'⟩" by fact
  have subtype: "P \<turnstile> Ts' [≤] Ts" by fact
  have dae: "\<D> (e•M(es)) ⌊dom l⌋" by fact
  show ?case
  proof(cases "final e")
    assume fine: "final e"
    with wte 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 fs where ha: "h a = ⌊Obj C fs⌋"  by(auto split: heapobj.split_asm)
        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)
        thus ?thesis using e_addr ha sees subtype es sees_wf_mdecl[OF wf sees] nexc
          by (fastsimp intro!: RedCall simp:list_all2_def 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(fastsimp 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(fastsimp 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(fastsimp intro!:CallParams)
        qed
      qed
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fast intro!:CallThrowObj)
    qed
  next
    assume "¬ final e"
    with prems show ?thesis by simp (blast intro!:CallObj)
  qed
next
  case (WTrtCallNT E e es Ts M T l)
  have wte: "P,E,h \<turnstile> e : NT" by fact
  have IHe: "!!l. [| \<D> e ⌊dom l⌋; ¬ final e |]
             ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e,(h, l)⟩ -tas-> ⟨e',s'⟩"  by fact
  have IHes: "!!l. [|\<D>s es ⌊dom l⌋; ¬ finals es|] ==> ∃es' s' ta. extTA,P \<turnstile> ⟨es,(h, l)⟩ [-ta->] ⟨es',s'⟩" by fact
  have wtes: "P,E,h \<turnstile> es [:] Ts" by fact
  have dae: "\<D> (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 prems by simp
      have ?case
      proof cases
        assume "finals es"
        moreover
        { fix vs assume "es = map Val vs"
          from prems have ?thesis by(fastsimp intro: RedCallNull) }
        moreover
        { fix vs a es' assume "es = map Val vs @ Throw a # es'"
          from prems have ?thesis by(fastsimp intro: CallThrowParams) }
        ultimately show ?thesis by(fastsimp simp:finals_def)
      next
        assume "¬ finals es" --"@{term es} reduces by IH"
        from prems show ?thesis by(fastsimp intro: CallParams)
      qed
    }
    moreover
    { fix a assume "e = Throw a"
      from prems have ?case by(fastsimp intro: CallThrowObj) }
    ultimately show ?thesis by(fastsimp simp:final_iff)
  next
    assume "¬ final e" --"@{term e} reduces by IH"
    from prems show ?thesis by (fastsimp intro:CallObj)
  qed
next
  case (WTrtCallExternal E e T es Ts M U l)
  have wte: "P,E,h \<turnstile> e : T" by fact
  have IHe: "!!l. [| \<D> e ⌊dom l⌋; ¬ final e |]
             ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e,(h, l)⟩ -tas-> ⟨e',s'⟩" by fact
  have wtes: "P,E,h \<turnstile> es [:] Ts" by fact
  have IHes: "!!l. [|\<D>s es ⌊dom l⌋; ¬ finals es|] ==> ∃es' s' ta. extTA,P \<turnstile> ⟨es,(h, l)⟩ [-ta->] ⟨es',s'⟩" by fact
  have wtext: "P \<turnstile> T•M(Ts) :: U" by fact
  have dae: "\<D> (e•M(es)) ⌊dom l⌋" by fact
  show ?case
  proof(cases "final e")
    assume fine: "final e"
    from wtext have "T ≠ NT" by(rule external_WT_not_NT)
    with is_external_call_is_refT[OF external_WT_is_external_call[OF wtext]] fine wte
    obtain a where e: "e = addr a ∨ e = Throw a" by(auto elim!: final.cases is_refT.cases)
    thus ?thesis
    proof
      assume e: "e = addr a"
      from e wte have tya: "typeofh (Addr a) = ⌊T⌋" by simp
      show ?thesis
      proof(cases "finals es")
        case True
        hence "(∃vs. es = map Val vs) ∨ (∃vs a es'. es = map Val vs @ Throw a # es')" unfolding finals_def .
        thus ?thesis
        proof
          assume "∃vs. es = map Val vs"
          then obtain vs where es: "es = map Val vs" ..
          with wtes have tyes: "map typeofh vs = map Some Ts" by simp
          with tya have "P,h \<turnstile> a•M(vs) : U" using wtext by(rule external_WT'.intros)
          from external_call_progress[OF this] obtain ta va h'
            where "P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩" by blast
          thus ?thesis using tya external_WT_is_external_call[OF wtext] e es
            by(fastsimp intro: RedCallExternal simp del: split_paired_Ex)
        next
          assume "∃vs a es'. es = map Val vs @ Throw a # es'"
          with e show ?thesis by(auto intro: CallThrowParams simp del: split_paired_Ex)
        qed
      next
        case False
        from dae IHes[OF _ this, of l] e show ?thesis by(fastsimp intro!: CallParams)
      qed
    next
      assume "e = Throw a"
      thus ?thesis by(auto intro: CallThrowObj simp del: split_paired_Ex)
    qed
  next
    case False
    with dae IHe[OF _ False, of l] show ?thesis by(fastsimp intro: CallObj)
  qed
next
  case (WTrtInitBlock v T1 T E V e2 T2 l)
  have IH2: "!!l.  [|\<D> e2 ⌊dom l⌋; ¬ final e2|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e2,(h, l)⟩ -tas-> ⟨e',s'⟩"
   and D: "\<D> {V:T=⌊v⌋; e2} ⌊dom l⌋" by fact+
  show ?case
  proof cases
    assume "final e2"
    thus ?thesis
    proof (rule finalE)
      fix v2 assume "e2 = Val v2"
      thus ?thesis by(fast intro:RedBlock)
    next
      fix a assume "e2 = Throw a"
      thus ?thesis by(fast intro:BlockThrow)
    qed
  next
    assume not_fin2: "¬ final e2"
    from D have D2: "\<D> e2 ⌊dom(l(V\<mapsto>v))⌋" by (auto simp:hyperset_defs)
    from IH2[OF D2 not_fin2]
    obtain h' l' e' tas where red2: "extTA,P \<turnstile> ⟨e2,(h, l(V\<mapsto>v))⟩ -tas-> ⟨e',(h', l')⟩"
      by fast
    from red_lcl_incr[OF red2] have "V ∈ dom l'" by auto
    with red2 show ?thesis by(fastsimp intro:BlockRed)
  qed
next
  case (WTrtBlock E V T e T' l)
  have IH: "!!l. [|\<D> e ⌊dom l⌋; ¬ final e|]
                 ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e,(h,l)⟩ -tas-> ⟨e',s'⟩"
   and D: "\<D> {V:T=None; 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: "\<D> e ⌊dom(l(V:=None))⌋" by(simp add:hyperset_defs)
    from IH[OF De not_fin]
    obtain h' l' e' tas where red: "extTA,P \<turnstile> ⟨e,(h,l(V:=None))⟩ -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 \<turnstile> o' : T`
  note IHe = `!!l. [|\<D> e ⌊dom l⌋; ¬ final e |] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e,(h, l)⟩ -tas-> ⟨e',s'⟩`
  note wte = `P,E,h \<turnstile> e : T'`
  note IHo = `!!l. [|\<D> o' ⌊dom l⌋; ¬ final o' |] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨o',(h, l)⟩ -tas-> ⟨e',s'⟩`
  note refT = `is_refT T`
  note TNT = `T ≠ NT`
  note dae = `\<D> (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(fastsimp intro: SynchronizedNull)
      next
        fix ad
        assume vaddr: "v = Addr ad"
        from wto oval vaddr obtain arrobj where ha: "h ad = ⌊arrobj⌋" by auto
        thus ?thesis using oval vaddr
          by(fastsimp intro: LockSynchronized)
      qed(auto elim: refTE)
    next
      fix a
      assume othrow: "o' = Throw a"
      thus ?thesis by(fastsimp intro: SynchronizedThrow1)
    qed
  next
    assume nfino: "¬ final o'"
    with dae IHo show ?case by(fastsimp intro: SynchronizedRed1)
  qed
next
  case (WTrtSynchronizedNT E o' e T T' l)
  have wto: "P,E,h \<turnstile> o' : NT" by fact
  have IHo: "!!l. [|\<D> o' ⌊dom l⌋; ¬ final o' |]
                  ==> ∃e' s' tas. extTA,P \<turnstile> ⟨o',(h, l)⟩ -tas-> ⟨e',s'⟩" by fact
  have dae: "\<D> (sync(o') e) ⌊dom l⌋" by fact
  show ?case
  proof(cases "final o'")
    assume "final o'" thus ?thesis using wto
      by(fastsimp elim!: finalE intro: SynchronizedNull SynchronizedThrow1)
  next
    assume nfino: "¬ final o'"
    with dae IHo nfino show ?thesis by(fastsimp intro: SynchronizedRed1)
  qed
next
  case (WTrtInSynchronized E a T e T' l)
  show ?case
  proof(cases "final e")
    case True thus ?thesis
      by(fastsimp elim!: finalE intro: UnlockSynchronized SynchronizedThrow2)
  next
    case False 
    moreover from `\<D> (insync(a) e) ⌊dom l⌋` have "\<D> e ⌊dom l⌋" by simp
    moreover note IHe = `!!l. [|\<D> e ⌊dom l⌋; ¬ final e|] ==> ∃e' s' tas. extTA,P \<turnstile> ⟨e,(h, l)⟩ -tas-> ⟨e',s'⟩`
    ultimately show ?thesis by(fastsimp 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" from prems show ?thesis
      by simp (blast intro:SeqRed)
  qed
next
  case (WTrtCond E e e1 T1 e2 T2 T l)
  have wt: "P,E,h \<turnstile> 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(fastsimp intro:RedCondT)
      next
        case False with val v show ?thesis by(fastsimp intro:RedCondF)
      qed
    next
      fix a assume "e = Throw a"
      thus ?thesis by(fast intro:CondThrow)
    qed
  next
    assume "¬ final e" from prems 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 \<turnstile> T ≤ Class Throwable` `¬ final (throw e)` `P,E,h \<turnstile> e : T`
      have "v = Null" by(auto simp add: final_iff widen_Class)
      thus ?thesis using Val by(fastsimp intro: RedThrowNull)
    next
      case (Throw a)
      thus ?thesis by(fastsimp intro: ThrowThrow)
    qed
  next
    assume "¬ final e" -- {*Then @{term e} must reduce*}
    from prems show ?thesis by simp (blast intro:ThrowRed)
  qed
next
  case (WTrtTry E e1 T1 V C e2 T2 l)
  have wt1: "P,E,h \<turnstile> 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(Obj D fs)"
        by(fastsimp split: heapobj.split_asm simp add: widen_Class)
      show ?thesis
      proof cases
        assume "P \<turnstile> D \<preceq>* C"
        with e1_Throw ha show ?thesis by(fastsimp intro!:RedTryCatch)
      next
        assume "¬ P \<turnstile> D \<preceq>* C"
        with e1_Throw ha show ?thesis by(force intro!:RedTryFail)
      qed
    qed
  next
    assume "¬ final e1"
    show ?thesis using prems by simp (fast intro:TryRed)
  qed
next
  case WTrtNil thus ?case by simp
next
  case (WTrtCons E e T es Ts)
  have IHe: "!!l. [|\<D> e ⌊dom l⌋; ¬ final e|]
                ==> ∃e' s' ta. extTA,P \<turnstile> ⟨e,(h,l)⟩ -ta-> ⟨e',s'⟩"
   and IHes: "!!l. [|\<D>s es ⌊dom l⌋; ¬ finals es|]
             ==> ∃es' s' ta. extTA,P \<turnstile> ⟨es,(h,l)⟩ [-ta->] ⟨es',s'⟩"
   and D: "\<D>s (e#es) ⌊dom l⌋" and not_fins: "¬ finals(e # es)" by fact+
  have De: "\<D> e ⌊dom l⌋" and Des: "\<D>s es (⌊dom l⌋ \<squnion> \<A> 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': "\<D>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