Theory Effect

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

header {* \isaheader{Effect of Instructions on the State Type} *}

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

-- FIXME
locale prog =
  fixes P :: "'a prog"

locale jvm_method = prog +
  fixes mxs :: nat  
  fixes mxl0 :: nat   
  fixes Ts :: "ty list" 
  fixes Tr :: ty
  fixes "is" :: "instr list" 
  fixes xt :: ex_table

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

text {* Program counter of successor instructions: *}
consts
  succs :: "instr => tyi => pc => pc list"
primrec 
  "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 (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 Pop τ 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:"

consts 
effi :: "instr × 'm prog × tyi => tyi"

recdef effi "{}"
effi_Load:
"effi (Load n,  P, (ST, LT))          = (ok_val (LT ! n) # ST, LT)"
effi_Store:
"effi (Store n, P, (T#ST, LT))        = (ST, LT[n:= OK T])"
effi_Push:
"effi (Push v, P, (ST, LT))             = (the (typeof v) # ST, LT)"
effi_Getfield:
"effi (Getfield F C, P, (T#ST, LT))    = (snd (field P C F) # ST, LT)"
effi_Putfield:
"effi (Putfield F C, P, (T1#T2#ST, LT)) = (ST,LT)"
effi_New:
"effi (New C, P, (ST,LT))               = (Class C # ST, LT)"
effi_NewArray:
"effi (NewArray Ty, P, (T#ST,LT))       = (Ty⌊⌉ # ST,LT)"
effi_ALoad:
"effi (ALoad, P, (T1#T2#ST,LT))       = (the_Array T2# ST,LT)"
effi_AStore:
"effi (AStore, P, (T1#T2#T3#ST,LT))  = (ST,LT)"
effi_ALength:
"effi (ALength, P, (T1#ST,LT))  = (Integer#ST,LT)"
effi_Checkcast:
"effi (Checkcast Ty, P, (T#ST,LT))       = (Ty # ST,LT)"
effi_Pop:
"effi (Pop, P, (T#ST,LT))               = (ST,LT)"
effi_BinOpInstr:
"effi (BinOpInstr bop, P, (T2#T1#ST,LT)) = ((THE T. P \<turnstile> T1«bop»T2 : T)#ST, LT)"
effi_IfFalse:
"effi (IfFalse b, P, (T1#ST,LT))        = (ST,LT)"
effi_Invoke:
"effi (Invoke M n, P, (ST,LT))          =
  (let T = ST ! n;
       C = the_Class T;
       Ts = rev(take n ST);
       U = if is_external_call P T M then (THE U. P \<turnstile> T•M(Ts) :: U) else fst (snd (snd (method P C M)))
   in (U # drop (n+1) ST, LT))"
effi_Goto:
"effi (Goto n, P, s)                    = s"
effi_MEnter:
"effi (MEnter, P, (T1#ST,LT))           = (ST,LT)"
effi_MExit:
"effi (MExit, P, (T1#ST,LT))            = (ST,LT)"


consts
  is_relevant_class :: "instr => 'm prog => cname => bool" 
recdef is_relevant_class "{}"
rel_Getfield:
  "is_relevant_class (Getfield F D) = (λP C. P \<turnstile> NullPointer \<preceq>* C)" 
rel_Putfield:
  "is_relevant_class (Putfield F D) = (λP C. P \<turnstile> NullPointer \<preceq>* C)" 
rel_Checcast:
  "is_relevant_class (Checkcast T)  = (λP C. P \<turnstile> ClassCast \<preceq>* C)" 
rel_New:
  "is_relevant_class (New D)        = (λP C. P \<turnstile> OutOfMemory \<preceq>* 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 \<turnstile> OutOfMemory \<preceq>* C) ∨ (P \<turnstile> NegativeArraySize \<preceq>* C))"
rel_ALoad:
  "is_relevant_class ALoad          = (λP C. P \<turnstile> ArrayIndexOutOfBounds \<preceq>* C ∨ P \<turnstile> NullPointer \<preceq>* C)"
rel_AStore:
  "is_relevant_class AStore         = (λP C. P \<turnstile> ArrayIndexOutOfBounds \<preceq>* C ∨ P \<turnstile> ArrayStore \<preceq>* C ∨ P \<turnstile> NullPointer \<preceq>* C)"
rel_ALength:
  "is_relevant_class ALength        = (λP C. P \<turnstile> NullPointer \<preceq>* C)"
rel_MEnter:
  "is_relevant_class MEnter         = (λP C. P \<turnstile> IllegalMonitorState \<preceq>* C ∨ P \<turnstile> NullPointer \<preceq>* C)"
rel_MExit:
  "is_relevant_class MExit          = (λP C. P \<turnstile> IllegalMonitorState \<preceq>* C ∨ P \<turnstile> NullPointer \<preceq>* C)"
rel_default:
  "is_relevant_class i              = (λP C. False)"

constdefs
  is_relevant_entry :: "'m prog => instr => pc => ex_entry => bool" 
  "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}"

  relevant_entries :: "'m prog => instr => pc => ex_table => ex_table" 
  "relevant_entries P i pc ≡ filter (is_relevant_entry P i pc)"

  xcpt_eff :: "instr => 'm prog => pc => tyi 
               => ex_table => (pc × tyi') list"                               
  "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)"

  norm_eff :: "instr => 'm prog => nat => tyi => (pc × tyi') list"
  "norm_eff i P pc τ ≡ map (λpc'. (pc',Some (effi (i,P,τ)))) (succs i τ pc)"

  eff :: "instr => 'm prog => pc => ex_table => tyi' => (pc × tyi') list"
  "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, ∃T D. P \<turnstile> C sees F:T in D ∧ .. *)

text "Conditions under which eff is applicable:"

fun appi :: "instr × 'm prog × pc × nat × ty × tyi => bool"
where
  appi_Load:
  "appi (Load n, P, pc, mxs, Tr, (ST,LT)) = 
    (n < length LT ∧ LT ! n ≠ Err ∧ length ST < mxs)"
| appi_Store:
  "appi (Store n, P, pc, mxs, Tr, (T#ST, LT)) = 
    (n < length LT)"
| appi_Push:
  "appi (Push v, P, pc, mxs, Tr, (ST,LT)) = 
    (length ST < mxs ∧ typeof v ≠ None)"
| appi_Getfield:
  "appi (Getfield F C, P, pc, mxs, Tr, (T#ST, LT)) = 
    (∃Tf. P \<turnstile> C sees F:Tf in C ∧ P \<turnstile> T ≤ Class C)"
| appi_Putfield:
  "appi (Putfield F C, P, pc, mxs, Tr, (T1#T2#ST, LT)) = 
    (∃Tf. P \<turnstile> C sees F:Tf in C ∧ P \<turnstile> T2 ≤ (Class C) ∧ P \<turnstile> T1 ≤ Tf)" 
| appi_New:
  "appi (New C, P, pc, mxs, Tr, (ST,LT)) = 
    (is_class P C ∧ length ST < mxs)"
| appi_NewArray:
  "appi (NewArray Ty, P, pc, mxs, Tr, (Integer#ST,LT)) = 
    is_type P Ty"
|  appi_ALoad:
  "appi (ALoad, P, pc, mxs, Tr, (T1#T2#ST,LT)) = 
    (T1 = Integer ∧ (T2 ≠ NT --> (∃Ty. T2 = Ty⌊⌉)))"
| appi_AStore:
  "appi (AStore, P, pc, mxs, Tr, (T1#T2#T3#ST,LT)) = 
    (T2 = Integer ∧ (T3 ≠ NT --> (∃Ty. T3 = Ty⌊⌉)))"
| appi_ALength:
  "appi (ALength, P, pc, mxs, Tr, (T1#ST,LT)) = 
    (T1 = NT ∨ (∃Ty. T1 = Ty⌊⌉))"
| appi_Checkcast:
  "appi (Checkcast Ty, P, pc, mxs, Tr, (T#ST,LT)) = 
    (is_type P Ty (* ∧ is_refT T *) )"
| appi_Pop:
  "appi (Pop, P, pc, mxs, Tr, (T#ST,LT)) = 
    True"
| appi_BinOpInstr:
  "appi (BinOpInstr bop, P, pc, mxs, Tr, (T2#T1#ST,LT)) = (∃T. P \<turnstile> T1«bop»T2 : T)"
| appi_IfFalse:
  "appi (IfFalse b, P, pc, mxs, Tr, (Boolean#ST,LT)) = 
    (0 ≤ int pc + b)"
| appi_Goto:
  "appi (Goto b, P, pc, mxs, Tr, s) =  (0 ≤ int pc + b)"
| appi_Return:
  "appi (Return, P, pc, mxs, Tr, (T#ST,LT)) = (P \<turnstile> T ≤ Tr)"
| appi_Throw:
  "appi (ThrowExc, P, pc, mxs, Tr, (T#ST,LT)) = 
    (T = NT ∨ (∃C. T = Class C ∧ P \<turnstile> C \<preceq>* Throwable))"
| appi_Invoke:
  "appi (Invoke M n, P, pc, mxs, Tr, (ST,LT)) =
    (n < length ST ∧ 
    (ST!n ≠ NT -->
      (if is_external_call P (ST ! n) M then ∃U. P \<turnstile> ST ! n•M(rev (take n ST)) :: U
       else ∃C D Ts T m. ST!n = Class C ∧ P \<turnstile> C sees M:Ts -> T = m in D ∧ P \<turnstile> rev (take n ST) [≤] Ts)))"
| appi_MEnter:
  "appi (MEnter,P, pc,mxs,Tr,(T#ST,LT)) = (is_refT T)"
| appi_MExit:
  "appi (MExit,P, pc,mxs,Tr,(T#ST,LT)) = (is_refT T)"
| appi_default:
  "appi (i,P, pc,mxs,Tr,s) = False"


constdefs
  xcpt_app :: "instr => 'm prog => pc => nat => ex_table => tyi => bool"
  "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"

  app :: "instr => 'm prog => nat => ty => nat => nat => ex_table => 
           tyi' => bool"                                          
  "app i P mxs Tr pc mpc xt t ≡ case t of None => True | Some τ => 
  appi (i,P,pc,mxs,Tr,τ) ∧ xcpt_app i P pc mxs xt τ ∧ 
  (∀(pc',τ') ∈ set (eff i P pc xt t). pc' < mpc)"


lemma app_Some:
  "app i P mxs Tr pc mpc xt (Some τ) = 
  (appi (i,P,pc,mxs,Tr,τ) ∧ 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 effi and appi and eff and app 
  fixes norm_eff and xcpt_app and xcpt_eff

  fixes mpc
  defines "mpc ≡ size is"

  defines "effi i τ ≡ Effect.effi (i,P,τ)"
  notes effi_simps [simp] = Effect.effi.simps [where P = P, folded effi_def]

  defines "appi i pc τ ≡ Effect.appi (i, P, pc, mxs, Tr, τ)"
  notes appi_simps [simp] = Effect.appi.simps [where P=P and mxs=mxs and Tr=Tr, folded appi_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 effi_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 Tr pc mpc xt"
  notes app = Effect.app_def [of _ P mxs Tr _ mpc xt, folded app_def xcpt_app_def appi_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 ST LT. P (l#ST,LT)"
  shows "P s"
(*<*)
proof -
  obtain xs LT where s: "s = (xs,LT)" by (cases s)
  show ?thesis
  proof (cases xs)
    case Nil thus ?thesis using s assms by (simp)
  next
    fix l xs' assume "xs = l#xs'"
    thus ?thesis using s assms by (simp)
  qed
qed
(*>*)

lemma length_cases4:
  assumes "!!LT. P ([],LT)"
  assumes "!!l LT. P ([l],LT)"
  assumes "!!l l' LT. P ([l,l'],LT)"
  assumes "!!l l' ST LT. P (l#l'#ST,LT)"
  shows "P s"
(*<*)
proof -
  obtain xs LT where s: "s = (xs,LT)" by (cases s)
  show ?thesis
  proof (cases xs)
    case Nil thus ?thesis using s assms by (simp)
  next
    fix l xs' assume xs: "xs = l#xs'"
    thus ?thesis
    proof (cases xs')
      case Nil thus ?thesis using s assms xs by (simp)
    next
      fix l' ST assume xs': "xs' = l'#ST"
      thus ?thesis using s assms xs xs' by (simp)
    qed
  qed
qed
(*>*)

text {* 
\medskip
simp rules for @{term app}
*}
lemma appNone[simp]: "app i P mxs Tr pc mpc et None = True" 
  by (simp add: app_def)


lemma appLoad[simp]:
"appi (Load idx, P, Tr, mxs, pc, s) = (∃ST LT. s = (ST,LT) ∧ idx < length LT ∧ LT!idx ≠ Err ∧ length ST < mxs)"
  by (cases s, simp)

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

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

lemma appGetField[simp]:
"appi (Getfield F C,P,pc,mxs,Tr,s) = 
 (∃ oT vT ST LT. s = (oT#ST, LT) ∧ 
  P \<turnstile> C sees F:vT in C ∧ P \<turnstile> oT ≤ (Class C))"
  by (rule length_cases2 [of _ s]) auto

lemma appPutField[simp]:
"appi (Putfield F C,P,pc,mxs,Tr,s) = 
 (∃ vT vT' oT ST LT. s = (vT#oT#ST, LT) ∧
  P \<turnstile> C sees F:vT' in C ∧ P \<turnstile> oT ≤ (Class C) ∧ P \<turnstile> vT ≤ vT')"
  by (rule length_cases4 [of _ s], auto)

lemma appNew[simp]:
  "appi (New C,P,pc,mxs,Tr,s) = 
  (∃ST LT. s=(ST,LT) ∧ is_class P C ∧ length ST < mxs)"
  by (cases s, simp)

lemma appNewArray[simp]:
  "appi (NewArray Ty,P,pc,mxs,Tr,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]:
  "appi (ALoad,P,pc,mxs,Tr,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]) ∨ (∃T1 T2 ST'. ST = T1#T2#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 T1 T2 ST' assume "ST = T1#T2#ST'"
    hence ?thesis by (cases T1, auto)
  }
  ultimately show ?thesis by blast
qed

lemma appAStore[simp]:
  "appi (AStore,P,pc,mxs,Tr,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]) ∨ (∃T1 T2. ST = [T1, T2]) ∨ (∃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]:
  "appi (ALength,P,pc,mxs,Tr,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]: 
  "appi (Checkcast Ty,P,pc,mxs,Tr,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 appiPop[simp]: 
"appi (Pop,P,pc,mxs,Tr,s) = (∃ts ST LT. s = (ts#ST,LT))"
  by (rule length_cases2, auto)

lemma appBinOp[simp]:
"appi (BinOpInstr bop,P,pc,mxs,Tr,s) = (∃T1 T2 ST LT T. s = (T2 # T1 # ST, LT) ∧ P \<turnstile> T1«bop»T2 : T)"
proof -
  obtain ST LT where [simp]: "s = (ST,LT)" by (cases s)
  have "ST = [] ∨ (∃T. ST = [T]) ∨ (∃T1 T2 ST'. ST = T1#T2#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 T1 T2 ST' assume "ST = T1#T2#ST'"
    hence ?thesis by simp
  }
  ultimately show ?thesis by blast
qed

lemma appIfFalse [simp]:
"appi (IfFalse b,P,pc,mxs,Tr,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]:
"appi (Return,P,pc,mxs,Tr,s) = (∃T ST LT. s = (T#ST,LT) ∧ P \<turnstile> T ≤ Tr)" 
  by (rule length_cases2, auto)

lemma appThrow[simp]:
  "appi (ThrowExc,P,pc,mxs,Tr,s) = (∃T ST LT. s=(T#ST,LT) ∧ (T = NT ∨ (∃C. T = Class C ∧ P \<turnstile> C \<preceq>* Throwable)))"
  by (rule length_cases2, auto)  

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

lemma appMExit[simp]:
  "appi (MExit,P,pc,mxs,Tr,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)


text {* some helpers to make the specification directly executable: *}
declare list_all2_Nil [code]
declare list_all2_Cons [code]

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

end