(* Title: CoreC++ Author: Daniel Wasserrab Maintainer: Daniel Wasserrab <wasserra at fmi.uni-passau.de> Based on the Jinja theory J/Progress.thy by Tobias Nipkow *) section ‹Progress of Small Step Semantics› theory Progress imports Equivalence DefAss Conform begin subsection ‹Some pre-definitions› lemma final_refE: "⟦ P,E,h ⊢ e : Class C; final e; ⋀r. e = ref r ⟹ Q; ⋀r. e = Throw r ⟹ Q ⟧ ⟹ Q" by (simp add:final_def,auto,case_tac v,auto) lemma finalRefE: "⟦ P,E,h ⊢ e : T; is_refT T; final e; e = null ⟹ Q; ⋀r. e = ref r ⟹ Q; ⋀r. e = Throw r ⟹ Q⟧ ⟹ Q" apply (cases T) apply (simp add:is_refT_def)+ apply (simp add:final_def) apply (erule disjE) apply clarsimp apply (erule exE)+ apply fastforce apply (auto simp:final_def is_refT_def) apply (case_tac v) apply auto done lemma subE: "⟦ P ⊢ T ≤ T'; is_type P T'; wf_prog wf_md P; ⟦ T = T'; ∀C. T ≠ Class C ⟧ ⟹ Q; ⋀C D. ⟦ T = Class C; T' = Class D; P ⊢ Path C to D unique ⟧ ⟹ Q; ⋀C. ⟦ T = NT; T' = Class C ⟧ ⟹ Q ⟧ ⟹ Q" apply(cases T') apply auto apply(drule_tac T = "T" in widen_Class) apply auto done lemma assumes wf:"wf_prog wf_md P" and typeof:" P ⊢ typeof⇘_{h}⇙ v = Some T'" and type:"is_type P T" shows sub_casts:"P ⊢ T' ≤ T ⟹ ∃v'. P ⊢ T casts v to v'" proof(erule subE) from type show "is_type P T" . next from wf show "wf_prog wf_md P" . next assume "T' = T" and "∀C. T' ≠ Class C" thus "∃v'. P ⊢ T casts v to v'" by(fastforce intro:casts_prim) next fix C D assume T':"T' = Class C" and T:"T = Class D" and path_unique:"P ⊢ Path C to D unique" from T' typeof obtain a Cs where v:"v = Ref(a,Cs)" and last:"last Cs = C" by(auto dest!:typeof_Class_Subo) from last path_unique obtain Cs' where "P ⊢ Path last Cs to D via Cs'" by(auto simp:path_unique_def path_via_def) hence "P ⊢ Class D casts Ref(a,Cs) to Ref(a,Cs@⇩_{p}Cs')" by -(rule casts_ref,simp_all) with T v show "∃v'. P ⊢ T casts v to v'" by auto next fix C assume "T' = NT" and T:"T = Class C" with typeof have "v = Null" by simp with T show "∃v'. P ⊢ T casts v to v'" by(fastforce intro:casts_null) qed text‹Derivation of new induction scheme for well typing:› inductive WTrt' :: "[prog,env,heap,expr, ty ] ⇒ bool" ("_,_,_ ⊢ _ :'' _" [51,51,51]50) and WTrts':: "[prog,env,heap,expr list,ty list] ⇒ bool" ("_,_,_ ⊢ _ [:''] _" [51,51,51]50) for P :: prog where "is_class P C ⟹ P,E,h ⊢ new C :' Class C" | "⟦is_class P C; P,E,h ⊢ e :' T; is_refT T⟧ ⟹ P,E,h ⊢ Cast C e :' Class C" | "⟦is_class P C; P,E,h ⊢ e :' T; is_refT T⟧ ⟹ P,E,h ⊢ ⦇C⦈e :' Class C" | "P ⊢ typeof⇘_{h}⇙ v = Some T ⟹ P,E,h ⊢ Val v :' T" | "E V = Some T ⟹ P,E,h ⊢ Var V :' T" | "⟦ P,E,h ⊢ e⇩_{1}:' T⇩_{1}; P,E,h ⊢ e⇩_{2}:' T⇩_{2}; case bop of Eq ⇒ T = Boolean | Add ⇒ T⇩_{1}= Integer ∧ T⇩_{2}= Integer ∧ T = Integer ⟧ ⟹ P,E,h ⊢ e⇩_{1}«bop» e⇩_{2}:' T" | "⟦ P,E,h ⊢ Var V :' T; P,E,h ⊢ e :' T' ⌦‹V ≠ This›; P ⊢ T' ≤ T ⟧ ⟹ P,E,h ⊢ V:=e :' T" | "⟦P,E,h ⊢ e :' Class C; Cs ≠ []; P ⊢ C has least F:T via Cs⟧ ⟹ P,E,h ⊢ e∙F{Cs} :' T" | "P,E,h ⊢ e :' NT ⟹ P,E,h ⊢ e∙F{Cs} :' T" | "⟦P,E,h ⊢ e⇩_{1}:' Class C; Cs ≠ []; P ⊢ C has least F:T via Cs; P,E,h ⊢ e⇩_{2}:' T'; P ⊢ T' ≤ T ⟧ ⟹ P,E,h ⊢ e⇩_{1}∙F{Cs}:=e⇩_{2}:' T" | "⟦ P,E,h ⊢ e⇩_{1}:'NT; P,E,h ⊢ e⇩_{2}:' T'; P ⊢ T' ≤ T ⟧ ⟹ P,E,h ⊢ e⇩_{1}∙F{Cs}:=e⇩_{2}:' T" | "⟦ P,E,h ⊢ e :' Class C; P ⊢ C has least M = (Ts,T,m) via Cs; P,E,h ⊢ es [:'] Ts'; P ⊢ Ts' [≤] Ts ⟧ ⟹ P,E,h ⊢ e∙M(es) :' T" | "⟦ P,E,h ⊢ e :' Class C'; P ⊢ Path C' to C unique; P ⊢ C has least M = (Ts,T,m) via Cs; P,E,h ⊢ es [:'] Ts'; P ⊢ Ts' [≤] Ts ⟧ ⟹ P,E,h ⊢ e∙(C::)M(es) :' T" | "⟦P,E,h ⊢ e :' NT; P,E,h ⊢ es [:'] Ts⟧ ⟹ P,E,h ⊢ Call e Copt M es :' T" | "⟦ P ⊢ typeof⇘_{h}⇙ v = Some T'; P,E(V↦T),h ⊢ e⇩_{2}:' T⇩_{2}; P ⊢ T' ≤ T; is_type P T ⟧ ⟹ P,E,h ⊢ {V:T := Val v; e⇩_{2}} :' T⇩_{2}" | "⟦ P,E(V↦T),h ⊢ e :' T'; ¬ assigned V e; is_type P T ⟧ ⟹ P,E,h ⊢ {V:T; e} :' T'" | "⟦ P,E,h ⊢ e⇩_{1}:' T⇩_{1}; P,E,h ⊢ e⇩_{2}:' T⇩_{2}⟧ ⟹ P,E,h ⊢ e⇩_{1};;e⇩_{2}:' T⇩_{2}" | "⟦ P,E,h ⊢ e :' Boolean; P,E,h ⊢ e⇩_{1}:' T; P,E,h ⊢ e⇩_{2}:' T ⟧ ⟹ P,E,h ⊢ if (e) e⇩_{1}else e⇩_{2}:' T" | "⟦ P,E,h ⊢ e :' Boolean; P,E,h ⊢ c:' T ⟧ ⟹ P,E,h ⊢ while(e) c :' Void" | "⟦ P,E,h ⊢ e :' T'; is_refT T'⟧ ⟹ P,E,h ⊢ throw e :' T" | "P,E,h ⊢ [] [:'] []" | "⟦ P,E,h ⊢ e :' T; P,E,h ⊢ es [:'] Ts ⟧ ⟹ P,E,h ⊢ e#es [:'] T#Ts" lemmas WTrt'_induct = WTrt'_WTrts'.induct [split_format (complete)] and WTrt'_inducts = WTrt'_WTrts'.inducts [split_format (complete)] inductive_cases WTrt'_elim_cases[elim!]: "P,E,h ⊢ V :=e :' T" text‹... and some easy consequences:› lemma [iff]: "P,E,h ⊢ e⇩_{1};;e⇩_{2}:' T⇩_{2}= (∃T⇩_{1}. P,E,h ⊢ e⇩_{1}:' T⇩_{1}∧ P,E,h ⊢ e⇩_{2}:' T⇩_{2})" apply(rule iffI) apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros) done lemma [iff]: "P,E,h ⊢ Val v :' T = (P ⊢ typeof⇘_{h}⇙ v = Some T)" apply(rule iffI) apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros) done lemma [iff]: "P,E,h ⊢ Var V :' T = (E V = Some T)" apply(rule iffI) apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros) done lemma wt_wt': "P,E,h ⊢ e : T ⟹ P,E,h ⊢ e :' T" and wts_wts': "P,E,h ⊢ es [:] Ts ⟹ P,E,h ⊢ es [:'] Ts" proof (induct rule:WTrt_inducts) case (WTrtBlock E V T h e T') thus ?case apply(case_tac "assigned V e") apply(auto intro:WTrt'_WTrts'.intros simp add:fun_upd_same assigned_def simp del:fun_upd_apply) done qed(auto intro:WTrt'_WTrts'.intros simp del:fun_upd_apply) lemma wt'_wt: "P,E,h ⊢ e :' T ⟹ P,E,h ⊢ e : T" and wts'_wts: "P,E,h ⊢ es [:'] Ts ⟹ P,E,h ⊢ es [:] Ts" apply (induct rule:WTrt'_inducts) apply (fastforce intro: WTrt_WTrts.intros)+ done corollary wt'_iff_wt: "(P,E,h ⊢ e :' T) = (P,E,h ⊢ e : T)" by(blast intro:wt_wt' wt'_wt) corollary wts'_iff_wts: "(P,E,h ⊢ es [:'] Ts) = (P,E,h ⊢ es [:] Ts)" by(blast intro:wts_wts' wts'_wts) lemmas WTrt_inducts2 = WTrt'_inducts [unfolded wt'_iff_wt wts'_iff_wts, case_names WTrtNew WTrtDynCast WTrtStaticCast WTrtVal WTrtVar WTrtBinOp WTrtLAss WTrtFAcc WTrtFAccNT WTrtFAss WTrtFAssNT WTrtCall WTrtStaticCall WTrtCallNT WTrtInitBlock WTrtBlock WTrtSeq WTrtCond WTrtWhile WTrtThrow WTrtNil WTrtCons, consumes 1] subsection‹The theorem ‹progress›› lemma mdc_leq_dyn_type: "P,E,h ⊢ e : T ⟹ ∀C a Cs D S. T = Class C ∧ e = ref(a,Cs) ∧ h a = Some(D,S) ⟶ P ⊢ D ≼⇧^{*}C" and "P,E,h ⊢ es [:] Ts ⟹ ∀T Ts' e es' C a Cs D S. Ts = T#Ts' ∧ es = e#es' ∧ T = Class C ∧ e = ref(a,Cs) ∧ h a = Some(D,S) ⟶ P ⊢ D ≼⇧^{*}C" proof (induct rule:WTrt_inducts2) case (WTrtVal h v T E) have type:"P ⊢ typeof⇘_{h}⇙ v = Some T" by fact { fix C a Cs D S assume "T = Class C" and "Val v = ref(a,Cs)" and "h a = Some(D,S)" with type have "Subobjs P D Cs" and "C = last Cs" by (auto split:if_split_asm) hence "P ⊢ D ≼⇧^{*}C" by simp (rule Subobjs_subclass) } thus ?case by blast qed auto lemma appendPath_append_last: assumes notempty:"Ds ≠ []" shows"(Cs @⇩_{p}Ds) @⇩_{p}[last Ds] = (Cs @⇩_{p}Ds)" proof - have "last Cs = hd Ds ⟹ last (Cs @ tl Ds) = last Ds" proof(cases "tl Ds = []") case True assume last:"last Cs = hd Ds" with True notempty have "Ds = [last Cs]" by (fastforce dest:hd_Cons_tl) hence "last Ds = last Cs" by simp with True show ?thesis by simp next case False assume last:"last Cs = hd Ds" from notempty False have "last (tl Ds) = last Ds" by -(drule hd_Cons_tl,drule_tac x="hd Ds" in last_ConsR,simp) with False show ?thesis by simp qed thus ?thesis by(simp add:appendPath_def) qed theorem assumes wf: "wwf_prog P" shows progress: "P,E,h ⊢ e : T ⟹ (⋀l. ⟦ P ⊢ h √; P ⊢ E √; 𝒟 e ⌊dom l⌋; ¬ final e ⟧ ⟹ ∃e' s'. P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩)" and "P,E,h ⊢ es [:] Ts ⟹ (⋀l. ⟦ P ⊢ h √; P ⊢ E √; 𝒟s es ⌊dom l⌋; ¬ finals es ⟧ ⟹ ∃es' s'. P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',s'⟩)" proof (induct rule:WTrt_inducts2) case (WTrtNew C E h) show ?case proof cases assume "∃a. h a = None" with WTrtNew show ?thesis by (fastforce del:exE intro!:RedNew simp:new_Addr_def) next assume "¬(∃a. h a = None)" with WTrtNew show ?thesis by(fastforce intro:RedNewFail simp add:new_Addr_def) qed next case (WTrtDynCast C E h e T) have wte: "P,E,h ⊢ e : T" and refT: "is_refT T" and "class": "is_class P C" and IH: "⋀l. ⟦P ⊢ h √; P ⊢ E √; 𝒟 e ⌊dom l⌋; ¬ final e⟧ ⟹ ∃e' s'. P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩" and D: "𝒟 (Cast C e) ⌊dom l⌋" and hconf: "P ⊢ h √" and envconf:"P ⊢ E √" by fact+ from D have De: "𝒟 e ⌊dom l⌋" by auto show ?case proof cases assume "final e" with wte refT show ?thesis proof (rule finalRefE) assume "e = null" thus ?case by(fastforce intro:RedDynCastNull) next fix r assume "e = ref r" then obtain a Cs where ref:"e = ref(a,Cs)" by (cases r) auto with wte obtain D S where h:"h a = Some(D,S)" by auto show ?thesis proof (cases "P ⊢ Path D to C unique") case True then obtain Cs' where path:"P ⊢ Path D to C via Cs'" by (fastforce simp:path_via_def path_unique_def) then obtain Ds where "Ds = appendPath Cs Cs'" by simp with h path True ref show ?thesis by (fastforce intro:RedDynCast) next case False hence path_not_unique:"¬ P ⊢ Path D to C unique" . show ?thesis proof(cases "P ⊢ Path last Cs to C unique") case True then obtain Cs' where "P ⊢ Path last Cs to C via Cs'" by(auto simp:path_via_def path_unique_def) with True ref show ?thesis by(fastforce intro:RedStaticUpDynCast) next case False hence path_not_unique':"¬ P ⊢ Path last Cs to C unique" . thus ?thesis proof(cases "C ∉ set Cs") case False then obtain Ds Ds' where "Cs = Ds@[C]@Ds'" by (auto simp:in_set_conv_decomp) with ref show ?thesis by(fastforce intro:RedStaticDownDynCast) next case True with path_not_unique path_not_unique' h ref show ?thesis by (fastforce intro:RedDynCastFail) qed qed qed next fix r assume "e = Throw r" thus ?thesis by(blast intro!:red_reds.DynCastThrow) qed next assume nf: "¬ final e" from IH[OF hconf envconf De nf] show ?thesis by (blast intro:DynCastRed) qed next case (WTrtStaticCast C E h e T) have wte: "P,E,h ⊢ e : T" and refT: "is_refT T" and "class": "is_class P C" and IH: "⋀l. ⟦P ⊢ h √; P ⊢ E √; 𝒟 e ⌊dom l⌋; ¬ final e⟧ ⟹ ∃e' s'. P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩" and D: "𝒟 (⦇C⦈e) ⌊dom l⌋" and hconf: "P ⊢ h √" and envconf:"P ⊢ E √" by fact+ from D have De: "𝒟 e ⌊dom l⌋" by auto show ?case proof cases assume "final e" with wte refT show ?thesis proof (rule finalRefE) assume "e = null" with "class" show ?case by(fastforce intro:RedStaticCastNull) next fix r assume "e = ref r" then obtain a Cs where ref:"e = ref(a,Cs)" by (cases r) auto with wte wf have "class":"is_class P (last Cs)" by (auto intro:Subobj_last_isClass split:if_split_asm) show ?thesis proof(cases "P ⊢ (last Cs) ≼⇧^{*}C") case True with "class" wf obtain Cs' where "P ⊢ Path last Cs to C via Cs'" by(fastforce dest:leq_implies_path) with True ref show ?thesis by(fastforce intro:RedStaticUpCast) next case False have notleq:"¬ P ⊢ last Cs ≼⇧^{*}C" by fact thus ?thesis proof(cases "C ∉ set Cs") case False then obtain Ds Ds' where "Cs = Ds@[C]@Ds'" by (auto simp:in_set_conv_decomp) with ref show ?thesis by(fastforce intro:RedStaticDownCast) next case True with ref notleq show ?thesis by (fastforce intro:RedStaticCastFail) qed qed next fix r assume "e = Throw r" thus ?thesis by(blast intro!:red_reds.StaticCastThrow) qed next assume nf: "¬ final e" from IH[OF hconf envconf De nf] show ?thesis by (blast intro:StaticCastRed) qed next case WTrtVal thus ?case by(simp add:final_def) next case WTrtVar thus ?case by(fastforce intro:RedVar simp:hyper_isin_def) next case (WTrtBinOp E h e1 T1 e2 T2 bop T') have bop:"case bop of Eq ⇒ T' = Boolean | Add ⇒ T1 = Integer ∧ T2 = Integer ∧ T' = Integer" and wte1:"P,E,h ⊢ e1 : T1" and wte2:"P,E,h ⊢ e2 : T2" by fact+ show ?case proof cases assume "final e1" thus ?thesis proof (rule finalE) fix v1 assume e1 [simp]:"e1 = Val v1" show ?thesis proof cases assume "final e2" thus ?thesis proof (rule finalE) fix v2 assume e2 [simp]:"e2 = Val v2" show ?thesis proof (cases bop) assume "bop = Eq" thus ?thesis using WTrtBinOp by(fastforce intro:RedBinOp) next assume Add:"bop = Add" with e1 e2 wte1 wte2 bop obtain i1 i2 where "v1 = Intg i1" and "v2 = Intg i2" by (auto dest!:typeof_Integer) with Add obtain v where "binop(bop,v1,v2) = Some v" by simp with e1 e2 show ?thesis by (fastforce intro:RedBinOp) qed next fix a assume "e2 = Throw a" thus ?thesis by(auto intro:red_reds.BinOpThrow2) qed next assume "¬ final e2" with WTrtBinOp show ?thesis by simp (fast intro!:BinOpRed2) qed next fix r assume "e1 = Throw r" thus ?thesis by simp (fast intro:red_reds.BinOpThrow1) qed next assume "¬ final e1" with WTrtBinOp show ?thesis by simp (fast intro:BinOpRed1) qed next case (WTrtLAss E h V T e T') have wte:"P,E,h ⊢ e : T'" and wtvar:"P,E,h ⊢ Var V : T" and sub:"P ⊢ T' ≤ T" and envconf:"P ⊢ E √" by fact+ from envconf wtvar have type:"is_type P T" by(auto simp:envconf_def) show ?case proof cases assume fin:"final e" from fin show ?case proof (rule finalE) fix v assume e:"e = Val v" from sub type wf show ?case proof(rule subE) assume eq:"T' = T" and "∀C. T' ≠ Class C" hence "P ⊢ T casts v to v" by simp(rule casts_prim) with wte wtvar eq e show ?thesis by(auto intro!:RedLAss) next fix C D assume T':"T' = Class C" and T:"T = Class D" and path_unique:"P ⊢ Path C to D unique" from wte e T' obtain a Cs where ref:"e = ref(a,Cs)" and last:"last Cs = C" by (auto dest!:typeof_Class_Subo) from path_unique obtain Cs' where path_via:"P ⊢ Path C to D via Cs'" by(auto simp:path_unique_def path_via_def) with last have "P ⊢ Class D casts Ref(a,Cs) to Ref(a,Cs@⇩_{p}Cs')" by (fastforce intro:casts_ref simp:path_via_def) with wte wtvar T ref show ?thesis by(auto intro!:RedLAss) next fix C assume T':"T' = NT" and T:"T = Class C" with wte e have null:"e = null" by auto have "P ⊢ Class C casts Null to Null" by -(rule casts_null) with wte wtvar T null show ?thesis by(auto intro!:RedLAss) qed next fix r assume "e = Throw r" thus ?thesis by(fastforce intro:red_reds.LAssThrow) qed next assume "¬ final e" with WTrtLAss show ?thesis by simp (fast intro:LAssRed) qed next case (WTrtFAcc E h e C Cs F T) have wte: "P,E,h ⊢ e : Class C" and field: "P ⊢ C has least F:T via Cs" and notemptyCs:"Cs ≠ []" and hconf: "P ⊢ h √" by fact+ show ?case proof cases assume "final e" with wte show ?thesis proof (rule final_refE) fix r assume e: "e = ref r" then obtain a Cs' where ref:"e = ref(a,Cs')" by (cases r) auto with wte obtain D S where h:"h a = Some(D,S)" and suboD:"Subobjs P D Cs'" and last:"last Cs' = C" by (fastforce split:if_split_asm) from field obtain Bs fs ms where "class": "class P (last Cs) = Some(Bs,fs,ms)" and fs:"map_of fs F = Some T" by (fastforce simp:LeastFieldDecl_def FieldDecls_def) obtain Ds where Ds:"Ds = Cs'@⇩_{p}Cs" by simp with notemptyCs "class" have class':"class P (last Ds) = Some(Bs,fs,ms)" by (drule_tac Cs'="Cs'" in appendPath_last) simp from field suboD last Ds wf have subo:"Subobjs P D Ds" by(fastforce intro:Subobjs_appendPath simp:LeastFieldDecl_def FieldDecls_def) with hconf h have "P,h ⊢ (D,S) √" by (auto simp:hconf_def) with class' subo obtain fs' where S:"(Ds,fs') ∈ S" and "P,h ⊢ fs' (:≤) map_of fs" apply (auto simp:oconf_def) apply (erule_tac x="Ds" in allE) apply auto apply (erule_tac x="Ds" in allE) apply (erule_tac x="fs'" in allE) apply auto done with fs obtain v where "fs' F = Some v" by (fastforce simp:fconf_def) with h last Ds S have "P,E ⊢ ⟨(ref (a,Cs'))∙F{Cs}, (h,l)⟩ → ⟨Val v,(h,l)⟩" by (fastforce intro:RedFAcc) with ref show ?thesis by blast next fix r assume "e = Throw r" thus ?thesis by(fastforce intro:red_reds.FAccThrow) qed next assume "¬ final e" with WTrtFAcc show ?thesis by(fastforce intro!:FAccRed) qed next case (WTrtFAccNT E h e F Cs T) show ?case proof cases assume "final e" ― ‹@{term e} is @{term null} or @{term throw}› with WTrtFAccNT show ?thesis by(fastforce simp:final_def intro: RedFAccNull red_reds.FAccThrow dest!:typeof_NT) next assume "¬ final e" ― ‹@{term e} reduces by IH› with WTrtFAccNT show ?thesis by simp (fast intro:FAccRed) qed next case (WTrtFAss E h e⇩_{1}C Cs F T e⇩_{2}T') have wte1:"P,E,h ⊢ e⇩_{1}: Class C" and wte2:"P,E,h ⊢ e⇩_{2}: T'" and field:"P ⊢ C has least F:T via Cs" and notemptyCs:"Cs ≠ []" and sub:"P ⊢ T' ≤ T" and hconf:"P ⊢ h √" by fact+ from field wf have type:"is_type P T" by(rule least_field_is_type) show ?case proof cases assume "final e⇩_{1}" with wte1 show ?thesis proof (rule final_refE) fix r assume e1: "e⇩_{1}= ref r" show ?thesis proof cases assume "final e⇩_{2}" thus ?thesis proof (rule finalE) fix v assume e2:"e⇩_{2}= Val v" from e1 obtain a Cs' where ref:"e⇩_{1}= ref(a,Cs')" by (cases r) auto with wte1 obtain D S where h:"h a = Some(D,S)" and suboD:"Subobjs P D Cs'" and last:"last Cs' = C" by (fastforce split:if_split_asm) from field obtain Bs fs ms where "class": "class P (last Cs) = Some(Bs,fs,ms)" and fs:"map_of fs F = Some T" by (fastforce simp:LeastFieldDecl_def FieldDecls_def) obtain Ds where Ds:"Ds = Cs'@⇩_{p}Cs" by simp with notemptyCs "class" have class':"class P (last Ds) = Some(Bs,fs,ms)" by (drule_tac Cs'="Cs'" in appendPath_last) simp from field suboD last Ds wf have subo:"Subobjs P D Ds" by(fastforce intro:Subobjs_appendPath simp:LeastFieldDecl_def FieldDecls_def) with hconf h have "P,h ⊢ (D,S) √" by (auto simp:hconf_def) with class' subo obtain fs' where S:"(Ds,fs') ∈ S" by (auto simp:oconf_def) from sub type wf show ?thesis proof(rule subE) assume eq:"T' = T" and "∀C. T' ≠ Class C" hence "P ⊢ T casts v to v" by simp(rule casts_prim) with h last field Ds notemptyCs S eq have "P,E ⊢ ⟨(ref (a,Cs'))∙F{Cs}:=(Val v), (h,l)⟩ → ⟨Val v, (h(a ↦ (D,insert (Ds,fs'(F↦v)) (S - {(Ds,fs')}))),l)⟩" by (fastforce intro:RedFAss) with ref e2 show ?thesis by blast next fix C' D' assume T':"T' = Class C'" and T:"T = Class D'" and path_unique:"P ⊢ Path C' to D' unique" from wte2 e2 T' obtain a' Cs'' where ref2:"e⇩_{2}= ref(a',Cs'')" and last':"last Cs'' = C'" by (auto dest!:typeof_Class_Subo) from path_unique obtain Ds' where "P ⊢ Path C' to D' via Ds'" by(auto simp:path_via_def path_unique_def) with last' have casts:"P ⊢ Class D' casts Ref(a',Cs'') to Ref(a',Cs''@⇩_{p}Ds')" by (fastforce intro:casts_ref simp:path_via_def) obtain v' where "v' = Ref(a',Cs''@⇩_{p}Ds')" by simp with h last field Ds notemptyCs S ref e2 ref2 T casts have "P,E ⊢ ⟨(ref (a,Cs'))∙F{Cs}:=(Val v), (h,l)⟩ → ⟨Val v',(h(a ↦ (D,insert (Ds,fs'(F↦v'))(S-{(Ds,fs')}))),l)⟩" by (fastforce intro:RedFAss) with ref e2 show ?thesis by blast next fix C' assume T':"T' = NT" and T:"T = Class C'" from e2 wte2 T' have null:"e⇩_{2}= null" by auto have casts:"P ⊢ Class C' casts Null to Null" by -(rule casts_null) obtain v' where "v' = Null" by simp with h last field Ds notemptyCs S ref e2 null T casts have "P,E ⊢ ⟨(ref (a,Cs'))∙F{Cs}:=(Val v), (h,l)⟩ → ⟨Val v', (h(a ↦ (D,insert (Ds,fs'(F↦v')) (S - {(Ds,fs')}))),l)⟩" by (fastforce intro:RedFAss) with ref e2 show ?thesis by blast qed next fix r assume "e⇩_{2}= Throw r" thus ?thesis using e1 by(fastforce intro:red_reds.FAssThrow2) qed next assume "¬ final e⇩_{2}" with WTrtFAss e1 show ?thesis by simp (fast intro!:FAssRed2) qed next fix r assume "e⇩_{1}= Throw r" thus ?thesis by(fastforce intro:red_reds.FAssThrow1) qed next assume "¬ final e⇩_{1}" with WTrtFAss show ?thesis by simp (blast intro!:FAssRed1) qed next case (WTrtFAssNT E h e⇩_{1}e⇩_{2}T' T F Cs) show ?case proof cases assume e1: "final e⇩_{1}" ― ‹@{term e⇩_{1}} is @{term null} or @{term throw}› show ?thesis proof cases assume "final e⇩_{2}" ― ‹@{term e⇩_{2}} is @{term Val} or @{term throw}› with WTrtFAssNT e1 show ?thesis by(fastforce simp:final_def intro:RedFAssNull red_reds.FAssThrow1 red_reds.FAssThrow2 dest!:typeof_NT) next assume "¬ final e⇩_{2}" ― ‹@{term e⇩_{2}} reduces by IH› with WTrtFAssNT e1 show ?thesis by (fastforce simp:final_def intro!:red_reds.FAssRed2 red_reds.FAssThrow1) qed next assume "¬ final e⇩_{1}" ― ‹@{term e⇩_{1}} reduces by IH› with WTrtFAssNT show ?thesis by (fastforce intro:FAssRed1) qed next case (WTrtCall E h e C M Ts T pns body Cs es Ts') have wte: "P,E,h ⊢ e : Class C" and "method":"P ⊢ C has least M = (Ts, T, pns, body) via Cs" and wtes: "P,E,h ⊢ es [:] Ts'"and sub: "P ⊢ Ts' [≤] Ts" and IHes: "⋀l. ⟦P ⊢ h √; P ⊢ E √; 𝒟s es ⌊dom l⌋; ¬ finals es⟧ ⟹ ∃es' s'. P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',s'⟩" and hconf: "P ⊢ h √" and envconf:"P ⊢ E √" and D: "𝒟 (e∙M(es)) ⌊dom l⌋" by fact+ show ?case proof cases assume final:"final e" with wte show ?thesis proof (rule final_refE) fix r assume ref: "e = ref r" show ?thesis proof cases assume es: "∃vs. es = map Val vs" from ref obtain a Cs' where ref:"e = ref(a,Cs')" by (cases r) auto with wte obtain D S where h:"h a = Some(D,S)" and suboD:"Subobjs P D Cs'" and last:"last Cs' = C" by (fastforce split:if_split_asm) from wte ref h have subcls:"P ⊢ D ≼⇧^{*}C" by -(drule mdc_leq_dyn_type,auto) from "method" have has:"P ⊢ C has M = (Ts,T,pns,body) via Cs" by(rule has_least_method_has_method) from es obtain vs where vs:"es = map Val vs" by auto obtain Cs'' Ts'' T' pns' body' where ass:"P ⊢ (D,Cs'@⇩_{p}Cs) selects M = (Ts'',T',pns',body') via Cs'' ∧ length Ts'' = length pns' ∧ length vs = length pns' ∧ P ⊢ T' ≤ T" proof (cases "∃Ts'' T' pns' body' Ds. P ⊢ D has least M = (Ts'',T',pns',body') via Ds") case True then obtain Ts'' T' pns' body' Cs'' where least:"P ⊢ D has least M = (Ts'',T',pns',body') via Cs''" by auto hence select:"P ⊢ (D,Cs'@⇩_{p}Cs) selects M = (Ts'',T',pns',body') via Cs''" by(rule dyn_unique) from subcls least wf has have "Ts = Ts''" and leq:"P ⊢ T' ≤ T" by -(drule leq_method_subtypes,simp_all,blast)+ hence "length Ts = length Ts''" by (simp add:list_all2_iff) with sub have "length Ts' = length Ts''" by (simp add:list_all2_iff) with WTrts_same_length[OF wtes] vs have length:"length vs = length Ts''" by simp from has_least_wf_mdecl[OF wf least] have lengthParams:"length Ts'' = length pns'" by (simp add:wf_mdecl_def) with length have "length vs = length pns'" by simp with select lengthParams leq show ?thesis using that by blast next case False hence non_dyn:"∀Ts'' T' pns' body' Ds. ¬ P ⊢ D has least M = (Ts'',T',pns',body') via Ds" by auto from suboD last have path:"P ⊢ Path D to C via Cs'" by(simp add:path_via_def) from "method" have notempty:"Cs ≠ []" by(fastforce intro!:Subobjs_nonempty simp:LeastMethodDef_def MethodDefs_def) from suboD have "class": "is_class P D" by(rule Subobjs_isClass) from suboD last have path:"P ⊢ Path D to C via Cs'" by(simp add:path_via_def) with "method" wf have "P ⊢ D has M = (Ts,T,pns,body) via Cs'@⇩_{p}Cs" by(auto intro:has_path_has has_least_method_has_method) with "class" wf obtain Cs'' Ts'' T' pns' body' where overrider: "P ⊢ (D,Cs'@⇩_{p}Cs) has overrider M = (Ts'',T',pns',body') via Cs''" by(auto dest!:class_wf simp:is_class_def wf_cdecl_def,blast) with non_dyn have select:"P ⊢ (D,Cs'@⇩_{p}Cs) selects M = (Ts'',T',pns',body') via Cs''" by-(rule dyn_ambiguous,simp_all) from notempty have eq:"(Cs' @⇩_{p}Cs) @⇩_{p}[last Cs] = (Cs' @⇩_{p}Cs)" by(rule appendPath_append_last) from "method" wf have "P ⊢ last Cs has least M = (Ts,T,pns,body) via [last Cs]" by(auto dest:Subobj_last_isClass intro:Subobjs_Base subobjs_rel simp:LeastMethodDef_def MethodDefs_def) with notempty have "P ⊢ last(Cs'@⇩_{p}Cs) has least M = (Ts,T,pns,body) via [last Cs]" by -(drule_tac Cs'="Cs'" in appendPath_last,simp) with overrider wf eq have "(Cs'',(Ts'',T',pns',body')) ∈ MinimalMethodDefs P D M" and "P,D ⊢ Cs'' ⊑ Cs'@⇩_{p}Cs" by(auto simp:FinalOverriderMethodDef_def OverriderMethodDefs_def) (drule wf_sees_method_fun,auto) with subcls wf notempty has path have "Ts = Ts''" and leq:"P ⊢ T' ≤ T" by -(drule leq_methods_subtypes,simp_all,blast)+ hence "length Ts = length Ts''" by (simp add:list_all2_iff) with sub have "length Ts' = length Ts''" by (simp add:list_all2_iff) with WTrts_same_length[OF wtes] vs have length:"length vs = length Ts''" by simp from select_method_wf_mdecl[OF wf select] have lengthParams:"length Ts'' = length pns'" by (simp add:wf_mdecl_def) with length have "length vs = length pns'" by simp with select lengthParams leq show ?thesis using that by blast qed obtain new_body where "case T of Class D ⇒ new_body = ⦇D⦈blocks(this#pns',Class(last Cs'')#Ts'',Ref(a,Cs'')#vs,body') | _ ⇒ new_body = blocks(this#pns',Class(last Cs'')#Ts'',Ref(a,Cs'')#vs,body')" by(cases T) auto with h "method" last ass ref vs show ?thesis by (auto intro!:exI RedCall) next assume "¬(∃vs. es = map Val vs)" hence not_all_Val: "¬(∀e ∈ set es. ∃v. e = Val v)" by(simp add:ex_map_conv) let ?ves = "takeWhile (λe. ∃v. e = Val v) es" let ?rest = "dropWhile (λe. ∃v. e = Val v) es" let ?ex = "hd ?rest" let ?rst = "tl ?rest" from not_all_Val have nonempty: "?rest ≠ []" by auto hence es: "es = ?ves @ ?ex # ?rst" by simp have "∀e ∈ set ?ves. ∃v. e = Val v" by(fastforce dest:set_takeWhileD) then obtain vs where ves: "?ves = map Val vs" using ex_map_conv by blast show ?thesis proof cases assume "final ?ex" moreover from nonempty have "¬(∃v. ?ex = Val v)" by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv) (simp add:dropWhile_eq_Cons_conv) ultimately obtain r' where ex_Throw: "?ex = Throw r'" by(fast elim!:finalE) show ?thesis using ref es ex_Throw ves by(fastforce intro:red_reds.CallThrowParams) next assume not_fin: "¬ final ?ex" have "finals es = finals(?ves @ ?ex # ?rst)" using es by(rule arg_cong) also have "… = finals(?ex # ?rst)" using ves by simp finally have "finals es = finals(?ex # ?rst)" . hence "¬ finals es" using not_finals_ConsI[OF not_fin] by blast thus ?thesis using ref D IHes[OF hconf envconf] by(fastforce intro!:CallParams) qed qed next fix r assume "e = Throw r" with WTrtCall.prems show ?thesis by(fast intro!:red_reds.CallThrowObj) qed next assume "¬ final e" with WTrtCall show ?thesis by simp (blast intro!:CallObj) qed next case (WTrtStaticCall E h e C' C M Ts T pns body Cs es Ts') have 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, pns, body) via Cs" and wtes: "P,E,h ⊢ es [:] Ts'"and sub: "P ⊢ Ts' [≤] Ts" and IHes: "⋀l. ⟦P ⊢ h √; envconf P E; 𝒟s es ⌊dom l⌋; ¬ finals es⟧ ⟹ ∃es' s'. P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',s'⟩" and hconf: "P ⊢ h √" and envconf:"envconf P E" and D: "𝒟 (e∙(C::)M(es)) ⌊dom l⌋" by fact+ show ?case proof cases assume final:"final e" with wte show ?thesis proof (rule final_refE) fix r assume ref: "e = ref r" show ?thesis proof cases assume es: "∃vs. es = map Val vs" from ref obtain a Cs' where ref:"e = ref(a,Cs')" by (cases r) auto with wte have last:"last Cs' = C'" by (fastforce split:if_split_asm) with path_unique obtain Cs'' where path_via:"P ⊢ Path (last Cs') to C via Cs''" by (auto simp add:path_via_def path_unique_def) obtain Ds where Ds:"Ds = (Cs'@⇩_{p}Cs'')@⇩_{p}Cs" by simp from es obtain vs where vs:"es = map Val vs" by auto from sub have "length Ts' = length Ts" by (simp add:list_all2_iff) with WTrts_same_length[OF wtes] vs have length:"length vs = length Ts" by simp from has_least_wf_mdecl[OF wf "method"] have lengthParams:"length Ts = length pns" by (simp add:wf_mdecl_def) with "method" last path_unique path_via Ds length ref vs show ?thesis by (auto intro!:exI RedStaticCall) next assume "¬(∃vs. es = map Val vs)" hence not_all_Val: "¬(∀e ∈ set es. ∃v. e = Val v)" by(simp add:ex_map_conv) let ?ves = "takeWhile (λe. ∃v. e = Val v) es" let ?rest = "dropWhile (λe. ∃v. e = Val v) es" let ?ex = "hd ?rest" let ?rst = "tl ?rest" from not_all_Val have nonempty: "?rest ≠ []" by auto hence es: "es = ?ves @ ?ex # ?rst" by simp have "∀e ∈ set ?ves. ∃v. e = Val v" by(fastforce dest:set_takeWhileD) then obtain vs where ves: "?ves = map Val vs" using ex_map_conv by blast show ?thesis proof cases assume "final ?ex" moreover from nonempty have "¬(∃v. ?ex = Val v)" by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv) (simp add:dropWhile_eq_Cons_conv) ultimately obtain r' where ex_Throw: "?ex = Throw r'" by(fast elim!:finalE) show ?thesis using ref es ex_Throw ves by(fastforce intro:red_reds.CallThrowParams) next assume not_fin: "¬ final ?ex" have "finals es = finals(?ves @ ?ex # ?rst)" using es by(rule arg_cong) also have "… = finals(?ex # ?rst)" using ves by simp finally have "finals es = finals(?ex # ?rst)" . hence "¬ finals es" using not_finals_ConsI[OF not_fin] by blast thus ?thesis using ref D IHes[OF hconf envconf] by(fastforce intro!:CallParams) qed qed next fix r assume "e = Throw r" with WTrtStaticCall.prems show ?thesis by(fast intro!:red_reds.CallThrowObj) qed next assume "¬ final e" with WTrtStaticCall show ?thesis by simp (blast intro!:CallObj) qed next case (WTrtCallNT E h e es Ts Copt M T) show ?case proof cases assume "final e" moreover { fix v assume e: "e = Val v" hence "e = null" using WTrtCallNT by simp have ?case proof cases assume "finals es" moreover { fix vs assume "es = map Val vs" with WTrtCallNT e have ?thesis by(fastforce intro: RedCallNull dest!:typeof_NT) } moreover { fix vs a es' assume "es = map Val vs @ Throw a # es'" with WTrtCallNT e have ?thesis by(fastforce intro: CallThrowParams) } ultimately show ?thesis by(fastforce simp:finals_def) next assume "¬ finals es" ― ‹@{term es} reduces by IH› with WTrtCallNT e show ?thesis by(fastforce intro: CallParams) qed } moreover { fix r assume "e = Throw r" with WTrtCallNT have ?case by(fastforce intro: CallThrowObj) } ultimately show ?thesis by(fastforce simp:final_def) next assume "¬ final e" ― ‹@{term e} reduces by IH› with WTrtCallNT show ?thesis by (fastforce intro:CallObj) qed next case (WTrtInitBlock h v T' E V T e⇩_{2}T⇩_{2}) have IH2: "⋀l. ⟦P ⊢ h √; P ⊢ E(V ↦ T) √; 𝒟 e⇩_{2}⌊dom l⌋; ¬ final e⇩_{2}⟧ ⟹ ∃e' s'. P,E(V ↦ T) ⊢ ⟨e⇩_{2},(h,l)⟩ → ⟨e',s'⟩" and typeof:"P ⊢ typeof⇘_{h}⇙ v = Some T'" and type:"is_type P T" and sub:"P ⊢ T' ≤ T" and hconf: "P ⊢ h √" and envconf:"P ⊢ E √" and D: "𝒟 {V:T := Val v; e⇩_{2}} ⌊dom l⌋" by fact+ from wf typeof type sub obtain v' where casts:"P ⊢ T casts v to v'" by(auto dest:sub_casts) show ?case proof cases assume fin:"final e⇩_{2}" with casts show ?thesis by(fastforce elim:finalE intro:RedInitBlock red_reds.InitBlockThrow) next assume not_fin2: "¬ final e⇩_{2}" from D have D2: "𝒟 e⇩_{2}⌊dom(l(V↦v'))⌋" by (auto simp:hyperset_defs) from envconf type have "P ⊢ E(V ↦ T) √" by(auto simp:envconf_def) from IH2[OF hconf this D2 not_fin2] obtain h' l' e' where red2: "P,E(V ↦ T) ⊢ ⟨e⇩_{2},(h, l(V↦v'))⟩ → ⟨e',(h', l')⟩" by auto from red_lcl_incr[OF red2] have "V ∈ dom l'" by auto with red2 casts show ?thesis by(fastforce intro:InitBlockRed) qed next case (WTrtBlock E V T h e T') have IH: "⋀l. ⟦P ⊢ h √; P ⊢ E(V ↦ T) √; 𝒟 e ⌊dom l⌋; ¬ final e⟧ ⟹ ∃e' s'. P,E(V ↦ T) ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩" and unass: "¬ assigned V e" and type:"is_type P T" and hconf: "P ⊢ h √" and envconf:"P ⊢ E √" and D: "𝒟 {V:T; e} ⌊dom l⌋" by fact+ show ?case proof cases assume "final e" thus ?thesis proof (rule finalE) fix v assume "e = Val v" with type show ?thesis by(fast intro:RedBlock) next fix r assume "e = Throw r" with type show ?thesis by(fast intro:red_reds.BlockThrow) qed next assume not_fin: "¬ final e" from D have De: "𝒟 e ⌊dom(l(V:=None))⌋" by(simp add:hyperset_defs) from envconf type have "P ⊢ E(V ↦ T) √" by(auto simp:envconf_def) from IH[OF hconf this De not_fin] obtain h' l' e' where red: "P,E(V ↦ T) ⊢ ⟨e,(h,l(V:=None))⟩ → ⟨e',(h',l')⟩" by auto show ?thesis proof (cases "l' V") assume "l' V = None" with red unass show ?thesis by(blast intro: BlockRedNone) next fix v assume "l' V = Some v" with red unass type show ?thesis by(blast intro: BlockRedSome) qed qed next case (WTrtSeq E h e⇩_{1}T⇩_{1}e⇩_{2}T⇩_{2}) show ?case proof cases assume "final e⇩_{1}" thus ?thesis by(fast elim:finalE intro:intro:RedSeq red_reds.SeqThrow) next assume "¬ final e⇩_{1}" with WTrtSeq show ?thesis by simp (blast intro:SeqRed) qed next case (WTrtCond E h e e⇩_{1}T e⇩_{2}) have wt: "P,E,h ⊢ e : Boolean" by fact show ?case proof cases assume "final e" thus ?thesis proof (rule finalE) fix v assume val: "e = Val v" then obtain b where v: "v = Bool b" using wt by (fastforce dest:typeof_Boolean) show ?thesis proof (cases b) case True with val v show ?thesis by(auto intro:RedCondT) next case False with val v show ?thesis by(auto intro:RedCondF) qed next fix r assume "e = Throw r" thus ?thesis by(fast intro:red_reds.CondThrow) qed next assume "¬ final e" with WTrtCond show ?thesis by simp (fast intro:CondRed) qed next case WTrtWhile show ?case by(fast intro:RedWhile) next case (WTrtThrow E h e T' T) show ?case proof cases assume "final e" ― ‹Then @{term e} must be @{term throw} or @{term null}› with WTrtThrow show ?thesis by(fastforce simp:final_def is_refT_def intro:red_reds.ThrowThrow red_reds.RedThrowNull dest!:typeof_NT typeof_Class_Subo) next assume "¬ final e" ― ‹Then @{term e} must reduce› with WTrtThrow show ?thesis by simp (blast intro:ThrowRed) qed next case WTrtNil thus ?case by simp next case (WTrtCons E h e T es Ts) have IHe: "⋀l. ⟦P ⊢ h √; P ⊢ E √; 𝒟 e ⌊dom l⌋; ¬ final e⟧ ⟹ ∃e' s'. P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩" and IHes: "⋀l. ⟦P ⊢ h √; P ⊢ E √; 𝒟s es ⌊dom l⌋; ¬ finals es⟧ ⟹ ∃es' s'. P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',s'⟩" and hconf: "P ⊢ h √" and envconf:"P ⊢ E √" and D: "𝒟s (e#es) ⌊dom l⌋" and not_fins: "¬ finals(e # es)" by fact+ have De: "𝒟 e ⌊dom l⌋" and Des: "𝒟s es (⌊dom l⌋ ⊔ 𝒜 e)" using D by auto show ?case proof cases assume "final e" thus ?thesis proof (rule finalE) fix v assume e: "e = Val v" hence Des': "𝒟s es ⌊dom l⌋" using De Des by auto have not_fins_tl: "¬ finals es" using not_fins e by simp show ?thesis using e IHes[OF hconf envconf Des' not_fins_tl] by (blast intro!:ListRed2) next fix r assume "e = Throw r" hence False using not_fins by simp thus ?thesis .. qed next assume "¬ final e" from IHe[OF hconf envconf De this] show ?thesis by(fast intro!:ListRed1) qed qed end