# Theory TypeSafe

```(*  Title:      Jinja/J/SmallTypeSafe.thy

Author:     Tobias Nipkow
*)

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)
(*>*)

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
(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)
(*>*)

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
(*>*)

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
(*>*)

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
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
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
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
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"
(*<*)
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