(* Title: CoreC++ Author: Daniel Wasserrab Maintainer: Daniel Wasserrab <wasserra at fmi.uni-passau.de> Based on the Jinja theory J/TypeSafe.thy by Tobias Nipkow *) section ‹Type Safety Proof› theory TypeSafe imports HeapExtension CWellForm begin subsection‹Basic preservation lemmas› lemma assumes wf:"wwf_prog P" and casts:"P ⊢ T casts v to v'" and typeof:"P ⊢ typeof⇘h⇙ v = Some T'" and leq:"P ⊢ T' ≤ T" shows casts_conf:"P,h ⊢ v' :≤ T" proof - { fix a' C Cs S' assume leq:"P ⊢ Class (last Cs) ≤ T" and subo:"Subobjs P C Cs" and casts':"P ⊢ T casts Ref (a',Cs) to v'" and h:"h a' = Some(C,S')" from subo wf have "is_class P (last Cs)" by(fastforce intro:Subobj_last_isClass) with leq wf obtain C' where T:"T = Class C'" and path_unique:"P ⊢ Path (last Cs) to C' unique" by(auto dest:Class_widen) from path_unique obtain Cs' where path_via:"P ⊢ Path (last Cs) to C' via Cs'" by(auto simp:path_via_def path_unique_def) with T path_unique casts' have v':"v' = Ref (a',Cs@⇩_{p}Cs')" by -(erule casts_to.cases,auto simp:path_unique_def path_via_def) from subo path_via wf have "Subobjs P C (Cs@⇩_{p}Cs')" and "last (Cs@⇩_{p}Cs') = C'" apply(auto intro:Subobjs_appendPath simp:path_via_def) apply(drule_tac Cs="Cs'" in Subobjs_nonempty) by(rule sym[OF appendPath_last]) with T h v' have ?thesis by auto } with casts typeof wf typeof leq show ?thesis by(cases v,auto elim:casts_to.cases split:if_split_asm) qed theorem assumes wf:"wwf_prog P" shows red_preserves_hconf: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ (⋀T. ⟦ P,E,h ⊢ e : T; P ⊢ h √ ⟧ ⟹ P ⊢ h' √)" and reds_preserves_hconf: "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ (⋀Ts. ⟦ P,E,h ⊢ es [:] Ts; P ⊢ h √ ⟧ ⟹ P ⊢ h' √)" proof (induct rule:red_reds_inducts) case (RedNew h a h' C E l) have new: "new_Addr h = Some a" and h':"h' = h(a ↦ (C, Collect (init_obj P C)))" and hconf:"P ⊢ h √" and wt_New:"P,E,h ⊢ new C : T" by fact+ from new have None: "h a = None" by(rule new_Addr_SomeD) with wf have oconf:"P,h ⊢ (C, Collect (init_obj P C)) √" apply (auto simp:oconf_def) apply (rule_tac x="init_class_fieldmap P (last Cs)" in exI) by (fastforce intro:init_obj.intros fconf_init_fields elim: init_obj.cases dest!:Subobj_last_isClass simp:is_class_def)+ thus ?case using h' None by(fast intro: hconf_new[OF hconf]) next case (RedFAss h a D S Cs' F T Cs v v' Ds fs' E l T') let ?fs' = "fs'(F ↦ v')" let ?S' = "insert (Ds, ?fs') (S - {(Ds, fs')})" have ha:"h a = Some(D,S)" and hconf:"P ⊢ h √" and field:"P ⊢ last Cs' has least F:T via Cs" and casts:"P ⊢ T casts v to v'" and Ds:"Ds = Cs' @⇩_{p}Cs" and S:"(Ds,fs') ∈ S" and wte:"P,E,h ⊢ ref(a,Cs')∙F{Cs} := Val v : T'" by fact+ from wte have "P ⊢ last Cs' has least F:T' via Cs" by (auto split:if_split_asm) with field have eq:"T = T'" by (rule sees_field_fun) with casts wte wf have conf:"P,h ⊢ v' :≤ T'" by(auto intro:casts_conf) from hconf ha have oconf:"P,h ⊢ (D,S) √" by (fastforce simp:hconf_def) with S have suboD:"Subobjs P D Ds" by (fastforce simp:oconf_def) from field obtain Bs fs ms where subo:"Subobjs P (last Cs') Cs" and "class": "class P (last Cs) = Some(Bs,fs,ms)" and map:"map_of fs F = Some T" by (auto simp:LeastFieldDecl_def FieldDecls_def) from Ds subo have last:"last Cs = last Ds" by(fastforce dest:Subobjs_nonempty intro:appendPath_last simp:appendPath_last) with "class" have classDs:"class P (last Ds) = Some(Bs,fs,ms)" by simp with S suboD oconf have "P,h ⊢ fs' (:≤) map_of fs" apply (auto simp:oconf_def) apply (erule allE) apply (erule_tac x="Ds" in allE) apply (erule_tac x="fs'" in allE) apply clarsimp done with map conf eq have fconf:"P,h ⊢ fs'(F ↦ v') (:≤) map_of fs" by (simp add:fconf_def) from oconf have "∀Cs fs'. (Cs,fs') ∈ S ⟶ Subobjs P D Cs ∧ (∃fs Bs ms. class P (last Cs) = Some (Bs,fs,ms) ∧ P,h ⊢ fs' (:≤) map_of fs)" by(simp add:oconf_def) with suboD classDs fconf have oconf':"∀Cs fs'. (Cs,fs') ∈ ?S' ⟶ Subobjs P D Cs ∧ (∃fs Bs ms. class P (last Cs) = Some (Bs,fs,ms) ∧ P,h ⊢ fs' (:≤) map_of fs)" by auto from oconf have all:"∀Cs. Subobjs P D Cs ⟶ (∃!fs'. (Cs,fs') ∈ S)" by(simp add:oconf_def) with S have "∀Cs. Subobjs P D Cs ⟶ (∃!fs'. (Cs,fs') ∈ ?S')" by blast with oconf' have oconf':"P,h ⊢ (D,?S') √" by (simp add:oconf_def) with hconf ha show ?case by (rule hconf_upd_obj) next case (CallObj E e h l e' h' l' Copt M es) thus ?case by (cases Copt) auto next case (CallParams E es h l es' h' l' v Copt M) thus ?case by (cases Copt) auto next case (RedCallNull E Copt M vs h l) thus ?case by (cases Copt) auto qed auto theorem assumes wf:"wwf_prog P" shows red_preserves_lconf: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ (⋀T. ⟦ P,E,h ⊢ e:T; P,h ⊢ l (:≤)⇩_{w}E; P ⊢ E √ ⟧ ⟹ P,h' ⊢ l' (:≤)⇩_{w}E)" and reds_preserves_lconf: "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ (⋀Ts. ⟦ P,E,h ⊢ es[:]Ts; P,h ⊢ l (:≤)⇩_{w}E; P ⊢ E √ ⟧ ⟹ P,h' ⊢ l' (:≤)⇩_{w}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 E V T v v' h l T') have casts:"P ⊢ T casts v to v'" and env:"E V = Some T" and wt:"P,E,h ⊢ V:=Val v : T'" and lconf:"P,h ⊢ l (:≤)⇩_{w}E" by fact+ from wt env have eq:"T = T'" by auto with casts wt wf have conf:"P,h ⊢ v' :≤ T'" by(auto intro:casts_conf) with lconf env eq show ?case by (simp del:fun_upd_apply)(erule lconf_upd,simp_all) next case RedFAss thus ?case by(auto intro:lconf_hext red_hext_incr[OF red_reds.RedFAss] simp del:fun_upd_apply) next case (BlockRedNone E V T e h l e' h' l' T') have red:"P,E(V ↦ T) ⊢ ⟨e,(h, l(V := None))⟩ → ⟨e',(h', l')⟩" and IH: "⋀T''. ⟦ P,E(V ↦ T),h ⊢ e : T''; P,h ⊢ l(V:=None) (:≤)⇩_{w}E(V ↦ T); envconf P (E(V ↦ T)) ⟧ ⟹ P,h' ⊢ l' (:≤)⇩_{w}E(V ↦ T)" and lconf: "P,h ⊢ l (:≤)⇩_{w}E" and wte: "P,E,h ⊢ {V:T; e} : T'" and envconf:"envconf P E" by fact+ from lconf_hext[OF lconf red_hext_incr[OF red]] have lconf':"P,h' ⊢ l (:≤)⇩_{w}E" . from wte have wte':"P,E(V↦T),h ⊢ e : T'" and type:"is_type P T" by (auto elim:WTrt.cases) from envconf type have envconf':"envconf P (E(V ↦ T))" by(auto simp:envconf_def) from lconf have "P,h ⊢ (l(V := None)) (:≤)⇩_{w}E(V↦T)" by (simp add:lconf_def fun_upd_apply) from IH[OF wte' this envconf'] have "P,h' ⊢ l' (:≤)⇩_{w}E(V↦T)" . with lconf' show ?case by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm) next case (BlockRedSome E V T e h l e' h' l' v T') have red:"P,E(V ↦ T) ⊢ ⟨e,(h, l(V := None))⟩ → ⟨e',(h', l')⟩" and IH: "⋀T''. ⟦ P,E(V ↦ T),h ⊢ e : T''; P,h ⊢ l(V:=None) (:≤)⇩_{w}E(V ↦ T); envconf P (E(V ↦ T)) ⟧ ⟹ P,h' ⊢ l' (:≤)⇩_{w}E(V ↦ T)" and lconf: "P,h ⊢ l (:≤)⇩_{w}E" and wte: "P,E,h ⊢ {V:T; e} : T'" and envconf:"envconf P E" by fact+ from lconf_hext[OF lconf red_hext_incr[OF red]] have lconf':"P,h' ⊢ l (:≤)⇩_{w}E" . from wte have wte':"P,E(V↦T),h ⊢ e : T'" and type:"is_type P T" by (auto elim:WTrt.cases) from envconf type have envconf':"envconf P (E(V ↦ T))" by(auto simp:envconf_def) from lconf have "P,h ⊢ (l(V := None)) (:≤)⇩_{w}E(V↦T)" by (simp add:lconf_def fun_upd_apply) from IH[OF wte' this envconf'] have "P,h' ⊢ l' (:≤)⇩_{w}E(V↦T)" . with lconf' show ?case by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm) next case (InitBlockRed E V T e h l v' e' h' l' v'' v T') have red: "P,E(V ↦ T) ⊢ ⟨e, (h, l(V↦v'))⟩ → ⟨e',(h', l')⟩" and IH: "⋀T''. ⟦ P,E(V ↦ T),h ⊢ e : T''; P,h ⊢ l(V ↦ v') (:≤)⇩_{w}E(V ↦ T); envconf P (E(V ↦ T)) ⟧ ⟹ P,h' ⊢ l' (:≤)⇩_{w}E(V ↦ T)" and lconf:"P,h ⊢ l (:≤)⇩_{w}E" and l':"l' V = Some v''" and wte:"P,E,h ⊢ {V:T; V:=Val v;; e} : T'" and casts:"P ⊢ T casts v to v'" and envconf:"envconf P E" by fact+ from lconf_hext[OF lconf red_hext_incr[OF red]] have lconf':"P,h' ⊢ l (:≤)⇩_{w}E" . from wte obtain T'' where wte':"P,E(V↦T),h ⊢ e : T'" and wt:"P,E(V ↦ T),h ⊢ V:=Val v : T''" and type:"is_type P T" by (auto elim:WTrt.cases) from envconf type have envconf':"envconf P (E(V ↦ T))" by(auto simp:envconf_def) from wt have "T'' = T" by auto with wf casts wt have "P,h ⊢ v' :≤ T" by(auto intro:casts_conf) with lconf have "P,h ⊢ l(V ↦ v') (:≤)⇩_{w}E(V↦T)" by -(rule lconf_upd2) from IH[OF wte' this envconf'] have "P,h' ⊢ l' (:≤)⇩_{w}E(V ↦ T)" . with lconf' show ?case by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm) next case (CallObj E e h l e' h' l' Copt M es) thus ?case by (cases Copt) auto next case (CallParams E es h l es' h' l' v Copt M) thus ?case by (cases Copt) auto next case (RedCallNull E Copt M vs h l) thus ?case by (cases Copt) auto 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⌋)" apply(induct Vs Ts vs e rule:blocks_old_induct) apply(simp_all add:hyperset_defs) done lemma red_lA_incr: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ ⌊dom l⌋ ⊔ 𝒜 e ⊑ ⌊dom l'⌋ ⊔ 𝒜 e'" and reds_lA_incr: "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ ⌊dom l⌋ ⊔ 𝒜s es ⊑ ⌊dom l'⌋ ⊔ 𝒜s es'" apply (induct rule:red_reds_inducts) apply (simp_all del: fun_upd_apply add: hyperset_defs) apply blast apply blast apply blast apply blast apply blast apply blast apply blast apply auto done text‹Now preservation of definite assignment.› lemma assumes wf: "wf_C_prog P" shows red_preserves_defass: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ 𝒟 e ⌊dom l⌋ ⟹ 𝒟 e' ⌊dom l'⌋" and "P,E ⊢ ⟨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 h l a C S Cs M Ts' T' pns' body' Ds Ts T pns body Cs' vs bs new_body E) thus ?case apply (auto dest!:select_method_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono') apply(cases T') apply auto by(rule_tac A="⌊insert this (set pns)⌋" in D_mono,clarsimp simp:hyperset_defs, assumption)+ next case RedStaticCall thus ?case apply (auto dest!:has_least_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono') by(auto simp:hyperset_defs) 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 RedWhile thus ?case by(auto simp:hyperset_defs elim!:D_mono') next case ListRed1 thus ?case by (auto elim!: Ds_mono[OF red_lA_incr]) qed (auto simp:hyperset_defs) text‹Combining conformance of heap and local variables:› definition sconf :: "prog ⇒ env ⇒ state ⇒ bool" ("_,_ ⊢ _ √" [51,51,51]50) where "P,E ⊢ s √ ≡ let (h,l) = s in P ⊢ h √ ∧ P,h ⊢ l (:≤)⇩_{w}E ∧ P ⊢ E √" lemma red_preserves_sconf: "⟦ P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩; P,E,hp s ⊢ e : T; P,E ⊢ s √; wwf_prog P⟧ ⟹ P,E ⊢ s' √" by(fastforce intro:red_preserves_hconf red_preserves_lconf simp add:sconf_def) lemma reds_preserves_sconf: "⟦ P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩; P,E,hp s ⊢ es [:] Ts; P,E ⊢ s √; wwf_prog P⟧ ⟹ 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; ∀T' ∈ set Ts. is_type P T'⟧ ⟹ (P,E,h ⊢ blocks(Vs,Ts,vs,e) : T) = (P,E(Vs[↦]Ts),h ⊢ e:T ∧ (∃Ts'. map (P ⊢ typeof⇘h⇙) vs = map Some Ts' ∧ P ⊢ Ts' [≤] Ts))" proof(induct Vs Ts vs e rule:blocks_old_induct) case (5 V Vs T' Ts v vs e) have length:"length (V#Vs) = length (T'#Ts)" "length (v#vs) = length (T'#Ts)" and type:"∀S ∈ set (T'#Ts). is_type P S" and IH:"⋀E. ⟦length Vs = length Ts; length vs = length Ts; ∀S ∈ set Ts. is_type P S⟧ ⟹ (P,E,h ⊢ blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [↦] Ts),h ⊢ e : T ∧ (∃Ts'. map P ⊢ typeof⇘h⇙ vs = map Some Ts' ∧ P ⊢ Ts' [≤] Ts))" by fact+ from type have typeT':"is_type P T'" and type':"∀S ∈ set Ts. is_type P S" by simp_all from length have "length Vs = length Ts" "length vs = length Ts" by simp_all from IH[OF this type'] have eq:"(P,E(V ↦ T'),h ⊢ blocks (Vs,Ts,vs,e) : T) = (P,E(V ↦ T', Vs [↦] Ts),h ⊢ e : T ∧ (∃Ts'. map P ⊢ typeof⇘h⇙ vs = map Some Ts' ∧ P ⊢ Ts' [≤] Ts))" . show ?case proof(rule iffI) assume "P,E,h ⊢ blocks (V#Vs,T'#Ts,v#vs,e) : T" then have wt:"P,E(V ↦ T'),h ⊢ V:=Val v : T'" and blocks:"P,E(V ↦ T'),h ⊢ blocks (Vs,Ts,vs,e) : T" by auto from blocks eq obtain Ts' where wte:"P,E(V ↦ T', Vs [↦] Ts),h ⊢ e : T" and typeof:"map P ⊢ typeof⇘h⇙ vs = map Some Ts'" and subs:"P ⊢ Ts' [≤] Ts" by auto from wt obtain T'' where "P ⊢ typeof⇘h⇙ v = Some T''" and "P ⊢ T'' ≤ T'" by auto with wte typeof subs show "P,E(V # Vs [↦] T' # Ts),h ⊢ e : T ∧ (∃Ts'. map P ⊢ typeof⇘h⇙ (v # vs) = map Some Ts' ∧ P ⊢ Ts' [≤] (T' # Ts))" by auto next assume "P,E(V # Vs [↦] T' # Ts),h ⊢ e : T ∧ (∃Ts'. map P ⊢ typeof⇘h⇙ (v # vs) = map Some Ts' ∧ P ⊢ Ts' [≤] (T' # Ts))" then obtain Ts' where wte:"P,E(V # Vs [↦] T' # Ts),h ⊢ e : T" and typeof:"map P ⊢ typeof⇘h⇙ (v # vs) = map Some Ts'" and subs:"P ⊢ Ts' [≤] (T'#Ts)" by auto from subs obtain U Us where Ts':"Ts' = U#Us" by(cases Ts') auto with wte typeof subs eq have blocks:"P,E(V ↦ T'),h ⊢ blocks (Vs,Ts,vs,e) : T" by auto from Ts' typeof subs have "P ⊢ typeof⇘h⇙ v = Some U" and "P ⊢ U ≤ T'" by (auto simp:fun_of_def) hence wtval:"P,E(V ↦ T'),h ⊢ V:=Val v : T'" by auto with blocks typeT' show "P,E,h ⊢ blocks (V#Vs,T'#Ts,v#vs,e) : T" by auto qed qed auto theorem assumes wf: "wf_C_prog P" shows subject_reduction2: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ (⋀T. ⟦ P,E ⊢ (h,l) √; P,E,h ⊢ e : T ⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T)" and subjects_reduction2: "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ (⋀Ts.⟦ P,E ⊢ (h,l) √; P,E,h ⊢ es [:] Ts ⟧ ⟹ types_conf P E h' es' Ts)" proof (induct rule:red_reds_inducts) case (RedNew h a h' C E l) have new:"new_Addr h = Some a" and h':"h' = h(a ↦ (C, Collect (init_obj P C)))" and wt:"P,E,h ⊢ new C : T" by fact+ from wt have eq:"T = Class C" and "class": "is_class P C" by auto from "class" have subo:"Subobjs P C [C]" by(rule Subobjs_Base) from h' have "h' a = Some(C, Collect (init_obj P C))" by(simp add:map_upd_Some_unfold) with subo have "P,E,h' ⊢ ref(a,[C]) : Class C" by auto with eq show ?case by auto next case (RedNewFail h E C l) have sconf:"P,E ⊢ (h, l) √" by fact from wf have "is_class P OutOfMemory" by (fastforce intro:is_class_xcpt wf_prog_wwf_prog) hence "preallocated h ⟹ P ⊢ typeof⇘h⇙ (Ref (addr_of_sys_xcpt OutOfMemory,[OutOfMemory])) = Some(Class OutOfMemory)" by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base) with sconf have "P,E,h ⊢ THROW OutOfMemory : T" by(auto simp:sconf_def hconf_def) thus ?case by (fastforce intro:wt_same_type_typeconf) next case (StaticCastRed E e h l e' h' l' C) have wt:"P,E,h ⊢ ⦇C⦈e : T" and IH:"⋀T'. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" and sconf:"P,E ⊢ (h, l) √" by fact+ from wt obtain T' where wte:"P,E,h ⊢ e : T'" and isref:"is_refT T'" and "class": "is_class P C" and T:"T = Class C" by auto from isref have "P,E,h' ⊢ ⦇C⦈e' : Class C" proof(rule refTE) assume "T' = NT" with IH[OF sconf wte] isref "class" show ?thesis by auto next fix D assume "T' = Class D" with IH[OF sconf wte] isref "class" show ?thesis by auto qed with T show ?case by (fastforce intro:wt_same_type_typeconf) next case RedStaticCastNull thus ?case by (auto elim:WTrt.cases) next case (RedStaticUpCast Cs C Cs' Ds E a h l) have wt:"P,E,h ⊢ ⦇C⦈ref (a,Cs) : T" and path_via:"P ⊢ Path last Cs to C via Cs'" and Ds:"Ds = Cs @⇩_{p}Cs'" by fact+ from wt have typeof:"P ⊢ typeof⇘h⇙ (Ref(a,Cs)) = Some(Class(last Cs))" and "class": "is_class P C" and T:"T = Class C" by auto from typeof obtain D S where h:"h a = Some(D,S)" and subo:"Subobjs P D Cs" by (auto dest:typeof_Class_Subo split:if_split_asm) from path_via subo wf Ds have "Subobjs P D Ds" and last:"last Ds = C" by(auto intro!:Subobjs_appendPath appendPath_last[THEN sym] Subobjs_nonempty simp:path_via_def) with h have "P,E,h ⊢ ref (a,Ds) : Class C" by auto with T show ?case by (fastforce intro:wt_same_type_typeconf) next case (RedStaticDownCast E C a Cs Cs' h l) have "P,E,h ⊢ ⦇C⦈ref (a,Cs@[C]@Cs') : T" by fact hence typeof:"P ⊢ typeof⇘h⇙ (Ref(a,Cs@[C]@Cs')) = Some(Class(last(Cs@[C]@Cs')))" and "class": "is_class P C" and T:"T = Class C" by auto from typeof obtain D S where h:"h a = Some(D,S)" and subo:"Subobjs P D (Cs@[C]@Cs')" by (auto dest:typeof_Class_Subo split:if_split_asm) from subo have "Subobjs P D (Cs@[C])" by(fastforce intro:appendSubobj) with h have "P,E,h ⊢ ref (a,Cs@[C]) : Class C" by auto with T show ?case by (fastforce intro:wt_same_type_typeconf) next case (RedStaticCastFail C Cs E a h l) have sconf:"P,E ⊢ (h, l) √" by fact from wf have "is_class P ClassCast" by (fastforce intro:is_class_xcpt wf_prog_wwf_prog) hence "preallocated h ⟹ P ⊢ typeof⇘h⇙ (Ref (addr_of_sys_xcpt ClassCast,[ClassCast])) = Some(Class ClassCast)" by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base) with sconf have "P,E,h ⊢ THROW ClassCast : T" by(auto simp:sconf_def hconf_def) thus ?case by (fastforce intro:wt_same_type_typeconf) next case (DynCastRed E e h l e' h' l' C) have wt:"P,E,h ⊢ Cast C e : T" and IH:"⋀T'. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" and sconf:"P,E ⊢ (h,l) √" by fact+ from wt obtain T' where wte:"P,E,h ⊢ e : T'" and isref:"is_refT T'" and "class": "is_class P C" and T:"T = Class C" by auto from isref have "P,E,h' ⊢ Cast C e' : Class C" proof(rule refTE) assume "T' = NT" with IH[OF sconf wte] isref "class" show ?thesis by auto next fix D assume "T' = Class D" with IH[OF sconf wte] isref "class" show ?thesis by auto qed with T show ?case by (fastforce intro:wt_same_type_typeconf) next case RedDynCastNull thus ?case by (auto elim:WTrt.cases) next case (RedDynCast h l a D S C Cs' E Cs) have wt:"P,E,h ⊢ Cast C (ref (a,Cs)) : T" and path_via:"P ⊢ Path D to C via Cs'" and hp:"hp (h,l) a = Some(D,S)" by fact+ from wt have typeof:"P ⊢ typeof⇘h⇙ (Ref(a,Cs)) = Some(Class(last Cs))" and "class": "is_class P C" and T:"T = Class C" by auto from typeof hp have subo:"Subobjs P D Cs" by (auto dest:typeof_Class_Subo split:if_split_asm) from path_via subo have "Subobjs P D Cs'" and last:"last Cs' = C" by (auto simp:path_via_def) with hp have "P,E,h ⊢ ref (a,Cs') : Class C" by auto with T show ?case by (fastforce intro:wt_same_type_typeconf) next case (RedStaticUpDynCast Cs C Cs' Ds E a h l) have wt:"P,E,h ⊢ Cast C (ref (a,Cs)) : T" and path_via:"P ⊢ Path last Cs to C via Cs'" and Ds:"Ds = Cs @⇩_{p}Cs'" by fact+ from wt have typeof:"P ⊢ typeof⇘h⇙ (Ref(a,Cs)) = Some(Class(last Cs))" and "class": "is_class P C" and T:"T = Class C" by auto from typeof obtain D S where h:"h a = Some(D,S)" and subo:"Subobjs P D Cs" by (auto dest:typeof_Class_Subo split:if_split_asm) from path_via subo wf Ds have "Subobjs P D Ds" and last:"last Ds = C" by(auto intro!:Subobjs_appendPath appendPath_last[THEN sym] Subobjs_nonempty simp:path_via_def) with h have "P,E,h ⊢ ref (a,Ds) : Class C" by auto with T show ?case by (fastforce intro:wt_same_type_typeconf) next case (RedStaticDownDynCast E C a Cs Cs' h l) have "P,E,h ⊢ Cast C (ref (a,Cs@[C]@Cs')) : T" by fact hence typeof:"P ⊢ typeof⇘h⇙ (Ref(a,Cs@[C]@Cs')) = Some(Class(last(Cs@[C]@Cs')))" and "class": "is_class P C" and T:"T = Class C" by auto from typeof obtain D S where h:"h a = Some(D,S)" and subo:"Subobjs P D (Cs@[C]@Cs')" by (auto dest:typeof_Class_Subo split:if_split_asm) from subo have "Subobjs P D (Cs@[C])" by(fastforce intro:appendSubobj) with h have "P,E,h ⊢ ref (a,Cs@[C]) : Class C" by auto with T show ?case by (fastforce intro:wt_same_type_typeconf) next case RedDynCastFail thus ?case by fastforce next case (BinOpRed1 E e h l e' h' l' bop e⇩_{2}) have red:"P,E ⊢ ⟨e,(h, l)⟩ → ⟨e',(h', l')⟩" and wt:"P,E,h ⊢ e «bop» e⇩_{2}: T" and IH:"⋀T'. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" and sconf:"P,E ⊢ (h,l) √" by fact+ from wt obtain T⇩_{1}T⇩_{2}where wte:"P,E,h ⊢ e : T⇩_{1}" and wte2:"P,E,h ⊢ e⇩_{2}: T⇩_{2}" and binop:"case bop of Eq ⇒ T = Boolean | Add ⇒ T⇩_{1}= Integer ∧ T⇩_{2}= Integer ∧ T = Integer" by auto from WTrt_hext_mono[OF wte2 red_hext_incr[OF red]] have wte2':"P,E,h' ⊢ e⇩_{2}: T⇩_{2}" . have "P,E,h' ⊢ e' «bop» e⇩_{2}: T" proof (cases bop) assume Eq:"bop = Eq" from IH[OF sconf wte] obtain T' where "P,E,h' ⊢ e' : T'" by (cases "T⇩_{1}") auto with wte2' binop Eq show ?thesis by(cases bop) auto next assume Add:"bop = Add" with binop have Intg:"T⇩_{1}= Integer" by simp with IH[OF sconf wte] have "P,E,h' ⊢ e' : Integer" by simp with wte2' binop Add show ?thesis by(cases bop) auto qed with binop show ?case by(cases bop) simp_all next case (BinOpRed2 E e h l e' h' l' v⇩_{1}bop) have red:"P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩" and wt:"P,E,h ⊢ Val v⇩_{1}«bop» e : T" and IH:"⋀T'. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" and sconf:"P,E ⊢ (h,l) √" by fact+ from wt obtain T⇩_{1}T⇩_{2}where wtval:"P,E,h ⊢ Val v⇩_{1}: T⇩_{1}" and wte:"P,E,h ⊢ e : T⇩_{2}" and binop:"case bop of Eq ⇒ T = Boolean | Add ⇒ T⇩_{1}= Integer ∧ T⇩_{2}= Integer ∧ T = Integer" by auto from WTrt_hext_mono[OF wtval red_hext_incr[OF red]] have wtval':"P,E,h' ⊢ Val v⇩_{1}: T⇩_{1}" . have "P,E,h' ⊢ Val v⇩_{1}«bop» e' : T" proof (cases bop) assume Eq:"bop = Eq" from IH[OF sconf wte] obtain T' where "P,E,h' ⊢ e' : T'" by (cases "T⇩_{2}") auto with wtval' binop Eq show ?thesis by(cases bop) auto next assume Add:"bop = Add" with binop have Intg:"T⇩_{2}= Integer" by simp with IH[OF sconf wte] have "P,E,h' ⊢ e' : Integer" by simp with wtval' binop Add show ?thesis by(cases bop) auto qed with binop show ?case by(cases bop) simp_all next case (RedBinOp bop v⇩_{1}v⇩_{2}v E a b) 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 h l V v E) have l:"lcl (h, l) V = Some v" and sconf:"P,E ⊢ (h, l) √" and wt:"P,E,h ⊢ Var V : T" by fact+ hence conf:"P,h ⊢ v :≤ T" by(force simp:sconf_def lconf_def) show ?case proof(cases "∀C. T ≠ Class C") case True with conf have "P ⊢ typeof⇘h⇙ v = Some T" by(cases T) auto hence "P,E,h ⊢ Val v : T" by auto thus ?thesis by(rule wt_same_type_typeconf) next case False then obtain C where T:"T = Class C" by auto with conf have "P ⊢ typeof⇘h⇙ v = Some(Class C) ∨ P ⊢ typeof⇘h⇙ v = Some NT" by simp with T show ?thesis by simp qed next case (LAssRed E e h l e' h' l' V) have wt:"P,E,h ⊢ V:=e : T" and sconf:"P,E ⊢ (h, l) √" and IH:"⋀T'. ⟦P,E ⊢ (h, l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" by fact+ from wt obtain T' where wte:"P,E,h ⊢ e : T'" and env:"E V = Some T" and sub:"P ⊢ T' ≤ T" by auto from sconf env have "is_type P T" by(auto simp:sconf_def envconf_def) from sub this wf show ?case proof(rule subE) assume eq:"T' = T" and notclass:"∀C. T' ≠ Class C" with IH[OF sconf wte] have "P,E,h' ⊢ e' : T" by(cases T) auto with eq env have "P,E,h' ⊢ V:=e' : T" by auto with eq show ?thesis by(cases T) auto next fix C D assume T':"T' = Class C" and T:"T = Class D" and path_unique:"P ⊢ Path C to D unique" with IH[OF sconf wte] have "P,E,h' ⊢ e' : Class C ∨ P,E,h' ⊢ e' : NT" by simp hence "P,E,h' ⊢ V:=e' : T" proof(rule disjE) assume "P,E,h' ⊢ e' : Class C" with env T' sub show ?thesis by (fastforce intro:WTrtLAss) next assume "P,E,h' ⊢ e' : NT" with env T show ?thesis by (fastforce intro:WTrtLAss) qed with T show ?thesis by(cases T) auto next fix C assume T':"T' = NT" and T:"T = Class C" with IH[OF sconf wte] have "P,E,h' ⊢ e' : NT" by simp with env T show ?thesis by (fastforce intro:WTrtLAss) qed next case (RedLAss E V T v v' h l T') have env:"E V = Some T" and casts:"P ⊢ T casts v to v'" and sconf:"P,E ⊢ (h, l) √" and wt:"P,E,h ⊢ V:=Val v : T'" by fact+ show ?case proof(cases "∀C. T ≠ Class C") case True with casts wt env show ?thesis by(cases T',auto elim!:casts_to.cases) next case False then obtain C where "T = Class C" by auto with casts wt env wf show ?thesis by(auto elim!:casts_to.cases, auto intro!:sym[OF appendPath_last] Subobjs_nonempty split:if_split_asm simp:path_via_def,drule_tac Cs="Cs" in Subobjs_appendPath,auto) qed next case (FAccRed E e h l e' h' l' F Cs) have red:"P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩" and wt:"P,E,h ⊢ e∙F{Cs} : T" and IH:"⋀T'. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" and sconf:"P,E ⊢ (h,l) √" by fact+ from wt have "P,E,h' ⊢ e'∙F{Cs} : T" proof(rule WTrt_elim_cases) fix C assume wte: "P,E,h ⊢ e : Class C" and field:"P ⊢ C has least F:T via Cs" and notemptyCs:"Cs ≠ []" from field have "class": "is_class P C" by (fastforce intro:Subobjs_isClass simp add:LeastFieldDecl_def FieldDecls_def) from IH[OF sconf wte] have "P,E,h' ⊢ e' : NT ∨ P,E,h' ⊢ e' : Class C" by auto thus ?thesis proof(rule disjE) assume "P,E,h' ⊢ e' : NT" thus ?thesis by (fastforce intro!:WTrtFAccNT) next assume wte':"P,E,h' ⊢ e' : Class C" from wte' notemptyCs field show ?thesis by(rule WTrtFAcc) qed next assume wte: "P,E,h ⊢ e : NT" from IH[OF sconf wte] have "P,E,h' ⊢ e' : NT" by auto thus ?thesis by (rule WTrtFAccNT) qed thus ?case by(rule wt_same_type_typeconf) next case (RedFAcc h l a D S Ds Cs' Cs fs' F v E) have h:"hp (h,l) a = Some(D,S)" and Ds:"Ds = Cs'@⇩_{p}Cs" and S:"(Ds,fs') ∈ S" and fs':"fs' F = Some v" and sconf:"P,E ⊢ (h,l) √" and wte:"P,E,h ⊢ ref (a,Cs')∙F{Cs} : T" by fact+ from wte have field:"P ⊢ last Cs' has least F:T via Cs" and notemptyCs:"Cs ≠ []" by (auto split:if_split_asm) from h S sconf obtain Bs fs ms where classDs:"class P (last Ds) = Some (Bs,fs,ms)" and fconf:"P,h ⊢ fs' (:≤) map_of fs" by (simp add:sconf_def hconf_def oconf_def) blast from field Ds have "last Cs = last Ds" by (fastforce intro!:appendPath_last Subobjs_nonempty simp:LeastFieldDecl_def FieldDecls_def) with field classDs have map:"map_of fs F = Some T" by (simp add:LeastFieldDecl_def FieldDecls_def) with fconf fs' have conf:"P,h ⊢ v :≤ T" by (simp add:fconf_def,erule_tac x="F" in allE,fastforce) thus ?case by (cases T) auto next case (RedFAccNull E F Cs h l) have sconf:"P,E ⊢ (h, l) √" by fact from wf have "is_class P NullPointer" by (fastforce intro:is_class_xcpt wf_prog_wwf_prog) hence "preallocated h ⟹ P ⊢ typeof⇘h⇙ (Ref (addr_of_sys_xcpt NullPointer,[NullPointer])) = Some(Class NullPointer)" by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base) with sconf have "P,E,h ⊢ THROW NullPointer : T" by(auto simp:sconf_def hconf_def) thus ?case by (fastforce intro:wt_same_type_typeconf wf_prog_wwf_prog) next case (FAssRed1 E e h l e' h' l' F Cs e⇩_{2}) have red:"P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩" and wt:"P,E,h ⊢ e∙F{Cs} := e⇩_{2}: T" and IH:"⋀T'. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" and sconf:"P,E ⊢ (h,l) √" by fact+ from wt have "P,E,h' ⊢ e'∙F{Cs} := e⇩_{2}: T" proof (rule WTrt_elim_cases) fix C T' assume wte: "P,E,h ⊢ e : Class C" and field:"P ⊢ C has least F:T via Cs" and notemptyCs:"Cs ≠ []" and wte2:"P,E,h ⊢ e⇩_{2}: T'" and sub:"P ⊢ T' ≤ T" have wte2': "P,E,h' ⊢ e⇩_{2}: T'" by(rule WTrt_hext_mono[OF wte2 red_hext_incr[OF red]]) from IH[OF sconf wte] have "P,E,h' ⊢ e' : Class C ∨ P,E,h' ⊢ e' : NT" by simp thus ?thesis proof(rule disjE) assume wte':"P,E,h' ⊢ e' : Class C" from wte' notemptyCs field wte2' sub show ?thesis by (rule WTrtFAss) next assume wte':"P,E,h' ⊢ e' : NT" from wte' wte2' sub show ?thesis by (rule WTrtFAssNT) qed next fix T' assume wte:"P,E,h ⊢ e : NT" and wte2:"P,E,h ⊢ e⇩_{2}: T'" and sub:"P ⊢ T' ≤ T" have wte2': "P,E,h' ⊢ e⇩_{2}: T'" by(rule WTrt_hext_mono[OF wte2 red_hext_incr[OF red]]) from IH[OF sconf wte] have wte':"P,E,h' ⊢ e' : NT" by simp from wte' wte2' sub show ?thesis by (rule WTrtFAssNT) qed thus ?case by(rule wt_same_type_typeconf) next case (FAssRed2 E e h l e' h' l' v F Cs) have red:"P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩" and wt:"P,E,h ⊢ Val v∙F{Cs} := e : T" and IH:"⋀T'. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" and sconf:"P,E ⊢ (h,l) √" by fact+ from wt have "P,E,h' ⊢ Val v∙F{Cs}:=e' : T" proof (rule WTrt_elim_cases) fix C T' assume wtval:"P,E,h ⊢ Val v : Class C" and field:"P ⊢ C has least F:T via Cs" and notemptyCs:"Cs ≠ []" and wte:"P,E,h ⊢ e : T'" and sub:"P ⊢ T' ≤ T" have wtval':"P,E,h' ⊢ Val v : Class C" by(rule WTrt_hext_mono[OF wtval red_hext_incr[OF red]]) from field wf have type:"is_type P T" by(rule least_field_is_type) from sub type wf show ?thesis proof(rule subE) assume "T' = T" and notclass:"∀C. T' ≠ Class C" from IH[OF sconf wte] notclass have wte':"P,E,h' ⊢ e' : T'" by(cases T') auto from wtval' notemptyCs field wte' sub show ?thesis by(rule WTrtFAss) next fix C' D assume T':"T' = Class C'" and T:"T = Class D" and path_unique:"P ⊢ Path C' to D unique" from IH[OF sconf wte] T' have "P,E,h' ⊢ e' : Class C' ∨ P,E,h' ⊢ e' : NT" by simp thus ?thesis proof(rule disjE) assume wte':"P,E,h' ⊢ e' : Class C'" from wtval' notemptyCs field wte' sub T' show ?thesis by (fastforce intro: WTrtFAss) next assume wte':"P,E,h' ⊢ e' : NT" from wtval' notemptyCs field wte' sub T show ?thesis by (fastforce intro: WTrtFAss) qed next fix C' assume T':"T' = NT" and T:"T = Class C'" from IH[OF sconf wte] T' have wte':"P,E,h' ⊢ e' : NT" by simp from wtval' notemptyCs field wte' sub T show ?thesis by (fastforce intro: WTrtFAss) qed next fix T' assume wtval:"P,E,h ⊢ Val v : NT" and wte:"P,E,h ⊢ e : T'" and sub:"P ⊢ T' ≤ T" have wtval':"P,E,h' ⊢ Val v : NT" by(rule WTrt_hext_mono[OF wtval red_hext_incr[OF red]]) from IH[OF sconf wte] sub obtain T'' where wte':"P,E,h' ⊢ e' : T''" and sub':"P ⊢ T'' ≤ T" by (cases T',auto,cases T,auto) from wtval' wte' sub' show ?thesis by(rule WTrtFAssNT) qed thus ?case by(rule wt_same_type_typeconf) next case (RedFAss h a D S Cs' F T Cs v v' Ds fs E l T') let ?fs' = "fs(F ↦ v')" let ?S' = "insert (Ds, ?fs') (S - {(Ds, fs)})" let ?h' = "h(a ↦ (D,?S'))" have h:"h a = Some(D,S)" and casts:"P ⊢ T casts v to v'" and field:"P ⊢ last Cs' has least F:T via Cs" and wt:"P,E,h ⊢ ref (a,Cs')∙F{Cs} := Val v : T'" by fact+ from wt wf have type:"is_type P T'" by (auto dest:least_field_is_type split:if_split_asm) from wt field obtain T'' where wtval:"P,E,h ⊢ Val v : T''" and eq:"T = T'" and leq:"P ⊢ T'' ≤ T'" by (auto dest:sees_field_fun split:if_split_asm) from casts eq wtval show ?case proof(induct rule:casts_to.induct) case (casts_prim T⇩_{0}w) have "T⇩_{0}= T'" and "∀C. T⇩_{0}≠ Class C" and wtval':"P,E,h ⊢ Val w : T''" by fact+ with leq have "T' = T''" by(cases T',auto) with wtval' have "P,E,h ⊢ Val w : T'" by simp with h have "P,E,(h(a↦(D,insert(Ds,fs(F ↦ w))(S-{(Ds,fs)})))) ⊢ Val w : T'" by(cases w,auto split:if_split_asm) thus "P,E,(h(a↦(D,insert(Ds,fs(F ↦ w))(S-{(Ds,fs)})))) ⊢ (Val w) :⇘_{NT}⇙ T'" by(rule wt_same_type_typeconf) next case (casts_null C'') have T':"Class C'' = T'" by fact have "P,E,(h(a↦(D,insert(Ds,fs(F ↦ Null))(S-{(Ds,fs)})))) ⊢ null : NT" by simp with sym[OF T'] show "P,E,(h(a↦(D,insert(Ds,fs(F ↦ Null))(S-{(Ds,fs)})))) ⊢ null :⇘_{NT}⇙ T'" by simp next case (casts_ref Xs C'' Xs' Ds'' a') have "Class C'' = T'" and "Ds'' = Xs @⇩_{p}Xs'" and "P ⊢ Path last Xs to C'' via Xs'" and "P,E,h ⊢ ref (a', Xs) : T''" by fact+ with wf have "P,E,h ⊢ ref (a',Ds'') : T'" by (auto intro!:appendPath_last[THEN sym] Subobjs_nonempty split:if_split_asm simp:path_via_def, drule_tac Cs="Xs" in Subobjs_appendPath,auto) with h have "P,E,(h(a↦(D,insert(Ds,fs(F ↦ Ref(a',Ds'')))(S-{(Ds,fs)})))) ⊢ ref (a',Ds'') : T'" by auto thus "P,E,(h(a↦(D,insert(Ds,fs(F ↦ Ref(a',Ds'')))(S-{(Ds,fs)})))) ⊢ ref (a',Ds'') :⇘_{NT}⇙ T'" by(rule wt_same_type_typeconf) qed next case (RedFAssNull E F Cs v h l) have sconf:"P,E ⊢ (h, l) √" by fact from wf have "is_class P NullPointer" by (fastforce intro:is_class_xcpt wf_prog_wwf_prog) hence "preallocated h ⟹ P ⊢ typeof⇘h⇙ (Ref (addr_of_sys_xcpt NullPointer,[NullPointer])) = Some(Class NullPointer)" by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base) with sconf have "P,E,h ⊢ THROW NullPointer : T" by(auto simp:sconf_def hconf_def) thus ?case by (fastforce intro:wt_same_type_typeconf wf_prog_wwf_prog) next case (CallObj E e h l e' h' l' Copt M es) have red: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩" and IH: "⋀T'. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ e : T'⟧ ⟹ P,E,h' ⊢ e' :⇘_{NT}⇙ T'" and sconf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ Call e Copt M es : T" by fact+ from wt have "P,E,h' ⊢ Call e' Copt M es : T" proof(cases Copt) case None with wt have "P,E,h ⊢ e∙M(es) : T" by simp hence "P,E,h' ⊢ e'∙M(es) : T" proof(rule WTrt_elim_cases) fix C Cs Ts Ts' m assume wte:"P,E,h ⊢ e : Class C" and "method":"P ⊢ C has least M = (Ts, T, m) via Cs" and wtes:"P,E,h ⊢ es [:] Ts'" and subs: "P ⊢ Ts' [≤] Ts" from IH[OF sconf wte] have "P,E,h' ⊢ e' : NT ∨ P,E,h' ⊢ e' : Class C" by auto thus ?thesis proof(rule disjE) assume wte':"P,E,h' ⊢ e' : NT" have "P,E,h' ⊢ es [:] Ts'" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) with wte' show ?thesis by(rule WTrtCallNT) next assume wte':"P,E,h' ⊢ e' : Class C" have wtes':"P,E,h' ⊢ es [:] Ts'" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) from wte' "method" wtes' subs show ?thesis by(rule WTrtCall) qed next fix Ts assume wte:"P,E,h ⊢ e : NT" and wtes:"P,E,h ⊢ es [:] Ts" from IH[OF sconf wte] have wte':"P,E,h' ⊢ e' : NT" by simp have "P,E,h' ⊢ es [:] Ts" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) with wte' show ?thesis by(rule WTrtCallNT) qed with None show ?thesis by simp next case (Some C) with wt have "P,E,h ⊢ e∙(C::)M(es) : T" by simp hence "P,E,h' ⊢ e'∙(C::)M(es) : T" proof(rule WTrt_elim_cases) fix C' Cs Ts Ts' m assume wte:"P,E,h ⊢ e : Class C'" and path_unique:"P ⊢ Path C' to C unique" and "method":"P ⊢ C has least M = (Ts, T, m) via Cs" and wtes:"P,E,h ⊢ es [:] Ts'" and subs: "P ⊢ Ts' [≤] Ts" from IH[OF sconf wte] have "P,E,h' ⊢ e' : NT ∨ P,E,h' ⊢ e' : Class C'" by auto thus ?thesis proof(rule disjE) assume wte':"P,E,h' ⊢ e' : NT" have "P,E,h' ⊢ es [:] Ts'" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) with wte' show ?thesis by(rule WTrtCallNT) next assume wte':"P,E,h' ⊢ e' : Class C'" have wtes':"P,E,h' ⊢ es [:] Ts'" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) from wte' path_unique "method" wtes' subs show ?thesis by(rule WTrtStaticCall) qed next fix Ts assume wte:"P,E,h ⊢ e : NT" and wtes:"P,E,h ⊢ es [:] Ts" from IH[OF sconf wte] have wte':"P,E,h' ⊢ e' : NT" by simp have "P,E,h' ⊢ es [:] Ts" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) with wte' show ?thesis by(rule WTrtCallNT) qed with Some show ?thesis by simp qed thus ?case by (rule wt_same_type_typeconf) next case (CallParams E es h l es' h' l' v Copt M) have reds: "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩" and IH: "⋀Ts. ⟦P,E ⊢ (h,l) √; P,E,h ⊢ es [:] Ts⟧ ⟹ types_conf P E h' es' Ts" and sconf: "P,E ⊢ (h,l) √" and wt: "P,E,h ⊢ Call (Val v) Copt M es : T" by fact+ from wt have "P,E,h' ⊢ Call (Val v) Copt M es' : T" proof(cases Copt) case None with wt have "P,E,h ⊢ (Val v)∙M(es) : T" by simp hence "P,E,h' ⊢ Val v∙M(es') : T" proof (rule WTrt_elim_cases) fix C Cs Ts Ts' m assume wte: "P,E,h ⊢ Val v : Class C" and "method":"P ⊢ C has least M = (Ts,T,m) via Cs" and wtes: "P,E,h ⊢ es [:] Ts'" and subs:"P ⊢ Ts' [≤] Ts" from wtes have "length es = length Ts'" by(rule WTrts_same_length) with reds have "length es' = length Ts'" by -(drule reds_length,simp) with IH[OF sconf wtes] subs obtain Ts'' where wtes':"P,E,h' ⊢ es' [:] Ts''" and subs':"P ⊢ Ts'' [≤] Ts" by(auto dest:types_conf_smaller_types) have wte':"P,E,h' ⊢ Val v : Class C" by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]]) from wte' "method" wtes' subs' show ?thesis by(rule WTrtCall) next fix Ts assume wte:"P,E,h ⊢ Val v : NT" and wtes:"P,E,h ⊢ es [:] Ts" from wtes have "length es = length Ts" by(rule WTrts_same_length) with reds have "length es' = length Ts" by -(drule reds_length,simp) with IH[OF sconf wtes] obtain Ts' where wtes':"P,E,h' ⊢ es' [:] Ts'" and "P ⊢ Ts' [≤] Ts" by(auto dest:types_conf_smaller_types) have wte':"P,E,h' ⊢ Val v : NT" by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]]) from wte' wtes' show ?thesis by(rule WTrtCallNT) qed with None show ?thesis by simp next case (Some C) with wt have "P,E,h ⊢ (Val v)∙(C::)M(es) : T" by simp hence "P,E,h' ⊢ (Val v)∙(C::)M(es') : T" proof(rule WTrt_elim_cases) fix C' Cs Ts Ts' m assume wte:"P,E,h ⊢ Val v : Class C'" and path_unique:"P ⊢ Path C' to C unique" and "method":"P ⊢ C has least M = (Ts,T,m) via Cs" and wtes:"P,E,h ⊢ es [:] Ts'" and subs: "P ⊢ Ts' [≤] Ts" from wtes have "length es = length Ts'" by(rule WTrts_same_length) with reds have "length es' = length Ts'" by -(drule reds_length,simp) with IH[OF sconf wtes] subs obtain Ts'' where wtes':"P,E,h' ⊢ es' [:] Ts''" and subs':"P ⊢ Ts'' [≤] Ts" by(auto dest:types_conf_smaller_types) have wte':"P,E,h' ⊢ Val v : Class C'" by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]]) from wte' path_unique "method" wtes' subs' show ?thesis by(rule WTrtStaticCall) next fix Ts assume wte:"P,E,h ⊢ Val v : NT" and wtes:"P,E,h ⊢ es [:] Ts" from wtes have "length es = length Ts" by(rule WTrts_same_length) with reds have "length es' = length Ts" by -(drule reds_length,simp) with IH[OF sconf wtes] obtain Ts' where wtes':"P,E,h' ⊢ es' [:] Ts'" and "P ⊢ Ts' [≤] Ts" by(auto dest:types_conf_smaller_types) have wte':"P,E,h' ⊢ Val v : NT" by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]]) from wte' wtes' show ?thesis by(rule WTrtCallNT) qed with Some show ?thesis by simp qed thus ?case by (rule wt_same_type_typeconf) next case (RedCall h l a C S Cs M Ts' T' pns' body' Ds Ts T pns body Cs' vs bs new_body E T'') have hp:"hp (h,l) a = Some(C,S)" and "method":"P ⊢ last Cs has least M = (Ts',T',pns',body') via Ds" and select:"P ⊢ (C,Cs@⇩_{p}Ds) selects M = (Ts,T,pns,body) via Cs'" and length1:"length vs = length pns" and length2:"length Ts = length pns" and bs:"bs = blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body)" and body_case:"new_body = (case T' of Class D ⇒ ⦇D⦈bs | _ ⇒ bs)" and wt:"P,E,h ⊢ ref (a,Cs)∙M(map Val vs) : T''" by fact+ from wt hp "method" wf obtain Ts'' where wtref:"P,E,h ⊢ ref (a,Cs) : Class (last Cs)" and eq:"T'' = T'" and wtes:"P,E,h ⊢ map Val vs [:] Ts''" and subs: "P ⊢ Ts'' [≤] Ts'" by(auto dest:wf_sees_method_fun split:if_split_asm) from select wf have "is_class P (last Cs')" by(induct rule:SelectMethodDef.induct, auto intro:Subobj_last_isClass simp:FinalOverriderMethodDef_def OverriderMethodDefs_def MinimalMethodDefs_def LeastMethodDef_def MethodDefs_def) with select_method_wf_mdecl[OF wf select] have length_pns:"length (this#pns) = length (Class(last Cs')#Ts)" and notNT:"T ≠ NT" and type:"∀T∈set (Class(last Cs')#Ts). is_type P T" and wtabody:"P,[this↦Class(last Cs'),pns[↦]Ts] ⊢ body :: T" by(auto simp:wf_mdecl_def) from wtes hp select have map:"map (P ⊢ typeof⇘h⇙) (Ref(a,Cs')#vs) = map Some (Class(last Cs')#Ts'')" by(auto elim:SelectMethodDef.cases split:if_split_asm simp:FinalOverriderMethodDef_def OverriderMethodDefs_def MinimalMethodDefs_def LeastMethodDef_def MethodDefs_def) from wtref hp have "P ⊢ Path C to (last Cs) via Cs" by (auto simp:path_via_def split:if_split_asm) with select "method" wf have "Ts' = Ts ∧ P ⊢ T ≤ T'" by -(rule select_least_methods_subtypes,simp_all) hence eqs:"Ts' = Ts" and sub:"P ⊢ T ≤ T'" by auto from wf wtabody have "P,Map.empty(this↦Class(last Cs'),pns[↦]Ts),h ⊢ body : T" by -(rule WT_implies_WTrt,simp_all) hence wtbody:"P,E(this#pns [↦] Class (last Cs')#Ts),h ⊢ body : T" by(rule WTrt_env_mono) simp from wtes have "length vs = length Ts''" by (fastforce dest:WTrts_same_length) with eqs subs have length_vs:"length (Ref(a,Cs')#vs) = length (Class(last Cs')#Ts)" by (simp add:list_all2_iff) from subs eqs have "P ⊢ (Class(last Cs')#Ts'') [≤] (Class(last Cs')#Ts)" by (simp add:fun_of_def) with wt_blocks[OF length_pns length_vs type] wtbody map eq have blocks:"P,E,h ⊢ blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body) : T" by auto have "P,E,h ⊢ new_body : T'" proof(cases "∀C. T' ≠ Class C") case True with sub notNT have "T = T'" by (cases T') auto with blocks True body_case bs show ?thesis by(cases T') auto next case False then obtain D where T':"T' = Class D" by auto with "method" sub wf have "class": "is_class P D" by (auto elim!:widen.cases dest:least_method_is_type intro:Subobj_last_isClass simp:path_unique_def) with blocks T' body_case bs "class" sub show ?thesis by(cases T',auto,cases T,auto) qed with eq show ?case by(fastforce intro:wt_same_type_typeconf) next case (RedStaticCall Cs C Cs'' M Ts T pns body Cs' Ds vs E a h l T') have "method":"P ⊢ C has least M = (Ts, T, pns, body) via Cs'" and length1:"length vs = length pns" and length2:"length Ts = length pns" and path_unique:"P ⊢ Path last Cs to C unique" and path_via:"P ⊢ Path last Cs to C via Cs''" and Ds:"Ds = (Cs @⇩_{p}Cs'') @⇩_{p}Cs'" and wt:"P,E,h ⊢ ref (a,Cs)∙(C::)M(map Val vs) : T'" by fact+ from wt "method" wf obtain Ts' where wtref:"P,E,h ⊢ ref (a,Cs) : Class (last Cs)" and wtes:"P,E,h ⊢ map Val vs [:] Ts'" and subs:"P ⊢ Ts' [≤] Ts" and TeqT':"T = T'" by(auto dest:wf_sees_method_fun split:if_split_asm) from wtref obtain D S where hp:"h a = Some(D,S)" and subo:"Subobjs P D Cs" by (auto split:if_split_asm) from length1 length2 have length_vs: "length (Ref(a,Ds)#vs) = length (Class (last Ds)#Ts)" by simp from length2 have length_pns:"length (this#pns) = length (Class (last Ds)#Ts)" by simp from "method" have "Cs' ≠ []" by (fastforce intro!:Subobjs_nonempty simp add:LeastMethodDef_def MethodDefs_def) with Ds have last:"last Cs' = last Ds" by (fastforce dest:appendPath_last) with "method" have "is_class P (last Ds)" by(auto simp:LeastMethodDef_def MethodDefs_def is_class_def) with last has_least_wf_mdecl[OF wf "method"] have wtabody: "P,[this#pns [↦] Class (last Ds)#Ts] ⊢ body :: T" and type:"∀T∈set (Class(last Ds)#Ts). is_type P T" by(auto simp:wf_mdecl_def) from path_via have suboCs'':"Subobjs P (last Cs) Cs''" and lastCs'':"last Cs'' = C" by (auto simp add:path_via_def) with subo wf have subo':"Subobjs P D (Cs@⇩_{p}Cs'')" by(fastforce intro: Subobjs_appendPath) from lastCs'' suboCs'' have lastC:"C = last(Cs@⇩_{p}Cs'')" by (fastforce dest:Subobjs_nonempty intro:appendPath_last) from "method" have "Subobjs P C Cs'" by (auto simp:LeastMethodDef_def MethodDefs_def) with subo' wf lastC have "Subobjs P D ((Cs @⇩_{p}Cs'') @⇩_{p}Cs')" by (fastforce intro:Subobjs_appendPath) with Ds have suboDs:"Subobjs P D Ds" by simp from wtabody have "P,Map.empty(this#pns [↦] Class (last Ds)#Ts),h ⊢ body : T" by(rule WT_implies_WTrt) hence "P,E(this#pns [↦] Class (last Ds)#Ts),h ⊢ body : T" by(rule WTrt_env_mono) simp hence "P,E,h ⊢ blocks(this#pns, Class (last Ds)#Ts, Ref(a,Ds)#vs, body) : T" using wtes subs wt_blocks[OF length_pns length_vs type] hp suboDs by(auto simp add:rel_list_all2_Cons2) with TeqT' show ?case by(fastforce intro:wt_same_type_typeconf) next case (RedCallNull E Copt M vs h l) have sconf:"P,E ⊢ (h, l) √" by fact from wf have "is_class P NullPointer" by (fastforce intro:is_class_xcpt wf_prog_wwf_prog) hence "preallocated h ⟹ P ⊢ typeof⇘h⇙ (Ref (addr_of_sys_xcpt NullPointer,[NullPointer])) = Some(Class NullPointer)" by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base) with sconf have "P,E,h ⊢ THROW NullPointer : T" by(auto simp:sconf_def hconf_def) thus ?case by (fastforce intro:wt_same_type_typeconf) next case (BlockRedNone E V T e h l e' h' l' T') have IH:"⋀T'. ⟦P,E(V ↦ T) ⊢ (h, l(V := None)) √; P,E(V ↦ T),h ⊢ e : T'⟧ ⟹ P,E(V ↦ T),h' ⊢ e' :⇘_{NT}⇙ T'" and sconf:"P,E ⊢ (h