(* 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∙⇩_{s}clinit([]) : 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∙⇩_{s}F{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∙⇩_{s}F{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∙⇩_{s}F{D} := e)" and wt: "P,E,h,sh ⊢ C∙⇩_{s}F{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∙⇩_{s}F{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∙⇩_{s}F{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∙⇩_{s}M(es))" and wt: "P,E,h,sh ⊢ C∙⇩_{s}M(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∙⇩_{s}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" 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∙⇩_{s}F(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∙⇩_{s}clinit([]) : Void" using wf_types_clinit[OF wf C] by simp have "P,E,h,sh ⊢ RI (C,C∙⇩_{s}clinit(<