Theory TypeSafe

(*  Title:      JinjaDCI/J/TypeSafe.thy

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

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

section ‹ Type Safety Proof ›

theory TypeSafe
imports Progress BigStep SmallStep JWellForm
begin

(* here because it requires well-typing def *)
lemma red_shext_incr: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩
  ⟹ (⋀E T. P,E,h,sh ⊢ e : T ⟹ sh ⊴⇩s sh')"
  and reds_shext_incr: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩
  ⟹ (⋀E Ts. P,E,h,sh ⊢ es [:] Ts ⟹ sh ⊴⇩s sh')"
(*<*)
proof(induct rule:red_reds_inducts) qed(auto simp: shext_def)
(*>*)

lemma wf_types_clinit:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a" and proc: "sh C = ⌊(sfs, Processing)⌋"
shows "P,E,h,sh ⊢ C∙⇩sclinit([]) : Void"
proof -
  from ex obtain D fs ms where "a = (D,fs,ms)" by(cases a)
  then have sP: "(C, D, fs, ms) ∈ set P" using ex map_of_SomeD[of P C a] by(simp add: class_def)
  then have "wf_clinit ms" using assms by(unfold wf_prog_def wf_cdecl_def, auto)
  then obtain pns body where sm: "(clinit, Static, [], Void, pns, body) ∈ set ms"
    by(unfold wf_clinit_def) auto
  then have "P ⊢ C sees clinit,Static:[] → Void = (pns,body) in C"
    using mdecl_visible[OF wf sP sm] by simp
  then show ?thesis using WTrtSCall proc by simp
qed

subsection‹Basic preservation lemmas›

text‹ First some easy preservation lemmas. ›

theorem red_preserves_hconf:
  "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ (⋀T E. ⟦ P,E,h,sh ⊢ e : T; P ⊢ h √ ⟧ ⟹ P ⊢ h' √)"
and reds_preserves_hconf:
  "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ (⋀Ts E. ⟦ P,E,h,sh ⊢ es [:] Ts; P ⊢ h √ ⟧ ⟹ P ⊢ h' √)"
(*<*)
proof (induct rule:red_reds_inducts)
  case (RedNew h a C FDTs h' l sh es)
  have new: "new_Addr h = Some a" and fields: "P ⊢ C has_fields FDTs"
   and h': "h' = h(a↦blank P C)"
   and hconf: "P ⊢ h √" by fact+
  from new have None: "h a = None" by(rule new_Addr_SomeD)
  moreover have "P,h ⊢ blank P C √"
    using fields by(rule oconf_blank)
  ultimately show "P ⊢ h' √" using h' by(fast intro: hconf_new[OF hconf])
next
  case (RedFAss C F t D h a fs v l sh b')
  let ?fs' = "fs((F,D)↦v)"
  have hconf: "P ⊢ h √" and ha: "h a = Some(C,fs)"
   and wt: "P,E,h,sh ⊢ addr a∙F{D}:=Val v : T" by fact+
  from wt ha obtain TF Tv where typeofv: "typeof⇘h⇙ v = Some Tv"
    and has: "P ⊢ C has F,NonStatic:TF in D"
    and sub: "P ⊢ Tv ≤ TF" by auto
  have "P,h ⊢ (C, ?fs') √"
  proof (rule oconf_fupd[OF has])
    show "P,h ⊢ (C, fs) √" using hconf ha by(simp add:hconf_def)
    show "P,h ⊢ v :≤ TF" using sub typeofv by(simp add:conf_def)
  qed
  with hconf ha show "P ⊢ h(a↦(C, ?fs')) √"  by (rule hconf_upd_obj)
qed(auto elim: WTrt.cases)
(*>*)


theorem red_preserves_lconf:
  "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹
  (⋀T E. ⟦ P,E,h,sh ⊢ e:T; P,h ⊢ l (:≤) E ⟧ ⟹ P,h' ⊢ l' (:≤) E)"
and reds_preserves_lconf:
  "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹
  (⋀Ts E. ⟦ P,E,h,sh ⊢ es[:]Ts; P,h ⊢ l (:≤) E ⟧ ⟹ P,h' ⊢ l' (:≤) E)"
(*<*)
proof(induct rule:red_reds_inducts)
  case RedNew thus ?case
    by(fast intro:lconf_hext red_hext_incr[OF red_reds.RedNew])
next
  case RedLAss thus ?case by(fastforce elim: lconf_upd simp:conf_def)
next
  case RedFAss thus ?case
    by(fast intro:lconf_hext red_hext_incr[OF red_reds.RedFAss])
next
  case (InitBlockRed e h l V v sh b e' h' l' sh' b' v' T T')
  have red: "P ⊢ ⟨e, (h, l(V↦v),sh),b⟩ → ⟨e',(h', l',sh'),b'⟩"
   and IH: "⋀T E . ⟦ P,E,h,sh ⊢ e:T; P,h ⊢ l(V↦v) (:≤) E ⟧
                     ⟹ P,h' ⊢ l' (:≤) E"
   and l'V: "l' V = Some v'" and lconf: "P,h ⊢ l (:≤) E"
   and wt: "P,E,h,sh ⊢ {V:T := Val v; e} : T'" by fact+
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have "P,h' ⊢ l (:≤) E" .
  moreover from IH lconf wt have "P,h' ⊢ l' (:≤) E(V↦T)"
    by(auto simp del: fun_upd_apply simp: fun_upd_same lconf_upd2 conf_def)
  ultimately show "P,h' ⊢ l'(V := l V) (:≤) E"
    by (fastforce simp:lconf_def split:if_split_asm)
next
  case (BlockRedNone e h l V sh b e' h' l' sh' b' T T')
  have red: "P ⊢ ⟨e,(h, l(V := None),sh),b⟩ → ⟨e',(h', l',sh'),b'⟩"
   and IH: "⋀E T. ⟦ P,E,h,sh ⊢ e : T; P,h ⊢ l(V:=None) (:≤) E ⟧
                   ⟹ P,h' ⊢ l' (:≤) E"
   and lconf: "P,h ⊢ l (:≤) E" and wt: "P,E,h,sh ⊢ {V:T; e} : T'" by fact+
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have "P,h' ⊢ l (:≤) E" .
  moreover have "P,h' ⊢ l' (:≤) E(V↦T)"
    by(rule IH, insert lconf wt, auto simp:lconf_def)
  ultimately show "P,h' ⊢ l'(V := l V) (:≤) E"
    by (fastforce simp:lconf_def split:if_split_asm)
next
  case (BlockRedSome e h l V sh b e' h' l' sh' b' v T T')
  have red: "P ⊢ ⟨e,(h, l(V := None),sh),b⟩ → ⟨e',(h', l',sh'),b'⟩"
   and IH: "⋀E T. ⟦P,E,h,sh ⊢ e : T; P,h ⊢ l(V:=None) (:≤) E⟧
                   ⟹ P,h' ⊢ l' (:≤) E"
   and lconf: "P,h ⊢ l (:≤) E" and wt: "P,E,h,sh ⊢ {V:T; e} : T'" by fact+
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have "P,h' ⊢ l (:≤) E" .
  moreover have "P,h' ⊢ l' (:≤) E(V↦T)"
    by(rule IH, insert lconf wt, auto simp:lconf_def)
  ultimately show "P,h' ⊢ l'(V := l V) (:≤) E"
    by (fastforce simp:lconf_def split:if_split_asm)
qed(auto elim: WTrt.cases)
(*>*)


theorem red_preserves_shconf:
  "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ (⋀T E. ⟦ P,E,h,sh ⊢ e : T; P,h ⊢⇩s sh √ ⟧ ⟹ P,h' ⊢⇩s sh' √)"
and reds_preserves_shconf:
  "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ (⋀Ts E. ⟦ P,E,h,sh ⊢ es [:] Ts; P,h ⊢⇩s sh √ ⟧ ⟹ P,h' ⊢⇩s sh' √)"
(*<*)
proof (induct rule:red_reds_inducts)
  case (RedNew h a C FDTs h' l sh es)
  have new: "new_Addr h = Some a"
   and h': "h' = h(a↦blank P C)"
   and shconf: "P,h ⊢⇩s sh √" by fact+
  from new have None: "h a = None" by(rule new_Addr_SomeD)
  then show "P,h' ⊢⇩s sh √" using h' by(fast intro: shconf_hnew[OF shconf])
next
  case (RedFAss C F t D h a fs v l sh b)
  let ?fs' = "fs((F,D)↦v)"
  have shconf: "P,h ⊢⇩s sh √" and ha: "h a = Some(C,fs)" by fact+
  then show "P,h(a↦(C, ?fs')) ⊢⇩s sh √" by (rule shconf_hupd_obj)
next
  case (RedSFAss C F t D sh sfs i sfs' v sh' h l)
  let ?sfs' = "sfs(F↦v)"
  have shconf: "P,h ⊢⇩s sh √" and shD: "sh D = ⌊(sfs, i)⌋"
    and wt: "P,E,h,sh ⊢ C∙⇩sF{D} := Val v : T" by fact+
  from wt obtain TF Tv where typeofv: "typeof⇘h⇙ v = Some Tv"
    and has: "P ⊢ C has F,Static:TF in D"
    and sub: "P ⊢ Tv ≤ TF" by (auto elim: WTrt.cases)
  have has': "P ⊢ D has F,Static:TF in D" using has by(rule has_field_idemp)
  have "P,h,D ⊢⇩s ?sfs' √"
  proof (rule soconf_fupd[OF has'])
    show "P,h,D ⊢⇩s sfs √" using shconf shD by(simp add:shconf_def)
    show "P,h ⊢ v :≤ TF" using sub typeofv by(simp add:conf_def)
  qed
  with shconf have "P,h ⊢⇩s sh(D↦(?sfs',i)) √" by (rule shconf_upd_obj)
  then show ?case using RedSFAss.hyps(3) RedSFAss.hyps(4) by blast
next
  case (InitNoneRed sh C C' Cs e h l)
  let ?sfs' = "sblank P C"
  have "P,h ⊢⇩s sh(C ↦ (?sfs', Prepared)) √"
  proof(rule shconf_upd_obj)
    show "P,h ⊢⇩s sh √" using InitNoneRed by simp
    show "P,h,C ⊢⇩s sblank P C √" by (metis has_field_def soconf_def soconf_sblank)
  qed
  then show ?case by blast
next
  case (InitObjectRed sh C sfs sh' C' Cs e h l)
  have sh': "sh' = sh(C ↦ (sfs, Processing))" by fact
  have "P,h ⊢⇩s sh(C ↦ (sfs, Processing)) √"
  proof(rule shconf_upd_obj)
    show "P,h ⊢⇩s sh √" using InitObjectRed by simp
    moreover have "sh C = ⌊(sfs, Prepared)⌋" using InitObjectRed by simp
    ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
  qed
  then show ?case using sh' by blast
next
  case (InitNonObjectSuperRed sh C sfs D a b sh' C' Cs e h l)
  have sh': "sh' = sh(C ↦ (sfs, Processing))" by fact
  have "P,h ⊢⇩s sh(C ↦ (sfs, Processing)) √"
  proof(rule shconf_upd_obj)
    show "P,h ⊢⇩s sh √" using InitNonObjectSuperRed by simp
    moreover have "sh C = ⌊(sfs, Prepared)⌋" using InitNonObjectSuperRed by simp
    ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
  qed
  then show ?case using sh' by blast
next
  case (RedRInit sh C sfs i sh' C' Cs e v h l)
  have sh': "sh' = sh(C ↦ (sfs, Done))" by fact
  have "P,h ⊢⇩s sh(C ↦ (sfs, Done)) √"
  proof(rule shconf_upd_obj)
    show "P,h ⊢⇩s sh √" using RedRInit by simp
    moreover have "sh C = ⌊(sfs, i)⌋" using RedRInit by simp
    ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
  qed
  then show ?case using sh' by blast
next
  case (RInitInitThrow sh C sfs i sh' a D Cs e h l)
  have sh': "sh' = sh(C ↦ (sfs, Error))" by fact
  have "P,h ⊢⇩s sh(C ↦ (sfs, Error)) √"
  proof(rule shconf_upd_obj)
    show "P,h ⊢⇩s sh √" using RInitInitThrow by simp
    moreover have "sh C = ⌊(sfs, i)⌋" using RInitInitThrow by simp
    ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
  qed
  then show ?case using sh' by blast
next
  case (RInitThrow sh C sfs i sh' a e' h l)
  have sh': "sh' = sh(C ↦ (sfs, Error))" by fact
  have "P,h ⊢⇩s sh(C ↦ (sfs, Error)) √"
  proof(rule shconf_upd_obj)
    show "P,h ⊢⇩s sh √" using RInitThrow by simp
    moreover have "sh C = ⌊(sfs, i)⌋" using RInitThrow by simp
    ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
  qed
  then show ?case using sh' by blast
qed(auto elim: WTrt.cases)
(*>*)

theorem assumes wf: "wwf_J_prog P"
shows red_preserves_iconf:
  "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ iconf sh e ⟹ iconf sh' e'"
and reds_preserves_iconf:
  "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ iconfs sh es ⟹ iconfs sh' es'"
(*<*)
proof (induct rule:red_reds_inducts)
  case (BinOpRed1 e h l sh b e' h' l' sh' b' bop e⇩2)
  then show ?case using BinOpRed1 nsub_RI_iconf[of e⇩2 sh'] val_of_spec
  proof(cases "val_of e") qed(simp,fast)
next
  case (FAssRed1 e h l sh b e' h' l' sh' b' F D e⇩2)
  then show ?case using FAssRed1 nsub_RI_iconf[of e⇩2 sh'] val_of_spec
  proof(cases "val_of e") qed(simp,fast)
next
  case (CallObj e h l sh b e' h' l' sh' b' M es)
  then show ?case using CallObj nsub_RIs_iconfs[of es sh'] val_of_spec
  proof(cases "val_of e") qed(simp,fast)
next
  case RedCall then show ?case using sees_wwf_nsub_RI[OF wf RedCall.hyps(2)]
    by (clarsimp simp: assigned_def nsub_RI_iconf)
next
  case (RedSCall C M Ts T pns body D vs a a b)
  then have "¬sub_RI (blocks (pns, Ts, vs, body))"
    using sees_wwf_nsub_RI[OF wf RedSCall.hyps(1)] by simp
  then show ?case by(rule nsub_RI_iconf)
next
  case SCallInitRed then show ?case by fastforce
next
  case (BlockRedNone e h l V sh b e' h' l' sh' b' T)
  then show ?case by auto
next
  case (SeqRed e h l sh b e' h' l' sh' b' e⇩2)
  then show ?case
  proof(cases "lass_val_of e")
    case None then show ?thesis using SeqRed nsub_RI_iconf by(auto dest: val_of_spec)
  next
    case (Some a)
    have "e' = unit ∧ sh' = sh" by(simp add: lass_val_of_red[OF Some SeqRed(1)])
    then show ?thesis using SeqRed Some by(auto dest: val_of_spec)
  qed
next
  case (ListRed1 e h l sh b e' h' l' sh' b' es)
  then show ?case using ListRed1 nsub_RIs_iconfs[of es sh'] val_of_spec
  proof(cases "val_of e") qed(simp,fast)
next
  case RedInit then show ?case by(auto simp: nsub_RI_iconf)
next
  case (RedInitDone sh C sfs C' Cs e h l b)
  then show ?case proof(cases Cs) qed(auto simp: initPD_def)
next
  case (RedInitProcessing sh C sfs C' Cs e h l b)
  then show ?case proof(cases Cs) qed(auto simp: initPD_def)
next
  case (RedRInit sh C sfs i sh' C' Cs v e h l b)
  then show ?case proof(cases Cs) qed(auto simp: initPD_def)
next
  case CallThrowParams then show ?case by(auto simp: iconfs_map_throw)
next
  case SCallThrowParams then show ?case by(auto simp: iconfs_map_throw)
qed(auto simp: nsub_RI_iconf lass_val_of_iconf)
(*>*)


lemma Seq_bconf_preserve_aux:
assumes "P ⊢ ⟨e,(h, l, sh),b⟩ → ⟨e',(h', l', sh'),b'⟩" and "P,sh ⊢⇩b (e;; e⇩2,b) √"
  and "P,sh ⊢⇩b (e::expr,b) √ ⟶ P,sh' ⊢⇩b (e'::expr,b') √"
shows "P,sh' ⊢⇩b (e';;e⇩2,b') √"
proof(cases "val_of e")
  case None show ?thesis
  proof(cases "lass_val_of e")
    case lNone: None show ?thesis
    proof(cases "lass_val_of e'")
      case lNone': None
      then show ?thesis using None assms lNone
        by(auto dest: val_of_spec simp: bconf_def option.distinct(1))
    next
      case (Some a)
      then show ?thesis using None assms lNone by(auto dest: lass_val_of_spec simp: bconf_def)
    qed
  next
    case (Some a)
    then show ?thesis using None assms by(auto dest: lass_val_of_spec)
  qed
next
  case (Some a)
  then show ?thesis using assms by(auto dest: val_of_spec)
qed

theorem red_preserves_bconf:
  "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ iconf sh e ⟹ P,sh ⊢⇩b (e,b) √ ⟹ P,sh' ⊢⇩b (e',b') √"
and reds_preserves_bconf:
  "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ iconfs sh es ⟹ P,sh ⊢⇩b (es,b) √ ⟹ P,sh' ⊢⇩b (es',b') √"
(*<*)
proof (induct rule:red_reds_inducts)
  case (CastRed e a a b b e' a a b b' C) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (BinOpRed1 e h l sh b e' h' l' sh' b' bop e⇩2) show ?case
  proof(cases b')
    case True with BinOpRed1 val_of_spec show ?thesis
    proof(cases "val_of e") qed(simp,fast)
  next
    case False then show ?thesis by (simp add: bconf_def)
  qed
next
case (BinOpRed2 e a a b b e' a a b b' v⇩1 bop) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (LAssRed e a a b b e' a a b b' V) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (FAccRed e a a b b e' a a b b' F D) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (RedSFAccNonStatic C F t D h l sh b) then show ?case
    using has_field_fun[of P C F NonStatic] by (auto simp: bconf_def)
next
  case (FAssRed1 e h l sh b e' h' l' sh' b' F D e⇩2) show ?case
  proof(cases b')
    case True with FAssRed1 val_of_spec show ?thesis
    proof(cases "val_of e'")qed((simp,fast)+)
  next
    case False then show ?thesis by(simp add: bconf_def)
  qed
next
  case (FAssRed2 e a a b b e' a a b b' v F D) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (SFAssRed e h l sh b e' h' l' sh' b' C F D) then show ?case
  proof(cases b') qed(fastforce simp: bconf_def val_no_step)+
next
  case (RedSFAssNonStatic C F t D v a a b b) then show ?case
    using has_field_fun[of P C F NonStatic] by (auto simp: bconf_def)
next
  case (CallObj e h l sh b e' h' l' sh' b' M es) show ?case
  proof(cases b')
    case True with CallObj val_of_spec show ?thesis
    proof(cases "val_of e'")qed((simp,fast)+)
  next
    case False then show ?thesis by(simp add: bconf_def)
  qed
next
  case (CallParams es a a b b es' a a b b' v M) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (SCallParams es h l sh b es' h' l' sh' b' C M) show ?case
  proof(cases b')
    case b': True show ?thesis
    proof(cases "map_vals_of es'")
      case None
      then show ?thesis using SCallParams b' vals_no_step
      proof(cases "map_vals_of es")qed(clarsimp,fast)
    next
      case f: Some
      then show ?thesis using SCallParams b' vals_no_step
      proof(cases "map_vals_of es")qed(clarsimp,fast)
    qed
  next
    case False then show ?thesis by(simp add: bconf_def)
  qed
next
  case (SCallInitDoneRed C M Ts T pns body D sh sfs vs h l)
    then show ?case by(auto simp: bconf_def initPD_def) (rule_tac x=D in exI, auto)+
next
  case (RedSCallNonStatic C M Ts T a b D vs h l sh b) then show ?case
    using sees_method_fun[of P C M NonStatic] by (auto simp: bconf_def)
next
  case (BlockRedNone e h l V sh b e' h' l' sh' b' T) show ?case
  proof(cases "assigned V e'")
    case True
    then obtain v e2 where "e' = V := Val v;;e2" by(clarsimp simp: assigned_def)
    then show ?thesis using BlockRedNone by(clarsimp simp: bconf_def)
  next
    case False then show ?thesis using BlockRedNone by simp
  qed
next
  case (BlockRedSome e h l V sh b e' h' l' sh' b' v T) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (InitBlockRed e h l V v sh b e' h' l' sh' b' v' T) show ?case
  proof(cases b')
    case True
    then show ?thesis using InitBlockRed by (simp add: assigned_def)
  next
    case False then show ?thesis by(simp add: bconf_def)
  qed
next
  case (RedBlock V T u)
  then have "¬assigned V (Val u)" by(clarsimp simp: assigned_def)
  then show ?case using RedBlock by(simp add: bconf_def)
next
  case (SeqRed e h l sh b e' h' l' sh' b' e⇩2)
  have "iconf sh e"
  proof(cases "lass_val_of e")
    case (Some a) show ?thesis by(rule lass_val_of_iconf[OF Some])
  next
    case None then show ?thesis using SeqRed by(auto dest: val_of_spec)
  qed
  then show ?case using SeqRed Seq_bconf_preserve_aux by simp
next
  case (CondRed e a a b b e' a a b b' e⇩1 e⇩2) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (ThrowRed e a a b b e' a a b b') then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (TryRed e a a b b e' a a b b' C V e⇩2) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (ListRed1 e h l sh b e' h' l' sh' b' es)
  with val_of_spec show ?case
  proof(cases b') qed((clarsimp,fast),simp add: bconfs_def)
next
  case (RedInit C b' e X Y b b'')
  then show ?case
   by(auto simp: bconf_def icheck_ss_exp icheck_init_class icheck_curr_init)
next
  case (RInitRed e a a b b e' a a b b' C Cs e⇩0) then show ?case
  proof(cases b') qed(simp, simp add: bconf_def)
next
  case (BlockThrow V T a)
  then have "¬assigned V (Throw a)" by(simp add: assigned_def)
  then show ?case using BlockThrow by simp
qed(simp_all, auto simp: bconf_def initPD_def)
(*>*)

text‹ Preservation of definite assignment more complex and requires a
few lemmas first. ›

lemma [iff]: "⋀A. ⟦ length Vs = length Ts; length vs = length Ts⟧ ⟹
 𝒟 (blocks (Vs,Ts,vs,e)) A = 𝒟 e (A ⊔ ⌊set Vs⌋)"
(*<*)
by (induct Vs Ts vs e rule:blocks_induct)
   (simp_all add:hyperset_defs)
(*>*)


lemma red_lA_incr: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩
   ⟹ ⌊dom l⌋ ⊔ 𝒜 e ⊑  ⌊dom l'⌋ ⊔ 𝒜 e'"
and reds_lA_incr: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩
   ⟹ ⌊dom l⌋ ⊔ 𝒜s es ⊑  ⌊dom l'⌋ ⊔ 𝒜s es'"
(*<*)
proof(induct rule:red_reds_inducts)
  case TryRed then show ?case
    by(simp del:fun_upd_apply add:hyperset_defs)
      (blast dest:red_lcl_incr)+
next
  case BinOpRed1 then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case BinOpRed2 then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case LAssRed then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case FAssRed1 then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case FAssRed2 then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case CallObj then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case CallParams then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case BlockRedNone then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case BlockRedSome then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case InitBlockRed then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case SeqRed then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case CondRed then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case RedCondT then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case RedCondF then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case ListRed1 then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
  case ListRed2 then show ?case
    by(auto simp del:fun_upd_apply simp:hyperset_defs)
qed (simp_all del:fun_upd_apply add:hyperset_defs)
(*>*)

text‹ Now preservation of definite assignment. ›

lemma assumes wf: "wf_J_prog P"
shows red_preserves_defass:
  "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ 𝒟 e ⌊dom l⌋ ⟹ 𝒟 e' ⌊dom l'⌋"
and "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ 𝒟s es ⌊dom l⌋ ⟹ 𝒟s es' ⌊dom l'⌋"
(*<*)
proof (induct rule:red_reds_inducts)
  case BinOpRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case FAssRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CallObj thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
next
  case RedCall thus ?case
    by (auto dest!:sees_wf_mdecl[OF wf] simp:wf_mdecl_def hyperset_defs elim!:D_mono')
next
  case RedSCall thus ?case
    by (auto dest!:sees_wf_mdecl[OF wf] simp:wf_mdecl_def hyperset_defs elim!:D_mono')
next
  case SCallInitRed
  then show ?case by(auto simp:hyperset_defs Ds_Vals)
next
  case InitBlockRed thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case BlockRedNone thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case BlockRedSome thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case SeqRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CondRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case TryRed thus ?case
    by (fastforce dest:red_lcl_incr intro:D_mono' simp:hyperset_defs)
next
  case ListRed1 thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
next
  case RedWhile thus ?case by(auto simp:hyperset_defs elim!:D_mono')
next
  case RedInit then show ?case by (auto intro: D_mono' simp: hyperset_defs)
next
  case (RInitRed e h l sh b e' h' l' sh' b' C Cs e⇩0)
  then show ?case by(auto simp:hyperset_defs dest:red_lcl_incr elim!:D_mono')
qed(auto simp:hyperset_defs)
(*>*)


text‹ Combining conformance of heap, static heap, and local variables: ›

definition sconf :: "J_prog ⇒ env ⇒ state ⇒ bool"   ("_,_ ⊢ _ √"   [51,51,51]50)
where
  "P,E ⊢ s √  ≡  let (h,l,sh) = s in P ⊢ h √ ∧ P,h ⊢ l (:≤) E ∧ P,h ⊢⇩s sh √"

lemma red_preserves_sconf:
  "⟦ P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩; P,E,hp s,shp s ⊢ e : T; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"
(*<*)
by(fastforce intro:red_preserves_hconf red_preserves_lconf red_preserves_shconf
            simp add:sconf_def)
(*>*)

lemma reds_preserves_sconf:
  "⟦ P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩; P,E,hp s,shp s ⊢ es [:] Ts; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"
(*<*)
by(fastforce intro:reds_preserves_hconf reds_preserves_lconf reds_preserves_shconf
            simp add:sconf_def)
(*>*)


subsection "Subject reduction"

lemma wt_blocks:
 "⋀E. ⟦ length Vs = length Ts; length vs = length Ts ⟧ ⟹
       (P,E,h,sh ⊢ blocks(Vs,Ts,vs,e) : T) =
       (P,E(Vs[↦]Ts),h,sh ⊢ e:T ∧ (∃Ts'. map (typeof⇘h⇙) vs = map Some Ts' ∧ P ⊢ Ts' [≤] Ts))"
(*<*)
proof(induct Vs Ts vs e rule:blocks_induct)
  case (1 V Vs T Ts v vs e)
  then show ?case by(force simp add:rel_list_all2_Cons2)
qed simp_all
(*>*)

theorem assumes wf: "wf_J_prog P"
shows subject_reduction2: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹
  (⋀E T. ⟦ P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e:T ⟧
           ⟹ ∃T'. P,E,h',sh' ⊢ e':T' ∧ P ⊢ T' ≤ T)"
and subjects_reduction2: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹
  (⋀E Ts. ⟦ P,E ⊢ (h,l,sh) √; iconfs sh es; P,E,h,sh ⊢ es [:] Ts ⟧
            ⟹ ∃Ts'. P,E,h',sh' ⊢ es' [:] Ts' ∧ P ⊢ Ts' [≤] Ts)"
(*<*)
proof (induct rule:red_reds_inducts)
  case RedNew then show ?case by (auto simp: blank_def)
next
  case RedNewFail thus ?case
    by (unfold sconf_def hconf_def) (fastforce elim!:typeof_OutOfMemory)
next
  case CastRed thus ?case
    by(clarsimp simp:is_refT_def)
      (blast intro: widens_trans dest!:widen_Class[THEN iffD1])
next
  case RedCastFail thus ?case
    by (unfold sconf_def hconf_def)  (fastforce elim!:typeof_ClassCast)
next
  case (BinOpRed1 e⇩1 h l sh b e⇩1' h' l' sh' b' bop e⇩2)
  have red: "P ⊢ ⟨e⇩1,(h,l,sh),b⟩ → ⟨e⇩1',(h',l',sh'),b'⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e⇩1; P,E,h,sh ⊢ e⇩1:T⟧
                 ⟹ ∃U. P,E,h',sh' ⊢ e⇩1' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (e⇩1 «bop» e⇩2)"
   and wt: "P,E,h,sh ⊢ e⇩1 «bop» e⇩2 : T" by fact+
  have val: "val_of e⇩1 = None" using red iconf val_no_step by auto
  then have iconf1: "iconf sh e⇩1" and nsub_RI2: "¬sub_RI e⇩2" using iconf by simp+
  have "P,E,h',sh' ⊢ e⇩1' «bop» e⇩2 : T"
  proof (cases bop)
    assume [simp]: "bop = Eq"
    from wt obtain T⇩1 T⇩2 where [simp]: "T = Boolean"
      and wt⇩1: "P,E,h,sh ⊢ e⇩1 : T⇩1" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : T⇩2" by auto
    show ?thesis
      using WTrt_hext_shext_mono[OF wt⇩2 red_hext_incr[OF red] red_shext_incr[OF red wt⇩1] nsub_RI2]
        IH[OF conf iconf1 wt⇩1] by auto
  next
    assume  [simp]: "bop = Add"
    from wt have [simp]: "T = Integer"
      and wt⇩1: "P,E,h,sh ⊢ e⇩1 : Integer" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : Integer"
      by auto
    show ?thesis
      using WTrt_hext_shext_mono[OF wt⇩2 red_hext_incr[OF red] red_shext_incr[OF red wt⇩1] nsub_RI2]
        IH[OF conf iconf1 wt⇩1] by auto
  qed
  thus ?case by auto
next
  case (BinOpRed2 e⇩2 h l sh b e⇩2' h' l' sh' b' v⇩1 bop)
  have red: "P ⊢ ⟨e⇩2,(h,l,sh),b⟩ → ⟨e⇩2',(h',l',sh'),b'⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e⇩2; P,E,h,sh ⊢ e⇩2:T⟧
                 ⟹ ∃U. P,E,h',sh' ⊢ e⇩2' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (Val v⇩1 «bop» e⇩2)"
   and wt: "P,E,h,sh ⊢ (Val v⇩1) «bop» e⇩2 : T" by fact+
  have iconf2: "iconf sh e⇩2" using iconf by simp
  have "P,E,h',sh' ⊢ (Val v⇩1) «bop» e⇩2' : T"
  proof (cases bop)
    assume [simp]: "bop = Eq"
    from wt obtain T⇩1 T⇩2 where [simp]: "T = Boolean"
      and wt⇩1: "P,E,h,sh ⊢ Val v⇩1 : T⇩1" and wt⇩2: "P,E,h,sh ⊢ e⇩2:T⇩2" by auto
    show ?thesis
      using IH[OF conf iconf2 wt⇩2] WTrt_hext_mono[OF wt⇩1 red_hext_incr[OF red]]
      by auto
  next
    assume  [simp]: "bop = Add"
    from wt have [simp]: "T = Integer"
      and wt⇩1: "P,E,h,sh ⊢ Val v⇩1 : Integer" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : Integer"
      by auto
    show ?thesis
      using IH[OF conf iconf2 wt⇩2] WTrt_hext_mono[OF wt⇩1 red_hext_incr[OF red]]
      by auto
  qed
  thus ?case by auto
next
  case (RedBinOp bop) thus ?case
  proof (cases bop)
    case Eq thus ?thesis using RedBinOp by auto
  next
    case Add thus ?thesis using RedBinOp by auto
  qed
next
  case RedVar thus ?case by (fastforce simp:sconf_def lconf_def conf_def)
next
  case (LAssRed e h l sh b e' h' l' sh' b' V)
  obtain Te where Te: "P,E,h,sh ⊢ e : Te ∧ P ⊢ Te ≤ the(E V)" using LAssRed.prems(3) by auto
  then have wide: "P ⊢ Te ≤ the(E V)" using LAssRed by simp
  then have "∃T'. P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ Te"
    using LAssRed.hyps(2) LAssRed.prems(1,2) Te widen_trans[OF _ wide] by auto
  then obtain T' where wt: "P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ Te" by clarsimp
  have "P,E,h',sh' ⊢ V:=e' : Void" using LAssRed wt widen_trans[OF _ wide] by auto
  then show ?case using LAssRed by(rule_tac x = Void in exI) auto
next
  case (FAccRed e h l sh b e' h' l' sh' b' F D)
  have IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
                 ⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (e∙F{D})"
   and wt: "P,E,h,sh ⊢ e∙F{D} : T" by fact+
  have iconf': "iconf sh e" using iconf by simp+
  ― ‹The goal: ?case = @{prop ?case}›
  ― ‹Now distinguish the two cases how wt can have arisen.›
  { fix C assume wte: "P,E,h,sh ⊢ e : Class C"
             and has: "P ⊢ C has F,NonStatic:T in D"
    from IH[OF conf iconf' wte]
    obtain U where wte': "P,E,h',sh' ⊢ e' : U" and UsubC: "P ⊢ U ≤ Class C"
      by auto
    ― ‹Now distinguish what @{term U} can be.›
    { assume "U = NT" hence ?case using wte'
        by(blast intro:WTrtFAccNT widen_refl) }
    moreover
    { fix C' assume U: "U = Class C'" and C'subC: "P ⊢ C' ≼⇧* C"
      from has_field_mono[OF has C'subC] wte' U
      have ?case by(blast intro:WTrtFAcc) }
    ultimately have ?case using UsubC by(simp add: widen_Class) blast }
  moreover
  { assume "P,E,h,sh ⊢ e : NT"
    hence "P,E,h',sh' ⊢ e' : NT" using IH[OF conf iconf'] by fastforce
    hence ?case  by(fastforce intro:WTrtFAccNT widen_refl) }
  ultimately show ?case using wt by blast
next
  case RedFAcc thus ?case
    by(fastforce simp:sconf_def hconf_def oconf_def conf_def has_field_def
                dest:has_fields_fun)
next
  case RedFAccNull thus ?case
    by(fastforce intro: widen_refl WTThrow[OF WTVal] elim!: typeof_NullPointer
                simp: sconf_def hconf_def)
next
  case RedSFAccNone then show ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_NoSuchFieldError
      simp: sconf_def hconf_def)
next
  case RedFAccStatic then show ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
      simp: sconf_def hconf_def)
next
  case (RedSFAcc C F t D sh sfs i v h l es)
  then have "P ⊢ C has F,Static:T in D" by fast
  then have dM: "P ⊢ D has F,Static:T in D" by(rule has_field_idemp)
  then show ?case using RedSFAcc by(fastforce simp:sconf_def shconf_def soconf_def conf_def)
next
  case SFAccInitDoneRed then show ?case by (meson widen_refl)
next
  case (SFAccInitRed C F t D sh h l E T)
  have "is_class P D" using SFAccInitRed.hyps(1) by(rule has_field_is_class')
  then have "P,E,h,sh ⊢ INIT D ([D],False) ← C∙⇩sF{D} : T ∧ P ⊢ T ≤ T"
    using SFAccInitRed WTrtInit[OF SFAccInitRed.prems(3)] by clarsimp
  then show ?case by(rule exI)
next
  case RedSFAccNonStatic then show ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
      simp: sconf_def hconf_def)
next
  case (FAssRed1 e h l sh b e' h' l' sh' b' F D e⇩2)
  have red: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
                 ⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (e∙F{D} := e⇩2)"
   and wt: "P,E,h,sh ⊢ e∙F{D}:=e⇩2 : T" by fact+
  have val: "val_of e = None" using red iconf val_no_step by auto
  then have iconf': "iconf sh e" and nsub_RI2: "¬sub_RI e⇩2" using iconf by simp+
  from wt have void: "T = Void" by blast
  ― ‹We distinguish if @{term e} has type @{term NT} or a Class type›
  ― ‹Remember ?case = @{term ?case}›
  { assume wt':"P,E,h,sh ⊢ e : NT"
    hence "P,E,h',sh' ⊢ e' : NT" using IH[OF conf iconf'] by fastforce
    moreover obtain T⇩2 where "P,E,h,sh ⊢ e⇩2 : T⇩2" using wt by auto
    from this red_hext_incr[OF red] red_shext_incr[OF red wt'] nsub_RI2 have  "P,E,h',sh' ⊢ e⇩2 : T⇩2"
      by(rule WTrt_hext_shext_mono)
    ultimately have ?case using void by(blast intro!:WTrtFAssNT)
  }
  moreover
  { fix C TF T⇩2 assume wt⇩1: "P,E,h,sh ⊢ e : Class C" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : T⇩2"
    and has: "P ⊢ C has F,NonStatic:TF in D" and sub: "P ⊢ T⇩2 ≤ TF"
    obtain U where wt⇩1': "P,E,h',sh' ⊢ e' : U" and UsubC: "P ⊢ U ≤ Class C"
      using IH[OF conf iconf' wt⇩1] by blast
    have wt⇩2': "P,E,h',sh' ⊢ e⇩2 : T⇩2"
      by(rule WTrt_hext_shext_mono[OF wt⇩2 red_hext_incr[OF red] red_shext_incr[OF red wt⇩1] nsub_RI2])
    ― ‹Is @{term U} the null type or a class type?›
    { assume "U = NT" with wt⇩1' wt⇩2' void have ?case
        by(blast intro!:WTrtFAssNT) }
    moreover
    { fix C' assume UClass: "U = Class C'" and "subclass": "P ⊢ C' ≼⇧* C"
      have "P,E,h',sh' ⊢ e' : Class C'" using wt⇩1' UClass by auto
      moreover have "P ⊢ C' has F,NonStatic:TF in D"
        by(rule has_field_mono[OF has "subclass"])
      ultimately have ?case using wt⇩2' sub void by(blast intro:WTrtFAss) }
    ultimately have ?case using UsubC by(auto simp add:widen_Class) }
  ultimately show ?case using wt by blast
next
  case (FAssRed2 e⇩2 h l sh b e⇩2' h' l' sh' b' v F D)
  have red: "P ⊢ ⟨e⇩2,(h,l,sh),b⟩ → ⟨e⇩2',(h',l',sh'),b'⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e⇩2; P,E,h,sh ⊢ e⇩2 : T⟧
                 ⟹ ∃U. P,E,h',sh' ⊢ e⇩2' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (Val v∙F{D} := e⇩2)"
   and wt: "P,E,h,sh ⊢ Val v∙F{D}:=e⇩2 : T" by fact+
  have iconf2: "iconf sh e⇩2" using iconf by simp
  from wt have [simp]: "T = Void" by auto
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix C TF T⇩2
    assume wt⇩1: "P,E,h,sh ⊢ Val v : Class C"
      and has: "P ⊢ C has F,NonStatic:TF in D"
      and wt⇩2: "P,E,h,sh ⊢ e⇩2 : T⇩2" and TsubTF: "P ⊢ T⇩2 ≤ TF"
    have wt⇩1': "P,E,h',sh' ⊢ Val v : Class C"
      using WTrt_hext_mono[OF wt⇩1 red_hext_incr[OF red]] by auto
    obtain T⇩2' where wt⇩2': "P,E,h',sh' ⊢ e⇩2' : T⇩2'" and T'subT: "P ⊢ T⇩2' ≤ T⇩2"
      using IH[OF conf iconf2 wt⇩2] by blast
    have "P,E,h',sh' ⊢ Val v∙F{D}:=e⇩2' : Void"
      by(rule WTrtFAss[OF wt⇩1' has wt⇩2' widen_trans[OF T'subT TsubTF]])
    thus ?case by auto
  next
    fix T⇩2 assume null: "P,E,h,sh ⊢ Val v : NT" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : T⇩2"
    from null have "v = Null" by simp
    moreover
    obtain T⇩2' where "P,E,h',sh' ⊢ e⇩2' : T⇩2' ∧ P ⊢ T⇩2' ≤ T⇩2"
      using IH[OF conf iconf2 wt⇩2] 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
    by(fastforce intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp:sconf_def hconf_def)
next
  case RedFAssStatic then show ?case 
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
      simp: sconf_def hconf_def)
next
  case (SFAssRed e h l sh b e' h' l' sh' b' C F D E T)
  have IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
                 ⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (C∙⇩sF{D} := e)"
   and wt: "P,E,h,sh ⊢ C∙⇩sF{D}:=e : T" by fact+
  have iconf': "iconf sh e" using iconf by simp
  from wt have [simp]: "T = Void" by auto
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix TF T1
    assume has: "P ⊢ C has F,Static:TF in D"
      and wt1: "P,E,h,sh ⊢ e : T1" and TsubTF: "P ⊢ T1 ≤ TF"
    obtain T' where wt1': "P,E,h',sh' ⊢ e' : T'" and T'subT: "P ⊢ T' ≤ T1"
      using IH[OF conf iconf' wt1] by blast
    have "P,E,h',sh' ⊢ C∙⇩sF{D}:=e' : Void"
      by(rule WTrtSFAss[OF wt1' has widen_trans[OF T'subT TsubTF]])
    thus ?case by auto
  qed
next
  case SFAssInitDoneRed then show ?case by (meson widen_refl)
next
  case (SFAssInitRed C F t D sh v h l E T)
  have "is_class P D" using SFAssInitRed.hyps(1) by(rule has_field_is_class')
  then have "P,E,h,sh ⊢ INIT D ([D],False) ← C∙⇩sF{D} := Val v : T ∧ P ⊢ T ≤ T"
    using SFAssInitRed WTrtInit[OF SFAssInitRed.prems(3)] by clarsimp
  then show ?case by(rule exI)
next
  case RedSFAssNone then show ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_NoSuchFieldError
      simp: sconf_def hconf_def)
next
  case RedSFAssNonStatic then show ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
      simp: sconf_def hconf_def)
next
  case (CallObj e h l sh b e' h' l' sh' b' M es)
  have red: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
                 ⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (e∙M(es))"
   and wt: "P,E,h,sh ⊢ e∙M(es) : T" by fact+
  have val: "val_of e = None" using red iconf val_no_step by auto
  then have iconf': "iconf sh e" and nsub_RIs: "¬sub_RIs es" using iconf by simp+
  ― ‹We distinguish if @{term e} has type @{term NT} or a Class type›
  ― ‹Remember ?case = @{term ?case}›
  { assume wt':"P,E,h,sh ⊢ e:NT"
    hence "P,E,h',sh' ⊢ e' : NT" using IH[OF conf iconf'] by fastforce
    moreover
    fix Ts assume wtes: "P,E,h,sh ⊢ es [:] Ts"
    have "P,E,h',sh' ⊢ es [:] Ts"
      by(rule WTrts_hext_shext_mono[OF wtes red_hext_incr[OF red] red_shext_incr[OF red wt'] nsub_RIs])
    ultimately have ?case by(blast intro!:WTrtCallNT) }
  moreover
  { fix C D Ts Us pns body
    assume wte: "P,E,h,sh ⊢ e : Class C"
      and "method": "P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D"
      and wtes: "P,E,h,sh ⊢ es [:] Us" and subs: "P ⊢ Us [≤] Ts"
    obtain U where wte': "P,E,h',sh' ⊢ e' : U" and UsubC: "P ⊢ U ≤ Class C"
      using IH[OF conf iconf' wte] by blast
    ― ‹Is @{term U} the null type or a class type?›
    { assume "U = NT"
      moreover have "P,E,h',sh' ⊢ es [:] Us"
        by(rule WTrts_hext_shext_mono[OF wtes red_hext_incr[OF red] red_shext_incr[OF red wte] nsub_RIs])
      ultimately have ?case using wte' by(blast intro!:WTrtCallNT) }
    moreover
    { fix C' assume UClass: "U = Class C'" and "subclass": "P ⊢ C' ≼⇧* C"
      have "P,E,h',sh' ⊢ e' : Class C'" using wte' UClass by auto
      moreover obtain Ts' T' pns' body' D'
        where method': "P ⊢ C' sees M,NonStatic:Ts'→T' = (pns',body') in D'"
        and subs': "P ⊢ Ts [≤] Ts'" and sub': "P ⊢ T' ≤ T"
        using Call_lemma[OF "method" "subclass" wf] by fast
      moreover have "P,E,h',sh' ⊢ es [:] Us"
        by(rule WTrts_hext_shext_mono[OF wtes red_hext_incr[OF red] red_shext_incr[OF red wte] nsub_RIs])
      ultimately have ?case
        using subs by(blast intro:WTrtCall rtrancl_trans widens_trans) }
    ultimately have ?case using UsubC by(auto simp add:widen_Class) }
  ultimately show ?case using wt by auto
next
  case (CallParams es h l sh b es' h' l' sh' b' v M)
  have reds: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩"
   and IH: "⋀E Ts. ⟦P,E ⊢ (h,l,sh) √; iconfs sh es; P,E,h,sh ⊢ es [:] Ts⟧
                 ⟹ ∃Us. P,E,h',sh' ⊢ es' [:] Us ∧ P ⊢ Us [≤] Ts"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (Val v∙M(es))"
   and wt: "P,E,h,sh ⊢ Val v∙M(es) : T" by fact+
  have iconfs: "iconfs sh es" using iconf by simp
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix C D Ts Us pns body
    assume wte: "P,E,h,sh ⊢ Val v : Class C"
      and "P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D"
      and wtes: "P,E,h,sh ⊢ es [:] Us" and "P ⊢ Us [≤] Ts"
    moreover have "P,E,h',sh' ⊢ Val v : Class C"
      using WTrt_hext_mono[OF wte reds_hext_incr[OF reds]] by auto
    moreover
    obtain Us' where "P,E,h',sh' ⊢ es' [:] Us' ∧ P ⊢ Us' [≤] Us"
      using IH[OF conf iconfs wtes] by blast
    ultimately show ?thesis by(blast intro:WTrtCall widens_trans)
  next
    fix Us
    assume null: "P,E,h,sh ⊢ Val v : NT" and wtes: "P,E,h,sh ⊢ es [:] Us"
    from null have "v = Null" by simp
    moreover
    obtain Us' where "P,E,h',sh' ⊢ es' [:] Us' ∧ P ⊢ Us' [≤] Us"
      using IH[OF conf iconfs wtes] by blast
    ultimately show ?thesis by(fastforce intro:WTrtCallNT)
  qed
next
  case (RedCall h a C fs M Ts T pns body D vs l sh b E T')
  have hp: "h a = Some(C,fs)"
   and "method": "P ⊢ C sees M,NonStatic: Ts→T = (pns,body) in D"
   and wt: "P,E,h,sh ⊢ addr a∙M(map Val vs) : T'" by fact+
  obtain Ts' where wtes: "P,E,h,sh ⊢ map Val vs [:] Ts'"
    and subs: "P ⊢ Ts' [≤] Ts" and T'isT: "T' = T"
    using wt "method" hp by (auto dest:sees_method_fun)
  from wtes subs have length_vs: "length vs = length Ts"
    by(fastforce simp:list_all2_iff dest!:WTrts_same_length)
  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),h,sh ⊢ body : T''"
    by(rule WT_implies_WTrt)
  hence "P,E(this#pns [↦] Class D#Ts),h,sh ⊢ body : T''"
    by(rule WTrt_env_mono) simp
  hence "P,E,h,sh ⊢ 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
    by(fastforce simp add:wt_blocks rel_list_all2_Cons2)
  with T''subT T'isT show ?case by blast
next
  case RedCallNull thus ?case
    by(fastforce intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp: sconf_def hconf_def)
next
  case RedCallStatic then show ?case 
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
      simp: sconf_def hconf_def)
next
  case (SCallParams es h l sh b es' h' l' sh' b' C M)
  have IH: "⋀E Ts. ⟦P,E ⊢ (h,l,sh) √; iconfs sh es; P,E,h,sh ⊢ es [:] Ts⟧
                 ⟹ ∃Us. P,E,h',sh' ⊢ es' [:] Us ∧ P ⊢ Us [≤] Ts"
   and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (C∙⇩sM(es))"
   and wt: "P,E,h,sh ⊢ C∙⇩sM(es) : T" by fact+
  have iconfs: "iconfs sh es" using iconf by simp
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix D Ts Us pns body sfs vs
    assume method: "P ⊢ C sees M,Static:Ts→T = (pns,body) in D"
      and wtes: "P,E,h,sh ⊢ es [:] Us" and us: "P ⊢ Us [≤] Ts"
      and clinit: "M = clinit ⟶ sh D = ⌊(sfs,Processing)⌋ ∧ es = map Val vs"
    obtain Us' where es': "P,E,h',sh' ⊢ es' [:] Us'" and us': "P ⊢ Us' [≤] Us"
      using IH[OF conf iconfs wtes] by blast
    show ?thesis
    proof(cases "M = clinit")
      case True then show ?thesis using clinit SCallParams.hyps(1) by blast
    next
      case False
      then show ?thesis using es' method us us' by(blast intro:WTrtSCall widens_trans)
    qed
  qed
next
  case (RedSCall C M Ts T pns body D vs h l sh E T')
  have "method": "P ⊢ C sees M,Static: Ts→T = (pns,body) in D"
   and wt: "P,E,h,sh ⊢ C∙⇩sM(map Val vs) : T'" by fact+
  obtain Ts' where wtes: "P,E,h,sh ⊢ map Val vs [:] Ts'"
    and subs: "P ⊢ Ts' [≤] Ts" and T'isT: "T' = T"
    using wt "method" map_Val_eq by(auto dest:sees_method_fun)+
  from wtes subs have length_vs: "length vs = length Ts"
    by(fastforce simp:list_all2_iff dest!:WTrts_same_length)
  from sees_wf_mdecl[OF wf "method"] obtain T''
    where wtabody: "P,[pns [↦] 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(pns [↦] Ts),h,sh ⊢ body : T''"
    by(rule WT_implies_WTrt)
  hence "P,E(pns [↦] Ts),h,sh ⊢ body : T''"
    by(rule WTrt_env_mono) simp
  hence "P,E,h,sh ⊢ blocks(pns, Ts, vs, body) : T''"
  using wtes subs sees_method_decl_above[OF "method"] length_vs length_pns
    by(fastforce simp add:wt_blocks rel_list_all2_Cons2)
  with T''subT T'isT show ?case by blast
next
  case SCallInitDoneRed then show ?case by (meson widen_refl)
next
  case (SCallInitRed C F Ts t pns body D sh v h l E T)
  have "is_class P D" using SCallInitRed.hyps(1) by(rule sees_method_is_class')
  then have "P,E,h,sh ⊢ INIT D ([D],False) ← C∙⇩sF(map Val v) : T ∧ P ⊢ T ≤ T"
    using SCallInitRed WTrtInit[OF SCallInitRed.prems(3)] by clarsimp
  then show ?case by(rule exI)
next
  case RedSCallNone then show ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_NoSuchMethodError
      simp: sconf_def hconf_def)
next
  case RedSCallNonStatic then show ?case 
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
      simp: sconf_def hconf_def)
next
  case BlockRedNone thus ?case
    by(auto simp del:fun_upd_apply)(fastforce simp:sconf_def lconf_def)
next
  case (BlockRedSome e h l V sh b e' h' l' sh' b' v T E Te)
  have red: "P ⊢ ⟨e,(h,l(V:=None),sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l(V:=None),sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
                   ⟹ ∃T'. P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ T"
   and Some: "l' V = Some v" and conf: "P,E ⊢ (h,l,sh) √"
   and iconf: "iconf sh {V:T; e}"
   and wt: "P,E,h,sh ⊢ {V:T; e} : Te" by fact+
  obtain Te' where IH': "P,E(V↦T),h',sh' ⊢ e' : Te' ∧ P ⊢ Te' ≤ Te"
    using IH conf iconf wt by(fastforce simp:sconf_def lconf_def)
  have "P,h' ⊢ l' (:≤) E(V↦T)" using conf wt
    by(fastforce intro:red_preserves_lconf[OF red] simp:sconf_def lconf_def)
  hence "P,h' ⊢ v :≤ T" using Some by(fastforce simp:lconf_def)
  with IH' show ?case
    by(fastforce simp:sconf_def conf_def fun_upd_same simp del:fun_upd_apply)
next
  case (InitBlockRed e h l V v sh b e' h' l' sh' b' v' T E T')
  have red: "P ⊢ ⟨e, (h,l(V↦v),sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l(V↦v),sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
                    ⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and v': "l' V = Some v'" and conf: "P,E ⊢ (h,l,sh) √"
   and iconf: "iconf sh {V:T; V:=Val v;; e}"
   and wt: "P,E,h,sh ⊢ {V:T := Val v; e} : T'" by fact+
  from wt obtain T⇩1 where wt⇩1: "typeof⇘h⇙ v = Some T⇩1"
    and T1subT: "P ⊢ T⇩1 ≤ T" and wt⇩2: "P,E(V↦T),h,sh ⊢ e : T'" by auto
  have lconf⇩2: "P,h ⊢ l(V↦v) (:≤) E(V↦T)" using conf wt⇩1 T1subT
    by(simp add:sconf_def lconf_upd2 conf_def)
  have "∃T⇩1'. typeof⇘h'⇙ v' = Some T⇩1' ∧ P ⊢ T⇩1' ≤ T"
    using v' red_preserves_lconf[OF red wt⇩2 lconf⇩2]
    by(fastforce simp:lconf_def conf_def)
  with IH conf iconf lconf⇩2 wt⇩2 show ?case by (fastforce simp add:sconf_def)
next
  case (SeqRed e h l sh b e' h' l' sh' b' e⇩2)
  then have val: "val_of e = None" by (simp add: val_no_step)
  show ?case
  proof(cases "lass_val_of e")
    case None
    then show ?thesis
      using SeqRed val by(auto elim: WTrt_hext_shext_mono[OF _ red_hext_incr red_shext_incr])
  next
    case (Some a)
    have "sh = sh'" using SeqRed lass_val_of_spec[OF Some] by auto
    then show ?thesis using SeqRed val Some
      by(auto intro: lass_val_of_iconf[OF Some] elim: WTrt_hext_mono[OF _ red_hext_incr])
  qed
next
  case CondRed thus ?case
    by auto (blast intro:WTrt_hext_shext_mono[OF _ red_hext_incr red_shext_incr])+
next
  case ThrowRed thus ?case
    by(auto simp:is_refT_def)(blast dest:widen_Class[THEN iffD1])+
next
  case RedThrowNull thus ?case
    by(fastforce intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp:sconf_def hconf_def)
next
  case TryRed thus ?case
    by auto (blast intro:widen_trans WTrt_hext_shext_mono[OF _ red_hext_incr red_shext_incr])
next
  case RedTryFail thus ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] simp:sconf_def hconf_def)
next
  case (ListRed1 e h l sh b e' h' l' sh' b' es)
    then have val: "val_of e = None" by(simp add: val_no_step)
    obtain U Us where Ts: "Ts = U # Us" using ListRed1 by auto
    then have nsub_RI: "¬ sub_RIs es" and wts: "P,E,h,sh ⊢ es [:] Us" and wt: "P,E,h,sh ⊢ e : U"
     and IH: "⋀E T. ⟦P,E ⊢ (h, l, sh) √; P,E,h,sh ⊢ e : T⟧ ⟹ ∃T'. P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ T"
      using ListRed1 val by auto
    obtain T' where
    "∀E0 E1. (∃T2. P,E1,h',sh' ⊢ e' : T2 ∧ P ⊢ T2 ≤ E0) = (P,E1,h',sh' ⊢ e' : T' E0 E1 ∧ P ⊢ T' E0 E1 ≤ E0)"
      by moura
    then have disj: "∀E t. ¬ P,E ⊢ (h, l, sh) √ ∨ ¬ P,E,h,sh ⊢ e : t ∨ P,E,h',sh' ⊢ e' : T' t E ∧ P ⊢ T' t E ≤ t"
      using IH by presburger
    have "P,E,h',sh' ⊢ es [:] Us"
      using nsub_RI wts wt by (metis (no_types) ListRed1.hyps(1) WTrts_hext_shext_mono red_hext_incr red_shext_incr)
    then have "∃ts. (∃t tsa. ts = t # tsa ∧ P,E,h',sh' ⊢ e' : t ∧ P,E,h',sh' ⊢ es [:] tsa) ∧ P ⊢ ts [≤] (U # Us)"
      using disj wt ListRed1.prems(1) by blast
    then show ?case using Ts by auto
next
  case ListRed2 thus ?case
    by(fastforce dest: hext_typeof_mono[OF reds_hext_incr])
next
  case (InitNoneRed sh C C' Cs e h l b)
  then have sh: "sh ⊴⇩s sh(C ↦ (sblank P C, Prepared))" by(simp add: shext_def)
  have wt: "P,E,h,sh(C ↦ (sblank P C, Prepared)) ⊢ INIT C' (C # Cs,False) ← e : T"
      using InitNoneRed WTrt_shext_mono[OF _ sh] by fastforce
  then show ?case by(rule_tac x = T in exI) (simp add: fun_upd_def)
next
  case (RedInitDone sh C sfs C' Cs e h l b)
  then have "P,E,h,sh ⊢ INIT C' (Cs,True) ← e : T" by auto (metis Nil_tl list.set_sel(2))
  then show ?case by(rule_tac x = T in exI) simp
next
  case (RedInitProcessing sh C sfs C' Cs e h l b)
  then have "P,E,h,sh ⊢ INIT C' (Cs,True) ← e : T" by auto (metis Nil_tl list.set_sel(2))+
  then show ?case by(rule_tac x = T in exI) simp
next
  case RedInitError then show ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_NoClassDefFoundError
      simp: sconf_def hconf_def)
next
  case (InitObjectRed sh C sfs sh' C' Cs e h l b)
  then have sh: "sh ⊴⇩s sh(Object ↦ (sfs, Processing))" by(simp add: shext_def)
  have "P,E,h,sh' ⊢ INIT C' (C # Cs,True) ← e : T"
    using InitObjectRed WTrt_shext_mono[OF _ sh] by auto
  then show ?case by(rule_tac x = T in exI) (simp add: fun_upd_def)
next
  case (InitNonObjectSuperRed sh C sfs D fs ms sh' C' Cs e h l b)
  then have sh: "sh ⊴⇩s sh(C ↦ (sfs, Processing))" by(simp add: shext_def)
  then have cd: "is_class P D" using InitNonObjectSuperRed class_wf wf wf_cdecl_supD by blast
  have sup': "supercls_lst P (C # Cs)" using InitNonObjectSuperRed.prems(3) by auto
  then have sup: "supercls_lst P (D # C # Cs)"
    using supercls_lst_app[of P C Cs D] subcls1I[OF InitNonObjectSuperRed.hyps(3,2)] by auto
  have "distinct (C # Cs)" using InitNonObjectSuperRed.prems(3) by auto
  then have dist: "distinct (D # C # Cs)"
    using wf_supercls_distinct_app[OF wf InitNonObjectSuperRed.hyps(2-3) sup'] by simp
  have "P,E,h,sh' ⊢ INIT C' (D # C # Cs,False) ← e : T"
    using InitNonObjectSuperRed WTrt_shext_mono[OF _ sh] cd sup dist by auto
  then show ?case by(rule_tac x = T in exI) simp
next
  case (RedInitRInit C' C Cs e' h l sh b E T)
  then obtain a sfs where C: "class P C = ⌊a⌋" and proc: "sh C = ⌊(sfs, Processing)⌋"
    using WTrtInit by(auto simp: is_class_def)
  then have T': "P,E,h,sh ⊢ C∙⇩sclinit([]) : Void" using wf_types_clinit[OF wf C] by simp
  have "P,E,h,sh ⊢ RI (C,C∙⇩sclinit([])) ; Cs ← e' : T"
    using RedInitRInit by(auto intro: T')
  then show ?case by(rule_tac x = T in exI) simp
next
  case (RInitRed e h l sh b e' h' l' sh' b' C Cs e⇩0 E T)
  then have "(⋀E T. P,E ⊢ (h, l, sh) √ ⟹ P,E,h,sh ⊢ e : T ⟹ ∃T'. P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ T)"
    by auto
  then have "∃T'. P,E,h',sh' ⊢ e' : T'" using RInitRed by blast
  then obtain T' where e': "P,E,h',sh' ⊢ e' : T'" by auto
  have wt⇩0: "P,E,h',sh' ⊢ e⇩0 : T"
   using RInitRed by simp (auto intro: WTrt_hext_shext_mono[OF _ red_hext_incr red_shext_incr])
  have nip: "∀C' ∈ set (C#Cs). not_init C' e' ∧ (∃sfs. sh' C' = ⌊(sfs, Processing)⌋)"
   using RInitRed red_proc_pres[OF wf_prog_wwf_prog[OF wf]] by auto
  have shC: "∃sfs. sh' C = ⌊(sfs, Processing)⌋ ∨ sh' C = ⌊(sfs, Error)⌋ ∧ e' = THROW NoClassDefFoundError"
    using RInitRed red_proc_pres[OF wf_prog_wwf_prog[OF wf] RInitRed.hyps(1)] by blast
  have "P,E,h',sh' ⊢ RI (C,e') ; Cs ← e⇩0 : T" using RInitRed e' wt⇩0 nip shC by auto
  then show ?case by(rule_tac x = T in exI) simp
next
  case (RedRInit sh C sfs i sh' C' Cs v e h l b)
  then have sh: "sh ⊴⇩s sh(C ↦ (sfs, Done))" by(auto simp: shext_def)
  have wt: "P,E,h,sh(C ↦ (sfs, Done)) ⊢ e : T"
    using RedRInit WTrt_shext_mono[OF _ sh] by auto
  have shC: "∀C' ∈ set(tl Cs). ∃sfs. sh C' = ⌊(sfs, Processing)⌋" using RedRInit by(cases Cs, auto)
  have "P,E,h,sh' ⊢ INIT C' (Cs,True) ← e : T" using RedRInit wt shC by(cases Cs, auto)
  then show ?case by(rule_tac x = T in exI) simp
next
  case (SCallThrowParams es vs e es' C M h l sh b)
    then show ?case using map_Val_nthrow_neq[of _ vs e es'] by fastforce
next
  case (RInitInitThrow sh C sfs i sh' a D Cs e h l b)
  then have sh: "sh ⊴⇩s sh(C ↦ (sfs, Error))" by(auto simp: shext_def)
  have wt: "P,E,h,sh(C ↦ (sfs, Error)) ⊢ e : T"
   using RInitInitThrow WTrt_shext_mono[OF _ sh] by clarsimp
  then have "P,E,h,sh' ⊢ RI (D,Throw a) ; Cs ← e : T" using RInitInitThrow by auto
  then show ?case by(rule_tac x = T in exI) simp
qed fastforce+ (* esp all Throw propagation rules except RInitInit are dealt with here *)
(*>*)


corollary subject_reduction:
  "⟦ wf_J_prog P; P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩; P,E ⊢ s √; iconf (shp s) e; P,E,hp s,shp s ⊢ e:T ⟧
  ⟹ ∃T'. P,E,hp s',shp s' ⊢ e':T' ∧ P ⊢ T' ≤ T"
(*<*)by(cases s, cases s', fastforce dest:subject_reduction2)(*>*)

corollary subjects_reduction:
  "⟦ wf_J_prog P; P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩; P,E ⊢ s √; iconfs (shp s) es; P,E,hp s,shp s ⊢ es[:]Ts ⟧
  ⟹ ∃Ts'. P,E,hp s',shp s' ⊢ es'[:]Ts' ∧ P ⊢ Ts' [≤] Ts"
(*<*)by(cases s, cases s', fastforce dest:subjects_reduction2)(*>*)


subsection ‹ Lifting to @{text"→*"} ›

text‹ Now all these preservation lemmas are first lifted to the transitive
closure \dots ›

lemma Red_preserves_sconf:
assumes wf: "wf_J_prog P" and Red: "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
shows "⋀T. ⟦ P,E,hp s,shp s ⊢ e : T; iconf (shp s) e; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct3)
  case refl show ?case by fact
next
  case (step e s b e' s' b')
  obtain h l sh h' l' sh' where s:"s = (h,l,sh)" and s':"s' = (h',l',sh')"
    by(cases s, cases s')
  then have "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩" using step.hyps(1) by simp
  then have iconf': "iconf (shp s') e'" using red_preserves_iconf[OF wf_prog_wwf_prog[OF wf]]
    step.prems(2) s s' by simp
  thus ?case using step
    by(blast intro:red_preserves_sconf dest: subject_reduction[OF wf])
qed
(*>*)

lemma Red_preserves_iconf:
assumes wf: "wwf_J_prog P" and Red: "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
shows "iconf (shp s) e ⟹ iconf (shp s') e'"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct3)
  case refl show ?case by fact
next
  case (step e s b e' s' b')
  thus ?case using wf step by(cases s, cases s', simp) (blast intro:red_preserves_iconf)
qed
(*>*)

lemma Reds_preserves_iconf:
assumes wf: "wwf_J_prog P" and Red: "P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',b'⟩"
shows "iconfs (shp s) es ⟹ iconfs (shp s') es'"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct3)
  case refl show ?case by fact
next
  case (step e s b e' s' b')
  thus ?case using wf step by(cases s, cases s', simp) (blast intro:reds_preserves_iconf)
qed
(*>*)

lemma Red_preserves_bconf:
assumes wf: "wwf_J_prog P" and Red: "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
shows "iconf (shp s) e ⟹ P,(shp s) ⊢⇩b (e,b) √ ⟹ P,(shp s') ⊢⇩b (e'::expr,b') √"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct3)
  case refl show ?case by fact
next
  case (step e s1 b e' s2 b')
  then have "iconf (shp s2) e'" using step red_preserves_iconf[OF wf]
   by(cases s1, cases s2) auto
  thus ?case using step by(cases s1, cases s2, simp) (blast intro:red_preserves_bconf)
qed
(*>*)

lemma Reds_preserves_bconf:
assumes wf: "wwf_J_prog P" and Red: "P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',b'⟩"
shows "iconfs (shp s) es ⟹ P,(shp s) ⊢⇩b (es,b) √ ⟹ P,(shp s') ⊢⇩b (es'::expr list,b') √"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct3)
  case refl show ?case by fact
next
  case (step es s1 b es' s2 b')
  then have "iconfs (shp s2) es'" using step reds_preserves_iconf[OF wf]
   by(cases s1, cases s2) auto
  thus ?case using step by(cases s1, cases s2, simp) (blast intro:reds_preserves_bconf)
qed
(*>*)

lemma Red_preserves_defass:
assumes wf: "wf_J_prog P" and reds: "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
shows "𝒟 e ⌊dom(lcl s)⌋ ⟹ 𝒟 e' ⌊dom(lcl s')⌋"
using reds
proof (induct rule:converse_rtrancl_induct3)
  case refl thus ?case .
next
  case (step e s b e' s' b') thus ?case
    by(cases s,cases s')(auto dest:red_preserves_defass[OF wf])
qed


lemma Red_preserves_type:
assumes wf: "wf_J_prog P" and Red: "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
shows "!!T. ⟦ P,E ⊢ s√; iconf (shp s) e; P,E,hp s,shp s ⊢ e:T ⟧
    ⟹ ∃T'. P ⊢ T' ≤ T ∧ P,E,hp s',shp s' ⊢ e':T'"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct3)
  case refl thus ?case by blast
next
  case step thus ?case
    by(blast intro:widen_trans red_preserves_sconf Red_preserves_iconf[OF wf_prog_wwf_prog[OF wf]]
             dest:subject_reduction[OF wf])
qed
(*>*)


subsection "The final polish"

text‹ The above preservation lemmas are now combined and packed nicely. ›

definition wf_config :: "J_prog ⇒ env ⇒ state ⇒ expr ⇒ ty ⇒ bool"   ("_,_,_ ⊢ _ : _ √"   [51,0,0,0,0]50)
where
  "P,E,s ⊢ e:T √  ≡  P,E ⊢ s √ ∧ iconf (shp s) e ∧ P,E,hp s,shp s ⊢ e:T"

theorem Subject_reduction: assumes wf: "wf_J_prog P"
shows "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹ P,E,s ⊢ e : T √
       ⟹ ∃T'. P,E,s' ⊢ e' : T' √ ∧ P ⊢ T' ≤ T"
(*<*)
by(cases s, cases s')
  (force simp: wf_config_def
         elim:red_preserves_sconf red_preserves_iconf[OF wf_prog_wwf_prog[OF wf]]
         dest:subject_reduction[OF wf])
(*>*)


theorem Subject_reductions:
assumes wf: "wf_J_prog P" and reds: "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
shows "⋀T. P,E,s ⊢ e:T √ ⟹ ∃T'. P,E,s' ⊢ e':T' √ ∧ P ⊢ T' ≤ T"
(*<*)
using reds
proof (induct rule:converse_rtrancl_induct3)
  case refl thus ?case by blast
next
  case step thus ?case
    by(blast dest:Subject_reduction[OF wf] intro:widen_trans)
qed
(*>*)


corollary Progress: assumes wf: "wf_J_prog P"
shows "⟦ P,E,s  ⊢ e : T √; 𝒟 e ⌊dom(lcl s)⌋; P,shp s ⊢⇩b (e,b) √; ¬ final e ⟧
   ⟹ ∃e' s' b'. P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩"
(*<*)
using progress[OF wf_prog_wwf_prog[OF wf]]
by(cases b) (auto simp:wf_config_def sconf_def)
(*>*)

corollary TypeSafety:
fixes s::state and e::expr
assumes wf: "wf_J_prog P" and sconf: "P,E ⊢ s √" and wt: "P,E ⊢ e::T"
  and 𝒟: "𝒟 e ⌊dom(lcl s)⌋"
  and iconf: "iconf (shp s) e" and bconf: "P,(shp s) ⊢⇩b (e,b) √"
  and steps: "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
  and nstep: "¬(∃e'' s'' b''. P ⊢ ⟨e',s',b'⟩ → ⟨e'',s'',b''⟩)"
shows "(∃v. e' = Val v ∧ P,hp s' ⊢ v :≤ T) ∨
      (∃a. e' = Throw a ∧ a ∈ dom(hp s'))"
(*<*)
proof -
  have wwf: "wwf_J_prog P" by(rule wf_prog_wwf_prog[OF wf])
  have wfc: "P,E,s ⊢ e:T √" using WT_implies_WTrt[OF wt] sconf iconf
    by(simp add:wf_config_def)
  obtain T' where wfc': "P,E,s' ⊢ e' : T' √" and T': "P ⊢ T' ≤ T"
    using Subject_reductions[OF wf steps wfc] by clarsimp
  have 𝒟': "𝒟 e' ⌊dom (lcl s')⌋"
    by(rule Red_preserves_defass[OF wf steps 𝒟])
  have bconf': "P,(shp s') ⊢⇩b (e',b') √"
    by(rule Red_preserves_bconf[OF wwf steps iconf bconf])
  have fin': "final e'" using Progress[OF wf wfc' 𝒟' bconf'] nstep by blast
  then show ?thesis using wfc wfc' T'
    by(fastforce simp:wf_config_def final_def conf_def)
qed
(*>*)


end