Theory TypeSafe
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@⇩pCs')"
by -(erule casts_to.cases,auto simp:path_unique_def path_via_def)
from subo path_via wf have "Subobjs P C (Cs@⇩pCs')"
and "last (Cs@⇩pCs') = 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'@⇩pCs" 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@⇩pDs) 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@⇩pCs'')"
by(fastforce intro: Subobjs_appendPath)
from lastCs'' suboCs'' have lastC:"C = last(Cs@⇩pCs'')"
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