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