# Theory Effect

```(*  Title:      JinjaThreads/BV/Effect.thy
Author:     Gerwin Klein, Andreas Lochbihler
*)

section ‹Effect of Instructions on the State Type›

theory Effect
imports
JVM_SemiType
"../JVM/JVMExceptions"
begin

locale jvm_method = prog +
fixes mxs :: nat
fixes mxl⇩0 :: nat
fixes Ts :: "ty list"
fixes T⇩r :: ty
fixes "is" :: "'addr instr list"
fixes xt :: ex_table

fixes mxl :: nat
defines mxl_def: "mxl ≡ 1+size Ts+mxl⇩0"

text ‹Program counter of successor instructions:›
primrec succs :: "'addr instr ⇒ ty⇩i ⇒ pc ⇒ pc list"
where
"succs (Load idx) τ pc     = [pc+1]"
| "succs (Store idx) τ pc    = [pc+1]"
| "succs (Push v) τ pc       = [pc+1]"
| "succs (Getfield F C) τ pc = [pc+1]"
| "succs (Putfield F C) τ pc = [pc+1]"
| "succs (CAS F C) τ pc      = [pc+1]"
| "succs (New C) τ pc        = [pc+1]"
| "succs (NewArray T) τ pc   = [pc+1]"
| "succs ALoad τ pc          = (if (fst τ)!1 = NT then [] else [pc+1])"
| "succs AStore τ pc         = (if (fst τ)!2 = NT then [] else [pc+1])"
| "succs ALength τ pc        = (if (fst τ)!0 = NT then [] else [pc+1])"
| "succs (Checkcast C) τ pc  = [pc+1]"
| "succs (Instanceof T) τ pc  = [pc+1]"
| "succs Pop τ pc            = [pc+1]"
| "succs Dup τ pc            = [pc+1]"
| "succs Swap τ pc           = [pc+1]"
| "succs (BinOpInstr b) τ pc = [pc+1]"
| succs_IfFalse:
"succs (IfFalse b) τ pc    = [pc+1, nat (int pc + b)]"
| succs_Goto:
"succs (Goto b) τ pc       = [nat (int pc + b)]"
| succs_Return:
"succs Return τ pc         = []"
| succs_Invoke:
"succs (Invoke M n) τ pc   = (if (fst τ)!n = NT then [] else [pc+1])"
| succs_Throw:
"succs ThrowExc τ pc          = []"
| "succs MEnter τ pc         = (if (fst τ)!0 = NT then [] else [pc+1])"
| "succs MExit τ pc          = (if (fst τ)!0 = NT then [] else [pc+1])"

text "Effect of instruction on the state type:"

fun eff⇩i :: "'addr instr × 'm prog × ty⇩i ⇒ ty⇩i"
where
"eff⇩i (Load n,  P, (ST, LT))          = (ok_val (LT ! n) # ST, LT)"

| eff⇩i_Store:
"eff⇩i (Store n, P, (T#ST, LT))        = (ST, LT[n:= OK T])"

| eff⇩i_Push:
"eff⇩i (Push v, P, (ST, LT))             = (the (typeof v) # ST, LT)"

| eff⇩i_Getfield:
"eff⇩i (Getfield F C, P, (T#ST, LT))    = (fst (snd (field P C F)) # ST, LT)"

| eff⇩i_Putfield:
"eff⇩i (Putfield F C, P, (T⇩1#T⇩2#ST, LT)) = (ST,LT)"

| eff⇩i_CAS:
"eff⇩i (CAS F C, P, (T⇩1#T⇩2#T⇩3#ST, LT)) = (Boolean # ST, LT)"

| eff⇩i_New:
"eff⇩i (New C, P, (ST,LT))               = (Class C # ST, LT)"

| eff⇩i_NewArray:
"eff⇩i (NewArray Ty, P, (T#ST,LT))       = (Ty⌊⌉ # ST,LT)"

"eff⇩i (ALoad, P, (T1#T2#ST,LT))       = (the_Array T2# ST,LT)"

| eff⇩i_AStore:
"eff⇩i (AStore, P, (T1#T2#T3#ST,LT))  = (ST,LT)"

| eff⇩i_ALength:
"eff⇩i (ALength, P, (T1#ST,LT))  = (Integer#ST,LT)"

| eff⇩i_Checkcast:
"eff⇩i (Checkcast Ty, P, (T#ST,LT))       = (Ty # ST,LT)"

| eff⇩i_Instanceof:
"eff⇩i (Instanceof Ty, P, (T#ST,LT))       = (Boolean # ST,LT)"

| eff⇩i_Pop:
"eff⇩i (Pop, P, (T#ST,LT))               = (ST,LT)"

| eff⇩i_Dup:
"eff⇩i (Dup, P, (T#ST,LT))               = (T#T#ST,LT)"

| eff⇩i_Swap:
"eff⇩i (Swap, P, (T1#T2#ST,LT))               = (T2#T1#ST,LT)"

| eff⇩i_BinOpInstr:
"eff⇩i (BinOpInstr bop, P, (T2#T1#ST,LT)) = ((THE T. P ⊢ T1«bop»T2 : T)#ST, LT)"

| eff⇩i_IfFalse:
"eff⇩i (IfFalse b, P, (T⇩1#ST,LT))        = (ST,LT)"

| eff⇩i_Invoke:
"eff⇩i (Invoke M n, P, (ST,LT))          =
(let U = fst (snd (snd (method P (the (class_type_of' (ST ! n))) M)))
in (U # drop (n+1) ST, LT))"

| eff⇩i_Goto:
"eff⇩i (Goto n, P, s)                    = s"

| eff⇩i_MEnter:
"eff⇩i (MEnter, P, (T1#ST,LT))           = (ST,LT)"

| eff⇩i_MExit:
"eff⇩i (MExit, P, (T1#ST,LT))            = (ST,LT)"

fun is_relevant_class :: "'addr instr ⇒ 'm prog ⇒ cname ⇒ bool"
where
rel_Getfield:
"is_relevant_class (Getfield F D) = (λP C. P ⊢ NullPointer ≼⇧* C)"
| rel_Putfield:
"is_relevant_class (Putfield F D) = (λP C. P ⊢ NullPointer ≼⇧* C)"
| rel_CAS:
"is_relevant_class (CAS F D)      = (λP C. P ⊢ NullPointer ≼⇧* C)"
| rel_Checcast:
"is_relevant_class (Checkcast T)  = (λP C. P ⊢ ClassCast ≼⇧* C)"
| rel_New:
"is_relevant_class (New D)        = (λP C. P ⊢ OutOfMemory ≼⇧* C)"
| rel_Throw:
"is_relevant_class ThrowExc       = (λP C. True)"
| rel_Invoke:
"is_relevant_class (Invoke M n)   = (λP C. True)"
| rel_NewArray:
"is_relevant_class (NewArray T)   = (λP C. (P ⊢ OutOfMemory ≼⇧* C) ∨ (P ⊢ NegativeArraySize ≼⇧* C))"
"is_relevant_class ALoad          = (λP C. P ⊢ ArrayIndexOutOfBounds ≼⇧* C ∨ P ⊢ NullPointer ≼⇧* C)"
| rel_AStore:
"is_relevant_class AStore         = (λP C. P ⊢ ArrayIndexOutOfBounds ≼⇧* C ∨ P ⊢ ArrayStore ≼⇧* C ∨ P ⊢ NullPointer ≼⇧* C)"
| rel_ALength:
"is_relevant_class ALength        = (λP C. P ⊢ NullPointer ≼⇧* C)"
| rel_MEnter:
"is_relevant_class MEnter         = (λP C. P ⊢ IllegalMonitorState ≼⇧* C ∨ P ⊢ NullPointer ≼⇧* C)"
| rel_MExit:
"is_relevant_class MExit          = (λP C. P ⊢ IllegalMonitorState ≼⇧* C ∨ P ⊢ NullPointer ≼⇧* C)"
| rel_BinOp:
"is_relevant_class (BinOpInstr bop) = binop_relevant_class bop"
| rel_default:
"is_relevant_class i              = (λP C. False)"

definition is_relevant_entry :: "'m prog ⇒ 'addr instr ⇒ pc ⇒ ex_entry ⇒ bool"
where
"is_relevant_entry P i pc e ≡
let (f,t,C,h,d) = e
in (case C of None ⇒ True | ⌊C'⌋ ⇒ is_relevant_class i P C') ∧ pc ∈ {f..<t}"

definition relevant_entries :: "'m prog ⇒ 'addr instr ⇒ pc ⇒ ex_table ⇒ ex_table"
where
"relevant_entries P i pc ≡ filter (is_relevant_entry P i pc)"

definition xcpt_eff :: "'addr instr ⇒ 'm prog ⇒ pc ⇒ ty⇩i ⇒ ex_table ⇒ (pc × ty⇩i') list"
where
"xcpt_eff i P pc τ et ≡ let (ST,LT) = τ in
map (λ(f,t,C,h,d). (h, Some ((case C of None ⇒ Class Throwable | Some C' ⇒ Class C')#drop (size ST - d) ST, LT))) (relevant_entries P i pc et)"

definition norm_eff :: "'addr instr ⇒ 'm prog ⇒ nat ⇒ ty⇩i ⇒ (pc × ty⇩i') list"
where "norm_eff i P pc τ ≡ map (λpc'. (pc',Some (eff⇩i (i,P,τ)))) (succs i τ pc)"

definition eff :: "'addr instr ⇒ 'm prog ⇒ pc ⇒ ex_table ⇒ ty⇩i' ⇒ (pc × ty⇩i') list"
where
"eff i P pc et t ≡
case t of
None ⇒ []
| Some τ ⇒ (norm_eff i P pc τ) @ (xcpt_eff i P pc τ et)"

lemma eff_None:
"eff i P pc xt None = []"

lemma eff_Some:
"eff i P pc xt (Some τ) = norm_eff i P pc τ @ xcpt_eff i P pc τ xt"

(* FIXME: getfield, ∃T D. P ⊢ C sees F:T in D ∧ .. *)

text "Conditions under which eff is applicable:"

fun app⇩i :: "'addr instr × 'm prog × pc × nat × ty × ty⇩i ⇒ bool"
where
"app⇩i (Load n, P, pc, mxs, T⇩r, (ST,LT)) =
(n < length LT ∧ LT ! n ≠ Err ∧ length ST < mxs)"
| app⇩i_Store:
"app⇩i (Store n, P, pc, mxs, T⇩r, (T#ST, LT)) =
(n < length LT)"
| app⇩i_Push:
"app⇩i (Push v, P, pc, mxs, T⇩r, (ST,LT)) =
(length ST < mxs ∧ typeof v ≠ None)"
| app⇩i_Getfield:
"app⇩i (Getfield F C, P, pc, mxs, T⇩r, (T#ST, LT)) =
(∃T⇩f fm. P ⊢ C sees F:T⇩f (fm) in C ∧ P ⊢ T ≤ Class C)"
| app⇩i_Putfield:
"app⇩i (Putfield F C, P, pc, mxs, T⇩r, (T⇩1#T⇩2#ST, LT)) =
(∃T⇩f fm. P ⊢ C sees F:T⇩f (fm) in C ∧ P ⊢ T⇩2 ≤ (Class C) ∧ P ⊢ T⇩1 ≤ T⇩f)"
| app⇩i_CAS:
"app⇩i (CAS F C, P, pc, mxs, T⇩r, (T⇩3#T⇩2#T⇩1#ST, LT)) =
(∃T⇩f fm. P ⊢ C sees F:T⇩f (fm) in C ∧ volatile fm ∧ P ⊢ T⇩1 ≤ Class C ∧ P ⊢ T⇩2 ≤ T⇩f ∧ P ⊢ T⇩3 ≤ T⇩f)"
| app⇩i_New:
"app⇩i (New C, P, pc, mxs, T⇩r, (ST,LT)) =
(is_class P C ∧ length ST < mxs)"
| app⇩i_NewArray:
"app⇩i (NewArray Ty, P, pc, mxs, T⇩r, (Integer#ST,LT)) =
is_type P (Ty⌊⌉)"
"app⇩i (ALoad, P, pc, mxs, T⇩r, (T1#T2#ST,LT)) =
(T1 = Integer ∧ (T2 ≠ NT ⟶ (∃Ty. T2 = Ty⌊⌉)))"
| app⇩i_AStore:
"app⇩i (AStore, P, pc, mxs, T⇩r, (T1#T2#T3#ST,LT)) =
(T2 = Integer ∧ (T3 ≠ NT ⟶ (∃Ty. T3 = Ty⌊⌉)))"
| app⇩i_ALength:
"app⇩i (ALength, P, pc, mxs, T⇩r, (T1#ST,LT)) =
(T1 = NT ∨ (∃Ty. T1 = Ty⌊⌉))"
| app⇩i_Checkcast:
"app⇩i (Checkcast Ty, P, pc, mxs, T⇩r, (T#ST,LT)) =
(is_type P Ty)"
| app⇩i_Instanceof:
"app⇩i (Instanceof Ty, P, pc, mxs, T⇩r, (T#ST,LT)) =
(is_type P Ty ∧ is_refT T)"
| app⇩i_Pop:
"app⇩i (Pop, P, pc, mxs, T⇩r, (T#ST,LT)) =
True"
| app⇩i_Dup:
"app⇩i (Dup, P, pc, mxs, T⇩r, (T#ST,LT)) =
(Suc (length ST) < mxs)"
| app⇩i_Swap:
"app⇩i (Swap, P, pc, mxs, T⇩r, (T1#T2#ST,LT)) = True"
| app⇩i_BinOpInstr:
"app⇩i (BinOpInstr bop, P, pc, mxs, T⇩r, (T2#T1#ST,LT)) = (∃T. P ⊢ T1«bop»T2 : T)"
| app⇩i_IfFalse:
"app⇩i (IfFalse b, P, pc, mxs, T⇩r, (Boolean#ST,LT)) =
(0 ≤ int pc + b)"
| app⇩i_Goto:
"app⇩i (Goto b, P, pc, mxs, T⇩r, s) =  (0 ≤ int pc + b)"
| app⇩i_Return:
"app⇩i (Return, P, pc, mxs, T⇩r, (T#ST,LT)) = (P ⊢ T ≤ T⇩r)"
| app⇩i_Throw:
"app⇩i (ThrowExc, P, pc, mxs, T⇩r, (T#ST,LT)) =
(T = NT ∨ (∃C. T = Class C ∧ P ⊢ C ≼⇧* Throwable))"
| app⇩i_Invoke:
"app⇩i (Invoke M n, P, pc, mxs, T⇩r, (ST,LT)) =
(n < length ST ∧
(ST!n ≠ NT ⟶
(∃C D Ts T m. class_type_of' (ST ! n) = ⌊C⌋ ∧ P ⊢ C sees M:Ts → T = m in D ∧ P ⊢ rev (take n ST) [≤] Ts)))"
| app⇩i_MEnter:
"app⇩i (MEnter,P, pc,mxs,T⇩r,(T#ST,LT)) = (is_refT T)"
| app⇩i_MExit:
"app⇩i (MExit,P, pc,mxs,T⇩r,(T#ST,LT)) = (is_refT T)"
| app⇩i_default:
"app⇩i (i,P, pc,mxs,T⇩r,s) = False"

definition xcpt_app :: "'addr instr ⇒ 'm prog ⇒ pc ⇒ nat ⇒ ex_table ⇒ ty⇩i ⇒ bool"
where
"xcpt_app i P pc mxs xt τ ≡ ∀(f,t,C,h,d) ∈ set (relevant_entries P i pc xt). (case C of None ⇒ True | Some C' ⇒ is_class P C') ∧ d ≤ size (fst τ) ∧ d < mxs"

definition app :: "'addr instr ⇒ 'm prog ⇒ nat ⇒ ty ⇒ nat ⇒ nat ⇒ ex_table ⇒ ty⇩i' ⇒ bool"
where
"app i P mxs T⇩r pc mpc xt t ≡ case t of None ⇒ True | Some τ ⇒
app⇩i (i,P,pc,mxs,T⇩r,τ) ∧ xcpt_app i P pc mxs xt τ ∧
(∀(pc',τ') ∈ set (eff i P pc xt t). pc' < mpc)"

lemma app_Some:
"app i P mxs T⇩r pc mpc xt (Some τ) =
(app⇩i (i,P,pc,mxs,T⇩r,τ) ∧ xcpt_app i P pc mxs xt τ ∧
(∀(pc',s') ∈ set (eff i P pc xt (Some τ)). pc' < mpc))"

locale eff = jvm_method +
fixes eff⇩i and app⇩i and eff and app
fixes norm_eff and xcpt_app and xcpt_eff

fixes mpc
defines "mpc ≡ size is"

defines "eff⇩i i τ ≡ Effect.eff⇩i (i,P,τ)"
notes eff⇩i_simps [simp] = Effect.eff⇩i.simps [where P = P, folded eff⇩i_def]

defines "app⇩i i pc τ ≡ Effect.app⇩i (i, P, pc, mxs, T⇩r, τ)"
notes app⇩i_simps [simp] = Effect.app⇩i.simps [where P=P and mxs=mxs and T⇩r=T⇩r, folded app⇩i_def]

defines "xcpt_eff i pc τ ≡ Effect.xcpt_eff i P pc τ xt"
notes xcpt_eff = Effect.xcpt_eff_def [of _ P _ _ xt, folded xcpt_eff_def]

defines "norm_eff i pc τ ≡ Effect.norm_eff i P pc τ"
notes norm_eff = Effect.norm_eff_def [of _ P, folded norm_eff_def eff⇩i_def]

defines "eff i pc ≡ Effect.eff i P pc xt"
notes eff = Effect.eff_def [of _ P  _ xt, folded eff_def norm_eff_def xcpt_eff_def]

defines "xcpt_app i pc τ ≡ Effect.xcpt_app i P pc mxs xt τ"
notes xcpt_app = Effect.xcpt_app_def [of _ P _ mxs xt, folded xcpt_app_def]

defines "app i pc ≡ Effect.app i P mxs T⇩r pc mpc xt"
notes app = Effect.app_def [of _ P mxs T⇩r _ mpc xt, folded app_def xcpt_app_def app⇩i_def eff_def]

lemma length_cases2:
assumes "⋀LT. P ([],LT)"
assumes "⋀l ST LT. P (l#ST,LT)"
shows "P s"
by (cases s, cases "fst s") (auto intro!: assms)

lemma length_cases3:
assumes "⋀LT. P ([],LT)"
assumes "⋀l LT. P ([l],LT)"
assumes "⋀l l' ST LT. P (l#l'#ST,LT)"
shows "P s"
apply(rule length_cases2; (rule assms)?)
subgoal for l ST LT by(cases ST; clarsimp simp: assms)
done

lemma length_cases4:
assumes "⋀LT. P ([],LT)"
assumes "⋀l LT. P ([l],LT)"
assumes "⋀l l' LT. P ([l,l'],LT)"
assumes "⋀l l' l'' ST LT. P (l#l'#l''#ST,LT)"
shows "P s"
apply(rule length_cases3; (rule assms)?)
subgoal for l l' ST LT by(cases ST; clarsimp simp: assms)
done

lemma length_cases5:
assumes "⋀LT. P ([],LT)"
assumes "⋀l LT. P ([l],LT)"
assumes "⋀l l' LT. P ([l,l'],LT)"
assumes "⋀l l' l'' LT. P ([l,l',l''],LT)"
assumes "⋀l l' l'' l''' ST LT. P (l#l'#l''#l'''#ST,LT)"
shows "P s"
apply(rule length_cases4; (rule assms)?)
subgoal for l l' l'' ST LT by(cases ST; clarsimp simp: assms)
done

text ‹
\medskip
simp rules for @{term app}
›
lemma appNone[simp]: "app i P mxs T⇩r pc mpc et None = True"

"app⇩i (Load idx, P, T⇩r, mxs, pc, s) = (∃ST LT. s = (ST,LT) ∧ idx < length LT ∧ LT!idx ≠ Err ∧ length ST < mxs)"
by (cases s, simp)

lemma appStore[simp]:
"app⇩i (Store idx,P,pc,mxs,T⇩r,s) = (∃ts ST LT. s = (ts#ST,LT) ∧ idx < length LT)"
by (rule length_cases2, auto)

lemma appPush[simp]:
"app⇩i (Push v,P,pc,mxs,T⇩r,s) =
(∃ST LT. s = (ST,LT) ∧ length ST < mxs ∧ typeof v ≠ None)"
by (cases s, simp)

lemma appGetField[simp]:
"app⇩i (Getfield F C,P,pc,mxs,T⇩r,s) =
(∃ oT vT ST LT fm. s = (oT#ST, LT) ∧
P ⊢ C sees F:vT (fm) in C ∧ P ⊢ oT ≤ (Class C))"
by (rule length_cases2 [of _ s]) auto

lemma appPutField[simp]:
"app⇩i (Putfield F C,P,pc,mxs,T⇩r,s) =
(∃ vT vT' oT ST LT fm. s = (vT#oT#ST, LT) ∧
P ⊢ C sees F:vT' (fm) in C ∧ P ⊢ oT ≤ (Class C) ∧ P ⊢ vT ≤ vT')"
by (rule length_cases4 [of _ s], auto)

lemma appCAS[simp]:
"app⇩i (CAS F C, P, pc, mxs, T⇩r, s) =
(∃ T1 T2 T3 T' ST LT fm. s = (T3 # T2 # T1 # ST, LT) ∧
P ⊢ C sees F:T' (fm) in C ∧ volatile fm ∧ P ⊢ T1 ≤ Class C ∧ P ⊢ T2 ≤ T' ∧ P ⊢ T3 ≤ T')"
by(rule length_cases4[of _ s]) auto

lemma appNew[simp]:
"app⇩i (New C,P,pc,mxs,T⇩r,s) =
(∃ST LT. s=(ST,LT) ∧ is_class P C ∧ length ST < mxs)"
by (cases s, simp)

lemma appNewArray[simp]:
"app⇩i (NewArray Ty,P,pc,mxs,T⇩r,s) =
(∃ST LT. s=(Integer#ST,LT) ∧ is_type P (Ty⌊⌉))"
by (cases s, simp, cases "fst s", simp)(cases "hd (fst s)", auto)

(∃T ST LT. s=(Integer#T#ST,LT) ∧ (T ≠ NT ⟶ (∃T'.  T = T'⌊⌉)))"
proof -
obtain ST LT where [simp]: "s = (ST, LT)" by (cases s)
have "ST = [] ∨ (∃T. ST = [T]) ∨ (∃T⇩1 T⇩2 ST'. ST = T⇩1#T⇩2#ST')"
by (cases ST, auto, case_tac list, auto)
moreover
{ assume "ST = []" hence ?thesis by simp }
moreover
{ fix T assume "ST = [T]" hence ?thesis by (cases T, auto) }
moreover
{ fix T⇩1 T⇩2 ST' assume "ST = T⇩1#T⇩2#ST'"
hence ?thesis by (cases T⇩1, auto)
}
ultimately show ?thesis by blast
qed

lemma appAStore[simp]:
"app⇩i (AStore,P,pc,mxs,T⇩r,s) =
(∃T U ST LT. s=(T#Integer#U#ST,LT) ∧ (U ≠ NT ⟶ (∃T'. U = T'⌊⌉)))"
proof -
obtain ST LT where [simp]: "s = (ST, LT)" by (cases s)
have "ST = [] ∨ (∃T. ST = [T]) ∨ (∃T⇩1 T⇩2. ST = [T⇩1, T⇩2]) ∨ (∃T1 T2 T3 ST'. ST = T1 # T2 # T3 # ST')"
by (cases ST, auto, case_tac list, auto, case_tac lista, auto)
moreover
{ assume "ST = []" hence ?thesis by simp }
moreover
{ fix T assume "ST = [T]" hence ?thesis by(simp) }
moreover
{ fix T1 T2 assume "ST = [T1, T2]" hence ?thesis by simp }
moreover
{ fix T1 T2 T3 ST' assume "ST = T1 # T2 # T3 # ST'" hence ?thesis by(cases T2, auto) }
ultimately show ?thesis by blast
qed

lemma appALength[simp]:
"app⇩i (ALength,P,pc,mxs,T⇩r,s) =
(∃T ST LT. s=(T#ST,LT) ∧ (T ≠ NT ⟶ (∃T'.  T = T'⌊⌉)))"
by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)

lemma appCheckcast[simp]:
"app⇩i (Checkcast Ty,P,pc,mxs,T⇩r,s) =
(∃T ST LT. s = (T#ST,LT) ∧ is_type P Ty)"
by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)

lemma appInstanceof[simp]:
"app⇩i (Instanceof Ty,P,pc,mxs,T⇩r,s) =
(∃T ST LT. s = (T#ST,LT) ∧ is_type P Ty ∧ is_refT T)"
by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)

lemma app⇩iPop[simp]:
"app⇩i (Pop,P,pc,mxs,T⇩r,s) = (∃ts ST LT. s = (ts#ST,LT))"
by (rule length_cases2, auto)

lemma appDup[simp]:
"app⇩i (Dup,P,pc,mxs,T⇩r,s) =
(∃T ST LT. s = (T#ST,LT) ∧ Suc (length ST) < mxs)"
by (cases s, cases "fst s", simp_all)

lemma app⇩iSwap[simp]:
"app⇩i (Swap,P,pc,mxs,T⇩r,s) = (∃T1 T2 ST LT. s = (T1#T2#ST,LT))"
by(rule length_cases4) auto

lemma appBinOp[simp]:
"app⇩i (BinOpInstr bop,P,pc,mxs,T⇩r,s) = (∃T1 T2 ST LT T. s = (T2 # T1 # ST, LT) ∧ P ⊢ T1«bop»T2 : T)"
proof -
obtain ST LT where [simp]: "s = (ST,LT)" by (cases s)
have "ST = [] ∨ (∃T. ST = [T]) ∨ (∃T⇩1 T⇩2 ST'. ST = T⇩1#T⇩2#ST')"
by (cases ST, auto, case_tac list, auto)
moreover
{ assume "ST = []" hence ?thesis by simp }
moreover
{ fix T assume "ST = [T]" hence ?thesis by (cases T, auto) }
moreover
{ fix T⇩1 T⇩2 ST' assume "ST = T⇩1#T⇩2#ST'"
hence ?thesis by simp
}
ultimately show ?thesis by blast
qed

lemma appIfFalse [simp]:
"app⇩i (IfFalse b,P,pc,mxs,T⇩r,s) =
(∃ST LT. s = (Boolean#ST,LT) ∧ 0 ≤ int pc + b)"
apply (rule length_cases2)
apply simp
apply (case_tac l)
apply auto
done

lemma appReturn[simp]:
"app⇩i (Return,P,pc,mxs,T⇩r,s) = (∃T ST LT. s = (T#ST,LT) ∧ P ⊢ T ≤ T⇩r)"
by (rule length_cases2, auto)

lemma appThrow[simp]:
"app⇩i (ThrowExc,P,pc,mxs,T⇩r,s) = (∃T ST LT. s=(T#ST,LT) ∧ (T = NT ∨ (∃C. T = Class C ∧ P ⊢ C ≼⇧* Throwable)))"
by (rule length_cases2, auto)

lemma appMEnter[simp]:
"app⇩i (MEnter,P,pc,mxs,T⇩r,s) = (∃T ST LT. s=(T#ST,LT) ∧ is_refT T)"
by (rule length_cases2, auto)

lemma appMExit[simp]:
"app⇩i (MExit,P,pc,mxs,T⇩r,s) = (∃T ST LT. s=(T#ST,LT) ∧ is_refT T)"
by (rule length_cases2, auto)

lemma effNone:
"(pc', s') ∈ set (eff i P pc et None) ⟹ s' = None"
by (auto simp add: eff_def xcpt_eff_def norm_eff_def)

lemma relevant_entries_append [simp]:
"relevant_entries P i pc (xt @ xt') = relevant_entries P i pc xt @ relevant_entries P i pc xt'"
by (unfold relevant_entries_def) simp

lemma xcpt_app_append [iff]:
"xcpt_app i P pc mxs (xt@xt') τ = (xcpt_app i P pc mxs xt τ ∧ xcpt_app i P pc mxs xt' τ)"
unfolding xcpt_app_def by force

lemma xcpt_eff_append [simp]:
"xcpt_eff i P pc τ (xt@xt') = xcpt_eff i P pc τ xt @ xcpt_eff i P pc τ xt'"
by (unfold xcpt_eff_def, cases τ) simp

lemma app_append [simp]:
"app i P pc T mxs mpc (xt@xt') τ = (app i P pc T mxs mpc xt τ ∧ app i P pc T mxs mpc xt' τ)"
by (unfold app_def eff_def) auto

subsection ‹Code generator setup›

declare list_all2_Nil [code]
declare list_all2_Cons [code]

lemma eff⇩i_BinOpInstr_code:
"eff⇩i (BinOpInstr bop, P, (T2#T1#ST,LT)) = (Predicate.the (WTrt_binop_i_i_i_i_o P T1 bop T2) # ST, LT)"

lemmas eff⇩i_code[code] =
eff⇩i_AStore eff⇩i_ALength eff⇩i_Checkcast eff⇩i_Instanceof eff⇩i_Pop eff⇩i_Dup eff⇩i_Swap eff⇩i_BinOpInstr_code
eff⇩i_IfFalse eff⇩i_Invoke eff⇩i_Goto eff⇩i_MEnter eff⇩i_MExit

lemma app⇩i_Getfield_code:
"app⇩i (Getfield F C, P, pc, mxs, T⇩r, (T#ST, LT)) ⟷
Predicate.holds (Predicate.bind (sees_field_i_i_i_o_o_i P C F C) (λT. Predicate.single ())) ∧ P ⊢ T ≤ Class C"
apply(clarsimp simp add: Predicate.bind_def Predicate.single_def holds_eq eval_sees_field_i_i_i_o_i_conv)
done

lemma app⇩i_Putfield_code:
"app⇩i (Putfield F C, P, pc, mxs, T⇩r, (T⇩1#T⇩2#ST, LT)) ⟷
P ⊢ T⇩2 ≤ (Class C) ∧
Predicate.holds (Predicate.bind (sees_field_i_i_i_o_o_i P C F C) (λ(T, fm). if P ⊢ T⇩1 ≤ T then Predicate.single () else bot))"
by (auto simp add: holds_eq eval_sees_field_i_i_i_o_i_conv split: if_splits)

lemma app⇩i_CAS_code:
"app⇩i (CAS F C, P, pc, mxs, T⇩r, (T⇩3#T⇩2#T⇩1#ST, LT)) ⟷
P ⊢ T⇩1 ≤ Class C ∧
Predicate.holds (Predicate.bind (sees_field_i_i_i_o_o_i P C F C) (λ(T, fm). if P ⊢ T⇩2 ≤ T ∧ P ⊢ T⇩3 ≤ T ∧ volatile fm then Predicate.single () else bot))"

"app⇩i (ALoad, P, pc, mxs, T⇩r, (T1#T2#ST,LT)) =
(T1 = Integer ∧ (case T2 of Ty⌊⌉ ⇒ True | NT ⇒ True | _ ⇒ False))"

lemma app⇩i_AStore_code:
"app⇩i (AStore, P, pc, mxs, T⇩r, (T1#T2#T3#ST,LT)) =
(T2 = Integer ∧ (case T3 of Ty⌊⌉ ⇒ True | NT ⇒ True | _ ⇒ False))"

lemma app⇩i_ALength_code:
"app⇩i (ALength, P, pc, mxs, T⇩r, (T1#ST,LT)) =
(case T1 of Ty⌊⌉ ⇒ True | NT ⇒ True | _ ⇒ False)"

lemma app⇩i_BinOpInstr_code:
"app⇩i (BinOpInstr bop, P, pc, mxs, T⇩r, (T2#T1#ST,LT)) =
Predicate.holds (Predicate.bind (WTrt_binop_i_i_i_i_o P T1 bop T2) (λT. Predicate.single ()))"
by (auto simp add: holds_eq eval_WTrt_binop_i_i_i_i_o)

lemma app⇩i_Invoke_code:
"app⇩i (Invoke M n, P, pc, mxs, T⇩r, (ST,LT)) =
(n < length ST ∧
(ST!n ≠ NT ⟶
(case class_type_of' (ST ! n) of Some C ⇒
Predicate.holds (Predicate.bind (Method_i_i_i_o_o_o_o P C M)
(λ(Ts, _). if P ⊢ rev (take n ST) [≤] Ts then Predicate.single () else bot))
| _ ⇒ False)))"
proof -
have bind_Ex: "⋀P f. Predicate.bind P f = Predicate.Pred (λx. (∃y. Predicate.eval P y ∧ Predicate.eval (f y) x))"
by (rule pred_eqI) auto
thus ?thesis
by (auto simp add: bind_Ex Predicate.single_def holds_eq eval_Method_i_i_i_o_o_o_o_conv split: ty.split)
qed

lemma app⇩i_Throw_code:
"app⇩i (ThrowExc, P, pc, mxs, T⇩r, (T#ST,LT)) =
(case T of NT ⇒ True | Class C ⇒ P ⊢ C ≼⇧* Throwable | _ ⇒ False)"
by(simp split: ty.split)

lemmas app⇩i_code [code] =