# Theory Determinism

```(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Determinism Proof›

theory Determinism
imports TypeSafe
begin

subsection‹Some lemmas›

lemma maps_nth:
"⟦(E(xs [↦] ys)) x = Some y; length xs = length ys; distinct xs⟧
⟹ ∀i. x = xs!i ∧ i < length xs ⟶ y = ys!i"
proof (induct xs arbitrary: ys E)
case Nil thus ?case by simp
next
case (Cons x' xs')
have map:"(E(x' # xs' [↦] ys)) x = Some y"
and length:"length (x'#xs') = length ys"
and dist:"distinct (x'#xs')"
and IH:"⋀ys E. ⟦(E(xs' [↦] ys)) x = Some y; length xs' = length ys;
distinct xs'⟧
⟹ ∀i. x = xs'!i ∧ i < length xs' ⟶ y = ys!i" by fact+
from length obtain y' ys' where ys:"ys = y'#ys'" by(cases ys) auto
{ fix i assume x:"x = (x'#xs')!i" and i:"i < length(x'#xs')"
have "y = ys!i"
proof(cases i)
case 0 with x map ys dist show ?thesis by simp
next
case (Suc n)
with x i have x':"x = xs'!n" and n:"n < length xs'" by simp_all
from map ys have map':"(E(x' ↦ y')(xs' [↦] ys')) x = Some y" by simp
from length ys have length':"length xs' = length ys'" by simp
from dist have dist':"distinct xs'" by simp
from IH[OF map' length' dist']
have "∀i. x = xs'!i ∧ i < length xs' ⟶ y = ys'!i" .
with x' n have "y = ys'!n" by simp
with ys n Suc show ?thesis by simp
qed }
thus ?case by simp
qed

lemma nth_maps:"⟦length pns = length Ts; distinct pns; i < length Ts⟧
⟹ (E(pns [↦] Ts)) (pns!i) = Some (Ts!i)"
proof (induct i arbitrary: E pns Ts)
case 0
have dist:"distinct pns" and length:"length pns = length Ts"
and i_length:"0 < length Ts" by fact+
from i_length obtain T' Ts' where Ts:"Ts = T'#Ts'" by(cases Ts) auto
with length obtain p' pns' where "pns = p'#pns'" by(cases pns) auto
with Ts dist show ?case by simp
next
case (Suc n)
have i_length:"Suc n < length Ts" and dist:"distinct pns"
and length:"length pns = length Ts" by fact+
from Suc obtain T' Ts' where Ts:"Ts = T'#Ts'" by(cases Ts) auto
with length obtain p' pns' where pns:"pns = p'#pns'" by(cases pns) auto
with Ts length dist have length':"length pns' = length Ts'"
and dist':"distinct pns'" and notin:"p' ∉ set pns'" by simp_all
from i_length Ts have n_length:"n < length Ts'" by simp
with length' dist' have map:"(E(p' ↦ T')(pns' [↦] Ts')) (pns'!n) = Some(Ts'!n)" by fact
with notin have "(E(p' ↦ T')(pns' [↦] Ts')) p' = Some T'" by simp
with pns Ts map show ?case by simp
qed

lemma casts_casts_eq_result:
fixes s :: state
assumes casts:"P ⊢ T casts v to v'" and casts':"P ⊢ T casts v to w'"
and type:"is_type P T" and wte:"P,E ⊢ e :: T'" and leq:"P ⊢ T' ≤ T"
and eval:"P,E ⊢ ⟨e,s⟩ ⇒ ⟨Val v,(h,l)⟩" and sconf:"P,E ⊢ s √"
and wf:"wf_C_prog P"
shows "v' = w'"
proof(cases "∀C. T ≠ Class C")
case True
with casts casts' show ?thesis
by(auto elim:casts_to.cases)
next
case False
then obtain C where T:"T = Class C" by auto
with type have "is_class P C" by simp
with wf T leq have "T' = NT ∨ (∃D. T' = Class D ∧ P ⊢ Path D to C unique)"
thus ?thesis
proof(rule disjE)
assume "T' = NT"
with wf eval sconf wte have "v = Null"
by(fastforce dest:eval_preserves_type)
with casts casts' show ?thesis by(fastforce elim:casts_to.cases)
next
assume "∃D. T' = Class D ∧ P ⊢ Path D to C unique"
then obtain D where T':"T' = Class D"
and path_unique:"P ⊢ Path D to C unique" by auto
with wf eval sconf wte
have "P,E,h ⊢ Val v : T' ∨ P,E,h ⊢ Val v : NT"
by(fastforce dest:eval_preserves_type)
thus ?thesis
proof(rule disjE)
assume "P,E,h ⊢ Val v : T'"
with T' obtain a Cs C' S where h:"h a = Some(C',S)" and v:"v = Ref(a,Cs)"
and last:"last Cs = D"
by(fastforce dest:typeof_Class_Subo)
from casts' v last T obtain Cs' Ds where "P ⊢ Path D to C via Cs'"
and "Ds = Cs@⇩pCs'" and "w' = Ref(a,Ds)"
by(auto elim:casts_to.cases)
with casts T v last path_unique show ?thesis
by auto(erule casts_to.cases,auto simp:path_via_def path_unique_def)
next
assume "P,E,h ⊢ Val v : NT"
with wf eval sconf wte have "v = Null"
by(fastforce dest:eval_preserves_type)
with casts casts' show ?thesis by(fastforce elim:casts_to.cases)
qed
qed
qed

lemma Casts_Casts_eq_result:
assumes wf:"wf_C_prog P"
shows "⟦P ⊢ Ts Casts vs to vs'; P ⊢ Ts Casts vs to ws'; ∀T ∈ set Ts. is_type P T;
P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts; P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs,(h,l)⟩;
P,E ⊢ s √⟧
⟹ vs' = ws'"
proof (induct vs arbitrary: vs' ws' Ts Ts' es s)
case Nil thus ?case by (auto elim!:Casts_to.cases)
next
case (Cons x xs)
have CastsCons:"P ⊢ Ts Casts x # xs to vs'"
and CastsCons':"P ⊢ Ts Casts x # xs to ws'"
and type:"∀T ∈ set Ts. is_type P T"
and wtes:"P,E ⊢ es [::] Ts'" and subs:"P ⊢ Ts' [≤] Ts"
and evals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val (x#xs),(h,l)⟩"
and sconf:"P,E ⊢ s √"
and IH:"⋀vs' ws' Ts Ts' es s.
⟦P ⊢ Ts Casts xs to vs'; P ⊢ Ts Casts xs to ws'; ∀T ∈ set Ts. is_type P T;
P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts; P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val xs,(h,l)⟩;
P,E ⊢ s √⟧
⟹ vs' = ws'" by fact+
from CastsCons obtain y ys S Ss where vs':"vs' = y#ys" and Ts:"Ts = S#Ss"
apply -
apply(frule length_Casts_vs,cases Ts,auto)
apply(frule length_Casts_vs',cases vs',auto)
done
with CastsCons have casts:"P ⊢ S casts x to y" and Casts:"P ⊢ Ss Casts xs to ys"
by(auto elim:Casts_to.cases)
from Ts type have type':"is_type P S" and types':"∀T ∈ set Ss. is_type P T"
by auto
from Ts CastsCons' obtain z zs where ws':"ws' = z#zs"
by simp(frule length_Casts_vs',cases ws',auto)
with Ts CastsCons' have casts':"P ⊢ S casts x to z"
and Casts':"P ⊢ Ss Casts xs to zs"
by(auto elim:Casts_to.cases)
from Ts subs obtain U Us where Ts':"Ts' = U#Us" and subs':"P ⊢ Us [≤] Ss"
and sub:"P ⊢ U ≤ S" by(cases Ts',auto simp:fun_of_def)
from wtes Ts' obtain e' es' where es:"es = e'#es'" and wte':"P,E ⊢ e' :: U"
and wtes':"P,E ⊢ es' [::] Us" by(cases es) auto
with evals obtain h' l' where eval:"P,E ⊢ ⟨e',s⟩ ⇒ ⟨Val x,(h',l')⟩"
and evals':"P,E ⊢ ⟨es',(h',l')⟩ [⇒] ⟨map Val xs,(h,l)⟩"
by (auto elim:evals.cases)
from wf eval wte' sconf have "P,E ⊢ (h',l') √" by(rule eval_preserves_sconf)
from IH[OF Casts Casts' types' wtes' subs' evals' this] have eq:"ys = zs" .
from casts casts' type' wte' sub eval sconf wf have "y = z"
by(rule casts_casts_eq_result)
with eq vs' ws' show ?case by simp
qed

lemma Casts_conf: assumes wf: "wf_C_prog P"
shows "P ⊢ Ts Casts vs to vs' ⟹
(⋀es s Ts'. ⟦ P,E ⊢ es [::] Ts'; P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs,(h,l)⟩; P,E ⊢ s √;
P ⊢ Ts' [≤] Ts⟧ ⟹
∀i < length Ts. P,h ⊢ vs'!i :≤ Ts!i)"
proof(induct rule:Casts_to.induct)
case Casts_Nil thus ?case by simp
next
case (Casts_Cons T v v' Ts vs vs')
have casts:"P ⊢ T casts v to v'" and wtes:"P,E ⊢ es [::] Ts'"
and evals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val (v#vs),(h,l)⟩"
and subs:"P ⊢ Ts' [≤] (T#Ts)" and sconf:"P,E ⊢ s √"
and IH:"⋀es s Ts'.⟦P,E ⊢ es [::] Ts'; P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs,(h,l)⟩;
P,E ⊢ s √; P ⊢ Ts' [≤] Ts⟧
⟹ ∀i<length Ts. P,h ⊢ vs' ! i :≤ Ts ! i" by fact+
from subs obtain U Us where Ts':"Ts' = U#Us" by(cases Ts') auto
with subs have sub':"P ⊢ U ≤ T" and subs':"P ⊢ Us [≤] Ts"
from wtes Ts' obtain e' es' where es:"es = e'#es'" by(cases es) auto
with Ts' wtes have wte':"P,E ⊢ e' :: U" and wtes':"P,E ⊢ es' [::] Us" by auto
from es evals obtain s' where eval':"P,E ⊢ ⟨e',s⟩ ⇒ ⟨Val v,s'⟩"
and evals':"P,E ⊢ ⟨es',s'⟩ [⇒] ⟨map Val vs,(h,l)⟩"
by(auto elim:evals.cases)
from wf eval' wte' sconf have sconf':"P,E ⊢ s' √" by(rule eval_preserves_sconf)
from evals' have hext:"hp s' ⊴ h" by(cases s',auto intro:evals_hext)
from wf eval' sconf wte' have "P,E,(hp s') ⊢ Val v :⇘NT⇙ U"
by(rule eval_preserves_type)
with hext have wtrt:"P,E,h ⊢ Val v :⇘NT⇙ U"
by(cases U,auto intro:hext_typeof_mono)
from casts wtrt sub' have "P,h ⊢ v' :≤ T"
proof(induct rule:casts_to.induct)
case (casts_prim T'' v'')
have "∀C. T'' ≠ Class C" and "P,E,h ⊢ Val v'' :⇘NT⇙ U" and "P ⊢ U ≤ T''" by fact+
thus ?case by(cases T'') auto
next
case (casts_null C) thus ?case by simp
next
case (casts_ref Cs C Cs' Ds a)
have path:"P ⊢ Path last Cs to C via Cs'"
and Ds:"Ds = Cs @⇩p Cs'"
and wtref:"P,E,h ⊢ ref (a, Cs) :⇘NT⇙ U" by fact+
from wtref obtain D S where subo:"Subobjs P D Cs" and h:"h a = Some(D,S)"
by(cases U,auto split:if_split_asm)
from path Ds have last:"C = last Ds"
by(fastforce intro!:appendPath_last Subobjs_nonempty simp:path_via_def)
from subo path Ds wf have "Subobjs P D Ds"
by(fastforce intro:Subobjs_appendPath simp:path_via_def)
with last h show ?case by simp
qed
with IH[OF wtes' evals' sconf' subs'] show ?case
by(auto simp:nth_Cons,case_tac i,auto)
qed

lemma map_Val_throw_False:"map Val vs = map Val ws @ throw ex # es ⟹ False"
proof (induct vs arbitrary: ws)
case Nil thus ?case by simp
next
case (Cons v' vs')
have eq:"map Val (v'#vs') = map Val ws @ throw ex # es"
and IH:"⋀ws'. map Val vs' = map Val ws' @ throw ex # es ⟹ False" by fact+
from eq obtain w' ws' where ws:"ws = w'#ws'" by(cases ws) auto
from eq have "tl(map Val (v'#vs')) = tl(map Val ws @ throw ex # es)" by simp
hence "map Val vs' = tl(map Val ws @ throw ex # es)" by simp
with ws have "map Val vs' = map Val ws' @ throw ex # es" by simp
from IH[OF this] show ?case .
qed

lemma map_Val_throw_eq:"map Val vs @ throw ex # es = map Val ws @ throw ex' # es'
⟹ vs = ws ∧ ex = ex' ∧ es = es'"
apply(clarsimp simp:append_eq_append_conv2)
apply(erule disjE)
apply(case_tac us)
apply(fastforce elim:map_injective simp:inj_on_def)
apply(fastforce dest:map_Val_throw_False)
apply(case_tac us)
apply(fastforce elim:map_injective simp:inj_on_def)
apply(fastforce dest:sym[THEN map_Val_throw_False])
done

subsection ‹The proof›

lemma deterministic_big_step:
assumes wf:"wf_C_prog P"
shows "P,E ⊢ ⟨e,s⟩ ⇒ ⟨e⇩1,s⇩1⟩ ⟹
(⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s √⟧
⟹ e⇩1 = e⇩2 ∧ s⇩1 = s⇩2)"
and "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es⇩1,s⇩1⟩ ⟹
(⋀es⇩2 s⇩2 Ts. ⟦P,E ⊢ ⟨es,s⟩ [⇒] ⟨es⇩2,s⇩2⟩; P,E ⊢ es [::] Ts; P,E ⊢ s √⟧
⟹ es⇩1 = es⇩2 ∧ s⇩1 = s⇩2)"
proof (induct rule:eval_evals.inducts)
case New thus ?case by(auto elim: eval_cases)
next
case NewFail thus ?case by(auto elim: eval_cases)
next
case (StaticUpCast E e s⇩0 a Cs s⇩1 C Cs' Ds e⇩2 s⇩2)
have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and path_via:"P ⊢ Path last Cs to C via Cs'" and Ds:"Ds = Cs @⇩p Cs'"
and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref (a,Cs) = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where "class":"is_class P C" and wte:"P,E ⊢ e :: Class D"
and disj:"P ⊢ Path D to C unique ∨
(P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs ⟶ Subobjs⇩R P C Cs))"
by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩"
and path_via':"P ⊢ Path last Xs to C via Xs'"
and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
with wf eval_ref sconf wte have last:"last Cs = D"
by(auto dest:eval_preserves_type split:if_split_asm)
from disj show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2"
proof (rule disjE)
assume "P ⊢ Path D to C unique"
with path_via path_via' eq last have "Cs' = Xs'"
with eq ref Ds show ?thesis by simp
next
assume "P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs  ⟶ Subobjs⇩R P C Cs)"
with "class" wf obtain Cs'' where "P ⊢ Path C to D via Cs''"
by(auto dest:leq_implies_path)
with path_via path_via' wf eq last have "Cs' = Xs'"
by(auto dest:path_via_reverse)
with eq ref Ds show ?thesis by simp
qed
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
and ref:"e⇩2 = ref (a',Xs@[C])"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs@C#Xs' ∧ s⇩1 = s⇩2" by simp
with wf eval_ref sconf wte obtain C' where
last:"last Cs = D" and "Subobjs P C' (Xs@C#Xs')"
by(auto dest:eval_preserves_type split:if_split_asm)
hence subo:"Subobjs P C (C#Xs')" by(fastforce intro:Subobjs_Subobjs)
with eq last have leq:"P ⊢ C ≼⇧* D" by(fastforce dest:Subobjs_subclass)
from path_via last have "P ⊢ D ≼⇧* C"
by(auto dest:Subobjs_subclass simp:path_via_def)
with leq wf have CeqD:"C = D" by(rule subcls_asym2)
with last path_via wf have "Cs' = [D]" by(fastforce intro:path_via_C)
with Ds last have Ds':"Ds = Cs" by(simp add:appendPath_def)
from subo CeqD last eq wf have "Xs' = []" by(auto dest:mdc_eq_last)
with eq Ds' ref show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩" and notin:"C ∉ set Xs"
and notleq:"¬ P ⊢ last Xs ≼⇧* C" and throw:"e⇩2 = THROW ClassCast"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
with wf eval_ref sconf wte have last:"last Cs = D" and notempty:"Cs ≠ []"
by(auto dest!:eval_preserves_type Subobjs_nonempty split:if_split_asm)
from disj have "C = D"
proof(rule disjE)
assume path_unique:"P ⊢ Path D to C unique"
with last have "P ⊢ D ≼⇧* C"
by(fastforce dest:Subobjs_subclass simp:path_unique_def)
with notleq last eq show ?thesis by simp
next
assume ass:"P ⊢ C ≼⇧* D ∧
(∀Cs. P ⊢ Path C to D via Cs  ⟶ Subobjs⇩R P C Cs)"
with "class" wf obtain Cs'' where path_via':"P ⊢ Path C to D via Cs''"
by(auto dest:leq_implies_path)
with path_via wf eq last have "Cs'' = [D]"
by(fastforce dest:path_via_reverse)
with ass path_via' have "Subobjs⇩R P C [D]" by simp
thus ?thesis by(fastforce dest:hd_SubobjsR)
qed
with last notin eq notempty show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2"
by(fastforce intro:last_in_set)
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (StaticDownCast E e s⇩0 a Cs C Cs' s⇩1 e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and eval':"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a,Cs@[C]@Cs'),s⇩1⟩"
and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref(a,Cs@[C]@Cs') = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where wte:"P,E ⊢ e :: Class D"
and disj:"P ⊢ Path D to C unique ∨
(P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs ⟶ Subobjs⇩R P C Cs))"
by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
and path_via:"P ⊢ Path last Xs to C via Xs'"
and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
by simp
with wf eval_ref sconf wte obtain C' where
last:"last(C#Cs') = D" and "Subobjs P C' (Cs@[C]@Cs')"
by(auto dest:eval_preserves_type split:if_split_asm)
hence "P ⊢ Path C to D via C#Cs'"
by(fastforce intro:Subobjs_Subobjs simp:path_via_def)
with eq last path_via wf have "Xs' = [C] ∧ Cs' = [] ∧ C = D"
apply clarsimp
apply(split if_split_asm)
by(simp,drule path_via_reverse,simp,simp)+
with ref eq show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by(fastforce simp:appendPath_def)
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
and ref:"e⇩2 = ref (a',Xs@[C])"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs@[C]@Cs' = Xs@C#Xs' ∧ s⇩1 = s⇩2"
by simp
with wf eval_ref sconf wte obtain C' where
last:"last(C#Xs') = D" and subo:"Subobjs P C' (Cs@[C]@Cs')"
by(auto dest:eval_preserves_type split:if_split_asm)
from subo wf have notin:"C ∉ set Cs" by -(rule unique2,simp)
from subo wf have "C ∉ set Cs'"  by -(rule unique1,simp,simp)
with notin eq have "Cs = Xs ∧ Cs' = Xs'"
by -(rule only_one_append,simp+)
with eq ref show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩" and notin:"C ∉ set Xs"
from IH[OF eval_ref wte sconf] have "a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
by simp
with notin show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by fastforce
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (StaticCastNull E e s⇩0 s⇩1 C e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ null = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩"
from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩" and "e⇩2 = null"
with IH[OF eval_null wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (StaticCastFail E e s⇩0 a Cs s⇩1 C e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and notleq:"¬ P ⊢ last Cs ≼⇧* C" and notin:"C ∉ set Cs"
and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ref (a, Cs) = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩"
and path_via:"P ⊢ Path last Xs to C via Xs'"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
with path_via wf have "P ⊢ last Cs ≼⇧* C"
by(auto dest:Subobjs_subclass simp:path_via_def)
with notleq show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
from IH[OF eval_ref wte sconf] have "a = a' ∧ Cs = Xs@C#Xs' ∧ s⇩1 = s⇩2" by simp
with notin show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
and throw:"e⇩2 = THROW ClassCast"
from IH[OF eval_ref wte sconf] have "a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2"
by simp
with throw show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (StaticCastThrow E e s⇩0 e' s⇩1 C e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩"
from IH[OF eval_ref wte sconf] show " throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix e'' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e'',s⇩2⟩"
and throw:"e⇩2 = throw e''"
from IH[OF eval_throw wte sconf] throw show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (StaticUpDynCast E e s⇩0 a Cs s⇩1 C Cs' Ds e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and path_via:"P ⊢ Path last Cs to C via Cs'"
and path_unique:"P ⊢ Path last Cs to C unique"
and Ds:"Ds = Cs@⇩pCs'" and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref(a,Cs) = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩"
and path_via':"P ⊢ Path last Xs to C via Xs'"
and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
with wf eval_ref sconf wte have last:"last Cs = D"
by(auto dest:eval_preserves_type split:if_split_asm)
with path_unique path_via path_via' eq have "Xs' = Cs'"
by(fastforce simp:path_via_def path_unique_def)
with eq Ds ref show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
and ref:"e⇩2 = ref (a',Xs@[C])"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs@C#Xs' ∧ s⇩1 = s⇩2" by simp
with wf eval_ref sconf wte obtain C' where
last:"last Cs = D" and "Subobjs P C' (Xs@C#Xs')"
by(auto dest:eval_preserves_type split:if_split_asm)
hence "Subobjs P C (C#Xs')" by(fastforce intro:Subobjs_Subobjs)
with last eq have "P ⊢ Path C to D via C#Xs'"
with path_via wf last have "Xs' = [] ∧ Cs' = [C] ∧ C = D"
by(fastforce dest:path_via_reverse)
with eq Ds ref show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by (simp add:appendPath_def)
next
fix Xs Xs' D' S a' h l
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
and h:"h a' = Some(D',S)" and path_via':"P ⊢ Path D' to C via Xs'"
and path_unique':"P ⊢ Path D' to C unique" and s2:"s⇩2 = (h,l)"
and ref:"e⇩2 = ref(a',Xs')"
from IH[OF eval_ref wte sconf] s2 have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
with wf eval_ref sconf wte h have "last Cs = D"
and "Subobjs P D' Cs"
by(auto dest:eval_preserves_type split:if_split_asm)
with path_via wf have "P ⊢ Path D' to C via Cs@⇩pCs'"
by(fastforce intro:Subobjs_appendPath appendPath_last[THEN sym]
dest:Subobjs_nonempty simp:path_via_def)
with path_via' path_unique' Ds have "Xs' = Ds"
by(fastforce simp:path_via_def path_unique_def)
with eq ref show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs D' S a' h l
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
and not_unique:"¬ P ⊢ Path last Xs to C unique" and s2:"s⇩2 = (h,l)"
from IH[OF eval_ref wte sconf] s2 have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
with path_unique not_unique show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (StaticDownDynCast E e s⇩0 a Cs C Cs' s⇩1 e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref(a,Cs@[C]@Cs') = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
and path_via:"P ⊢ Path last Xs to C via Xs'"
and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
by simp
with wf eval_ref sconf wte obtain C' where
last:"last(C#Cs') = D" and "Subobjs P C' (Cs@[C]@Cs')"
by(auto dest:eval_preserves_type split:if_split_asm)
hence "P ⊢ Path C to D via C#Cs'"
by(fastforce intro:Subobjs_Subobjs simp:path_via_def)
with eq last path_via wf have "Xs' = [C] ∧ Cs' = [] ∧ C = D"
apply clarsimp
apply(split if_split_asm)
by(simp,drule path_via_reverse,simp,simp)+
with ref eq show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by(fastforce simp:appendPath_def)
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
and ref:"e⇩2 = ref (a',Xs@[C])"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs@[C]@Cs' = Xs@C#Xs' ∧ s⇩1 = s⇩2"
by simp
with wf eval_ref sconf wte obtain C' where
last:"last(C#Xs') = D" and subo:"Subobjs P C' (Cs@[C]@Cs')"
by(auto dest:eval_preserves_type split:if_split_asm)
from subo wf have notin:"C ∉ set Cs" by -(rule unique2,simp)
from subo wf have "C ∉ set Cs'"  by -(rule unique1,simp,simp)
with notin eq have "Cs = Xs ∧ Cs' = Xs'"
by -(rule only_one_append,simp+)
with eq ref show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' D' S a' h l
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
and h:"h a' = Some(D',S)" and path_via:"P ⊢ Path D' to C via Xs'"
and path_unique:"P ⊢ Path D' to C unique" and s2:"s⇩2 = (h,l)"
and ref:"e⇩2 = ref(a',Xs')"
from IH[OF eval_ref wte sconf] s2 have eq:"a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
by simp
with wf eval_ref sconf wte h have "Subobjs P D' (Cs@[C]@Cs')"
by(auto dest:eval_preserves_type split:if_split_asm)
hence "Subobjs P D' (Cs@[C])" by(fastforce intro:appendSubobj)
with path_via path_unique have "Xs' = Cs@[C]"
by(fastforce simp:path_via_def path_unique_def)
with eq ref show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs D' S a' h l
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
and notin:"C ∉ set Xs" and s2:"s⇩2 = (h,l)"
from IH[OF eval_ref wte sconf] s2 have "a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
by simp
with notin show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by fastforce
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (DynCast E e s⇩0 a Cs h l D S C Cs' e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and path_via:"P ⊢ Path D to C via Cs'" and path_unique:"P ⊢ Path D to C unique"
and h:"h a = Some(D,S)" and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref(a,Cs) = e⇩2 ∧ (h,l) = s⇩2" by fact+
from wt obtain D' where wte:"P,E ⊢ e :: Class D'" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
and path_via':"P ⊢ Path last Xs to C via Xs'"
and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ (h,l) = s⇩2" by simp
with wf eval_ref sconf wte h have "last Cs = D'"
and "Subobjs P D Cs"
by(auto dest:eval_preserves_type split:if_split_asm)
with path_via' wf eq have "P ⊢ Path D to C via Xs@⇩pXs'"
by(fastforce intro:Subobjs_appendPath appendPath_last[THEN sym]
dest:Subobjs_nonempty simp:path_via_def)
with path_via path_unique have "Cs' = Xs@⇩pXs'"
by(fastforce simp:path_via_def path_unique_def)
with ref eq show "ref(a,Cs') = e⇩2 ∧ (h, l) = s⇩2" by simp
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
and ref:"e⇩2 = ref (a',Xs@[C])"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs@C#Xs' ∧ (h,l) = s⇩2"
by simp
with wf eval_ref sconf wte h have "Subobjs P D (Xs@[C]@Xs')"
by(auto dest:eval_preserves_type split:if_split_asm)
hence "Subobjs P D (Xs@[C])" by(fastforce intro:appendSubobj)
with path_via path_unique have "Cs' = Xs@[C]"
by(fastforce simp:path_via_def path_unique_def)
with eq ref show "ref(a,Cs') = e⇩2 ∧ (h, l) = s⇩2" by simp
next
fix Xs Xs' D'' S' a' h' l'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
and h':"h' a' = Some(D'',S')" and path_via':"P ⊢ Path D'' to C via Xs'"
and s2:"s⇩2 = (h',l')" and ref:"e⇩2 = ref(a',Xs')"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ h = h' ∧ l = l'"
by simp
with h h' path_via path_via' path_unique s2 ref
show "ref(a,Cs') = e⇩2 ∧ (h,l) = s⇩2"
by(fastforce simp:path_via_def path_unique_def)
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "ref(a,Cs') = e⇩2 ∧ (h,l) = s⇩2" by simp
next
fix Xs D'' S' a' h' l'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
and h':"h' a' = Some(D'',S')" and not_unique:"¬ P ⊢ Path D'' to C unique"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ h = h' ∧ l = l'"
by simp
with h h' path_unique not_unique show "ref(a,Cs') = e⇩2 ∧ (h,l) = s⇩2" by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "ref (a,Cs') = e⇩2 ∧ (h,l) = s⇩2" by simp
qed
next
case (DynCastNull E e s⇩0 s⇩1 C e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ null = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩"
from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' D' S a' h l
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩" and "e⇩2 = null"
with IH[OF eval_null wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs D' S a' h l
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩" and s2:"s⇩2 = (h,l)"
from IH[OF eval_ref wte sconf] s2 show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (DynCastFail E e s⇩0 a Cs h l D S C e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and h:"h a = Some(D,S)" and not_unique1:"¬ P ⊢ Path D to C unique"
and not_unique2:"¬ P ⊢ Path last Cs to C unique" and notin:"C ∉ set Cs"
and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref (a, Cs) = e⇩2 ∧ (h,l) = s⇩2" by fact+
from wt obtain D' where wte:"P,E ⊢ e :: Class D'" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
and path_unique:"P ⊢ Path last Xs to C unique"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ (h,l) = s⇩2" by simp
with path_unique not_unique2 show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs@C#Xs' ∧ (h,l) = s⇩2"
by simp
with notin show "null = e⇩2 ∧ (h,l) = s⇩2" by fastforce
next
fix Xs Xs' D'' S' a' h' l'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
and h':"h' a' = Some(D'',S')" and path_unique:"P ⊢ Path D'' to C unique"
from IH[OF eval_ref wte sconf] have "a = a' ∧ Cs = Xs ∧ h = h' ∧ l = l'"
by simp
with h h' not_unique1 path_unique show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
next
fix Xs D'' S' a' h' l'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
and null:"e⇩2 = null" and s2:"s⇩2 = (h',l')"
from IH[OF eval_ref wte sconf] null s2 show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
qed
next
case (DynCastThrow E e s⇩0 e' s⇩1 C e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩"
from IH[OF eval_ref wte sconf] show " throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' a'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs Xs' D'' S' a' h' l'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix Xs D'' S' a' h' l'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix e'' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e'',s⇩2⟩"
and throw:"e⇩2 = throw e''"
from IH[OF eval_throw wte sconf] throw show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case Val thus ?case by(auto elim: eval_cases)
next
case (BinOp E e⇩1 s⇩0 v⇩1 s⇩1 e⇩2 v⇩2 s⇩2 bop v e⇩2' s⇩2' T)
have eval:"P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
and binop:"binop (bop, v⇩1, v⇩2) = Some v"
and wt:"P,E ⊢ e⇩1 «bop» e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
⟹ Val v⇩1 = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩2 :: T; P,E ⊢ s⇩1 √⟧
⟹ Val v⇩2 = ei ∧ s⇩2 = si" by fact+
from wt obtain T⇩1 T⇩2 where wte1:"P,E ⊢ e⇩1 :: T⇩1" and wte2:"P,E ⊢ e⇩2 :: T⇩2"
by auto
from eval show ?case
proof(rule eval_cases)
fix s w w⇩1 w⇩2
assume eval_val1:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w⇩1,s⟩"
and eval_val2:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨Val w⇩2,s⇩2'⟩"
and binop':"binop(bop,w⇩1,w⇩2) = Some w" and e2':"e⇩2' = Val w"
from IH1[OF eval_val1 wte1 sconf] have w1:"v⇩1 = w⇩1" and s:"s = s⇩1" by simp_all
with wf eval_val1 wte1 sconf have "P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_val2[simplified s] wte2 this] have "v⇩2 = w⇩2" and s2:"s⇩2 = s⇩2'"
by simp_all
with w1 binop binop' have "w = v" by simp
with e2' s2 show "Val v = e⇩2' ∧ s⇩2 = s⇩2'" by simp
next
fix e assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e,s⇩2'⟩"
from IH1[OF eval_throw wte1 sconf] show "Val v = e⇩2' ∧ s⇩2 = s⇩2'" by simp
next
fix e s w
assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and eval_throw:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨throw e,s⇩2'⟩"
from IH1[OF eval_val wte1 sconf] have s:"s = s⇩1" by simp_all
with wf eval_val wte1 sconf have "P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_throw[simplified s] wte2 this] show "Val v = e⇩2' ∧ s⇩2 = s⇩2'"
by simp
qed
next
case (BinOpThrow1 E e⇩1 s⇩0 e s⇩1 bop e⇩2 e⇩2' s⇩2 T)
have eval:"P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2⟩"
and wt:"P,E ⊢ e⇩1 «bop» e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e = ei ∧ s⇩1 = si" by fact+
from wt obtain T⇩1 T⇩2 where wte1:"P,E ⊢ e⇩1 :: T⇩1" by auto
from eval show ?case
proof(rule eval_cases)
fix s w w⇩1 w⇩2
assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w⇩1,s⟩"
from IH[OF eval_val wte1 sconf] show "throw e = e⇩2' ∧ s⇩1 = s⇩2" by simp
next
fix e'
assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩" and throw:"e⇩2' = throw e'"
from IH[OF eval_throw wte1 sconf] throw show "throw e = e⇩2' ∧ s⇩1 = s⇩2" by simp
next
fix e s w
assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
from IH[OF eval_val wte1 sconf] show "throw e = e⇩2' ∧ s⇩1 = s⇩2" by simp
qed
next
case (BinOpThrow2 E e⇩1 s⇩0 v⇩1 s⇩1 e⇩2 e s⇩2 bop e⇩2' s⇩2' T)
have eval:"P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
and wt:"P,E ⊢ e⇩1 «bop» e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
⟹ Val v⇩1 = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩2 :: T; P,E ⊢ s⇩1 √⟧
⟹ throw e = ei ∧ s⇩2 = si" by fact+
from wt obtain T⇩1 T⇩2 where wte1:"P,E ⊢ e⇩1 :: T⇩1" and wte2:"P,E ⊢ e⇩2 :: T⇩2"
by auto
from eval show ?case
proof(rule eval_cases)
fix s w w⇩1 w⇩2
assume eval_val1:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w⇩1,s⟩"
and eval_val2:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨Val w⇩2,s⇩2'⟩"
from IH1[OF eval_val1 wte1 sconf] have s:"s = s⇩1" by simp_all
with wf eval_val1 wte1 sconf have "P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_val2[simplified s] wte2 this] show "throw e = e⇩2' ∧ s⇩2 = s⇩2'"
by simp
next
fix e'
assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e',s⇩2'⟩"
from IH1[OF eval_throw wte1 sconf] show "throw e = e⇩2' ∧ s⇩2 = s⇩2'" by simp
next
fix e' s w
assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and eval_throw:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨throw e',s⇩2'⟩"
and throw:"e⇩2' = throw e'"
from IH1[OF eval_val wte1 sconf] have s:"s = s⇩1" by simp_all
with wf eval_val wte1 sconf have "P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_throw[simplified s] wte2 this] throw
show "throw e = e⇩2' ∧ s⇩2 = s⇩2'"
by simp
qed
next
case Var thus ?case by(auto elim: eval_cases)
next
case (LAss E e s⇩0 v h l V T v' l' e⇩2 s⇩2 T')
have eval:"P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and env:"E V = Some T" and casts:"P ⊢ T casts v to v'" and l':"l' = l(V ↦ v')"
and wt:"P,E ⊢ V:=e :: T'" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ Val v = e⇩2 ∧ (h,l) = s⇩2" by fact+
from wt env obtain T'' where wte:"P,E ⊢ e :: T''" and leq:"P ⊢ T'' ≤ T" by auto
from eval show ?case
proof(rule eval_cases)
fix U h' l'' w w'
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,(h',l'')⟩" and env':"E V = Some U"
and casts':"P ⊢ U casts w to w'" and e2:"e⇩2 = Val w'"
and s2:"s⇩2 = (h',l''(V ↦ w'))"
from env env' have UeqT:"U = T" by simp
from IH[OF eval_val wte sconf] have eq:"v = w ∧ h = h' ∧ l = l''" by simp
from sconf env have "is_type P T"
by(clarsimp simp:sconf_def envconf_def)
with casts casts' eq UeqT wte leq eval_val sconf wf have "v' = w'"
by(auto intro:casts_casts_eq_result)
with e2 s2 l' eq show "Val v' = e⇩2 ∧ (h, l') = s⇩2" by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "Val v' = e⇩2 ∧ (h, l') = s⇩2" by simp
qed
next
case (LAssThrow E e s⇩0 e' s⇩1 V e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ V:=e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain T'' where wte:"P,E ⊢ e :: T''" by auto
from eval show ?case
proof(rule eval_cases)
fix U h' l'' w w'
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,(h',l'')⟩"
from IH[OF eval_val wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex
assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2:"e⇩2 = throw ex"
from IH[OF eval_throw wte sconf] e2 show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (FAcc E e s⇩0 a Cs' h l D S Ds Cs fs F v e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and eval':"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a, Cs'),(h,l)⟩"
and h:"h a = Some(D,S)" and Ds:"Ds = Cs'@⇩pCs"
and S:"(Ds,fs) ∈ S" and fs:"fs F = Some v"
and wt:"P,E ⊢ e∙F{Cs} :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref (a, Cs') = e⇩2 ∧ (h,l) = s⇩2" by fact+
from wt obtain C where wte:"P,E ⊢ e :: Class C" by auto
from eval_preserves_sconf[OF wf eval' wte sconf] h have oconf:"P,h ⊢ (D,S) √"
from eval show ?case
proof(rule eval_cases)
fix Xs' D' S' a' fs' h' l' v'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs'),(h',l')⟩"
and h':"h' a' = Some(D',S')" and S':"(Xs'@⇩pCs,fs') ∈ S'"
and fs':"fs' F = Some v'" and e2:"e⇩2 = Val v'" and s2:"s⇩2 = (h',l')"
from IH[OF eval_ref wte sconf] h h'
have eq:"a = a' ∧ Cs' = Xs' ∧ h = h' ∧ l = l' ∧ D = D' ∧ S = S'" by simp
with oconf S S' Ds have "fs = fs'" by (auto simp:oconf_def)
with fs fs' have "v = v'" by simp
with e2 s2 eq show "Val v = e⇩2 ∧ (h,l) = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "Val v = e⇩2 ∧ (h,l) = s⇩2" by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "Val v = e⇩2 ∧ (h,l) = s⇩2" by simp
qed
next
case (FAccNull E e s⇩0 s⇩1 F Cs e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ e∙F{Cs} :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ null = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain C where wte:"P,E ⊢ e :: Class C" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs' D' S' a' fs' h' l' v'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs'),(h',l')⟩"
from IH[OF eval_ref wte sconf] show "THROW NullPointer = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩" and e2:"e⇩2 = THROW NullPointer"
from IH[OF eval_null wte sconf] e2 show "THROW NullPointer = e⇩2 ∧ s⇩1 = s⇩2"
by simp
next
fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
from IH[OF eval_throw wte sconf] show "THROW NullPointer = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (FAccThrow E e s⇩0 e' s⇩1 F Cs e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ e∙F{Cs} :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain C where wte:"P,E ⊢ e :: Class C" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs' D' S' a' fs' h' l' v'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs'),(h',l')⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex
assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2:"e⇩2 = throw ex"
from IH[OF eval_throw wte sconf] e2 show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (FAss E e⇩1 s⇩0 a Cs' s⇩1 e⇩2 v h⇩2 l⇩2 D S F T Cs v' Ds fs fs' S' h⇩2' e⇩2' s⇩2 T')
have eval:"P,E ⊢ ⟨e⇩1∙F{Cs} := e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2⟩"
and eval':"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ref(a,Cs'),s⇩1⟩"
and eval'':"P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,(h⇩2,l⇩2)⟩"
and h2:"h⇩2 a = Some(D, S)"
and has_least:"P ⊢ last Cs' has least F:T via Cs"
and casts:"P ⊢ T casts v to v'" and Ds:"Ds = Cs'@⇩pCs"
and S:"(Ds, fs) ∈ S" and fs':"fs' = fs(F ↦ v')"
and S':"S' = S - {(Ds, fs)} ∪ {(Ds, fs')}"
and h2':"h⇩2' = h⇩2(a ↦ (D, S'))"
and wt:"P,E ⊢ e⇩1∙F{Cs} := e⇩2 :: T'" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
⟹ ref(a,Cs') = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩2 :: T; P,E ⊢ s⇩1 √⟧
⟹ Val v = ei ∧ (h⇩2,l⇩2) = si" by fact+
from wt obtain C T'' where wte1:"P,E ⊢ e⇩1 :: Class C"
and has_least':"P ⊢ C has least F:T' via Cs"
and wte2:"P,E ⊢ e⇩2 :: T''" and leq:"P ⊢ T'' ≤ T'"
by auto
from wf eval' wte1 sconf have "last Cs' = C"
by(auto dest!:eval_preserves_type split:if_split_asm)
with has_least has_least' have TeqT':"T = T'" by (fastforce intro:sees_field_fun)
from eval show ?case
proof(rule eval_cases)
fix Xs D' S'' U a' fs'' h l s w w'
assume eval_ref:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
and eval_val:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨Val w,(h,l)⟩"
and h:"h a' = Some(D',S'')"
and has_least'':"P ⊢ last Xs has least F:U via Cs"
and casts':"P ⊢ U casts w to w'"
and S'':"(Xs@⇩pCs,fs'') ∈ S''" and e2':"e⇩2' = Val w'"
and s2:"s⇩2 = (h(a'↦(D',insert (Xs@⇩pCs,fs''(F ↦ w'))
(S''-{(Xs@⇩pCs,fs'')}))),l)"
from IH1[OF eval_ref wte1 sconf] have eq:"a = a' ∧ Cs' = Xs ∧ s⇩1 = s" by simp
with wf eval_ref wte1 sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF _ wte2 this] eval_val eq have eq':"v = w ∧ h = h⇩2 ∧ l = l⇩2" by auto
from has_least'' eq has_least have UeqT:"U = T" by (fastforce intro:sees_field_fun)
from has_least wf have "is_type P T" by(rule least_field_is_type)
with casts casts' eq eq' UeqT TeqT' wte2 leq eval_val sconf' wf have v':"v' = w'"
by(auto intro!:casts_casts_eq_result)
from eval_preserves_sconf[OF wf eval'' wte2 sconf'] h2
have oconf:"P,h⇩2 ⊢ (D,S) √"
from eq eq' h2 h have "S = S''" by simp
with oconf eq S S' S'' Ds have "fs = fs''" by (auto simp:oconf_def)
with h2' h h2 eq eq' s2 S' Ds fs' v' e2' show "Val v' = e⇩2' ∧ (h⇩2',l⇩2) = s⇩2"
by simp
next
fix s w assume eval_null:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨null,s⟩"
from IH1[OF eval_null wte1 sconf] show "Val v' = e⇩2' ∧ (h⇩2',l⇩2) = s⇩2" by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"
from IH1[OF eval_throw wte1 sconf] show "Val v' = e⇩2' ∧ (h⇩2',l⇩2) = s⇩2" by simp
next
fix ex s w
assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and eval_throw:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨throw ex,s⇩2⟩"
from IH1[OF eval_val wte1 sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte1 sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_throw[simplified eq] wte2 this]
show "Val v' = e⇩2' ∧ (h⇩2',l⇩2) = s⇩2" by simp
qed
next
case (FAssNull E e⇩1 s⇩0 s⇩1 e⇩2 v s⇩2 F Cs e⇩2' s⇩2' T)
have eval:"P,E ⊢ ⟨e⇩1∙F{Cs} := e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
and wt:"P,E ⊢ e⇩1∙F{Cs} := e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
⟹ null = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩2 :: T; P,E ⊢ s⇩1 √⟧
⟹ Val v = ei ∧ s⇩2 = si" by fact+
from wt obtain C T'' where wte1:"P,E ⊢ e⇩1 :: Class C"
and wte2:"P,E ⊢ e⇩2 :: T''" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs D' S'' U a' fs'' h l s w w'
assume eval_ref:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
from IH1[OF eval_ref wte1 sconf] show "THROW NullPointer = e⇩2' ∧ s⇩2 = s⇩2'"
by simp
next
fix s w
assume eval_null:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨null,s⟩"
and eval_val:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨Val w,s⇩2'⟩"
and e2':"e⇩2' = THROW NullPointer"
from IH1[OF eval_null wte1 sconf] have eq:"s = s⇩1" by simp
with wf eval_null wte1 sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_val[simplified eq] wte2 this] e2'
show "THROW NullPointer = e⇩2' ∧ s⇩2 = s⇩2'" by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_throw wte1 sconf] show "THROW NullPointer = e⇩2' ∧ s⇩2 = s⇩2'"
by simp
next
fix ex s w
assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and eval_throw:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_val wte1 sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte1 sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_throw[simplified eq] wte2 this]
show "THROW NullPointer = e⇩2' ∧ s⇩2 = s⇩2'" by simp
qed
next
case (FAssThrow1 E e⇩1 s⇩0 e' s⇩1 F Cs e⇩2 e⇩2' s⇩2 T)
have eval:"P,E ⊢ ⟨e⇩1∙F{Cs} := e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2⟩"
and wt:"P,E ⊢ e⇩1∙F{Cs} := e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = ei ∧ s⇩1 = si" by fact+
from wt obtain C T'' where wte1:"P,E ⊢ e⇩1 :: Class C" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs D' S'' U a' fs'' h l s w w'
assume eval_ref:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
from IH[OF eval_ref wte1 sconf] show "throw e' = e⇩2' ∧ s⇩1 = s⇩2" by simp
next
fix s w
assume eval_null:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨null,s⟩"
from IH[OF eval_null wte1 sconf] show "throw e' = e⇩2' ∧ s⇩1 = s⇩2" by simp
next
fix ex
assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2':"e⇩2' = throw ex"
from IH[OF eval_throw wte1 sconf] e2' show "throw e' = e⇩2' ∧ s⇩1 = s⇩2" by simp
next
fix ex s w assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
from IH[OF eval_val wte1 sconf] show "throw e' = e⇩2' ∧ s⇩1 = s⇩2" by simp
qed
next
case (FAssThrow2 E e⇩1 s⇩0 v s⇩1 e⇩2 e' s⇩2 F Cs e⇩2' s⇩2' T)
have eval:"P,E ⊢ ⟨e⇩1∙F{Cs} := e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
and wt:"P,E ⊢ e⇩1∙F{Cs} := e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
⟹ Val v = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩2 :: T; P,E ⊢ s⇩1 √⟧
⟹ throw e' = ei ∧ s⇩2 = si" by fact+
from wt obtain C T'' where wte1:"P,E ⊢ e⇩1 :: Class C"
and wte2:"P,E ⊢ e⇩2 :: T''" by auto
from eval show ?case
proof(rule eval_cases)
fix Xs D' S'' U a' fs'' h l s w w'
assume eval_ref:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
and eval_val:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨Val w,(h,l)⟩"
from IH1[OF eval_ref wte1 sconf] have eq:"s = s⇩1" by simp
with wf eval_ref wte1 sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_val[simplified eq] wte2 this] show "throw e' = e⇩2' ∧ s⇩2 = s⇩2'"
by simp
next
fix s w
assume eval_null:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨null,s⟩"
and eval_val:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨Val w,s⇩2'⟩"
from IH1[OF eval_null wte1 sconf] have eq:"s = s⇩1" by simp
with wf eval_null wte1 sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_val[simplified eq] wte2 this] show "throw e' = e⇩2' ∧ s⇩2 = s⇩2'"
by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_throw wte1 sconf] show "throw e' = e⇩2' ∧ s⇩2 = s⇩2'" by simp
next
fix ex s w
assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and eval_throw:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨throw ex,s⇩2'⟩" and e2':"e⇩2' = throw ex"
from IH1[OF eval_val wte1 sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte1 sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_throw[simplified eq] wte2 this] e2'
show "throw e' = e⇩2' ∧ s⇩2 = s⇩2'" by simp
qed
next
case (CallObjThrow E e s⇩0 e' s⇩1 Copt M es e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ Call e Copt M es :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt obtain C where wte:"P,E ⊢ e :: Class C" by(cases Copt)auto
show ?case
proof(cases Copt)
assume "Copt = None"
with eval have "P,E ⊢ ⟨e∙M(es),s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩" by simp
thus ?thesis
proof(rule eval_cases)
fix ex
assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2:"e⇩2 = throw ex"
from IH[OF eval_throw wte sconf] e2 show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix es' ex' s w ws assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
from IH[OF eval_val wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix C' Xs Xs' Ds' S' U U' Us Us' a' body'' body''' h h' l l' pns'' pns'''
s ws ws'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix s ws
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⟩"
from IH[OF eval_null wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
fix C' assume "Copt = Some C'"
with eval have "P,E ⊢ ⟨e∙(C'::)M(es),s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩" by simp
thus ?thesis
proof(rule eval_cases)
fix ex
assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2:"e⇩2 = throw ex"
from IH[OF eval_throw wte sconf] e2 show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix es' ex' s w ws assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
from IH[OF eval_val wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix C'' Xs Xs' Ds' S' U U' Us Us' a' body'' body''' h h' l l' pns'' pns'''
s ws ws'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix s ws
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⟩"
from IH[OF eval_null wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
qed
next
case (CallParamsThrow E e s⇩0 v s⇩1 es vs ex es' s⇩2 Copt M e⇩2 s⇩2' T)
have eval:"P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2'⟩"
and wt:"P,E ⊢ Call e Copt M es :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ Val v = ei ∧ s⇩1 = si"
and IH2:"⋀esi si Ts. ⟦P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨esi,si⟩; P,E ⊢ es [::] Ts; P,E ⊢ s⇩1 √⟧
⟹ map Val vs @ throw ex # es' = esi ∧ s⇩2 = si" by fact+
from wt obtain C Ts where wte:"P,E ⊢ e :: Class C" and wtes:"P,E ⊢ es [::] Ts"
by(cases Copt)auto
show ?case
proof(cases Copt)
assume "Copt = None"
with eval have "P,E ⊢ ⟨e∙M(es),s⇩0⟩ ⇒ ⟨e⇩2,s⇩2'⟩" by simp
thus ?thesis
proof(rule eval_cases)
fix ex' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex',s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "throw ex = e⇩2 ∧ s⇩2 = s⇩2'" by simp
next
fix es'' ex' s w ws
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and evals_throw:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws@throw ex'#es'',s⇩2'⟩"
and e2:"e⇩2 = throw ex'"
from IH1[OF eval_val wte sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_throw[simplified eq] wtes this] e2
have "vs = ws ∧ ex = ex' ∧ es' = es'' ∧ s⇩2 = s⇩2'"
by(fastforce dest:map_Val_throw_eq)
with e2 show "throw ex = e⇩2 ∧ s⇩2 = s⇩2'" by simp
next
fix C' Xs Xs' Ds' S' U U' Us Us' a' body'' body''' h h' l l' pns'' pns'''
s ws ws'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws,(h,l)⟩"
from IH1[OF eval_ref wte sconf] have eq:"s = s⇩1" by simp
with wf eval_ref wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified eq] wtes this]
show "throw ex = e⇩2 ∧ s⇩2 = s⇩2'"
by(fastforce dest:sym[THEN map_Val_throw_False])
next
fix s ws
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws,s⇩2'⟩"
and e2:"e⇩2 = THROW NullPointer"
from IH1[OF eval_null wte sconf] have eq:"s = s⇩1" by simp
with wf eval_null wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified eq] wtes this]
show "throw ex = e⇩2 ∧ s⇩2 = s⇩2'"
by(fastforce dest:sym[THEN map_Val_throw_False])
qed
next
fix C' assume "Copt = Some C'"
with eval have "P,E ⊢ ⟨e∙(C'::)M(es),s⇩0⟩ ⇒ ⟨e⇩2,s⇩2'⟩" by simp
thus ?thesis
proof(rule eval_cases)
fix ex' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex',s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "throw ex = e⇩2 ∧ s⇩2 = s⇩2'" by simp
next
fix es'' ex' s w ws
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and evals_throw:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws@throw ex'#es'',s⇩2'⟩"
and e2:"e⇩2 = throw ex'"
from IH1[OF eval_val wte sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_throw[simplified eq] wtes this] e2
have "vs = ws ∧ ex = ex' ∧ es' = es'' ∧ s⇩2 = s⇩2'"
by(fastforce dest:map_Val_throw_eq)
with e2 show "throw ex = e⇩2 ∧ s⇩2 = s⇩2'" by simp
next
fix C' Xs Xs' Ds' S' U U' Us Us' a' body'' body''' h h' l l' pns'' pns'''
s ws ws'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws,(h,l)⟩"
from IH1[OF eval_ref wte sconf] have eq:"s = s⇩1" by simp
with wf eval_ref wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified eq] wtes this]
show "throw ex = e⇩2 ∧ s⇩2 = s⇩2'"
by(fastforce dest:sym[THEN map_Val_throw_False])
next
fix s ws
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws,s⇩2'⟩"
and e2:"e⇩2 = THROW NullPointer"
from IH1[OF eval_null wte sconf] have eq:"s = s⇩1" by simp
with wf eval_null wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified eq] wtes this]
show "throw ex = e⇩2 ∧ s⇩2 = s⇩2'"
by(fastforce dest:sym[THEN map_Val_throw_False])
qed
qed
next
case (Call E e s⇩0 a Cs s⇩1 es vs h⇩2 l⇩2 C S M Ts' T' pns' body' Ds Ts T pns
body Cs' vs' l⇩2' new_body e' h⇩3 l⇩3 e⇩2 s⇩2 T'')
have eval:"P,E ⊢ ⟨e∙M(es),s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and eval':"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a,Cs),s⇩1⟩"
and eval'':"P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2)⟩" and h2:"h⇩2 a = Some(C,S)"
and has_least:"P ⊢ last Cs has least M = (Ts',T',pns',body') via Ds"
and selects:"P ⊢ (C,Cs@⇩pDs) selects M = (Ts,T,pns,body) via Cs'"
and length:"length vs = length pns" and Casts:"P ⊢ Ts Casts vs to vs'"
and l2':"l⇩2' = [this ↦ Ref (a, Cs'), pns [↦] vs']"
and new_body:"new_body = (case T' of Class D ⇒ ⦇D⦈body | _ ⇒ body)"
and eval_body:"P,E(this ↦ Class (last Cs'), pns [↦] Ts) ⊢
⟨new_body,(h⇩2,l⇩2')⟩ ⇒ ⟨e',(h⇩3,l⇩3)⟩"
and wt:"P,E ⊢ e∙M(es) :: T''" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref (a,Cs) = ei ∧ s⇩1 = si"
and IH2:"⋀esi si Ts. ⟦P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨esi,si⟩; P,E ⊢ es [::] Ts; P,E ⊢ s⇩1 √⟧
⟹ map Val vs = esi ∧ (h⇩2,l⇩2) = si"
and IH3:"⋀ei si T.
⟦P,E(this ↦ Class (last Cs'), pns [↦] Ts) ⊢ ⟨new_body,(h⇩2,l⇩2')⟩ ⇒ ⟨ei,si⟩;
P,E(this ↦ Class (last Cs'), pns [↦] Ts) ⊢ new_body :: T;
P,E(this ↦ Class (last Cs'), pns [↦] Ts) ⊢ (h⇩2,l⇩2') √⟧
⟹ e' = ei ∧ (h⇩3, l⇩3) = si" by fact+
from wt obtain D Ss Ss' m Cs'' where wte:"P,E ⊢ e :: Class D"
and has_least':"P ⊢ D has least M = (Ss,T'',m) via Cs''"
and wtes:"P,E ⊢ es [::] Ss'" and subs:"P ⊢ Ss' [≤] Ss" by auto
from eval_preserves_type[OF wf eval' sconf wte]
have last:"last Cs = D" by (auto split:if_split_asm)
with has_least has_least' wf
have eq:"Ts' = Ss ∧ T' = T'' ∧ (pns',body') = m ∧ Ds = Cs''"
by(fastforce dest:wf_sees_method_fun)
from wf selects have param_type:"∀T ∈ set Ts. is_type P T"
and return_type:"is_type P T" and TnotNT:"T ≠ NT"
by(auto dest:select_method_wf_mdecl simp:wf_mdecl_def)
from selects wf have subo:"Subobjs P C Cs'"
by(induct rule:SelectMethodDef.induct,
auto simp:FinalOverriderMethodDef_def OverriderMethodDefs_def
MinimalMethodDefs_def LeastMethodDef_def MethodDefs_def)
with wf have "class":"is_class P (last Cs')" by(auto intro!:Subobj_last_isClass)
from eval'' have hext:"hp s⇩1 ⊴ h⇩2" by (cases s⇩1,auto intro: evals_hext)
from wf eval' sconf wte last have "P,E,(hp s⇩1) ⊢ ref(a,Cs) :⇘NT⇙ Class(last Cs)"
by -(rule eval_preserves_type,simp_all)
with hext have "P,E,h⇩2 ⊢ ref(a,Cs) :⇘NT⇙ Class(last Cs)"
by(auto intro:WTrt_hext_mono dest:hext_objD split:if_split_asm)
with h2 have "Subobjs P C Cs" by (auto split:if_split_asm)
hence "P ⊢ Path C to (last Cs) via Cs"
by (auto simp:path_via_def split:if_split_asm)
with selects has_least wf have param_types:"Ts' = Ts ∧ P ⊢ T ≤ T'"
by -(rule select_least_methods_subtypes,simp_all)
from wf selects have wt_body:"P,[this↦Class(last Cs'),pns[↦]Ts] ⊢ body :: T"
and this_not_pns:"this ∉ set pns" and length:"length pns = length Ts"
and dist:"distinct pns"
by(auto dest!:select_method_wf_mdecl simp:wf_mdecl_def)
have "P,[this↦Class(last Cs'),pns[↦]Ts] ⊢ new_body :: T'"
proof(cases "∃C. T' = Class C")
case False with wt_body new_body param_types show ?thesis by(cases T') auto
next
case True
then obtain D' where T':"T' = Class D'" by auto
with wf has_least have "class":"is_class P D'"
by(fastforce dest:has_least_wf_mdecl simp:wf_mdecl_def)
with wf T' TnotNT param_types obtain D'' where T:"T = Class D''"
by(fastforce dest:widen_Class)
with wf return_type T' param_types have "P ⊢ Path D'' to D' unique"
with wt_body "class" T T' new_body show ?thesis by auto
qed
hence wt_new_body:"P,E(this↦Class(last Cs'),pns[↦]Ts) ⊢ new_body :: T'"
by(fastforce intro:wt_env_mono)
from eval show ?case
proof(rule eval_cases)
fix ex' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex',s⇩2⟩"
from IH1[OF eval_throw wte sconf] show "e' = e⇩2 ∧ (h⇩3, l⇩2) = s⇩2" by simp
next
fix es'' ex' s w ws
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and evals_throw:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws@throw ex'#es'',s⇩2⟩"
from IH1[OF eval_val wte sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_throw[simplified eq] wtes this] show "e' = e⇩2 ∧ (h⇩3, l⇩2) = s⇩2"
by(fastforce dest:map_Val_throw_False)
next
fix C' Xs Xs' Ds' S' U U' Us Us' a' body'' body''' h h' l l' pns'' pns''' s ws ws'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws,(h,l)⟩"
and h:"h a' = Some(C',S')"
and has_least'':"P ⊢ last Xs has least M = (Us',U',pns''',body''') via Ds'"
and selects':"P ⊢ (C',Xs@⇩pDs') selects M = (Us,U,pns'',body'') via Xs'"
and length':"length ws = length pns''" and Casts':"P ⊢ Us Casts ws to ws'"
and eval_body':"P,E(this ↦ Class (last Xs'), pns'' [↦] Us) ⊢
⟨case U' of Class D ⇒ ⦇D⦈body'' | _ ⇒ body'',
(h,[this ↦ Ref(a',Xs'), pns'' [↦] ws'])⟩ ⇒ ⟨e⇩2,(h',l')⟩"
and s2:"s⇩2 = (h',l)"
from IH1[OF eval_ref wte sconf] have eq1:"a = a' ∧ Cs = Xs" and s:"s = s⇩1"
by simp_all
with has_least has_least'' wf have eq2:"T' = U' ∧ Ts' = Us' ∧ Ds = Ds'"
by(fastforce dest:wf_sees_method_fun)
from s wf eval_ref wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified s] wtes this]
have eq3:"vs = ws ∧ h⇩2 = h ∧ l⇩2 = l"
by(fastforce elim:map_injective simp:inj_on_def)
with eq1 h2 h have eq4:"C = C' ∧ S = S'" by simp
with eq1 eq2 selects selects' wf
have eq5:"Ts = Us ∧ T = U ∧ pns'' = pns ∧ body'' = body ∧ Cs' = Xs'"
by simp(drule_tac mthd'="(Us,U,pns'',body'')" in wf_select_method_fun,auto)
with subs eq param_types have "P ⊢ Ss' [≤] Us" by simp
with wf Casts Casts' param_type wtes evals_vals sconf' s eq eq2 eq3 eq5
have eq6:"vs' = ws'"
by(fastforce intro:Casts_Casts_eq_result)
with eval_body' l2' eq1 eq2 eq3 eq5 new_body
have eval_body'':"P,E(this ↦ Class(last Cs'), pns [↦] Ts) ⊢
⟨new_body,(h⇩2,l⇩2')⟩ ⇒ ⟨e⇩2,(h',l')⟩"
by fastforce
from wf evals_vals wtes sconf' s eq3 have sconf'':"P,E ⊢ (h⇩2,l⇩2) √"
by(fastforce intro:evals_preserves_sconf)
have "P,E(this ↦ Class (last Cs'), pns [↦] Ts) ⊢ (h⇩2,l⇩2') √"
proof(auto simp:sconf_def)
from sconf'' show "P ⊢ h⇩2 √" by(simp add:sconf_def)
next
{ fix V v assume map:"[this ↦ Ref (a,Cs'), pns [↦] vs'] V = Some v"
have "∃T. (E(this ↦ Class (last Cs'), pns [↦] Ts)) V = Some T ∧
P,h⇩2 ⊢ v :≤ T"
proof(cases "V ∈ set (this#pns)")
case False with map show ?thesis by simp
next
case True
hence "V = this ∨ V ∈ set pns" by simp
thus ?thesis
proof(rule disjE)
assume V:"V = this"
with map this_not_pns have "v = Ref(a,Cs')" by simp
with V h2 subo this_not_pns have
"(E(this ↦ Class (last Cs'),pns [↦] Ts)) V = Some(Class (last Cs'))"
and "P,h⇩2 ⊢ v :≤ Class (last Cs')" by simp_all
thus ?thesis by simp
next
assume "V ∈ set pns"
then obtain i where V:"V = pns!i" and length_i:"i < length pns"
by(auto simp:in_set_conv_nth)
from Casts have "length Ts = length vs'"
by(induct rule:Casts_to.induct,auto)
with length have "length pns = length vs'" by simp
with map dist V length_i have v:"v = vs'!i" by(fastforce dest:maps_nth)
from length dist length_i
have env:"(E(this ↦ Class (last Cs'))(pns [↦] Ts)) (pns!i) = Some(Ts!i)"
by(rule_tac E="E(this ↦ Class (last Cs'))" in nth_maps,simp_all)
from wf Casts wtes subs eq param_types eval'' sconf'
have "∀i < length Ts. P,h⇩2 ⊢ vs'!i :≤ Ts!i"
by simp(rule Casts_conf,auto)
with length_i length env V v show ?thesis by simp
qed
qed }
thus "P,h⇩2 ⊢ l⇩2' (:≤)⇩w E(this ↦ Class (last Cs'), pns [↦] Ts)"
next
{ fix V Tx assume env:"(E(this ↦ Class (last Cs'), pns [↦] Ts)) V = Some Tx"
have "is_type P Tx"
proof(cases "V ∈ set (this#pns)")
case False
with env sconf'' show ?thesis
by(clarsimp simp:sconf_def envconf_def)
next
case True
hence "V = this ∨ V ∈ set pns" by simp
thus ?thesis
proof(rule disjE)
assume "V = this"
with env this_not_pns have "Tx = Class(last Cs')" by simp
with "class" show ?thesis by simp
next
assume "V ∈ set pns"
then obtain i where V:"V = pns!i" and length_i:"i < length pns"
by(auto simp:in_set_conv_nth)
with dist length env have "Tx = Ts!i" by(fastforce dest:maps_nth)
with length_i length have "Tx ∈ set Ts"
by(fastforce simp:in_set_conv_nth)
with param_type show ?thesis by simp
qed
qed }
thus "P ⊢ E(this ↦ Class (last Cs'), pns [↦] Ts) √" by (simp add:envconf_def)
qed
from IH3[OF eval_body'' wt_new_body this] have "e' = e⇩2 ∧ (h⇩3, l⇩3) = (h',l')" .
with eq3 s2 show "e' = e⇩2 ∧ (h⇩3,l⇩2) = s⇩2" by simp
next
fix s ws
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⟩"
from IH1[OF eval_null wte sconf] show "e' = e⇩2 ∧ (h⇩3,l⇩2) = s⇩2" by simp
qed
next
case (StaticCall E e s⇩0 a Cs s⇩1 es vs h⇩2 l⇩2 C Cs'' M Ts T pns body  Cs'
Ds vs' l⇩2' e' h⇩3 l⇩3 e⇩2 s⇩2 T')
have eval:"P,E ⊢ ⟨e∙(C::)M(es),s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and eval':"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a,Cs),s⇩1⟩"
and eval'':"P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2, l⇩2)⟩"
and path_unique:"P ⊢ Path last Cs to C unique"
and path_via:"P ⊢ Path last Cs to C via Cs''"
and has_least:"P ⊢ C has least M = (Ts,T,pns,body) via Cs'"
and Ds:"Ds = (Cs@⇩pCs'')@⇩pCs'" and length:"length vs = length pns"
and Casts:"P ⊢ Ts Casts vs to vs'"
and l2':"l⇩2' = [this ↦ Ref (a, Ds), pns [↦] vs']"
and eval_body:"P,E(this ↦ Class (last Ds), pns [↦] Ts) ⊢
⟨body,(h⇩2,l⇩2')⟩ ⇒ ⟨e',(h⇩3,l⇩3)⟩"
and wt:"P,E ⊢ e∙(C::)M(es) :: T'" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref (a,Cs) = ei ∧ s⇩1 = si"
and IH2:"⋀esi si Ts.
⟦P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨esi,si⟩; P,E ⊢ es [::] Ts; P,E ⊢ s⇩1 √⟧
⟹ map Val vs = esi ∧ (h⇩2,l⇩2) = si"
and IH3:"⋀ei si T.
⟦P,E(this ↦ Class (last Ds), pns [↦] Ts) ⊢ ⟨body,(h⇩2,l⇩2')⟩ ⇒ ⟨ei,si⟩;
P,E(this ↦ Class (last Ds), pns [↦] Ts) ⊢ body :: T;
P,E(this ↦ Class (last Ds), pns [↦] Ts) ⊢ (h⇩2,l⇩2') √⟧
⟹ e' = ei ∧ (h⇩3, l⇩3) = si" by fact+
from wt has_least wf obtain C' Ts' where wte:"P,E ⊢ e :: Class C'"
and wtes:"P,E ⊢ es [::] Ts'" and subs:"P ⊢ Ts' [≤] Ts"
by(auto dest:wf_sees_method_fun)
from eval_preserves_type[OF wf eval' sconf wte]
have last:"last Cs = C'" by (auto split:if_split_asm)
from wf has_least have param_type:"∀T ∈ set Ts. is_type P T"
and return_type:"is_type P T" and TnotNT:"T ≠ NT"
by(auto dest:has_least_wf_mdecl simp:wf_mdecl_def)
from path_via have last':"last Cs'' = last(Cs@⇩pCs'')"
by(fastforce intro!:appendPath_last Subobjs_nonempty simp:path_via_def)
from eval'' have hext:"hp s⇩1 ⊴ h⇩2" by (cases s⇩1,auto intro: evals_hext)
from wf eval' sconf wte last have "P,E,(hp s⇩1) ⊢ ref(a,Cs) :⇘NT⇙ Class(last Cs)"
by -(rule eval_preserves_type,simp_all)
with hext have "P,E,h⇩2 ⊢ ref(a,Cs) :⇘NT⇙ Class(last Cs)"
by(auto intro:WTrt_hext_mono dest:hext_objD split:if_split_asm)
then obtain D S where h2:"h⇩2 a = Some(D,S)" and "Subobjs P D Cs"
by (auto split:if_split_asm)
with path_via wf have "Subobjs P D (Cs@⇩pCs'')" and "last Cs'' = C"
by(auto intro:Subobjs_appendPath simp:path_via_def)
with has_least wf last' Ds have subo:"Subobjs P D Ds"
by(fastforce intro:Subobjs_appendPath simp:LeastMethodDef_def MethodDefs_def)
with wf have "class":"is_class P (last Ds)" by(auto intro!:Subobj_last_isClass)
from has_least wf obtain D' where "Subobjs P D' Cs'"
by(auto simp:LeastMethodDef_def MethodDefs_def)
with Ds have last_Ds:"last Cs' = last Ds"
by(fastforce intro!:appendPath_last Subobjs_nonempty)
with wf has_least have "P,[this↦Class(last Ds),pns[↦]Ts] ⊢ body :: T"
and this_not_pns:"this ∉ set pns" and length:"length pns = length Ts"
and dist:"distinct pns"
by(auto dest!:has_least_wf_mdecl simp:wf_mdecl_def)
hence wt_body:"P,E(this↦Class(last Ds),pns[↦]Ts) ⊢ body :: T"
by(fastforce intro:wt_env_mono)
from eval show ?case
proof(rule eval_cases)
fix ex' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex',s⇩2⟩"
from IH1[OF eval_throw wte sconf] show "e' = e⇩2 ∧ (h⇩3, l⇩2) = s⇩2" by simp
next
fix es'' ex' s w ws
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and evals_throw:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws@throw ex'#es'',s⇩2⟩"
from IH1[OF eval_val wte sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_throw[simplified eq] wtes this] show "e' = e⇩2 ∧ (h⇩3, l⇩2) = s⇩2"
by(fastforce dest:map_Val_throw_False)
next
fix Xs Xs' Xs'' U Us a' body' h h' l l' pns' s ws ws'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws,(h,l)⟩"
and path_unique':"P ⊢ Path last Xs to C unique"
and path_via':"P ⊢ Path last Xs to C via Xs''"
and has_least':"P ⊢ C has least M = (Us,U,pns',body') via Xs'"
and length':"length ws = length pns'"
and Casts':"P ⊢ Us Casts ws to ws'"
and eval_body':"P,E(this ↦ Class(last((Xs@⇩pXs'')@⇩pXs')),pns' [↦] Us) ⊢
⟨body',(h,[this ↦ Ref(a',(Xs@⇩pXs'')@⇩pXs'),pns' [↦] ws'])⟩ ⇒ ⟨e⇩2,(h',l')⟩"
and s2:"s⇩2 = (h',l)"
from IH1[OF eval_ref wte sconf] have eq1:"a = a' ∧ Cs = Xs" and s:"s = s⇩1"
by simp_all
from has_least has_least' wf
have eq2:"T = U ∧ Ts = Us ∧ Cs' = Xs' ∧ pns = pns' ∧ body = body'"
by(fastforce dest:wf_sees_method_fun)
from s wf eval_ref wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified s] wtes this]
have eq3:"vs = ws ∧ h⇩2 = h ∧ l⇩2 = l"
by(fastforce elim:map_injective simp:inj_on_def)
from path_unique path_via path_via' eq1 have "Cs'' = Xs''"
by(fastforce simp:path_unique_def path_via_def)
with Ds eq1 eq2 have Ds':"Ds = (Xs@⇩pXs'')@⇩pXs'" by simp
from wf Casts Casts' param_type wtes subs evals_vals sconf' s eq2 eq3
have eq4:"vs' = ws'"
by(fastforce intro:Casts_Casts_eq_result)
with eval_body' Ds' l2' eq1 eq2 eq3
have eval_body'':"P,E(this ↦ Class(last Ds),pns [↦] Ts) ⊢
⟨body,(h⇩2,l⇩2')⟩ ⇒ ⟨e⇩2,(h',l')⟩"
by simp
from wf evals_vals wtes sconf' s eq3 have sconf'':"P,E ⊢ (h⇩2,l⇩2) √"
by(fastforce intro:evals_preserves_sconf)
have "P,E(this ↦ Class (last Ds), pns [↦] Ts) ⊢ (h⇩2,l⇩2') √"
proof(auto simp:sconf_def)
from sconf'' show "P ⊢ h⇩2 √" by(simp add:sconf_def)
next
{ fix V v assume map:"[this ↦ Ref (a,Ds), pns [↦] vs'] V = Some v"
have "∃T. (E(this ↦ Class (last Ds), pns [↦] Ts)) V = Some T ∧
P,h⇩2 ⊢ v :≤ T"
proof(cases "V ∈ set (this#pns)")
case False with map show ?thesis by simp
next
case True
hence "V = this ∨ V ∈ set pns" by simp
thus ?thesis
proof(rule disjE)
assume V:"V = this"
with map this_not_pns have "v = Ref(a,Ds)" by simp
with V h2 subo this_not_pns have
"(E(this ↦ Class (last Ds),pns [↦] Ts)) V = Some(Class (last Ds))"
and "P,h⇩2 ⊢ v :≤ Class (last Ds)" by simp_all
thus ?thesis by simp
next
assume "V ∈ set pns"
then obtain i where V:"V = pns!i" and length_i:"i < length pns"
by(auto simp:in_set_conv_nth)
from Casts have "length Ts = length vs'"
by(induct rule:Casts_to.induct,auto)
with length have "length pns = length vs'" by simp
with map dist V length_i have v:"v = vs'!i" by(fastforce dest:maps_nth)
from length dist length_i
have env:"(E(this ↦ Class (last Ds))(pns [↦] Ts)) (pns!i) = Some(Ts!i)"
by(rule_tac E="E(this ↦ Class (last Ds))" in nth_maps,simp_all)
from wf Casts wtes subs eval'' sconf'
have "∀i < length Ts. P,h⇩2 ⊢ vs'!i :≤ Ts!i"
by -(rule Casts_conf,auto)
with length_i length env V v show ?thesis by simp
qed
qed }
thus "P,h⇩2 ⊢ l⇩2' (:≤)⇩w E(this ↦ Class (last Ds), pns [↦] Ts)"
next
{ fix V Tx assume env:"(E(this ↦ Class (last Ds), pns [↦] Ts)) V = Some Tx"
have "is_type P Tx"
proof(cases "V ∈ set (this#pns)")
case False
with env sconf'' show ?thesis
by(clarsimp simp:sconf_def envconf_def)
next
case True
hence "V = this ∨ V ∈ set pns" by simp
thus ?thesis
proof(rule disjE)
assume "V = this"
with env this_not_pns have "Tx = Class(last Ds)" by simp
with "class" show ?thesis by simp
next
assume "V ∈ set pns"
then obtain i where V:"V = pns!i" and length_i:"i < length pns"
by(auto simp:in_set_conv_nth)
with dist length env have "Tx = Ts!i" by(fastforce dest:maps_nth)
with length_i length have "Tx ∈ set Ts"
by(fastforce simp:in_set_conv_nth)
with param_type show ?thesis by simp
qed
qed }
thus "P ⊢ E(this ↦ Class (last Ds), pns [↦] Ts) √" by (simp add:envconf_def)
qed
from IH3[OF eval_body'' wt_body this] have "e' = e⇩2 ∧ (h⇩3, l⇩3) = (h',l')" .
with eq3 s2 show "e' = e⇩2 ∧ (h⇩3, l⇩2) = s⇩2" by simp
next
fix s ws
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⟩"
from IH1[OF eval_null wte sconf] show "e' = e⇩2 ∧ (h⇩3,l⇩2) = s⇩2" by simp
qed
next
case (CallNull E e s⇩0 s⇩1 es vs s⇩2 Copt M e⇩2 s⇩2' T)
have eval:"P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2'⟩"
and wt:"P,E ⊢ Call e Copt M es :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ null = ei ∧ s⇩1 = si"
and IH2:"⋀esi si Ts. ⟦P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨esi,si⟩; P,E ⊢ es [::] Ts; P,E ⊢ s⇩1 √⟧
⟹ map Val vs = esi ∧ s⇩2 = si" by fact+
from wt obtain C Ts where wte:"P,E ⊢ e :: Class C" and wtes:"P,E ⊢ es [::] Ts"
by(cases Copt)auto
show ?case
proof(cases Copt)
assume "Copt = None"
with eval have "P,E ⊢ ⟨e∙M(es),s⇩0⟩ ⇒ ⟨e⇩2,s⇩2'⟩" by simp
thus ?thesis
proof(rule eval_cases)
fix ex' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex',s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "THROW NullPointer = e⇩2 ∧ s⇩2 = s⇩2'"
by simp
next
fix es' ex' s w ws
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and evals_throw:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws@throw ex'#es',s⇩2'⟩"
from IH1[OF eval_val wte sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_throw[simplified eq] wtes this]
show "THROW NullPointer = e⇩2 ∧ s⇩2 = s⇩2'" by(fastforce dest:map_Val_throw_False)
next
fix C' Xs Xs' Ds' S' U U' Us Us' a' body'' body''' h h' l l' pns'' pns'''
s ws ws'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
from IH1[OF eval_ref wte sconf] show "THROW NullPointer = e⇩2 ∧ s⇩2 = s⇩2'"
by simp
next
fix s ws
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws,s⇩2'⟩"
and e2:"e⇩2 = THROW NullPointer"
from IH1[OF eval_null wte sconf] have eq:"s = s⇩1" by simp
with wf eval_null wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified eq] wtes this] e2
show "THROW NullPointer = e⇩2 ∧ s⇩2 = s⇩2'" by simp
qed
next
fix C' assume "Copt = Some C'"
with eval have "P,E ⊢ ⟨e∙(C'::)M(es),s⇩0⟩ ⇒ ⟨e⇩2,s⇩2'⟩" by simp
thus ?thesis
proof(rule eval_cases)
fix ex' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex',s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "THROW NullPointer = e⇩2 ∧ s⇩2 = s⇩2'"
by simp
next
fix es' ex' s w ws
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and evals_throw:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws@throw ex'#es',s⇩2'⟩"
from IH1[OF eval_val wte sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_throw[simplified eq] wtes this]
show "THROW NullPointer = e⇩2 ∧ s⇩2 = s⇩2'" by(fastforce dest:map_Val_throw_False)
next
fix C' Xs Xs' Ds' S' U U' Us Us' a' body'' body''' h h' l l' pns'' pns'''
s ws ws'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⟩"
from IH1[OF eval_ref wte sconf] show "THROW NullPointer = e⇩2 ∧ s⇩2 = s⇩2'"
by simp
next
fix s ws
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val ws,s⇩2'⟩"
and e2:"e⇩2 = THROW NullPointer"
from IH1[OF eval_null wte sconf] have eq:"s = s⇩1" by simp
with wf eval_null wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified eq] wtes this] e2
show "THROW NullPointer = e⇩2 ∧ s⇩2 = s⇩2'" by simp
qed
qed
next
case (Block E V T e⇩0 h⇩0 l⇩0 e⇩1 h⇩1 l⇩1 e⇩2 s⇩2 T')
have eval:"P,E ⊢ ⟨{V:T; e⇩0},(h⇩0, l⇩0)⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ {V:T; e⇩0} :: T'" and sconf:"P,E ⊢ (h⇩0, l⇩0) √"
and IH:"⋀e⇩2 s⇩2 T'. ⟦P,E(V ↦ T) ⊢ ⟨e⇩0,(h⇩0, l⇩0(V := None))⟩ ⇒ ⟨e⇩2,s⇩2⟩;
P,E(V ↦ T) ⊢ e⇩0 :: T'; P,E(V ↦ T) ⊢ (h⇩0, l⇩0(V := None)) √⟧
⟹ e⇩1 = e⇩2 ∧ (h⇩1, l⇩1) = s⇩2" by fact+
from wt have type:"is_type P T" and wte:"P,E(V ↦ T) ⊢ e⇩0 :: T'" by auto
from sconf type have sconf':"P,E(V ↦ T) ⊢ (h⇩0, l⇩0(V := None)) √"
by(auto simp:sconf_def lconf_def envconf_def)
from eval obtain h l where
eval':"P,E(V ↦ T) ⊢ ⟨e⇩0,(h⇩0,l⇩0(V:=None))⟩ ⇒ ⟨e⇩2,(h,l)⟩"
and s2:"s⇩2 = (h,l(V:=l⇩0 V))" by (auto elim:eval_cases)
from IH[OF eval' wte sconf'] s2 show ?case by simp
next
case (Seq E e⇩0 s⇩0 v s⇩1 e⇩1 e⇩2 s⇩2 e⇩2' s⇩2' T)
have eval:"P,E ⊢ ⟨e⇩0;; e⇩1,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
and wt:"P,E ⊢ e⇩0;; e⇩1 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩0 :: T; P,E ⊢ s⇩0 √⟧
⟹ Val v = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩1 √⟧
⟹ e⇩2 = ei ∧ s⇩2 = si" by fact+
from wt obtain T' where wte0:"P,E ⊢ e⇩0 :: T'" and wte1:"P,E ⊢ e⇩1 :: T" by auto
from eval show ?case
proof(rule eval_cases)
fix s w
assume eval_val:"P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and eval':"P,E ⊢ ⟨e⇩1,s⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
from IH1[OF eval_val wte0 sconf] have eq:"s = s⇩1" by simp
with wf eval_val wte0 sconf have "P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval'[simplified eq] wte1 this] show "e⇩2 = e⇩2' ∧ s⇩2 = s⇩2'" .
next
fix ex assume eval_throw:"P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_throw wte0 sconf] show "e⇩2 = e⇩2' ∧ s⇩2 = s⇩2'" by simp
qed
next
case (SeqThrow E e⇩0 s⇩0 e s⇩1 e⇩1 e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨e⇩0;; e⇩1,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ e⇩0;; e⇩1 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩0 :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e = ei ∧ s⇩1 = si" by fact+
from wt obtain T' where wte0:"P,E ⊢ e⇩0 :: T'" by auto
from eval show ?case
proof(rule eval_cases)
fix s w
assume eval_val:"P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨Val w,s⟩"
from IH[OF eval_val wte0 sconf] show "throw e = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex
assume eval_throw:"P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2:"e⇩2 = throw ex"
from IH[OF eval_throw wte0 sconf] e2 show "throw e = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (CondT E e s⇩0 s⇩1 e⇩1 e' s⇩2 e⇩2 e⇩2' s⇩2' T)
have eval:"P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
and wt:"P,E ⊢ if (e) e⇩1 else e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ true = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩1 √⟧
⟹ e' = ei ∧ s⇩2 = si" by fact+
from wt have wte:"P,E ⊢ e :: Boolean" and wte1:"P,E ⊢ e⇩1 :: T" by auto
from eval show ?case
proof(rule eval_cases)
fix s
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩" and eval':"P,E ⊢ ⟨e⇩1,s⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
from IH1[OF eval_true wte sconf] have eq:"s = s⇩1" by simp
with wf eval_true wte sconf have "P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval'[simplified eq] wte1 this] show "e' = e⇩2' ∧ s⇩2 = s⇩2'" .
next
fix s assume eval_false:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⟩"
from IH1[OF eval_false wte sconf] show "e' = e⇩2' ∧ s⇩2 = s⇩2'" by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "e' = e⇩2' ∧ s⇩2 = s⇩2'" by simp
qed
next
case (CondF E e s⇩0 s⇩1 e⇩2 e' s⇩2 e⇩1 e⇩2' s⇩2' T)
have eval:"P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
and wt:"P,E ⊢ if (e) e⇩1 else e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ false = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩2 :: T; P,E ⊢ s⇩1 √⟧
⟹ e' = ei ∧ s⇩2 = si" by fact+
from wt have wte:"P,E ⊢ e :: Boolean" and wte2:"P,E ⊢ e⇩2 :: T" by auto
from eval show ?case
proof(rule eval_cases)
fix s
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
from IH1[OF eval_true wte sconf] show "e' = e⇩2' ∧ s⇩2 = s⇩2'" by simp
next
fix s
assume eval_false:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⟩"
and eval':"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
from IH1[OF eval_false wte sconf] have eq:"s = s⇩1" by simp
with wf eval_false wte sconf have "P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval'[simplified eq] wte2 this] show "e' = e⇩2' ∧ s⇩2 = s⇩2'" .
next
fix ex assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "e' = e⇩2' ∧ s⇩2 = s⇩2'" by simp
qed
next
case (CondThrow E e s⇩0 e' s⇩1 e⇩1 e⇩2 e⇩2' s⇩2 T)
have eval:"P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2⟩"
and wt:"P,E ⊢ if (e) e⇩1 else e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = ei ∧ s⇩1 = si" by fact+
from wt have wte:"P,E ⊢ e :: Boolean" by auto
from eval show ?case
proof(rule eval_cases)
fix s
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
from IH[OF eval_true wte sconf] show "throw e' = e⇩2' ∧ s⇩1 = s⇩2" by simp
next
fix s assume eval_false:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⟩"
from IH[OF eval_false wte sconf] show "throw e' = e⇩2' ∧ s⇩1 = s⇩2" by simp
next
fix ex
assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2':"e⇩2' = throw ex"
from IH[OF eval_throw wte sconf] e2' show "throw e' = e⇩2' ∧ s⇩1 = s⇩2" by simp
qed
next
case (WhileF E e s⇩0 s⇩1 c e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ while (e) c :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ false = e⇩2 ∧ s⇩1 = s⇩2" by fact+
from wt have wte:"P,E ⊢ e :: Boolean" by auto
from eval show ?case
proof(rule eval_cases)
assume eval_false:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩2⟩" and e2:"e⇩2 = unit"
from IH[OF eval_false wte sconf] e2 show "unit = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix s s' w
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
from IH[OF eval_true wte sconf] show "unit = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"
from IH[OF eval_throw wte sconf] show "unit = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex s
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
from IH[OF eval_true wte sconf] show "unit = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (WhileT E e s⇩0 s⇩1 c v⇩1 s⇩2 e⇩3 s⇩3 e⇩2 s⇩2' T)
have eval:"P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2'⟩"
and wt:"P,E ⊢ while (e) c :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ true = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨c,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ c :: T; P,E ⊢ s⇩1 √⟧
⟹ Val v⇩1 = ei ∧ s⇩2 = si"
and IH3:"⋀ei si T. ⟦P,E ⊢ ⟨while (e) c,s⇩2⟩ ⇒ ⟨ei,si⟩; P,E ⊢ while (e) c :: T;
P,E ⊢ s⇩2 √⟧
⟹ e⇩3 = ei ∧ s⇩3 = si" by fact+
from wt obtain T' where wte:"P,E ⊢ e :: Boolean" and wtc:"P,E ⊢ c :: T'" by auto
from eval show ?case
proof(rule eval_cases)
assume eval_false:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩2'⟩"
from IH1[OF eval_false wte sconf] show "e⇩3 = e⇩2 ∧ s⇩3 = s⇩2'" by simp
next
fix s s' w
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
and eval_val:"P,E ⊢ ⟨c,s⟩ ⇒ ⟨Val w,s'⟩"
and eval_while:"P,E ⊢ ⟨while (e) c,s'⟩ ⇒ ⟨e⇩2,s⇩2'⟩"
from IH1[OF eval_true wte sconf] have eq:"s = s⇩1" by simp
with wf eval_true wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_val[simplified eq] wtc this] have eq':"s' = s⇩2" by simp
with wf eval_val wtc sconf' eq have "P,E ⊢ s⇩2 √"
by(fastforce intro:eval_preserves_sconf)
from IH3[OF eval_while[simplified eq'] wt this] show "e⇩3 = e⇩2 ∧ s⇩3 = s⇩2'" .
next
fix ex assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "e⇩3 = e⇩2 ∧ s⇩3 = s⇩2'" by simp
next
fix ex s
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
and eval_throw:"P,E ⊢ ⟨c,s⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_true wte sconf] have eq:"s = s⇩1" by simp
with wf eval_true wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_throw[simplified eq] wtc this] show "e⇩3 = e⇩2 ∧ s⇩3 = s⇩2'" by simp
qed
next
case (WhileCondThrow E e s⇩0 e' s⇩1 c e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ while (e) c :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = ei ∧ s⇩1 = si" by fact+
from wt have wte:"P,E ⊢ e :: Boolean" by auto
from eval show ?case
proof(rule eval_cases)
assume eval_false:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩2⟩"
from IH[OF eval_false wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix s s' w
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
from IH[OF eval_true wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex
assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2:"e⇩2 = throw ex"
from IH[OF eval_throw wte sconf] e2 show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex s
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
from IH[OF eval_true wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (WhileBodyThrow E e s⇩0 s⇩1 c e' s⇩2 e⇩2 s⇩2' T)
have eval:"P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2'⟩"
and wt:"P,E ⊢ while (e) c :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ true = ei ∧ s⇩1 = si"
and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨c,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ c :: T; P,E ⊢ s⇩1 √⟧
⟹ throw e' = ei ∧ s⇩2 = si" by fact+
from wt obtain T' where wte:"P,E ⊢ e :: Boolean" and wtc:"P,E ⊢ c :: T'" by auto
from eval show ?case
proof(rule eval_cases)
assume eval_false:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩2'⟩"
from IH1[OF eval_false wte sconf] show "throw e' = e⇩2 ∧ s⇩2 = s⇩2'" by simp
next
fix s s' w
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
and eval_val:"P,E ⊢ ⟨c,s⟩ ⇒ ⟨Val w,s'⟩"
from IH1[OF eval_true wte sconf] have eq:"s = s⇩1" by simp
with wf eval_true wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_val[simplified eq] wtc this] show "throw e' = e⇩2 ∧ s⇩2 = s⇩2'"
by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "throw e' = e⇩2 ∧ s⇩2 = s⇩2'" by simp
next
fix ex s
assume eval_true:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⟩"
and eval_throw:"P,E ⊢ ⟨c,s⟩ ⇒ ⟨throw ex,s⇩2'⟩" and e2:"e⇩2 = throw ex"
from IH1[OF eval_true wte sconf] have eq:"s = s⇩1" by simp
with wf eval_true wte sconf have sconf':"P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF eval_throw[simplified eq] wtc this] e2 show "throw e' = e⇩2 ∧ s⇩2 = s⇩2'"
by simp
qed
next
case (Throw E e s⇩0 r s⇩1 e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ throw e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ ref r = ei ∧ s⇩1 = si" by fact+
from wt obtain C where wte:"P,E ⊢ e :: Class C" by auto
from eval show ?case
proof(rule eval_cases)
fix r'
assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref r',s⇩2⟩" and e2:"e⇩2 = Throw r'"
from IH[OF eval_ref wte sconf] e2 show "Throw r = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "Throw r = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"
from IH[OF eval_throw wte sconf] show "Throw r = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (ThrowNull E e s⇩0 s⇩1 e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ throw e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ null = ei ∧ s⇩1 = si" by fact+
from wt obtain C where wte:"P,E ⊢ e :: Class C" by auto
from eval show ?case
proof(rule eval_cases)
fix r' assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref r',s⇩2⟩"
from IH[OF eval_ref wte sconf] show "THROW NullPointer = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩" and e2:"e⇩2 = THROW NullPointer"
from IH[OF eval_null wte sconf] e2 show "THROW NullPointer = e⇩2 ∧ s⇩1 = s⇩2"
by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"
from IH[OF eval_throw wte sconf] show "THROW NullPointer = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case (ThrowThrow E e s⇩0 e' s⇩1 e⇩2 s⇩2 T)
have eval:"P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
and wt:"P,E ⊢ throw e :: T" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = ei ∧ s⇩1 = si" by fact+
from wt obtain C where wte:"P,E ⊢ e :: Class C" by auto
from eval show ?case
proof(rule eval_cases)
fix r' assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref r',s⇩2⟩"
from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
from IH[OF eval_null wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex
assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2:"e⇩2 = throw ex"
from IH[OF eval_throw wte sconf] e2 show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
qed
next
case Nil thus ?case by (auto elim:evals_cases)
next
case (Cons E e s⇩0 v s⇩1 es es' s⇩2 es⇩2 s⇩2' Ts)
have evals:"P,E ⊢ ⟨e#es,s⇩0⟩ [⇒] ⟨es⇩2,s⇩2'⟩"
and wt:"P,E ⊢ e#es [::] Ts" and sconf:"P,E ⊢ s⇩0 √"
and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ Val v = ei ∧ s⇩1 = si"
and IH2:"⋀esi si Ts. ⟦P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨esi,si⟩; P,E ⊢ es [::] Ts; P,E ⊢ s⇩1 √⟧
⟹ es' = esi ∧ s⇩2 = si" by fact+
from wt obtain T' Ts' where Ts:"Ts = T'#Ts'" by(cases Ts) auto
with wt have wte:"P,E ⊢ e :: T'" and wtes:"P,E ⊢ es [::] Ts'" by auto
from evals show ?case
proof(rule evals_cases)
fix es'' s w
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
and evals_vals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨es'',s⇩2'⟩" and es2:"es⇩2 = Val w#es''"
from IH1[OF eval_val wte sconf] have s:"s = s⇩1" and v:"v = w" by simp_all
with wf eval_val wte sconf have "P,E ⊢ s⇩1 √"
by(fastforce intro:eval_preserves_sconf)
from IH2[OF evals_vals[simplified s] wtes this] have "es' = es'' ∧ s⇩2 = s⇩2'" .
with es2 v show "Val v # es' = es⇩2 ∧ s⇩2 = s⇩2'" by simp
next
fix ex assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2'⟩"
from IH1[OF eval_throw wte sconf] show "Val v # es' = es⇩2 ∧ s⇩2 = s⇩2'" by simp
qed
next
case (ConsThrow E e s⇩0 e' s⇩1 es es⇩2 s⇩2 Ts)
have evals:"P,E ⊢ ⟨e#es,s⇩0⟩ [⇒] ⟨es⇩2,s⇩2⟩"
and wt:"P,E ⊢ e#es [::] Ts" and sconf:"P,E ⊢ s⇩0 √"
and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
⟹ throw e' = ei ∧ s⇩1 = si" by fact+
from wt obtain T' Ts' where Ts:"Ts = T'#Ts'" by(cases Ts) auto
with wt have wte:"P,E ⊢ e :: T'" by auto
from evals show ?case
proof(rule evals_cases)
fix es'' s w
assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,s⟩"
from IH[OF eval_val wte sconf] show "throw e'#es = es⇩2 ∧ s⇩1 = s⇩2" by simp
next
fix ex
assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and es2:"es⇩2 = throw ex#es"
from IH[OF eval_throw wte sconf] es2 show "throw e'#es = es⇩2 ∧ s⇩1 = s⇩2" by simp
qed
qed

end
```