# Theory Progress

Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Progress of Small Step Semantics›

theory Progress
imports
WellTypeRT
DefAss
SmallStep

WWellForm
begin

context J_heap begin

" P,E,h  e : T; class_type_of' T = U; final e;
a. e = addr a  R;
a. e = Throw a  R   R"
apply(auto elim!: final.cases)
apply(case_tac v)
apply auto
done

lemma finalRefE [consumes 3, case_names null Class Array Throw]:
" P,E,h  e : T; is_refT T; final e;
e = null  R;
a C.  e = addr a; T = Class C   R;
a U.  e = addr a; T = U⌊⌉   R;
a. e = Throw a  R   R"
apply(auto simp:final_iff)
apply(case_tac v)
apply(auto elim!: is_refT.cases)
done

end

theorem (in J_progress) red_progress:
assumes wf: "wwf_J_prog P" and hconf: "hconf h"
shows progress: " P,E,h  e : T; 𝒟 e dom l; ¬ final e   e' s' ta. extTA,P,t  e,(h,l) -ta e',s'"
and progresss: " P,E,h  es [:] Ts; 𝒟s es dom l; ¬ finals es   es' s' ta. extTA,P,t  es,(h,l) [-ta→] es',s'"
proof (induct arbitrary: l and l rule:WTrt_WTrts.inducts)
case (WTrtNew C)
thus ?case using WTrtNew
by(cases "allocate h (Class_type C) = {}")(fastforce intro: RedNewFail RedNew)+
next
case (WTrtNewArray E e T l)
have IH: "l. 𝒟 e dom l; ¬ final e  e' s' tas. extTA,P,t  e,(h,l) -tas e', s'"
and D: "𝒟 (newA Te) dom l"
and ei: "P,E,h  e : Integer" by fact+
from D have De: "𝒟 e dom l" by auto
show ?case
proof cases
assume "final e"
thus ?thesis
proof (rule finalE)
fix v
assume e [simp]: "e = Val v"
with ei have "typeof⇘hv = Some Integer" by fastforce
hence exei: "i. v = Intg i" by fastforce
then obtain i where v: "v = Intg i" by blast
thus ?thesis
proof (cases "0 <=s i")
case True
thus ?thesis using True v = Intg i WTrtNewArray.prems
by(cases "allocate h (Array_type T (nat (sint i))) = {}")(auto simp del: split_paired_Ex intro: RedNewArrayFail RedNewArray)
next
assume "¬ 0 <=s i"
hence "i <s 0" by simp
then have "extTA,P,t  newA TVal(Intg i),(h, l) -ε THROW NegativeArraySize,(h, l)"
by - (rule RedNewArrayNegative, auto)
with e v show ?thesis by blast
qed
next
fix exa
assume e: "e = Throw exa"
then have "extTA,P,t  newA TThrow exa,(h, l) -ε Throw exa,(h, l)"
by - (rule NewArrayThrow)
with e show ?thesis by blast
qed
next
assume "¬ final e"
with IH De have exes: "e' s' ta. extTA,P,t  e,(h, l) -ta e',s'" by simp
then obtain e' s' ta where "extTA,P,t  e,(h, l) -ta e',s'" by blast
hence "extTA,P,t  newA Te,(h, l) -ta newA Te',s'" by - (rule NewArrayRed)
thus ?thesis by blast
qed
next
case (WTrtCast E e T U l)
have wte: "P,E,h  e : T"
and IH: "l. 𝒟 e dom l; ¬ final e
e' s' tas. extTA,P,t  e,(h,l) -tas e',s'"
and D: "𝒟 (Cast U e) dom l" by fact+
from D have De: "𝒟 e dom l" by auto
show ?case
proof (cases "final e")
assume "final e"
thus ?thesis
proof (rule finalE)
fix v
assume ev: "e = Val v"
with WTrtCast obtain V where thvU: "typeof⇘hv = V" by fastforce
thus ?thesis
proof (cases "P  V  U")
assume "P  V  U"
with thvU have "extTA,P,t  Cast U (Val v),(h, l) -ε Val v,(h,l)"
by - (rule RedCast, auto)
with ev show ?thesis by blast
next
assume "¬ P  V  U"
with thvU have "extTA,P,t  Cast U (Val v),(h, l) -ε THROW ClassCast,(h,l)"
by - (rule RedCastFail, auto)
with ev show ?thesis by blast
qed
next
fix a
assume "e = Throw a"
thus ?thesis by(blast intro!:CastThrow)
qed
next
assume nf: "¬ final e"
from IH[OF De nf] show ?thesis by (blast intro:CastRed)
qed
next
case (WTrtInstanceOf E e T U l)
have wte: "P,E,h  e : T"
and IH: "l. 𝒟 e dom l; ¬ final e
e' s' tas. extTA,P,t  e,(h,l) -tas e',s'"
and D: "𝒟 (e instanceof U) dom l" by fact+
from D have De: "𝒟 e dom l" by auto
show ?case
proof (cases "final e")
assume "final e"
thus ?thesis
proof (rule finalE)
fix v
assume ev: "e = Val v"
with WTrtInstanceOf obtain V where thvU: "typeof⇘hv = V" by fastforce
hence "extTA,P,t  (Val v) instanceof U,(h, l) -ε Val (Bool (v  Null  P  V  U)),(h,l)"
by -(rule RedInstanceOf, auto)
with ev show ?thesis by blast
next
fix a
assume "e = Throw a"
thus ?thesis by(blast intro!:InstanceOfThrow)
qed
next
assume nf: "¬ final e"
from IH[OF De nf] show ?thesis by (blast intro:InstanceOfRed)
qed
next
case WTrtVal thus ?case by(simp add:final_iff)
next
case WTrtVar thus ?case by(fastforce intro:RedVar simp:hyper_isin_def)
next
case (WTrtBinOp E e1 T1 e2 T2 bop T)
show ?case
proof cases
assume "final e1"
thus ?thesis
proof (rule finalE)
fix v1 assume [simp]: "e1 = Val v1"
show ?thesis
proof cases
assume "final e2"
thus ?thesis
proof (rule finalE)
fix v2 assume [simp]: "e2 = Val v2"
with WTrtBinOp have type: "typeof⇘hv1 = T1" "typeof⇘hv2 = T2" by auto
from binop_progress[OF this P  T1«bop»T2 : T] obtain va
where "binop bop v1 v2 = va" by blast
thus ?thesis by(cases va)(fastforce intro: RedBinOp RedBinOpFail)+
next
fix a assume "e2 = Throw a"
thus ?thesis by(fastforce intro:BinOpThrow2)
qed
next
assume "¬ final e2" with WTrtBinOp show ?thesis
by simp (fast intro!:BinOpRed2)
qed
next
fix a assume "e1 = Throw a"
thus ?thesis by simp (fast intro:BinOpThrow1)
qed
next
assume "¬ final e1" with WTrtBinOp show ?thesis
by simp (fast intro:BinOpRed1)
qed
next
case (WTrtLAss E V T e T')
show ?case
proof cases
assume "final e" with WTrtLAss show ?thesis
by(fastforce simp:final_iff intro!:RedLAss LAssThrow)
next
assume "¬ final e" with WTrtLAss show ?thesis
by simp (fast intro:LAssRed)
qed
next
case (WTrtAAcc E a T i l)
have wte: "P,E,h  a : T⌊⌉"
and wtei: "P,E,h  i : Integer"
and IHa: "l. 𝒟 a dom l; ¬ final a
e' s' tas. extTA,P,t  a,(h,l) -tas e',s'"
and IHi: "l. 𝒟 i dom l; ¬ final i
e' s' tas. extTA,P,t  i,(h,l) -tas e',s'"
and D: "𝒟 (ai) dom l" by fact+
have ref: "is_refT (T⌊⌉)" by simp
from D have Da: "𝒟 a dom l" by simp
show ?case
proof (cases "final a")
assume "final a"
with wte ref show ?case
proof (cases rule: finalRefE)
case null
thus ?thesis
proof (cases "final i")
assume "final i"
thus ?thesis
proof (rule finalE)
fix v
assume i: "i = Val v"
have "extTA,P,t  nullVal v, (h, l) -ε THROW NullPointer, (h,l)"
by(rule RedAAccNull)
with i null show ?thesis by blast
next
fix ex
assume i: "i = Throw ex"
have "extTA,P,t  nullThrow ex, (h, l) -ε Throw ex, (h,l)"
by(rule AAccThrow2)
with i null show ?thesis by blast
qed
next
assume "¬ final i"
from WTrtAAcc null show ?thesis
by simp
qed
next
with wte obtain n where ty: "typeof_addr h ad = Array_type U n" by auto
thus ?thesis
proof (cases "final i")
assume "final i"
thus ?thesis
proof(rule finalE)
fix v
assume [simp]: "i = Val v"
with wtei have "typeof⇘hv = Some Integer" by fastforce
hence "i. v = Intg i" by fastforce
then obtain i where [simp]: "v = Intg i" by blast
thus ?thesis
proof (cases "i <s 0  sint i  int n")
case True
with WTrtAAcc Array ty show ?thesis by (fastforce intro: RedAAccBounds)
next
case False
then have "nat (sint i) < n"
by (simp add: not_le word_sless_alt nat_less_iff)
with ty have "P,h  ad@ACell (nat (sint i)) : U" by(auto intro!: addr_loc_type.intros)
obtain v where "heap_read h ad (ACell (nat (sint i))) v" by blast
with False Array ty show ?thesis by(fastforce intro: RedAAcc)
qed
next
fix ex
assume "i = Throw ex"
with WTrtAAcc Array show ?thesis by (fastforce intro: AAccThrow2)
qed
next
assume "¬ final i"
with WTrtAAcc Array show ?thesis by (fastforce intro: AAccRed2)
qed
next
fix ex
assume "a = Throw ex"
with WTrtAAcc show ?thesis by (fastforce intro: AAccThrow1)
qed simp
next
assume "¬ final a"
with WTrtAAcc show ?thesis by (fastforce intro: AAccRed1)
qed
next
case (WTrtAAccNT E a i T l)
have wte: "P,E,h  a : NT"
and wtei: "P,E,h  i : Integer"
and IHa: "l. 𝒟 a dom l; ¬ final a
e' s' tas. extTA,P,t  a,(h,l) -tas e',s'"
and IHi: "l. 𝒟 i dom l; ¬ final i
e' s' tas. extTA,P,t  i,(h,l) -tas e',s'" by fact+
have ref:  by simp
with WTrtAAccNT have Da: "𝒟 a dom l" by simp
thus ?case
proof (cases "final a")
case True
with wte ref show ?thesis
proof (cases rule: finalRefE)
case null
thus ?thesis
proof (cases "final i")
assume "final i"
thus ?thesis
proof (rule finalE)
fix v
assume i: "i = Val v"
have "extTA,P,t  nullVal v, (h, l) -ε THROW NullPointer, (h,l)"
by (rule RedAAccNull)
with WTrtAAccNT final a null final i i show ?thesis by blast
next
fix ex
assume i: "i = Throw ex"
have "extTA,P,t  nullThrow ex, (h, l) -ε Throw ex, (h,l)"
by(rule AAccThrow2)
with WTrtAAccNT final a null final i i show ?thesis by blast
qed
next
assume "¬ final i"
with WTrtAAccNT null show ?thesis
by(fastforce intro: AAccRed2)
qed
next
case Throw thus ?thesis by (fastforce intro: AAccThrow1)
qed simp_all
next
case False
with WTrtAAccNT Da show ?thesis by (fastforce intro:AAccRed1)
qed
next
case (WTrtAAss E a T i e T' l)
have wta: "P,E,h  a : T⌊⌉"
and wti: "P,E,h  i : Integer"
and wte: "P,E,h  e : T'"
and D: "𝒟 (ai := e) dom l"
and IH1: "l. 𝒟 a dom l; ¬ final a  e' s' tas. extTA,P,t  a,(h, l) -tas e',s'"
and IH2: "l. 𝒟 i dom l; ¬ final i  e' s' tas. extTA,P,t  i,(h, l) -tas e',s'"
and IH3: "l. 𝒟 e dom l; ¬ final e  e' s' tas. extTA,P,t  e,(h, l) -tas e',s'" by fact+
have ref: "is_refT (T⌊⌉)" by simp
show ?case
proof (cases "final a")
assume fa: "final a"
with wta ref show ?thesis
proof(cases rule: finalRefE)
case null
show ?thesis
proof(cases "final i")
assume "final i"
thus ?thesis
proof (rule finalE)
fix v
assume i: "i = Val v"
with wti have "typeof⇘hv = Some Integer" by fastforce
then obtain idx where "v = Intg idx" by fastforce
thus ?thesis
proof (cases "final e")
assume "final e"
thus ?thesis
proof (rule finalE)
fix w
assume "e = Val w"
with WTrtAAss null show ?thesis by (fastforce intro: RedAAssNull)
next
fix ex
assume "e = Throw ex"
with WTrtAAss null show ?thesis by (fastforce intro: AAssThrow3)
qed
next
assume "¬ final e"
with WTrtAAss null show ?thesis by (fastforce intro: AAssRed3)
qed
next
fix ex
assume "i = Throw ex"
with WTrtAAss null show ?thesis by (fastforce intro: AAssThrow2)
qed
next
assume "¬ final i"
with WTrtAAss null show ?thesis by (fastforce intro: AAssRed2)
qed
next
with wta obtain n where ty: "typeof_addr h ad = Array_type U n" by auto
thus ?thesis
proof (cases "final i")
assume fi: "final i"
thus ?thesis
proof (rule finalE)
fix v
assume ivalv: "i = Val v"
with wti have "typeof⇘hv = Some Integer" by fastforce
then obtain idx where vidx: "v = Intg idx" by fastforce
thus ?thesis
proof (cases "final e")
assume fe: "final e"
thus ?thesis
proof(rule finalE)
fix w
assume evalw: "e = Val w"
show ?thesis
proof(cases "idx <s 0  sint idx  int n")
case True
with ty evalw Array ivalv vidx show ?thesis by(fastforce intro: RedAAssBounds)
next
case False
then have "nat (sint idx) < n"
by (simp add: not_le word_sless_alt nat_less_iff)
show ?thesis
proof(cases "P  T'  U")
case True
with wte evalw have "P,h  w :≤ U"
obtain h' where h': "heap_write h ad (ACell (nat (sint idx))) w h'" ..
with ty False vidx ivalv evalw Array wte True
show ?thesis by(fastforce intro: RedAAss)
next
case False
with ty vidx ivalv evalw Array wte ¬ (idx <s 0  sint idx  int n)
show ?thesis by(fastforce intro: RedAAssStore)
qed
qed
next
fix ex
assume "e = Throw ex"
with Array ivalv show ?thesis by (fastforce intro: AAssThrow3)
qed
next
assume "¬ final e"
with WTrtAAss Array fi ivalv vidx show ?thesis by (fastforce intro: AAssRed3)
qed
next
fix ex
assume "i = Throw ex"
with WTrtAAss Array show ?thesis by (fastforce intro: AAssThrow2)
qed
next
assume "¬ final i"
with WTrtAAss Array show ?thesis by (fastforce intro: AAssRed2)
qed
next
fix ex
assume "a = Throw ex"
with WTrtAAss show ?thesis by (fastforce intro:AAssThrow1)
qed simp_all
next
assume "¬ final a"
with WTrtAAss show ?thesis by (fastforce intro: AAssRed1)
qed
next
case (WTrtAAssNT E a i e T' l)
have wta: "P,E,h  a : NT"
and wti: "P,E,h  i : Integer"
and wte: "P,E,h  e : T'"
and D: "𝒟 (ai := e) dom l"
and IH1: "l. 𝒟 a dom l; ¬ final a  e' s' tas. extTA,P,t  a,(h, l) -tas e',s'"
and IH2: "l. 𝒟 i dom l; ¬ final i  e' s' tas. extTA,P,t  i,(h, l) -tas e',s'"
and IH3: "l. 𝒟 e dom l; ¬ final e  e' s' tas. extTA,P,t  e,(h, l) -tas e',s'" by fact+
have ref:  by simp
show ?case
proof (cases "final a")
assume fa: "final a"
show ?case
proof (cases "final i")
assume fi: "final i"
show ?case
proof (cases "final e")
assume fe: "final e"
with WTrtAAssNT fa fi show ?thesis
by (fastforce simp:final_iff intro: RedAAssNull AAssThrow1 AAssThrow2 AAssThrow3)
next
assume "¬ final e"
with WTrtAAssNT fa fi show ?thesis
by (fastforce simp: final_iff intro!:AAssRed3 AAssThrow1 AAssThrow2)
qed
next
assume "¬ final i"
with WTrtAAssNT fa show ?thesis
by (fastforce simp: final_iff intro!:AAssRed2 AAssThrow1)
qed
next
assume "¬ final a"
with WTrtAAssNT show ?thesis by (fastforce simp: final_iff intro!:AAssRed1)
qed
next
case (WTrtALength E a T l)
show ?case
proof(cases "final a")
case True
note wta = P,E,h  a : T⌊⌉
thus ?thesis
proof(rule finalRefE[OF _ _ True])
show "is_refT (T⌊⌉)" by simp
next
assume "a = null"
thus ?thesis by(fastforce intro: RedALengthNull)
next
with wta show ?thesis by(fastforce intro: RedALength)
next
thus ?thesis by (fastforce intro: ALengthThrow)
qed simp
next
case False
from 𝒟 (a∙length) dom l have "𝒟 a dom l" by simp
with False 𝒟 a dom l; ¬ final a  e' s' ta. extTA,P,t  a,(h, l) -ta e',s'
obtain e' s' ta where "extTA,P,t  a,(h, l) -ta e',s'" by blast
thus ?thesis by(blast intro: ALengthRed)
qed
next
case (WTrtALengthNT E a T l)
show ?case
proof(cases "final a")
case True
note wta = P,E,h  a : NT
thus ?thesis
proof(rule finalRefE[OF _ _ True])
show  by simp
next
assume "a = null"
thus ?thesis by(blast intro: RedALengthNull)
next
thus ?thesis by(blast intro: ALengthThrow)
qed simp_all
next
case False
from 𝒟 (a∙length) dom l have "𝒟 a dom l" by simp
with False 𝒟 a dom l; ¬ final a  e' s' ta. extTA,P,t  a,(h, l) -ta e',s'
obtain e' s' ta where "extTA,P,t  a,(h, l) -ta e',s'" by blast
thus ?thesis by(blast intro: ALengthRed)
qed
next
case (WTrtFAcc E e U C F T fm D l)
have wte: "P,E,h  e : U"
and icto:
and field: "P  C has F:T (fm) in D" by fact+
show ?case
proof cases
assume "final e"
with wte icto show ?thesis
with wte obtain hU where ty: "typeof_addr h a = hU" "U = ty_of_htype hU" by auto
with icto field have "P,h  a@CField D F : T" by(auto intro: addr_loc_type.intros)
obtain v where "heap_read h a (CField D F) v" by blast
with addr ty show ?thesis by(fastforce intro: RedFAcc)
next
fix a assume "e = Throw a"
thus ?thesis by(fastforce intro:FAccThrow)
qed
next
assume "¬ final e" with WTrtFAcc show ?thesis
by(fastforce intro!:FAccRed)
qed
next
case (WTrtFAccNT E e F D T l)
show ?case
proof cases
assume "final e"  ― ‹@{term e} is @{term null} or @{term throw}
with WTrtFAccNT show ?thesis
by(fastforce simp:final_iff intro: RedFAccNull FAccThrow)
next
assume "¬ final e" ― ‹@{term e} reduces by IH›
with WTrtFAccNT show ?thesis by simp (fast intro:FAccRed)
qed
next
case (WTrtFAss E e1 U C F T fm D e2 T2 l)
have wte1: "P,E,h  e1 : U"
and icto:
and field: "P  C has F:T (fm) in D" by fact+
show ?case
proof cases
assume "final e1"
with wte1 icto show ?thesis
fix a assume e1: "e1 = addr a"
show ?thesis
proof cases
assume "final e2"
thus ?thesis
proof (rule finalE)
fix v assume e2: "e2 = Val v"
from wte1 field icto e1 have adal: "P,h  a@CField D F : T"
from e2 P  T2  T P,E,h  e2 : T2
have "P,h  v :≤ T" by(auto simp add: conf_def)
from heap_write_total[OF hconf adal this] obtain h'
where "heap_write h a (CField D F) v h'" ..
with wte1 field e1 e2 show ?thesis
by(fastforce intro: RedFAss)
next
fix a assume "e2 = Throw a"
thus ?thesis using e1 by(fastforce intro:FAssThrow2)
qed
next
assume "¬ final e2" with WTrtFAss final e1 e1 show ?thesis
by simp (fast intro!:FAssRed2)
qed
next
fix a assume "e1 = Throw a"
thus ?thesis by(fastforce intro:FAssThrow1)
qed
next
assume "¬ final e1" with WTrtFAss show ?thesis
by(simp del: split_paired_Ex)(blast intro!:FAssRed1)
qed
next
case (WTrtFAssNT E e1 e2 T2 F D l)
show ?case
proof cases
assume "final e1"  ― ‹@{term e1} is @{term null} or @{term throw}
show ?thesis
proof cases
assume "final e2"  ― ‹@{term e2} is @{term Val} or @{term throw}
with WTrtFAssNT final e1 show ?thesis
by(fastforce simp:final_iff intro: RedFAssNull FAssThrow1 FAssThrow2)
next
assume "¬ final e2" ― ‹@{term e2} reduces by IH›
with WTrtFAssNT final e1 show ?thesis
by (fastforce  simp:final_iff intro!:FAssRed2 FAssThrow1)
qed
next
assume "¬ final e1" ― ‹@{term e1} reduces by IH›
with WTrtFAssNT show ?thesis by (fastforce intro:FAssRed1)
qed
next
case (WTrtCAS E e1 U C F T fm D e2 T2 e3 T3)
show ?case
proof(cases "final e1")
case e1: True
with WTrtCAS.hyps(1,3) show ?thesis
fix a
assume e1: "e1 = addr a"
with WTrtCAS.hyps(1) obtain hU
where ty: "typeof_addr h a = hU" "U = ty_of_htype hU" by auto
with WTrtCAS.hyps(3,4) have adal: "P,h  a@CField D F : T" by(auto intro: addr_loc_type.intros)
obtain v where v: "heap_read h a (CField D F) v" by blast
show ?thesis
proof(cases "final e2")
case e2: True
show ?thesis
proof(cases "final e3")
case e3: True
consider (Val2) v2 where "e2 = Val v2" | (Throw2) a2 where "e2 = Throw a2"
using e2 by(auto simp add: final_iff)
then show ?thesis
proof(cases)
case Val2
consider (Succeed) v3 where "e3 = Val v3" "v2 = v"
| (Fail) v3 where "e3 = Val v3" "v2  v"
| (Throw3) a3 where "e3 = Throw a3"
using e3 by(auto simp add: final_iff)
then show ?thesis
proof cases
case Succeed
with WTrtCAS.hyps(9,11) adal have "P,h  v3 :≤ T" by(auto simp add: conf_def)
from heap_write_total[OF hconf adal this] obtain h'
where "heap_write h a (CField D F) v3 h'" ..
with Val2 e1 v Succeed show ?thesis
by(auto intro: RedCASSucceed simp del: split_paired_Ex)
next
case Fail
with Val2 e1 v show ?thesis
by(auto intro: RedCASFail simp del: split_paired_Ex)
next
case Throw3
then show ?thesis using e1 Val2 by(auto intro: CASThrow3 simp del: split_paired_Ex)
qed
next
case Throw2
then show ?thesis using e1 by(auto intro: CASThrow2 simp del: split_paired_Ex)
qed
next
case False
with WTrtCAS e1 e2 show ?thesis
by(fastforce simp del: split_paired_Ex simp add: final_iff intro: CASRed3 CASThrow2)
qed
next
case False
with WTrtCAS e1 show ?thesis
by(fastforce intro: CASRed2 CASThrow2 simp del: split_paired_Ex)
qed
qed(fastforce intro: CASThrow)
next
case False
then show ?thesis using WTrtCAS by(fastforce intro: CASRed1)
qed
next
case (WTrtCASNT E e1 e2 T2 e3 T3 D F)
note [simp del] = split_paired_Ex
show ?case
proof(cases "final e1")
case e1: True
show ?thesis
proof(cases "final e2")
case e2: True
show ?thesis
proof(cases "final e3")
case True
with e1 e2 WTrtCASNT show ?thesis
by(fastforce simp add: final_iff intro: CASNull CASThrow CASThrow2 CASThrow3)
next
case False
with e1 e2 WTrtCASNT show ?thesis
by(fastforce simp add: final_iff intro: CASRed3 CASThrow CASThrow2)
qed
next
case False
with e1 WTrtCASNT show ?thesis
by(fastforce simp add: final_iff intro: CASRed2 CASThrow)
qed
next
case False
with WTrtCASNT show ?thesis
by(fastforce simp add: final_iff intro: CASRed1)
qed
next
case (WTrtCall E e U C M Ts T meth D es Ts' l)
have wte: "P,E,h  e : U"
and icto:  by fact+
have IHe: "l.  𝒟 e dom l; ¬ final e
e' s' tas. extTA,P,t  e,(h, l) -tas e',s'" by fact
have sees: "P  C sees M: TsT = meth in D" by fact
have wtes: "P,E,h  es [:] Ts'" by fact
have IHes: "l. 𝒟s es dom l; ¬ finals es  es' s' ta. extTA,P,t  es,(h, l) [-ta→] es',s'" by fact
have subtype: "P  Ts' [≤] Ts" by fact
have dae: "𝒟 (eM(es)) dom l" by fact
show ?case
proof(cases "final e")
assume fine: "final e"
with wte icto show ?thesis
show ?thesis
proof(cases "vs. es = map Val vs")
assume es: "vs. es = map Val vs"
from wte e_addr obtain hU where ha: "typeof_addr h a = hU" "U = ty_of_htype hU"  by(auto)
have "length es = length Ts'" using wtes by(auto simp add: WTrts_conv_list_all2 dest: list_all2_lengthD)
moreover from subtype have "length Ts' = length Ts" by(auto dest: list_all2_lengthD)
ultimately have esTs: "length es = length Ts" by(auto)
show ?thesis
proof(cases meth)
case (Some pnsbody)
with esTs e_addr ha sees subtype es sees_wf_mdecl[OF wf sees] icto
show ?thesis by(cases pnsbody) (fastforce intro!: RedCall simp:list_all2_iff wf_mdecl_def)
next
case None
with sees wf have "DM(Ts) :: T" by(auto intro: sees_wf_native)
moreover from es obtain vs where vs: "es = map Val vs" ..
with wtes have tyes: "map typeof⇘hvs = map Some Ts'" by simp
with ha DM(Ts) :: T icto sees None
have "P,h  aM(vs) : T" using subtype by(auto simp add: external_WT'_iff)
from external_call_progress[OF wf this hconf, of t] obtain ta va h'
where "P,t  aM(vs), h -ta→ext va, h'" by blast
thus ?thesis using ha icto None sees vs e_addr
by(fastforce intro: RedCallExternal simp del: split_paired_Ex)
qed
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 b where ex_Throw: "?ex = Throw b"
by(fast elim!:finalE)
show ?thesis using e_addr es ex_Throw ves
by(fastforce intro: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 e_addr dae IHes  by(fastforce intro!:CallParams)
qed
qed
next
fix a assume "e = Throw a"
thus ?thesis by(fast intro!:CallThrowObj)
qed
next
assume "¬ final e"
with WTrtCall show ?thesis by(simp del: split_paired_Ex)(blast intro!:CallObj)
qed
next
case (WTrtCallNT E e es Ts M T l)
have wte: "P,E,h  e : NT" by fact
have IHe: "l.  𝒟 e dom l; ¬ final e
e' s' tas. extTA,P,t  e,(h, l) -tas e',s'"  by fact
have IHes: "l. 𝒟s es dom l; ¬ finals es  es' s' ta. extTA,P,t  es,(h, l) [-ta→] es',s'" by fact
have wtes: "P,E,h  es [:] Ts" by fact
have dae: "𝒟 (eM(es)) dom l" by fact
show ?case
proof(cases "final e")
assume "final e"
moreover
{ fix v assume "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 = null finals es have ?thesis by(fastforce intro: RedCallNull) }
moreover
{ fix vs a es' assume "es = map Val vs @ Throw a # es'"
with WTrtCallNT e = null finals es have ?thesis by(fastforce intro: CallThrowParams) }
ultimately show ?thesis by(fastforce simp:finals_iff)
next
assume "¬ finals es" ― ‹@{term es} reduces by IH›
with WTrtCallNT e = null show ?thesis by(fastforce intro: CallParams)
qed
}
moreover
{ fix a assume "e = Throw a"
with WTrtCallNT have ?case by(fastforce intro: CallThrowObj) }
ultimately show ?thesis by(fastforce simp:final_iff)
next
assume "¬ final e" ― ‹@{term e} reduces by IH›
with WTrtCallNT show ?thesis by (fastforce intro:CallObj)
qed
next
case (WTrtBlock E V T e T' vo l)
have IH: "l. 𝒟 e dom l; ¬ final e
e' s' tas. extTA,P,t  e,(h,l) -tas e',s'"
and D: "𝒟 {V:T=vo; e} dom l" by fact+
show ?case
proof cases
assume "final e"
thus ?thesis
proof (rule finalE)
fix v assume "e = Val v" thus ?thesis by(fast intro:RedBlock)
next
fix a assume "e = Throw a"
thus ?thesis by(fast intro:BlockThrow)
qed
next
assume not_fin: "¬ final e"
from D have De: "𝒟 e dom(l(V:=vo))" by(auto simp add:hyperset_defs)
from IH[OF De not_fin]
obtain h' l' e' tas where red: "extTA,P,t  e,(h,l(V:=vo)) -tas e',(h',l')"
by auto
thus ?thesis by(blast intro: BlockRed)
qed
next
case (WTrtSynchronized E o' T e T' l)
note wto = P,E,h  o' : T
note IHe = l. 𝒟 e dom l; ¬ final e   e' s' tas. extTA,P,t  e,(h, l) -tas e',s'
note wte = P,E,h  e : T'
note IHo = l. 𝒟 o' dom l; ¬ final o'   e' s' tas. extTA,P,t  o',(h, l) -tas e',s'
note refT = is_refT T
note dae = 𝒟 (sync(o') e) dom l
show ?case
proof(cases "final o'")
assume fino: "final o'"
thus ?thesis
proof (rule finalE)
fix v
assume oval: "o' = Val v"
with wto refT show ?thesis
proof(cases "v")
assume vnull: "v = Null"
with oval vnull show ?thesis
by(fastforce intro: SynchronizedNull)
next
thus ?thesis using oval
by(fastforce intro: LockSynchronized)
qed(auto elim: refTE)
next
fix a
assume othrow: "o' = Throw a"
thus ?thesis by(fastforce intro: SynchronizedThrow1)
qed
next
assume nfino: "¬ final o'"
with dae IHo show ?case by(fastforce intro: SynchronizedRed1)
qed
next
case (WTrtInSynchronized E a T e T' l)
show ?case
proof(cases "final e")
case True thus ?thesis
by(fastforce elim!: finalE intro: UnlockSynchronized SynchronizedThrow2)
next
case False
moreover from 𝒟 (insync(a) e) dom l have "𝒟 e dom l" by simp
moreover note IHe = l. 𝒟 e dom l; ¬ final e  e' s' tas. extTA,P,t  e,(h, l) -tas e',s'
ultimately show ?thesis by(fastforce intro: SynchronizedRed2)
qed
next
case (WTrtSeq E e1 T1 e2 T2 l)
show ?case
proof cases
assume "final e1"
thus ?thesis
by(fast elim:finalE intro:intro:RedSeq SeqThrow)
next
assume "¬ final e1" with WTrtSeq show ?thesis
by(simp del: split_paired_Ex)(blast intro!:SeqRed)
qed
next
case (WTrtCond E e e1 T1 e2 T2 T l)
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 auto
show ?thesis
proof (cases b)
case True with val v show ?thesis by(fastforce intro:RedCondT)
next
case False with val v show ?thesis by(fastforce intro:RedCondF)
qed
next
fix a assume "e = Throw a"
thus ?thesis by(fast intro: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 e T T' l)
show ?case
proof cases
assume "final e" ― ‹Then @{term e} must be @{term throw} or @{term null}
thus ?thesis
proof(induct rule: finalE)
case (Val v)
with P  T  Class Throwable ¬ final (throw e) P,E,h  e : T
have "v = Null" by(cases v)(auto simp add: final_iff widen_Class)
thus ?thesis using Val by(fastforce intro: RedThrowNull)
next
case (Throw a)
thus ?thesis by(fastforce intro: ThrowThrow)
qed
next
assume "¬ final e" ― ‹Then @{term e} must reduce›
with WTrtThrow show ?thesis by simp (blast intro:ThrowRed)
qed
next
case (WTrtTry E e1 T1 V C e2 T2 l)
have wt1: "P,E,h  e1 : T1" by fact
show ?case
proof cases
assume "final e1"
thus ?thesis
proof (rule finalE)
fix v assume "e1 = Val v"
thus ?thesis by(fast intro:RedTry)
next
fix a
assume e1_Throw: "e1 = Throw a"
with wt1 obtain D where ha: "typeof_addr h a = Class_type D"
thus ?thesis using e1_Throw
by(cases "P  D * C")(fastforce intro:RedTryCatch RedTryFail)+
qed
next
assume "¬ final e1"
with WTrtTry show ?thesis by simp (fast intro:TryRed)
qed
next
case WTrtNil thus ?case by simp
next
case (WTrtCons E e T es Ts)
have IHe: "l. 𝒟 e dom l; ¬ final e
e' s' ta. extTA,P,t  e,(h,l) -ta e',s'"
and IHes: "l. 𝒟s es dom l; ¬ finals es
es' s' ta. extTA,P,t  es,(h,l) [-ta→] es',s'"
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 Des' not_fins_tl]
by (blast intro!:ListRed2)
next
fix a assume "e = Throw a"
hence False using not_fins by simp
thus ?thesis ..
qed
next
assume "¬ final e"
with IHe[OF De] show ?thesis by(fast intro!:ListRed1)
qed
qed

end