Theory TypeSafe

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

section ‹Type Safety Proof›

theory TypeSafe
imports
  Progress
  DefAssPreservation
begin

subsection‹Basic preservation lemmas›

text‹First two easy preservation lemmas.›

theorem (in J_conf_read)
  shows red_preserves_hconf:
  "⟦ extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩; P,E,hp s ⊢ e : T; hconf (hp s) ⟧ ⟹ hconf (hp s')"
  and reds_preserves_hconf:
  "⟦ extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩; P,E,hp s ⊢ es [:] Ts; hconf (hp s) ⟧ ⟹ hconf (hp s')"
proof (induct arbitrary: T E and Ts E rule: red_reds.inducts)
  case RedNew thus ?case
    by(auto intro: hconf_heap_ops_mono)
next
  case RedNewFail thus ?case
    by(auto intro: hconf_heap_ops_mono)
next
  case RedNewArray thus ?case
    by(auto intro: hconf_heap_ops_mono)
next
  case RedNewArrayFail thus ?case
    by(auto intro: hconf_heap_ops_mono)
next
  case (RedAAss h a U n i v U' h' l)
  from ‹sint i < int n› ‹0 <=s i›
  have "nat (sint i) < n"
    by (simp add: word_sle_eq nat_less_iff)
  thus ?case using RedAAss
    by(fastforce elim: hconf_heap_write_mono intro: addr_loc_type.intros simp add: conf_def)
next
  case RedFAss thus ?case
    by(fastforce elim: hconf_heap_write_mono intro: addr_loc_type.intros simp add: conf_def)
next
  case RedCASSucceed thus ?case
    by(fastforce elim: hconf_heap_write_mono intro: addr_loc_type.intros simp add: conf_def)
next
  case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s')
  hence "P,hp s ⊢ a∙M(vs) : T"
    by(fastforce simp add: external_WT'_iff dest: sees_method_fun)
  with RedCallExternal show ?case by(auto dest: external_call_hconf)
qed auto

theorem (in J_heap) red_preserves_lconf:
  "⟦ extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩; P,E,hp s ⊢ e:T; P,hp s ⊢ lcl s (:≤) E ⟧ ⟹ P,hp s' ⊢ lcl s' (:≤) E"
  and reds_preserves_lconf:
  "⟦ extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩; P,E,hp s ⊢ es[:]Ts; P,hp s ⊢ lcl s (:≤) E ⟧ ⟹ P,hp s' ⊢ lcl s' (:≤) E"
proof(induct arbitrary: T E and Ts E rule:red_reds.inducts)
  case RedNew thus ?case
    by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply)
next
  case RedNewFail thus ?case
    by(auto intro:lconf_hext hext_heap_ops simp del: fun_upd_apply)
next
  case RedNewArray thus ?case
    by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply)
next
  case RedNewArrayFail thus ?case
    by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply)
next
  case RedLAss thus ?case 
    by(fastforce elim: lconf_upd simp add: conf_def simp del: fun_upd_apply )
next
  case RedAAss thus ?case
    by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply)
next
  case RedFAss thus ?case
    by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply)
next
  case RedCASSucceed thus ?case
    by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply)
next
  case (BlockRed e h x V vo ta e' h' x' T T' E)
  note red = ‹extTA,P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩›
  note IH = ‹⋀T E. ⟦P,E,hp (h, x(V := vo)) ⊢ e : T;
               P,hp (h, x(V := vo)) ⊢ lcl (h, x(V := vo)) (:≤) E⟧
              ⟹ P,hp (h', x') ⊢ lcl (h', x') (:≤) E›
  note wt = ‹P,E,hp (h, x) ⊢ {V:T=vo; e} : T'›
  note lconf = ‹P,hp (h, x) ⊢ lcl (h, x) (:≤) E›
  from lconf_hext[OF lconf[simplified] red_hext_incr[OF red, simplified]]
  have "P,h' ⊢ x (:≤) E" .
  moreover from wt have "P,E(V↦T),h ⊢ e : T'" by(cases vo, auto)
  moreover from lconf wt have "P,h ⊢ x(V := vo) (:≤) E(V ↦ T)"
    by(cases vo)(simp add: lconf_def,auto intro: lconf_upd2 simp add: conf_def)
  ultimately have "P,h' ⊢ x' (:≤) E(V↦T)" 
    by(auto intro: IH[simplified])
  with ‹P,h' ⊢ x (:≤) E› show ?case
    by(auto simp add: lconf_def split: if_split_asm)
next
  case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s')
  from ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩› have "hp s ⊴ h'" by(rule red_external_hext)
  with ‹s' = (h', lcl s)› ‹P,hp s ⊢ lcl s (:≤) E› show ?case by(auto intro: lconf_hext)
qed auto

text‹Combining conformance of heap and local variables:›

definition (in J_heap_conf_base) sconf :: "env ⇒ ('addr, 'heap) Jstate ⇒ bool" ("_ ⊢ _ √"   [51,51]50)
  where "E ⊢ s √  ≡  let (h,l) = s in hconf h ∧ P,h ⊢ l (:≤) E ∧ preallocated h"

context J_conf_read begin

lemma red_preserves_sconf:
  "⟦ extTA,P,t ⊢ ⟨e,s⟩ -tas→ ⟨e',s'⟩; P,E,hp s ⊢ e : T; E ⊢ s √ ⟧ ⟹ E ⊢ s' √"
apply(auto dest: red_preserves_hconf red_preserves_lconf simp add:sconf_def)
apply(fastforce dest: red_hext_incr intro: preallocated_hext)
done

lemma reds_preserves_sconf:
  "⟦ extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩; P,E,hp s ⊢ es [:] Ts; E ⊢ s √ ⟧ ⟹ E ⊢ s' √"
apply(auto dest: reds_preserves_hconf reds_preserves_lconf simp add: sconf_def)
apply(fastforce dest: reds_hext_incr intro: preallocated_hext)
done

end

lemma (in J_heap_base) wt_external_call:
  "⟦ conf_extRet P h va T; P,E,h ⊢ e : T ⟧ ⟹ ∃T'. P,E,h ⊢ extRet2J e va : T' ∧ P ⊢ T' ≤ T"
by(cases va)(auto simp add: conf_def)

subsection "Subject reduction"

theorem (in J_conf_read) assumes wf: "wf_J_prog P"
  shows subject_reduction:
  "⟦ extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩; E ⊢ s √; P,E,hp s ⊢ e:T; P,hp s ⊢ t √t ⟧
  ⟹ ∃T'. P,E,hp s' ⊢ e':T' ∧ P ⊢ T' ≤ T"
  and subjects_reduction:
  "⟦ extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩; E ⊢ s √; P,E,hp s ⊢ es[:]Ts; P,hp s ⊢ t √t ⟧
  ⟹ ∃Ts'. P,E,hp s' ⊢ es'[:]Ts' ∧ P ⊢ Ts' [≤] Ts"
proof (induct arbitrary: T E and Ts E rule:red_reds.inducts)
  case RedNew
  thus ?case by(auto dest: allocate_SomeD)
next
  case RedNewFail thus ?case unfolding sconf_def
    by(fastforce intro:typeof_OutOfMemory preallocated_heap_ops simp add: xcpt_subcls_Throwable[OF _ wf]) 
next
  case NewArrayRed
  thus ?case by fastforce
next
  case RedNewArray
  thus ?case by(auto dest: allocate_SomeD)
next
  case RedNewArrayNegative thus ?case unfolding sconf_def
    by(fastforce intro: preallocated_heap_ops simp add: xcpt_subcls_Throwable[OF _ wf]) 
next
  case RedNewArrayFail thus ?case unfolding sconf_def
    by(fastforce intro:typeof_OutOfMemory preallocated_heap_ops simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (CastRed e s ta e' s' C T E)
  have esse: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" 
    and IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T"
    and hconf: "E ⊢ s √"
    and wtc: "P,E,hp s ⊢ Cast C e : T" by fact+
  thus ?case
  proof(clarsimp)
    fix T'
    assume wte: "P,E,hp s ⊢ e : T'" "is_type P C"
    from wte and hconf and IH and ‹P,hp s ⊢ t √t› have "∃U. P,E,hp s' ⊢ e' : U ∧ P ⊢ U ≤ T'" by simp
    then obtain U where wtee: "P,E,hp s' ⊢ e' : U" and UsTT: "P ⊢ U ≤ T'" by blast
    from wtee ‹is_type P C› have "P,E,hp s' ⊢ Cast C e' : C" by(rule WTrtCast)
    thus "∃T'. P,E,hp s' ⊢ Cast C e' : T' ∧ P ⊢ T' ≤ C" by blast
  qed
next
  case RedCast thus ?case
    by(clarsimp simp add: is_refT_def)
next
  case RedCastFail thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (InstanceOfRed e s ta e' s' U T E)
  have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T"
    and hconf: "E ⊢ s √"
    and wtc: "P,E,hp s ⊢ e instanceof U : T" 
    and tconf: "P,hp s ⊢ t √t" by fact+
  from wtc obtain T' where "P,E,hp s ⊢ e : T'" by auto
  from IH[OF hconf this tconf] obtain T'' where "P,E,hp s' ⊢ e' : T''" by auto
  with wtc show ?case by auto
next
  case RedInstanceOf thus ?case
    by(clarsimp)
next
  case (BinOpRed1 e⇩1 s ta e⇩1' s' bop e⇩2 T E)
  have red: "extTA,P,t ⊢ ⟨e⇩1, s⟩ -ta→ ⟨e⇩1', s'⟩"
   and IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e⇩1:T; P,hp s ⊢ t √t⟧
                 ⟹ ∃U. P,E,hp s' ⊢ e⇩1' : U ∧ P ⊢ U ≤ T"
   and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ e⇩1 «bop» e⇩2 : T" 
   and tconf: "P,hp s ⊢ t √t" by fact+
  from wt obtain T1 T2 where wt1: "P,E,hp s ⊢ e⇩1 : T1"
    and wt2: "P,E,hp s ⊢ e⇩2 : T2" and wtbop: "P ⊢ T1«bop»T2 : T" by auto
  from IH[OF conf wt1 tconf] obtain T1' where wt1': "P,E,hp s' ⊢ e⇩1' : T1'"
    and sub: "P ⊢ T1' ≤ T1" by blast
  from WTrt_binop_widen_mono[OF wtbop sub widen_refl]
  obtain T' where wtbop': "P ⊢ T1'«bop»T2 : T'" and sub': "P ⊢ T' ≤ T" by blast
  from wt1' WTrt_hext_mono[OF wt2 red_hext_incr[OF red]] wtbop'
  have "P,E,hp s' ⊢ e⇩1' «bop» e⇩2 : T'" by(rule WTrtBinOp)
  with sub' show ?case by blast
next
  case (BinOpRed2 e⇩2 s ta e⇩2' s' v⇩1 bop T E)
  have red: "extTA,P,t ⊢ ⟨e⇩2,s⟩ -ta→ ⟨e⇩2',s'⟩" by fact
  have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e⇩2:T; P,hp s ⊢ t √t⟧
                 ⟹ ∃U. P,E,hp s' ⊢ e⇩2' : U ∧ P ⊢ U ≤ T" 
    and tconf: "P,hp s ⊢ t √t" by fact+
  have conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ (Val v⇩1) «bop» e⇩2 : T" by fact+
  from wt obtain T1 T2 where wt1: "P,E,hp s ⊢ Val v⇩1 : T1"
    and wt2: "P,E,hp s ⊢ e⇩2 : T2" and wtbop: "P ⊢ T1«bop»T2 : T" by auto
  from IH[OF conf wt2 tconf] obtain T2' where wt2': "P,E,hp s' ⊢ e⇩2' : T2'"
    and sub: "P ⊢ T2' ≤ T2" by blast
  from WTrt_binop_widen_mono[OF wtbop widen_refl sub]
  obtain T' where wtbop': "P ⊢ T1«bop»T2' : T'" and sub': "P ⊢ T' ≤ T" by blast
  from WTrt_hext_mono[OF wt1 red_hext_incr[OF red]] wt2' wtbop'
  have "P,E,hp s' ⊢ Val v⇩1 «bop» e⇩2' : T'" by(rule WTrtBinOp)
  with sub' show ?case by blast
next
  case (RedBinOp bop v1 v2 v s)
  from ‹E ⊢ s √› have preh: "preallocated (hp s)" by(cases s)(simp add: sconf_def)
  from ‹P,E,hp s ⊢ Val v1 «bop» Val v2 : T› obtain T1 T2
    where "typeof⇘hp s⇙ v1 = ⌊T1⌋" "typeof⇘hp s⇙ v2 = ⌊T2⌋" "P ⊢ T1«bop»T2 : T" by auto
  with wf preh have "P,hp s ⊢ v :≤ T" using ‹binop bop v1 v2 = ⌊Inl v⌋›
    by(rule binop_type)
  thus ?case by(auto simp add: conf_def)
next
  case (RedBinOpFail bop v1 v2 a s)
  from ‹E ⊢ s √› have preh: "preallocated (hp s)" by(cases s)(simp add: sconf_def)
  from ‹P,E,hp s ⊢ Val v1 «bop» Val v2 : T› obtain T1 T2
    where "typeof⇘hp s⇙ v1 = ⌊T1⌋" "typeof⇘hp s⇙ v2 = ⌊T2⌋" "P ⊢ T1«bop»T2 : T" by auto
  with wf preh have "P,hp s ⊢ Addr a :≤ Class Throwable" using ‹binop bop v1 v2 = ⌊Inr a⌋›
    by(rule binop_type)
  thus ?case by(auto simp add: conf_def)
next
  case RedVar thus ?case by (fastforce simp:sconf_def lconf_def conf_def)
next
  case LAssRed thus ?case by(blast intro:widen_trans)
next
  case RedLAss thus ?case by fastforce
next
  case (AAccRed1 a s ta a' s' i T E)
  have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ a : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ a' : T' ∧ P ⊢ T' ≤ T"
    and assa: "extTA,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩"
    and wt: "P,E,hp s ⊢ a⌊i⌉ : T"
    and hconf: "E ⊢ s √" 
    and tconf: "P,hp s ⊢ t √t" by fact+
  from wt have wti: "P,E,hp s ⊢ i : Integer" by auto
  from wti red_hext_incr[OF assa] have wti': "P,E,hp s' ⊢ i : Integer" by - (rule WTrt_hext_mono)
  { assume wta: "P,E,hp s ⊢ a : T⌊⌉"
    from IH[OF hconf wta tconf]
    obtain U where wta': "P,E,hp s' ⊢ a' : U" and UsubT: "P ⊢ U ≤ T⌊⌉" by fastforce
    with wta' wti' have ?case by(cases U, auto simp add: widen_Array) }
  moreover
  { assume wta: "P,E,hp s ⊢ a : NT"
    from IH[OF hconf wta tconf] have "P,E,hp s' ⊢ a' : NT" by fastforce
    from this wti' have ?case
      by(fastforce intro:WTrtAAccNT) }
  ultimately show ?case using wt by auto
next
  case (AAccRed2 i s ta i' s' a T E)
  have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ i : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ i' : T' ∧ P ⊢ T' ≤ T"
    and issi: "extTA,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩"
    and wt: "P,E,hp s ⊢ Val a⌊i⌉ : T"
    and sconf: "E ⊢ s √" 
    and tconf: "P,hp s ⊢ t √t" by fact+
  from wt have wti: "P,E,hp s ⊢ i : Integer" by auto
  from wti IH sconf tconf have wti': "P,E,hp s' ⊢ i' : Integer" by blast
  from wt show ?case
  proof (rule WTrt_elim_cases)
    assume wta: "P,E,hp s ⊢ Val a : T⌊⌉"
    from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : T⌊⌉" by (rule WTrt_hext_mono)
    from wta' wti' show ?case by(fastforce)
  next
    assume wta: "P,E,hp s ⊢ Val a : NT"
    from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : NT" by (rule WTrt_hext_mono)
    from wta' wti' show ?case
      by(fastforce elim:WTrtAAccNT)
  qed
next
  case RedAAccNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case RedAAccBounds thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (RedAAcc h a T n i v l T' E)
  from ‹E ⊢ (h, l) √› have "hconf h" by(clarsimp simp add: sconf_def)
  from ‹0 <=s i› ‹sint i < int n›
  have "nat (sint i) < n"
    by (simp add: word_sle_eq nat_less_iff)
  with ‹typeof_addr h a = ⌊Array_type T n⌋› have "P,h ⊢ a@ACell (nat (sint i)) : T"
    by(auto intro: addr_loc_type.intros)
  from heap_read_conf[OF ‹heap_read h a (ACell (nat (sint i))) v› this] ‹hconf h›
  have "P,h ⊢ v :≤ T" by simp
  thus ?case using RedAAcc by(auto simp add: conf_def)
next
  case (AAssRed1 a s ta a' s' i e T E)
  have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ a : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ a' : T' ∧ P ⊢ T' ≤ T"
    and assa: "extTA,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩"
    and wt: "P,E,hp s ⊢ a⌊i⌉ := e : T"
    and sconf: "E ⊢ s √" 
    and tconf: "P,hp s ⊢ t √t" by fact+
  from wt have void: "T = Void" by blast
  from wt have wti: "P,E,hp s ⊢ i : Integer" by auto
  from wti red_hext_incr[OF assa] have wti': "P,E,hp s' ⊢ i : Integer" by - (rule WTrt_hext_mono)
  { assume wta: "P,E,hp s ⊢ a : NT"
    from IH[OF sconf wta tconf] have wta': "P,E,hp s' ⊢ a' : NT" by fastforce
    from wt wta obtain V where wte: "P,E,hp s ⊢ e : V" by(auto)
    from wte red_hext_incr[OF assa] have wte': "P,E,hp s' ⊢ e : V" by - (rule WTrt_hext_mono)
    from wta' wti' wte' void have ?case
      by(fastforce elim: WTrtAAssNT) }
  moreover
  { fix U
    assume wta: "P,E,hp s ⊢ a : U⌊⌉"
    from IH[OF sconf wta tconf]
    obtain U' where wta': "P,E,hp s' ⊢ a' : U'" and UsubT: "P ⊢ U' ≤ U⌊⌉" by fastforce
    with wta' have ?case
    proof(cases U')
      case NT
      assume UNT: "U' = NT"
      from UNT wt wta obtain V where wte: "P,E,hp s ⊢ e : V" by(auto)
      from wte red_hext_incr[OF assa] have wte': "P,E,hp s' ⊢ e : V" by - (rule WTrt_hext_mono)
      from wta' UNT wti' wte' void show ?thesis
        by(fastforce elim: WTrtAAssNT)
    next
      case (Array A)
      have UA: "U' = A⌊⌉" by fact
      with UA UsubT wt wta obtain V where wte: "P,E,hp s ⊢ e : V" by auto
      from wte red_hext_incr[OF assa] have wte': "P,E,hp s' ⊢ e : V" by - (rule WTrt_hext_mono)
      with wta' wte' UA wti' void show ?thesis by (fast elim:WTrtAAss)
    qed(simp_all add: widen_Array) }
  ultimately show ?case using wt by blast
next
  case (AAssRed2 i s ta i' s' a e T E)
  have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ i : T; P,hp s ⊢ t √t ⟧ ⟹ ∃T'. P,E,hp s' ⊢ i' : T' ∧ P ⊢ T' ≤ T" 
    and issi: "extTA,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩" 
    and wt: "P,E,hp s ⊢ Val a⌊i⌉ := e : T" 
    and sconf: "E ⊢ s √" and tconf: "P,hp s ⊢ t √t" by fact+
  from wt have void: "T = Void" by blast
  from wt have wti: "P,E,hp s ⊢ i : Integer" by auto
  from IH[OF sconf wti tconf] have wti': "P,E,hp s' ⊢ i' : Integer" by fastforce
  from wt show ?case
  proof(rule WTrt_elim_cases)
    fix U T'
    assume wta: "P,E,hp s ⊢ Val a : U⌊⌉"
      and wte: "P,E,hp s ⊢ e : T'"
    from wte red_hext_incr[OF issi] have wte': "P,E,hp s' ⊢ e : T'" by - (rule WTrt_hext_mono)
    from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : U⌊⌉" by - (rule WTrt_hext_mono)
    from wta' wti' wte' void show ?case by (fastforce elim:WTrtAAss)
  next
    fix T'
    assume wta: "P,E,hp s ⊢ Val a : NT"
      and wte: "P,E,hp s ⊢ e : T'"
    from wte red_hext_incr[OF issi] have wte': "P,E,hp s' ⊢ e : T'" by - (rule WTrt_hext_mono)
    from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : NT" by - (rule WTrt_hext_mono)
    from wta' wti' wte' void show ?case by (fastforce elim:WTrtAAss)
  qed
next
  case (AAssRed3 e s ta e' s' a i T E)
  have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" 
    and issi: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" 
    and wt: "P,E,hp s ⊢ Val a⌊Val i⌉ := e : T" 
    and sconf: "E ⊢ s √" and tconf: "P,hp s ⊢ t √t" by fact+
  from wt have void: "T = Void" by blast
  from wt have wti: "P,E,hp s ⊢ Val i : Integer" by auto
  from wti red_hext_incr[OF issi] have wti': "P,E,hp s' ⊢ Val i : Integer" by - (rule WTrt_hext_mono)
  from wt show ?case
  proof(rule WTrt_elim_cases)
    fix U T'
    assume wta: "P,E,hp s ⊢ Val a : U⌊⌉"
      and wte: "P,E,hp s ⊢ e : T'"
    from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : U⌊⌉" by - (rule WTrt_hext_mono)
    from IH[OF sconf wte tconf]
    obtain V where wte': "P,E,hp s' ⊢ e' : V" by fastforce
    from wta' wti' wte' void show ?case by (fastforce elim:WTrtAAss)
  next
    fix T'
    assume wta: "P,E,hp s ⊢ Val a : NT"
      and wte: "P,E,hp s ⊢ e : T'"
    from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : NT" by - (rule WTrt_hext_mono)
    from IH[OF sconf wte tconf]
    obtain V where wte': "P,E,hp s' ⊢ e' : V" by fastforce
    from wta' wti' wte' void show ?case by (fastforce elim:WTrtAAss)
  qed
next
  case RedAAssNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case RedAAssBounds thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case RedAAssStore thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case RedAAss thus ?case
    by(auto simp del:fun_upd_apply)
next
  case (ALengthRed a s ta a' s' T E)
  note IH = ‹⋀T'. ⟦E ⊢ s √; P,E,hp s ⊢ a : T'; P,hp s ⊢ t √t⟧
      ⟹ ∃T''. P,E,hp s' ⊢ a' : T'' ∧ P ⊢ T'' ≤ T'›
  from ‹P,E,hp s ⊢ a∙length : T›
  show ?case
  proof(rule WTrt_elim_cases)
    fix T'
    assume [simp]: "T = Integer"
      and wta: "P,E,hp s ⊢ a : T'⌊⌉"
    from wta ‹E ⊢ s √› IH ‹P,hp s ⊢ t √t›
    obtain T'' where wta': "P,E,hp s' ⊢ a' : T''" 
      and sub: "P ⊢ T'' ≤ T'⌊⌉" by blast
    from sub have "P,E,hp s' ⊢ a'∙length : Integer"
      unfolding widen_Array
    proof(rule disjE)
      assume "T'' = NT"
      with wta' show ?thesis by(auto)
    next
      assume "∃V. T'' = V⌊⌉ ∧ P ⊢ V ≤ T'"
      then obtain V where "T'' = V⌊⌉" "P ⊢ V ≤ T'" by blast
      with wta' show ?thesis by -(rule WTrtALength, simp)
    qed
    thus ?thesis by(simp)
  next
    assume "P,E,hp s ⊢ a : NT"
    with ‹E ⊢ s √› IH ‹P,hp s ⊢ t √t›
    obtain T'' where wta': "P,E,hp s' ⊢ a' : T''" 
      and sub: "P ⊢ T'' ≤ NT" by blast
    from sub have "T'' = NT" by auto
    with wta' show ?thesis by(auto)
  qed
next
  case (RedALength h a T n l T' E)
  from ‹P,E,hp (h, l) ⊢ addr a∙length : T'› ‹typeof_addr h a = ⌊Array_type T n⌋›
  have [simp]: "T' = Integer" by(auto)
  thus ?case by(auto)
next
  case RedALengthNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (FAccRed e s ta e' s' F D T E)
  have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧
                 ⟹ ∃U. P,E,hp s' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ e∙F{D} : T" 
   and tconf: "P,hp s ⊢ t √t" by fact+
  ― ‹Now distinguish the two cases how wt can have arisen.›
  { fix T' C fm
    assume wte: "P,E,hp s ⊢ e : T'"
      and icto: "class_type_of' T' = ⌊C⌋"
      and has: "P ⊢ C has F:T (fm) in D"
    from IH[OF conf wte tconf]
    obtain U where wte': "P,E,hp s' ⊢ e' : U" and UsubC: "P ⊢ U ≤ T'" by auto
    ― ‹Now distinguish what @{term U} can be.›
    with UsubC have ?case
    proof(cases "U = NT")
      case True
      thus ?thesis using wte' by(blast intro:WTrtFAccNT widen_refl) 
    next
      case False
      with icto UsubC obtain C' where icto': "class_type_of' U = ⌊C'⌋"
        and C'subC: "P ⊢ C' ≼⇧* C"
        by(rule widen_is_class_type_of)
      from has_field_mono[OF has C'subC] wte' icto'
      show ?thesis by(auto intro!:WTrtFAcc) 
    qed }
  moreover
  { assume "P,E,hp s ⊢ e : NT"
    hence "P,E,hp s' ⊢ e' : NT" using IH[OF conf _ tconf] by fastforce
    hence ?case  by(fastforce intro:WTrtFAccNT widen_refl) }
  ultimately show ?case using wt by blast
next
  case RedFAcc thus ?case unfolding sconf_def
    by(fastforce dest: heap_read_conf intro: addr_loc_type.intros simp add: conf_def)
next
  case RedFAccNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (FAssRed1 e s ta e' s' F D e⇩2)
  have red: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩"
   and IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧
                 ⟹ ∃U. P,E,hp s' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ e∙F{D}:=e⇩2 : T"
   and tconf: "P,hp s ⊢ t √t" by fact+
  from wt have void: "T = Void" by blast
  ― ‹We distinguish if @{term e} has type @{term NT} or a Class type›
  { assume "P,E,hp s ⊢ e : NT"
    hence "P,E,hp s' ⊢ e' : NT" using IH[OF conf _ tconf] by fastforce
    moreover obtain T⇩2 where "P,E,hp s ⊢ e⇩2 : T⇩2" using wt by auto
    from this red_hext_incr[OF red] have  "P,E,hp s' ⊢ e⇩2 : T⇩2"
      by(rule WTrt_hext_mono)
    ultimately have ?case using void by(blast intro!:WTrtFAssNT)
  }
  moreover
  { fix T' C TF T⇩2 fm
    assume wt⇩1: "P,E,hp s ⊢ e : T'" and icto: "class_type_of' T' = ⌊C⌋" and wt⇩2: "P,E,hp s ⊢ e⇩2 : T⇩2"
      and has: "P ⊢ C has F:TF (fm) in D" and sub: "P ⊢ T⇩2 ≤ TF"
    obtain U where wt⇩1': "P,E,hp s' ⊢ e' : U" and UsubC: "P ⊢ U ≤ T'"
      using IH[OF conf wt⇩1 tconf] by blast
    have wt⇩2': "P,E,hp s' ⊢ e⇩2 : T⇩2"
      by(rule WTrt_hext_mono[OF wt⇩2 red_hext_incr[OF red]])
    ― ‹Is @{term U} the null type or a class type?›
    have ?case
    proof(cases "U = NT")
      case True
      with wt⇩1' wt⇩2' void show ?thesis by(blast intro!:WTrtFAssNT)
    next
      case False
      with icto UsubC obtain C' where icto': "class_type_of' U = ⌊C'⌋"
        and "subclass": "P ⊢ C' ≼⇧* C" by(rule widen_is_class_type_of)
      have "P ⊢ C' has F:TF (fm) in D" by(rule has_field_mono[OF has "subclass"])
      with wt⇩1' show ?thesis using wt⇩2' sub void icto' by(blast intro:WTrtFAss)
    qed }
  ultimately show ?case using wt by blast
next
  case (FAssRed2 e⇩2 s ta e⇩2' s' v F D T E)
  have red: "extTA,P,t ⊢ ⟨e⇩2,s⟩ -ta→ ⟨e⇩2',s'⟩"
   and IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e⇩2 : T; P,hp s ⊢ t √t⟧
                 ⟹ ∃U. P,E,hp s' ⊢ e⇩2' : U ∧ P ⊢ U ≤ T"
   and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ Val v∙F{D}:=e⇩2 : T" 
   and tconf: "P,hp s ⊢ t √t" by fact+
  from wt have [simp]: "T = Void" by auto
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix U C TF T⇩2 fm
    assume wt⇩1: "P,E,hp s ⊢ Val v : U"
      and icto: "class_type_of' U = ⌊C⌋"
      and has: "P ⊢ C has F:TF (fm) in D"
      and wt⇩2: "P,E,hp s ⊢ e⇩2 : T⇩2" and TsubTF: "P ⊢ T⇩2 ≤ TF"
    have wt⇩1': "P,E,hp s' ⊢ Val v : U"
      by(rule WTrt_hext_mono[OF wt⇩1 red_hext_incr[OF red]])
    obtain T⇩2' where wt⇩2': "P,E,hp s' ⊢ e⇩2' : T⇩2'" and T'subT: "P ⊢ T⇩2' ≤ T⇩2"
      using IH[OF conf wt⇩2 tconf] by blast
    have "P,E,hp s' ⊢ Val v∙F{D}:=e⇩2' : Void"
      by(rule WTrtFAss[OF wt⇩1' icto has wt⇩2' widen_trans[OF T'subT TsubTF]])
    thus ?case by auto
  next
    fix T⇩2 assume null: "P,E,hp s ⊢ Val v : NT" and wt⇩2: "P,E,hp s ⊢ e⇩2 : T⇩2"
    from null have "v = Null" by simp
    moreover
    obtain T⇩2' where "P,E,hp s' ⊢ e⇩2' : T⇩2' ∧ P ⊢ T⇩2' ≤ T⇩2"
      using IH[OF conf wt⇩2 tconf] by blast
    ultimately show ?thesis by(fastforce intro:WTrtFAssNT)
  qed
next
  case RedFAss thus ?case by(auto simp del:fun_upd_apply)
next
  case RedFAssNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (CASRed1 e s ta e' s' D F e2 e3)
  from CASRed1.prems(2) consider (NT) T2 T3 where 
      "P,E,hp s ⊢ e : NT" "T = Boolean" "P,E,hp s ⊢ e2 : T2" "P,E,hp s ⊢ e3 : T3"
    | (RefT) U T' C fm T2 T3 where
      "P,E,hp s ⊢ e : U" "T = Boolean" "class_type_of' U = ⌊C⌋" "P ⊢ C has F:T' (fm) in D"
      "P,E,hp s ⊢ e2 : T2" "P ⊢ T2 ≤ T'" "P,E,hp s ⊢ e3 : T3" "P ⊢ T3 ≤ T'" "volatile fm" by fastforce
  thus ?case
  proof cases
    case NT
    have "P,E,hp s' ⊢ e' : NT" using CASRed1.hyps(2)[OF CASRed1.prems(1) NT(1) CASRed1.prems(3)] by auto
    moreover from NT CASRed1.hyps(1)[THEN red_hext_incr]
    have "P,E,hp s' ⊢ e2 : T2" "P,E,hp s' ⊢ e3 : T3" by(auto intro: WTrt_hext_mono)
    ultimately show ?thesis using NT by(auto intro: WTrtCASNT)
  next
    case RefT
    from CASRed1.hyps(2)[OF CASRed1.prems(1) RefT(1) CASRed1.prems(3)]
    obtain U' where wt1: "P,E,hp s' ⊢ e' : U'" "P ⊢ U' ≤ U" by blast
    from RefT CASRed1.hyps(1)[THEN red_hext_incr]
    have wt2: "P,E,hp s' ⊢ e2 : T2" and wt3: "P,E,hp s' ⊢ e3 : T3" by(auto intro: WTrt_hext_mono)
    show ?thesis
    proof(cases "U' = NT")
      case True
      with RefT wt1 wt2 wt3 show ?thesis by(auto intro: WTrtCASNT)
    next
      case False
      with RefT(3) wt1 obtain C' where icto': "class_type_of' U' = ⌊C'⌋"
        and "subclass": "P ⊢ C' ≼⇧* C" by(blast intro: widen_is_class_type_of)
      have "P ⊢ C' has F:T' (fm) in D" by(rule has_field_mono[OF RefT(4) "subclass"])
      with RefT wt1 wt2 wt3 icto' show ?thesis by(auto intro!: WTrtCAS)
    qed
  qed
next
  case (CASRed2 e s ta e' s' v D F e3)
  consider (Null) "v = Null" | (Val) U C T' fm T2 T3 where
    "class_type_of' U = ⌊C⌋" "P ⊢ C has F:T' (fm) in D" "volatile fm"
    "P,E,hp s ⊢ e : T2" "P ⊢ T2 ≤ T'" "P,E,hp s ⊢ e3 : T3" "P ⊢ T3 ≤ T'" "T = Boolean"
    "typeof⇘hp s⇙ v = ⌊U⌋" using CASRed2.prems(2) by auto
  then show ?case 
  proof cases
    case Null
    then show ?thesis using CASRed2 
      by(force dest: red_hext_incr intro: WTrt_hext_mono WTrtCASNT)
  next
    case Val
    from CASRed2.hyps(1) have hext: "hp s ⊴ hp s'" by(auto dest: red_hext_incr)
    with Val(9) have "typeof⇘hp s'⇙ v = ⌊U⌋" by(rule type_of_hext_type_of)
    moreover from CASRed2.hyps(2)[OF CASRed2.prems(1) Val(4) CASRed2.prems(3)] Val(5)
    obtain T2' where "P,E,hp s' ⊢ e' : T2'" "P ⊢ T2' ≤ T'" by(auto intro: widen_trans)
    moreover from Val(6) hext have "P,E,hp s' ⊢ e3 : T3" by(rule WTrt_hext_mono)
    ultimately show ?thesis using Val by(auto intro: WTrtCAS)
  qed
next
  case (CASRed3 e s ta e' s' v D F v')
  consider (Null) "v = Null" | (Val) U C T' fm T2 T3 where 
    "T = Boolean" "class_type_of' U = ⌊C⌋" "P ⊢ C has F:T' (fm) in D" "volatile fm"
    "P ⊢ T2 ≤ T'" "P,E,hp s ⊢ e : T3" "P ⊢ T3 ≤ T'"
    "typeof⇘hp s⇙ v = ⌊U⌋" "typeof⇘hp s⇙ v' = ⌊T2⌋"
    using CASRed3.prems(2) by auto
  then show ?case
  proof cases
    case Null
    then show ?thesis using CASRed3
      by(force dest: red_hext_incr intro: type_of_hext_type_of WTrtCASNT)
  next
    case Val
    from CASRed3.hyps(1) have hext: "hp s ⊴ hp s'" by(auto dest: red_hext_incr)
    with Val(8,9) have "typeof⇘hp s'⇙ v = ⌊U⌋" "typeof⇘hp s'⇙ v' = ⌊T2⌋"
      by(blast intro: type_of_hext_type_of)+
    moreover from CASRed3.hyps(2)[OF CASRed3.prems(1) Val(6) CASRed3.prems(3)] Val(7)
    obtain T3' where "P,E,hp s' ⊢ e' : T3'" "P ⊢ T3' ≤ T'" by(auto intro: widen_trans)
    ultimately show ?thesis using Val by(auto intro: WTrtCAS)
  qed
next
  case CASNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (CallObj e s ta e' s' M es T E)
  have red: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩"
   and IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧
                 ⟹ ∃U. P,E,hp s' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ e∙M(es) : T"
   and tconf: "P,hp s ⊢ t √t" by fact+
  ― ‹We distinguish if @{term e} has type @{term NT} or a Class type›
  from wt show ?case
  proof(rule WTrt_elim_cases)
    fix T' C Ts meth D Us
    assume wte: "P,E,hp s ⊢ e : T'" and icto: "class_type_of' T' = ⌊C⌋"
      and "method": "P ⊢ C sees M:Ts→T = meth in D"
      and wtes: "P,E,hp s ⊢ es [:] Us" and subs: "P ⊢ Us [≤] Ts"
    obtain U where wte': "P,E,hp s' ⊢ e' : U" and UsubC: "P ⊢ U ≤ T'"
      using IH[OF conf wte tconf] by blast
    show ?thesis
    proof(cases "U = NT")
      case True
      moreover have "P,E,hp s' ⊢ es [:] Us"
        by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
      ultimately show ?thesis using wte' by(blast intro!:WTrtCallNT)
    next
      case False
      with icto UsubC obtain C'
        where icto': "class_type_of' U = ⌊C'⌋" and "subclass": "P ⊢ C' ≼⇧* C"
        by(rule widen_is_class_type_of)

      obtain Ts' T' meth' D'
        where method': "P ⊢ C' sees M:Ts'→T' = meth' in D'"
        and subs': "P ⊢ Ts [≤] Ts'" and sub': "P ⊢ T' ≤ T"
        using Call_lemma[OF "method" "subclass" wf] by fast
      have wtes': "P,E,hp s' ⊢ es [:] Us"
        by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
      show ?thesis using wtes' wte' icto' subs method' subs' sub' by(blast intro:widens_trans)
    qed
  next
    fix Ts
    assume "P,E,hp s ⊢ e:NT"
    hence "P,E,hp s' ⊢ e' : NT" using IH[OF conf _ tconf] by fastforce
    moreover
    fix Ts assume wtes: "P,E,hp s ⊢ es [:] Ts"
    have "P,E,hp s' ⊢ es [:] Ts"
      by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
    ultimately show ?thesis by(blast intro!:WTrtCallNT)
  qed
next
  case (CallParams es s ta es' s' v M T E)
  have reds: "extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩"
   and IH: "⋀Ts E. ⟦E ⊢ s √; P,E,hp s ⊢ es [:] Ts; P,hp s ⊢ t √t⟧
           ⟹ ∃Ts'. P,E,hp s' ⊢ es' [:] Ts' ∧ P ⊢ Ts' [≤] Ts"
   and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ Val v∙M(es) : T" 
   and tconf: "P,hp s ⊢ t √t" by fact+
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix U C Ts meth D Us
    assume wte: "P,E,hp s ⊢ Val v : U" and icto: "class_type_of' U = ⌊C⌋"
      and "P ⊢ C sees M:Ts→T = meth in D"
      and wtes: "P,E,hp s ⊢ es [:] Us" and "P ⊢ Us [≤] Ts"
    moreover have "P,E,hp s' ⊢ Val v : U"
      by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]])
    moreover obtain Us' where "P,E,hp s' ⊢ es' [:] Us'" "P ⊢ Us' [≤] Us"
      using IH[OF conf wtes tconf] by blast
    ultimately show ?thesis by(fastforce intro:WTrtCall widens_trans)
  next
    fix Us
    assume null: "P,E,hp s ⊢ Val v : NT" and wtes: "P,E,hp s ⊢ es [:] Us"
    from null have "v = Null" by simp
    moreover
    obtain Us' where "P,E,hp s' ⊢ es' [:] Us' ∧ P ⊢ Us' [≤] Us"
      using IH[OF conf wtes tconf] by blast
    ultimately show ?thesis by(fastforce intro:WTrtCallNT)
  qed
next
  case (RedCall s a U M Ts T pns body D vs T' E)
  have hp: "typeof_addr (hp s) a = ⌊U⌋"
    and "method": "P ⊢ class_type_of U sees M: Ts→T = ⌊(pns,body)⌋ in D"
    and wt: "P,E,hp s ⊢ addr a∙M(map Val vs) : T'" by fact+
  obtain Ts' where wtes: "P,E,hp s ⊢ map Val vs [:] Ts'"
    and subs: "P ⊢ Ts' [≤] Ts" and T'isT: "T' = T"
    using wt "method" hp wf by(auto 4 3 dest: sees_method_fun)
  from wtes subs have length_vs: "length vs = length Ts"
    by(auto simp add: WTrts_conv_list_all2 dest!: list_all2_lengthD)
  have UsubD: "P ⊢ ty_of_htype U ≤ Class (class_type_of U)"
    by(cases U)(simp_all add: widen_array_object)
  from sees_wf_mdecl[OF wf "method"] obtain T''
    where wtabody: "P,[this#pns [↦] Class D#Ts] ⊢ body :: T''"
    and T''subT: "P ⊢ T'' ≤ T" and length_pns: "length pns = length Ts"
    by(fastforce simp:wf_mdecl_def simp del:map_upds_twist)
  from wtabody have "P,Map.empty(this#pns [↦] Class D#Ts),hp s ⊢ body : T''"
    by(rule WT_implies_WTrt)
  hence "P,E(this#pns [↦] Class D#Ts),hp s ⊢ body : T''"
    by(rule WTrt_env_mono) simp
  hence "P,E,hp s ⊢ blocks (this#pns) (Class D#Ts) (Addr a#vs) body : T''"
    using wtes subs hp sees_method_decl_above[OF "method"] length_vs length_pns UsubD
    by(auto simp add:wt_blocks rel_list_all2_Cons2 intro: widen_trans)
  with T''subT T'isT show ?case by blast
next
  case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s')
  from ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩› have "hp s ⊴ h'" by(rule red_external_hext)
  with ‹P,E,hp s ⊢ addr a∙M(map Val vs) : T›
  have "P,E,h' ⊢ addr a∙M(map Val vs) : T" by(rule WTrt_hext_mono)
  moreover from ‹typeof_addr (hp s) a = ⌊U⌋› ‹P ⊢ class_type_of U sees M: Ts→T' = Native in D› ‹P,E,hp s ⊢ addr a∙M(map Val vs) : T›
  have "P,hp s ⊢ a∙M(vs) : T'"
    by(fastforce simp add: external_WT'_iff dest: sees_method_fun)
  ultimately show ?case using RedCallExternal
    by(auto 4 3 intro: red_external_conf_extRet[OF wf] intro!: wt_external_call simp add: sconf_def dest: sees_method_fun[where C="class_type_of U"])
next
  case RedCallNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (BlockRed e h x V vo ta e' h' x' T T' E)
  note IH = ‹⋀T E. ⟦E ⊢ (h, x(V := vo)) √; P,E,hp (h, x(V := vo)) ⊢ e : T; P,hp (h, x(V := vo)) ⊢ t √t⟧
             ⟹ ∃T'. P,E,hp (h', x') ⊢ e' : T' ∧ P ⊢ T' ≤ T›[simplified]
  from ‹P,E,hp (h, x) ⊢ {V:T=vo; e} : T'› have "P,E(V↦T),h ⊢ e : T'" by(cases vo, auto)
  moreover from ‹E ⊢ (h, x) √› ‹P,E,hp (h, x) ⊢ {V:T=vo; e} : T'›
  have "(E(V ↦ T)) ⊢ (h, x(V := vo)) √"
    by(cases vo)(simp add: lconf_def sconf_def,auto simp add: sconf_def conf_def intro: lconf_upd2)
  ultimately obtain T'' where wt': "P,E(V↦T),h' ⊢ e' : T''" "P ⊢ T'' ≤ T'" using ‹P,hp (h, x) ⊢ t √t›
    by(auto dest: IH)
  { fix v
    assume vo: "x' V = ⌊v⌋"
    from ‹(E(V ↦ T)) ⊢ (h, x(V := vo)) √› ‹extTA,P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩› ‹P,E(V↦T),h ⊢ e : T'›
    have "P,h' ⊢ x' (:≤) (E(V ↦ T))" by(auto simp add: sconf_def dest: red_preserves_lconf)
    with vo have "∃T'. typeof⇘h'⇙ v = ⌊T'⌋ ∧ P ⊢ T' ≤ T" by(fastforce simp add: sconf_def lconf_def conf_def)
    then obtain T' where "typeof⇘h'⇙ v = ⌊T'⌋" "P ⊢ T' ≤ T" by blast
    hence ?case using wt' vo by(auto) }
  moreover
  { assume "x' V = None" with wt' have ?case by(auto) }
  ultimately show ?case by blast
next 
  case RedBlock thus ?case by auto
next
  case (SynchronizedRed1 o' s ta o'' s' e T E)
  have red: "extTA,P,t ⊢ ⟨o',s⟩ -ta→ ⟨o'',s'⟩" by fact
  have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ o' : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ o'' : T' ∧ P ⊢ T' ≤ T" by fact
  have conf: "E ⊢ s √" by fact
  have wt: "P,E,hp s ⊢ sync(o') e : T" by fact+
  thus ?case
  proof(rule WTrt_elim_cases)
    fix To
    assume wto: "P,E,hp s ⊢ o' : To"
      and refT: "is_refT To" 
      and wte: "P,E,hp s ⊢ e : T"
    from IH[OF conf wto ‹P,hp s ⊢ t √t›] obtain To' where "P,E,hp s' ⊢ o'' : To'" and sub: "P ⊢ To' ≤ To" by auto
    moreover have "P,E,hp s' ⊢ e : T"
      by(rule WTrt_hext_mono[OF wte red_hext_incr[OF red]])
    moreover have "is_refT To'" using refT sub by(auto intro: widen_refT)
    ultimately show ?thesis by(auto)
  qed
next
  case SynchronizedNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case LockSynchronized thus ?case by(auto)
next
  case (SynchronizedRed2 e s ta e' s' a T E)
  have red: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" by fact
  have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" by fact
  have conf: "E ⊢ s √" by fact
  have wt: "P,E,hp s ⊢ insync(a) e : T" by fact
  thus ?case
  proof(rule WTrt_elim_cases)
    fix Ta
    assume "P,E,hp s ⊢ e : T"
      and hpa: "typeof_addr (hp s) a = ⌊Ta⌋"
    from ‹P,E,hp s ⊢ e : T› conf ‹P,hp s ⊢ t √t› obtain T'
      where "P,E,hp s' ⊢ e' : T'" "P ⊢ T' ≤ T" by(blast dest: IH)
    moreover from red have hext: "hp s ⊴ hp s'" by(auto dest: red_hext_incr)
    with hpa have "P,E,hp s' ⊢ addr a : ty_of_htype Ta"
      by(auto intro: typeof_addr_hext_mono)
    ultimately show ?thesis by auto
  qed
next
  case UnlockSynchronized thus ?case by(auto)
next
  case SeqRed thus ?case
    apply(auto)
    apply(drule WTrt_hext_mono[OF _ red_hext_incr], assumption)
    by auto
next
  case (CondRed b s ta b' s' e1 e2 T E)
  have red: "extTA,P,t ⊢ ⟨b,s⟩ -ta→ ⟨b',s'⟩" by fact
  have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ b : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ b' : T' ∧ P ⊢ T' ≤ T" by fact
  have conf: "E ⊢ s √" by fact
  have wt: "P,E,hp s ⊢ if (b) e1 else e2 : T" by fact
  thus ?case
  proof(rule WTrt_elim_cases)
    fix T1 T2
    assume wtb: "P,E,hp s ⊢ b : Boolean"
      and wte1: "P,E,hp s ⊢ e1 : T1"
      and wte2: "P,E,hp s ⊢ e2 : T2"
      and lub: "P ⊢ lub(T1, T2) = T"
    from IH[OF conf wtb ‹P,hp s ⊢ t √t›] have "P,E,hp s' ⊢ b' : Boolean" by(auto)
    moreover have "P,E,hp s' ⊢ e1 : T1"
      by(rule WTrt_hext_mono[OF wte1 red_hext_incr[OF red]])
    moreover have "P,E,hp s' ⊢ e2 : T2"
      by(rule WTrt_hext_mono[OF wte2 red_hext_incr[OF red]])
    ultimately show ?thesis using lub by auto
  qed
next
  case (ThrowRed e s ta e' s' T E)
  have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" by fact
  have conf: "E ⊢ s √" by fact
  have wt: "P,E,hp s ⊢ throw e : T" by fact
  then obtain T'
    where wte: "P,E,hp s ⊢ e : T'" 
    and nobject: "P ⊢ T' ≤ Class Throwable" by auto
  from IH[OF conf wte ‹P,hp s ⊢ t √t›] obtain T'' 
    where wte': "P,E,hp s' ⊢ e' : T''"
    and PT'T'': "P ⊢ T'' ≤ T'" by blast
  from nobject PT'T'' have "P ⊢ T'' ≤ Class Throwable"
    by(auto simp add: widen_Class)(erule notE, rule rtranclp_trans)
  hence "P,E,hp s' ⊢ throw e' : T" using wte' PT'T''
    by -(erule WTrtThrow)
  thus ?case by(auto)
next
  case RedThrowNull thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case (TryRed e s ta e' s' C V e2 T E)
  have red: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" by fact
  have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" by fact
  have conf: "E ⊢ s √" by fact
  have wt: "P,E,hp s ⊢ try e catch(C V) e2 : T" by fact
  thus ?case
  proof(rule WTrt_elim_cases)
    fix T1
    assume wte: "P,E,hp s ⊢ e : T1"
      and wte2: "P,E(V ↦ Class C),hp s ⊢ e2 : T"
      and sub: "P ⊢ T1 ≤ T"
    from IH[OF conf wte ‹P,hp s ⊢ t √t›] obtain T1' where "P,E,hp s' ⊢ e' : T1'" and "P ⊢ T1' ≤ T1" by(auto)
    moreover have "P,E(V ↦ Class C),hp s' ⊢ e2 : T"
      by(rule WTrt_hext_mono[OF wte2 red_hext_incr[OF red]])
    ultimately show ?thesis using sub by(auto elim: widen_trans)
  qed
next
  case RedTryFail thus ?case unfolding sconf_def
    by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf])
next
  case RedSeq thus ?case by auto
next
  case RedCondT thus ?case by(auto dest: is_lub_upper)
next
  case RedCondF thus ?case by(auto dest: is_lub_upper)
next
  case RedWhile thus ?case by(fastforce) 
next
  case RedTry thus ?case by auto
next
  case RedTryCatch thus ?case by(fastforce)
next
  case (ListRed1 e s ta e' s' es Ts E)
  note IH = ‹⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T›
  from ‹P,E,hp s ⊢ e # es [:] Ts› obtain T Ts' where "Ts = T # Ts'" "P,E,hp s ⊢ e : T" "P,E,hp s ⊢ es [:] Ts'" by auto
  with IH[of E T] ‹E ⊢ s √› WTrts_hext_mono[OF ‹P,E,hp s ⊢ es [:] Ts'› red_hext_incr[OF ‹extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›]]
  show ?case using ‹P,hp s ⊢ t √t› by(auto simp add: list_all2_Cons2 intro: widens_refl)
next
  case ListRed2 thus ?case
    by(fastforce dest: hext_typeof_mono[OF reds_hext_incr])
qed(fastforce)+

end