theory CSpace_R

lemma n'_prev_eq:
  "n' \<turnstile> p \<leftarrow> p' =
  (if p' = mdbNext src_node \<and> p' \<noteq> 0 then p = dest
   else if p' = dest then p = src
   else m \<turnstile> p \<leftarrow> p')" using src dest dest_prev dest_next apply (cases "p' = 0", simp) apply (simp split del: if_split) apply (cases "p' = mdbNext src_node") apply (clarsimp simp: modify_map_apply n'_def n_def mdb_prev_def) apply (clarsimp simp: modify_map_if) apply (rule iffI, clarsimp) apply clarsimp apply (rule dlistEn, assumption, simp) apply clarsimp apply (case_tac cte') apply clarsimp apply (cases "p' = dest") apply (clarsimp simp: modify_map_if n'_def n_def mdb_prev_def) apply clarsimp apply (clarsimp simp: modify_map_if n'_def n_def mdb_prev_def) apply (cases "p' = src", simp) apply clarsimp apply (rule iffI, clarsimp) apply clarsimp apply (case_tac z) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node \<and> p' \<noteq> 0 then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)
mdbPrev dest_node = 0
mdbNext dest_node = 0

goal (1 subgoal):
 1. n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node \<and> p' \<noteq> 0 then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node \<and> p' \<noteq> 0 then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' = mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p')
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; p' = mdbNext src_node\<rbrakk> \<Longrightarrow> (\<exists>z. modify_map (m(dest \<mapsto> CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))), src \<mapsto> CTE src_cap (mdbNext_update (\<lambda>a. dest) src_node))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext src_node) = Some z \<and> p = mdbPrev (cteMDBNode z)) = (p = dest)
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; p' = mdbNext src_node\<rbrakk> \<Longrightarrow> (\<exists>z. (\<exists>cap node. m (mdbNext src_node) = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = z) \<and> p = mdbPrev (cteMDBNode z)) = (p = dest)
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; p' = mdbNext src_node; p = dest\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbNext src_node) = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = z) \<and> p = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; p' = mdbNext src_node; p = dest\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbNext src_node) = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = z) \<and> dest = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; p' = mdbNext src_node; p = dest; m (mdbNext (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbPrev (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbNext src_node) = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = z) \<and> dest = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>m (mdbPrev (cteMDBNode cte')) = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; p' = mdbNext src_node; p = dest; m (mdbNext src_node) = Some cte'; src = mdbPrev (cteMDBNode cte')\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. cte' = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = z) \<and> dest = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<And>cte' x1 x2. \<lbrakk>m (mdbPrev (cteMDBNode cte')) = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; mdbNext src_node \<noteq> 0; p' = mdbNext src_node; p = dest; m (mdbNext src_node) = Some cte'; src = mdbPrev (cteMDBNode cte'); cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. cte' = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = z) \<and> dest = mdbPrev (cteMDBNode z)
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' = dest\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p')
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = (if p' = mdbNext src_node then p = dest else if p' = dest then p = src else m \<turnstile> p \<leftarrow> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest\<rbrakk> \<Longrightarrow> n' \<turnstile> p \<leftarrow> p' = m \<turnstile> p \<leftarrow> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest\<rbrakk> \<Longrightarrow> (\<exists>z. (\<exists>cap node. (src = p' \<longrightarrow> (\<exists>nodea. m p' = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>a. dest) nodea = node) \<and> z = CTE cap node) \<and> (src \<noteq> p' \<longrightarrow> m p' = Some (CTE cap node) \<and> z = CTE cap node)) \<and> p = mdbPrev (cteMDBNode z)) = (\<exists>z. m p' = Some z \<and> p = mdbPrev (cteMDBNode z)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (\<exists>z. (\<exists>cap node. (src = p' \<longrightarrow> (\<exists>nodea. m p' = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>a. dest) nodea = node) \<and> z = CTE cap node) \<and> (src \<noteq> p' \<longrightarrow> m p' = Some (CTE cap node) \<and> z = CTE cap node)) \<and> p = mdbPrev (cteMDBNode z)) = (\<exists>z. m p' = Some z \<and> p = mdbPrev (cteMDBNode z)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> (\<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z)) = (\<exists>z. m p' = Some z \<and> p = mdbPrev (cteMDBNode z)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest; p' \<noteq> src; \<exists>z. m p' = Some z \<and> p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m p' = Some (CTE cap node) \<and> z = CTE cap node) \<and> p = mdbPrev (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest; p' \<noteq> src; m p' = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> \<exists>za. (\<exists>cap node. z = CTE cap node \<and> za = CTE cap node) \<and> mdbPrev (cteMDBNode z) = mdbPrev (cteMDBNode za) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0; p' \<noteq> 0; p' \<noteq> mdbNext src_node; p' \<noteq> dest; p' \<noteq> src; m p' = Some z; p = mdbPrev (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>za. (\<exists>cap node. z = CTE cap node \<and> za = CTE cap node) \<and> mdbPrev (cteMDBNode z) = mdbPrev (cteMDBNode za) proof (prove)
goal:
No subgoals!