# Theory Progress

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

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 (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@⇩pCs')"
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
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
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
next
assume "¬(∃a. h a = None)"
with WTrtNew show ?thesis
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
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@⇩pCs')"
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'@⇩pCs" 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'@⇩pCs" 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''@⇩pDs')"
by (fastforce intro:casts_ref simp:path_via_def)
obtain v' where "v' = Ref(a',Cs''@⇩pDs')" 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'@⇩pCs) 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'@⇩pCs) 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'"
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'"
with "method" wf have "P ⊢ D has M = (Ts,T,pns,body) via Cs'@⇩pCs"
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'@⇩pCs) 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'@⇩pCs) 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'@⇩pCs) 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'@⇩pCs"
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)"
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)
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''"
obtain Ds where Ds:"Ds = (Cs'@⇩pCs'')@⇩pCs" 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)"
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)
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
```