(*  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₀ :: 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₀"

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}:
  "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₁#T₂#ST, LT)) = (ST,LT)"

| eff_{i_CAS}:
  "eff_i (CAS F C, P, (T₁#T₂#T₃#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}:
  "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₁#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))"
| rel_ALoad:
  "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 = []"
by (simp add: eff_def)

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

(* FIXME: getfield, \<exists>T D. P \<turnstile> C sees F:T in D \<and> .. *)

text "Conditions under which eff is applicable:"

fun app_i :: "'addr instr × 'm prog × pc × nat × ty × ty_i → bool"
where
  app_{i_Load}:
  "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₁#T₂#ST, LT)) =
    (∃T_f fm. P ⊨ C sees F:T_f (fm) in C ∧ P ⊨ T₂ ≤ (Class C) ∧ P ⊨ T₁ ≤ T_f)" 
| app_{i_CAS}:
  "app_i (CAS F C, P, pc, mxs, T_r, (T₃#T₂#T₁#ST, LT)) =
    (∃T_f fm. P ⊨ C sees F:T_f (fm) in C ∧ volatile fm ∧ P ⊨ T₁ ≤ Class C ∧ P ⊨ T₂ ≤ T_f ∧ P ⊨ T₃ ≤ 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}:
  "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))"
by (simp add: app_def)

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
  rules for @{term app}
 ›
lemma appNone[simp]: "app i P mxs T_r pc mpc et None = True" 
  by (simp add: app_def)


lemma appLoad[simp]:
"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)

lemma appALoad[simp]:
  "app_i (ALoad,P,pc,mxs,T_r,s) =
  (∃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₁ T₂ ST'. ST = T₁#T₂#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₁ T₂ ST' assume "ST = T₁#T₂#ST'"
    hence ?thesis by (cases T₁, 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₁ T₂. ST = [T₁, T₂]) ∨ (∃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₁ T₂ ST'. ST = T₁#T₂#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₁ T₂ ST' assume "ST = T₁#T₂#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›

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)"
by(simp add: the_WTrt_binop_code)

lemmas eff_{i_code}[code] =
  eff_{i_Load} eff_{i_Store} eff_{i_Push} eff_{i_Getfield} eff_{i_Putfield} eff_{i_New} eff_{i_NewArray} eff_{i_ALoad}
  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₁#T₂#ST, LT)) ⟷
   P ⊨ T₂ ≤ (Class C) ∧
   Predicate.holds (Predicate.bind (sees_field_i_i_i_o_o_i P C F C) (λ(T, fm). if P ⊨ T₁ ≤ 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₃#T₂#T₁#ST, LT)) ⟷
   P ⊨ T₁ ≤ Class C ∧
  Predicate.holds (Predicate.bind (sees_field_i_i_i_o_o_i P C F C) (λ(T, fm). if P ⊨ T₂ ≤ T ∧ P ⊨ T₃ ≤ T ∧ volatile fm then Predicate.single () else bot))"
by(auto simp add: holds_eq eval_sees_field_i_i_i_o_i_conv)

lemma app_{i_ALoad_code}:
  "app_i (ALoad, P, pc, mxs, T_r, (T1#T2#ST,LT)) =
   (T1 = Integer ∧ (case T2 of Ty⌊⌉ → True | NT → True | _ → False))"
by(simp add: split: ty.split)

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))"
by(simp add: split: ty.split)

lemma app_{i_ALength_code}:
  "app_i (ALength, P, pc, mxs, T_r, (T1#ST,LT)) =
   (case T1 of Ty⌊⌉ → True | NT → True | _ → False)"
by(simp add: split: ty.split)

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] =
  app_{i_Load} app_{i_Store} app_{i_Push}
  app_{i_Getfield_code} app_{i_Putfield_code} app_{i_CAS_code}
  app_{i_New} app_{i_NewArray}
  app_{i_ALoad_code} app_{i_AStore_code} app_{i_ALength_code}
  app_{i_Checkcast} app_{i_Instanceof}
  app_{i_Pop} app_{i_Dup} app_{i_Swap} app_{i_BinOpInstr_code} app_{i_IfFalse} app_{i_Goto}
  app_{i_Return} app_{i_Throw_code} app_{i_Invoke_code} app_{i_MEnter} app_{i_MExit}
  app_{i_default}

end