Theory TypeSafe

(*  Title:      Jinja/J/SmallTypeSafe.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Type Safety Proof›

theory TypeSafe
imports Progress JWellForm
begin

subsection‹Basic preservation lemmas›

text‹First two easy preservation lemmas.›

theorem red_preserves_hconf:
  "P ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ (⋀T E. ⟦ P,E,h ⊢ e : T; P ⊢ h √ ⟧ ⟹ P ⊢ h' √)"
and reds_preserves_hconf:
  "P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ (⋀Ts E. ⟦ P,E,h ⊢ es [:] Ts; P ⊢ h √ ⟧ ⟹ P ⊢ h' √)"
(*<*)
proof (induct rule:red_reds_inducts)
  case (RedNew h a C FDTs h' l)
  have new: "new_Addr h = Some a" and fields: "P ⊢ C has_fields FDTs"
   and h': "h' = h(a↦(C, init_fields FDTs))"
   and hconf: "P ⊢ h √" by fact+
  from new have None: "h a = None" by(rule new_Addr_SomeD)
  moreover have "P,h ⊢ (C,init_fields FDTs) √"
    using fields by(rule oconf_init_fields)
  ultimately show "P ⊢ h' √" using h' by(fast intro: hconf_new[OF hconf])
next
  case (RedFAss h a C fs F D v l)
  let ?fs' = "fs((F,D)↦v)"
  have hconf: "P ⊢ h √" and ha: "h a = Some(C,fs)"
   and wt: "P,E,h ⊢ 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: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
(*>*)


theorem red_preserves_lconf:
  "P ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹
  (⋀T E. ⟦ P,E,h ⊢ e:T; P,h ⊢ l (:≤) E ⟧ ⟹ P,h' ⊢ l' (:≤) E)"
and reds_preserves_lconf:
  "P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹
  (⋀Ts E. ⟦ P,E,h ⊢ 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 e' h' l' v' T T')
  have red: "P ⊢ ⟨e, (h, l(V↦v))⟩ → ⟨e',(h', l')⟩"
   and IH: "⋀T E . ⟦ P,E,h ⊢ 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 ⊢ {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 e' h' l' T T')
  have red: "P ⊢ ⟨e,(h, l(V := None))⟩ → ⟨e',(h', l')⟩"
   and IH: "⋀E T. ⟦ P,E,h ⊢ e : T; P,h ⊢ l(V:=None) (:≤) E ⟧
                   ⟹ P,h' ⊢ l' (:≤) E"
   and lconf: "P,h ⊢ l (:≤) E" and wt: "P,E,h ⊢ {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 e' h' l' v T T')
  have red: "P ⊢ ⟨e,(h, l(V := None))⟩ → ⟨e',(h', l')⟩"
   and IH: "⋀E T. ⟦P,E,h ⊢ e : T; P,h ⊢ l(V:=None) (:≤) E⟧
                   ⟹ P,h' ⊢ l' (:≤) E"
   and lconf: "P,h ⊢ l (:≤) E" and wt: "P,E,h ⊢ {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
(*>*)


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)⟩ → ⟨e',(h',l')⟩ ⟹ ⌊dom l⌋ ⊔ 𝒜 e ⊑  ⌊dom l'⌋ ⊔ 𝒜 e'"
and reds_lA_incr: "P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ ⌊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)⟩ → ⟨e',(h',l')⟩ ⟹ 𝒟 e ⌊dom l⌋ ⟹ 𝒟 e' ⌊dom l'⌋"
and "P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ 𝒟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 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')
qed (auto simp:hyperset_defs)
(*>*)


text‹Combining conformance of heap and local variables:›

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

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

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


subsection "Subject reduction"

lemma wt_blocks:
 "⋀E. ⟦ length Vs = length Ts; length vs = length Ts ⟧ ⟹
       (P,E,h ⊢ blocks(Vs,Ts,vs,e) : T) =
       (P,E(Vs[↦]Ts),h ⊢ 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)⟩ → ⟨e',(h',l')⟩ ⟹
  (⋀E T. ⟦ P,E ⊢ (h,l) √; P,E,h ⊢ e:T ⟧
           ⟹ ∃T'. P,E,h' ⊢ e':T' ∧ P ⊢ T' ≤ T)"
and subjects_reduction2: "P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹
  (⋀E Ts. ⟦ P,E ⊢ (h,l) √; P,E,h ⊢ es [:] Ts ⟧
            ⟹ ∃Ts'. P,E,h' ⊢ es' [:] Ts' ∧ P ⊢ Ts' [≤] Ts)"
(*<*)
proof (induct rule:red_reds_inducts)
  case (RedCall h l a C fs M Ts T pns body D vs E T')
  have hp: "hp(h,l) a = Some(C,fs)"
   and "method": "P ⊢ C sees M: Ts→T = (pns,body) in D"
   and wt: "P,E,h ⊢ addr a∙M(map Val vs) : T'" by fact+
  obtain Ts' where wtes: "P,E,h ⊢ 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 ⊢ body : T''"
    by(rule WT_implies_WTrt)
  hence "P,E(this#pns [↦] Class D#Ts),h ⊢ body : T''"
    by(rule WTrt_env_mono) simp
  hence "P,E,h ⊢ 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 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 e⇩1' h' l' bop e⇩2)
  have red: "P ⊢ ⟨e⇩1,(h,l)⟩ → ⟨e⇩1',(h',l')⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e⇩1:T⟧
                 ⟹ ∃U. P,E,h' ⊢ e⇩1' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ e⇩1 «bop» e⇩2 : T" by fact+
  have "P,E,h' ⊢ 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 ⊢ e⇩1 : T⇩1" and wt⇩2: "P,E,h ⊢ e⇩2 : T⇩2" by auto
    show ?thesis
      using WTrt_hext_mono[OF wt⇩2 red_hext_incr[OF red]] IH[OF conf wt⇩1]
      by auto
  next
    assume  [simp]: "bop = Add"
    from wt have [simp]: "T = Integer"
      and wt⇩1: "P,E,h ⊢ e⇩1 : Integer" and wt⇩2: "P,E,h ⊢ e⇩2 : Integer"
      by auto
    show ?thesis
      using IH[OF conf wt⇩1] WTrt_hext_mono[OF wt⇩2 red_hext_incr[OF red]]
      by auto
  qed
  thus ?case by auto
next
  case (BinOpRed2 e⇩2 h l e⇩2' h' l' v⇩1 bop)
  have red: "P ⊢ ⟨e⇩2,(h,l)⟩ → ⟨e⇩2',(h',l')⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e⇩2:T⟧
                 ⟹ ∃U. P,E,h' ⊢ e⇩2' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ (Val v⇩1) «bop» e⇩2 : T" by fact+
  have "P,E,h' ⊢ (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 ⊢ Val v⇩1 : T⇩1" and wt⇩2: "P,E,h ⊢ e⇩2:T⇩2" by auto
    show ?thesis
      using IH[OF conf 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 ⊢ Val v⇩1 : Integer" and wt⇩2: "P,E,h ⊢ e⇩2 : Integer"
      by auto
    show ?thesis
      using IH[OF conf 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 thus ?case by(blast intro:widen_trans)
next
  case (FAccRed e h l e' h' l' F D)
  have IH: "⋀E T. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T⟧
                 ⟹ ∃U. P,E,h' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ e∙F{D} : T" by fact+
  ― ‹The goal: ?case = @{prop ?case}›
  ― ‹Now distinguish the two cases how wt can have arisen.›
  { fix C assume wte: "P,E,h ⊢ e : Class C"
             and has: "P ⊢ C has F:T in D"
    from IH[OF conf wte]
    obtain U where wte': "P,E,h' ⊢ 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 ⊢ e : NT"
    hence "P,E,h' ⊢ e' : NT" using IH[OF conf] 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 (FAssRed1 e h l e' h' l' F D e⇩2)
  have red: "P ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T⟧
                 ⟹ ∃U. P,E,h' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ e∙F{D}:=e⇩2 : T" by fact+
  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 "P,E,h ⊢ e : NT"
    hence "P,E,h' ⊢ e' : NT" using IH[OF conf] by fastforce
    moreover obtain T⇩2 where "P,E,h ⊢ e⇩2 : T⇩2" using wt by auto
    from this red_hext_incr[OF red] have  "P,E,h' ⊢ e⇩2 : T⇩2"
      by(rule WTrt_hext_mono)
    ultimately have ?case using void by(blast intro!:WTrtFAssNT)
  }
  moreover
  { fix C TF T⇩2 assume wt⇩1: "P,E,h ⊢ e : Class C" and wt⇩2: "P,E,h ⊢ e⇩2 : T⇩2"
    and has: "P ⊢ C has F:TF in D" and sub: "P ⊢ T⇩2 ≤ TF"
    obtain U where wt⇩1': "P,E,h' ⊢ e' : U" and UsubC: "P ⊢ U ≤ Class C"
      using IH[OF conf wt⇩1] by blast
    have wt⇩2': "P,E,h' ⊢ 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?›
    { 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' ⊢ e' : Class C'" using wt⇩1' UClass by auto
      moreover have "P ⊢ C' has F: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 e⇩2' h' l' v F D)
  have red: "P ⊢ ⟨e⇩2,(h,l)⟩ → ⟨e⇩2',(h',l')⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e⇩2 : T⟧
                 ⟹ ∃U. P,E,h' ⊢ e⇩2' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ Val v∙F{D}:=e⇩2 : T" by fact+
  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 ⊢ Val v : Class C"
      and has: "P ⊢ C has F:TF in D"
      and wt⇩2: "P,E,h ⊢ e⇩2 : T⇩2" and TsubTF: "P ⊢ T⇩2 ≤ TF"
    have wt⇩1': "P,E,h' ⊢ Val v : Class C"
      by(rule WTrt_hext_mono[OF wt⇩1 red_hext_incr[OF red]])
    obtain T⇩2' where wt⇩2': "P,E,h' ⊢ e⇩2' : T⇩2'" and T'subT: "P ⊢ T⇩2' ≤ T⇩2"
      using IH[OF conf wt⇩2] by blast
    have "P,E,h' ⊢ 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 ⊢ Val v : NT" and wt⇩2: "P,E,h ⊢ e⇩2 : T⇩2"
    from null have "v = Null" by simp
    moreover
    obtain T⇩2' where "P,E,h' ⊢ e⇩2' : T⇩2' ∧ P ⊢ T⇩2' ≤ T⇩2"
      using IH[OF conf 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 (CallObj e h l e' h' l' M es)
  have red: "P ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T⟧
                 ⟹ ∃U. P,E,h' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and conf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ e∙M(es) : T" by fact+
  ― ‹We distinguish if @{term e} has type @{term NT} or a Class type›
  ― ‹Remember ?case = @{term ?case}›
  { assume "P,E,h ⊢ e:NT"
    hence "P,E,h' ⊢ e' : NT" using IH[OF conf] by fastforce
    moreover
    fix Ts assume wtes: "P,E,h ⊢ es [:] Ts"
    have "P,E,h' ⊢ es [:] Ts"
      by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
    ultimately have ?case by(blast intro!:WTrtCallNT) }
  moreover
  { fix C D Ts Us pns body
    assume wte: "P,E,h ⊢ e : Class C"
      and "method": "P ⊢ C sees M:Ts→T = (pns,body) in D"
      and wtes: "P,E,h ⊢ es [:] Us" and subs: "P ⊢ Us [≤] Ts"
    obtain U where wte': "P,E,h' ⊢ e' : U" and UsubC: "P ⊢ U ≤ Class C"
      using IH[OF conf wte] by blast
    ― ‹Is @{term U} the null type or a class type?›
    { assume "U = NT"
      moreover have "P,E,h' ⊢ es [:] Us"
        by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
      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' ⊢ e' : Class C'" using wte' UClass by auto
      moreover obtain Ts' T' pns' body' D'
        where method': "P ⊢ C' sees M: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' ⊢ es [:] Us"
        by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
      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 es' h' l' v M)
  have reds: "P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩"
   and IH: "⋀E Ts. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ es [:] Ts⟧
                 ⟹ ∃Us. P,E,h' ⊢ es' [:] Us ∧ P ⊢ Us [≤] Ts"
   and conf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ Val v∙M(es) : T" by fact+
  from wt show ?case
  proof (rule WTrt_elim_cases)
    fix C D Ts Us pns body
    assume wte: "P,E,h ⊢ Val v : Class C"
      and "P ⊢ C sees M:Ts→T = (pns,body) in D"
      and wtes: "P,E,h ⊢ es [:] Us" and "P ⊢ Us [≤] Ts"
    moreover have "P,E,h' ⊢ Val v : Class C"
      by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]])
    moreover
    obtain Us' where "P,E,h' ⊢ es' [:] Us' ∧ P ⊢ Us' [≤] Us"
      using IH[OF conf wtes] by blast
    ultimately show ?thesis by(blast intro:WTrtCall widens_trans)
  next
    fix Us
    assume null: "P,E,h ⊢ Val v : NT" and wtes: "P,E,h ⊢ es [:] Us"
    from null have "v = Null" by simp
    moreover
    obtain Us' where "P,E,h' ⊢ es' [:] Us' ∧ P ⊢ Us' [≤] Us"
      using IH[OF conf wtes] by blast
    ultimately show ?thesis by(fastforce intro:WTrtCallNT)
  qed
next
  case RedCallNull thus ?case
    by(fastforce intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp: sconf_def hconf_def)
next
  case (InitBlockRed e h l V v e' h' l' v' T E T')
  have red: "P ⊢ ⟨e, (h,l(V↦v))⟩ → ⟨e',(h',l')⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l(V↦v)) √; P,E,h ⊢ e : T⟧
                    ⟹ ∃U. P,E,h' ⊢ e' : U ∧ P ⊢ U ≤ T"
   and v': "l' V = Some v'" and conf: "P,E ⊢ (h,l) √"
   and wt: "P,E,h ⊢ {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 ⊢ 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 lconf⇩2 wt⇩2 show ?case by (fastforce simp add:sconf_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 e' h' l' v T E Te)
  have red: "P ⊢ ⟨e,(h,l(V:=None))⟩ → ⟨e',(h',l')⟩"
   and IH: "⋀E T. ⟦P,E ⊢ (h,l(V:=None)) √; P,E,h ⊢ e : T⟧
                   ⟹ ∃T'. P,E,h' ⊢ e' : T' ∧ P ⊢ T' ≤ T"
   and Some: "l' V = Some v" and conf: "P,E ⊢ (h,l) √"
   and wt: "P,E,h ⊢ {V:T; e} : Te" by fact+
  obtain Te' where IH': "P,E(V↦T),h' ⊢ e' : Te' ∧ P ⊢ Te' ≤ Te"
    using IH conf 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 SeqRed thus ?case
    by auto (blast dest:WTrt_hext_mono[OF _ red_hext_incr])
next
  case CondRed thus ?case
    by auto (blast intro:WTrt_hext_mono[OF _ red_hext_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_mono[OF _ red_hext_incr])
next
  case RedTryFail thus ?case
    by(fastforce intro: WTrtThrow[OF WTrtVal] simp:sconf_def hconf_def)
next
  case ListRed1 thus ?case
    by(fastforce dest: WTrts_hext_mono[OF _ red_hext_incr])
next
  case ListRed2 thus ?case
    by(fastforce dest: hext_typeof_mono[OF reds_hext_incr])
qed fastforce+ (* esp all Throw propagation rules are dealt with here *)
(*>*)


corollary subject_reduction:
  "⟦ wf_J_prog P; P ⊢ ⟨e,s⟩ → ⟨e',s'⟩; P,E ⊢ s √; P,E,hp s ⊢ e:T ⟧
  ⟹ ∃T'. P,E,hp 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⟩ [→] ⟨es',s'⟩; P,E ⊢ s √; P,E,hp s ⊢ es[:]Ts ⟧
  ⟹ ∃Ts'. P,E,hp s' ⊢ es'[:]Ts' ∧ P ⊢ Ts' [≤] Ts"
(*<*)by(cases s, cases s', fastforce dest:subjects_reduction2)(*>*)


subsection ‹Lifting to ‹→*››

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⟩ →* ⟨e',s'⟩"
shows "⋀T. ⟦ P,E,hp s ⊢ e : T; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct2)
  case refl show ?case by fact
next
  case step thus ?case
    by(blast intro:red_preserves_sconf dest: subject_reduction[OF wf])
qed
(*>*)


lemma Red_preserves_defass:
assumes wf: "wf_J_prog P" and reds: "P ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
shows "𝒟 e ⌊dom(lcl s)⌋ ⟹ 𝒟 e' ⌊dom(lcl s')⌋"
using reds
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case .
next
  case (step e s e' s') 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⟩ →* ⟨e',s'⟩"
shows "!!T. ⟦ P,E ⊢ s√; P,E,hp s ⊢ e:T ⟧
    ⟹ ∃T'. P ⊢ T' ≤ T ∧ P,E,hp s' ⊢ e':T'"
(*<*)
using Red
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case by blast
next
  case step thus ?case
    by(blast intro:widen_trans red_preserves_sconf
             dest:subject_reduction[OF wf])
qed
(*>*)


subsection ‹Lifting to ‹⇒››

text‹\dots and now to the big step semantics, just for fun.›

lemma eval_preserves_sconf:
  "⟦ wf_J_prog P; P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩; P,E ⊢ e::T; P,E ⊢ s√ ⟧ ⟹ P,E ⊢ s'√"
(*<*)
by(blast intro:Red_preserves_sconf big_by_small WT_implies_WTrt wf_prog_wwf_prog)
(*>*)


lemma eval_preserves_type: assumes wf: "wf_J_prog P"
shows "⟦ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩; P,E ⊢ s√; P,E ⊢ e::T ⟧
   ⟹ ∃T'. P ⊢ T' ≤ T ∧ P,E,hp s' ⊢ e':T'"
(*<*)
by(blast dest:big_by_small[OF wf_prog_wwf_prog[OF wf]]
              WT_implies_WTrt Red_preserves_type[OF wf])
(*>*)


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 √ ∧ P,E,hp s ⊢ e:T"

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


theorem Subject_reductions:
assumes wf: "wf_J_prog P" and reds: "P ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
shows "⋀T. P,E,s ⊢ e:T √ ⟹ ∃T'. P,E,s' ⊢ e':T' √ ∧ P ⊢ T' ≤ T"
(*<*)
using reds
proof (induct rule:converse_rtrancl_induct2)
  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)⌋; ¬ final e ⟧ ⟹ ∃e' s'. P ⊢ ⟨e,s⟩ → ⟨e',s'⟩"
(*<*)
using progress[OF wf_prog_wwf_prog[OF wf]]
by(auto simp:wf_config_def sconf_def)
(*>*)


corollary TypeSafety:
fixes s::state
assumes wf: "wf_J_prog P" and sconf: "P,E ⊢ s √" and wt: "P,E ⊢ e::T"
  and 𝒟: "𝒟 e ⌊dom(lcl s)⌋"
  and steps: "P ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
  and nstep: "¬(∃e'' s''. P ⊢ ⟨e',s'⟩ → ⟨e'',s''⟩)"
shows "(∃v. e' = Val v ∧ P,hp s' ⊢ v :≤ T) ∨
      (∃a. e' = Throw a ∧ a ∈ dom(hp s'))"
(*<*)
proof -
  have wfc: "P,E,s ⊢ e:T √" using WT_implies_WTrt[OF wt] sconf
    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 fin': "final e'" using Progress[OF wf wfc' 𝒟'] nstep by blast
  then show ?thesis using wfc wfc' T'
    by(fastforce simp:wf_config_def final_def conf_def)
qed
(*>*)


end