theory CNodeInv_R

lemma m'_next_eq:
  notes if_cong [cong]
  shows
  "m' \<turnstile> p \<leadsto> p' =
  (if p = src then p' = 0
  else if p = dest then m \<turnstile> src \<leadsto> p'
  else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0
  else m \<turnstile> p \<leadsto> p')" apply (insert src dest) apply (rule iffI) apply (drule m'_nextD, simp) apply (cases "p=0") apply (clarsimp simp: mdb_next_unfold split: if_split_asm) apply (simp split: if_split_asm) apply (simp add: mdb_next_unfold m'_def n_def modify_map_cases) apply (simp add: mdb_next_unfold m'_def n_def modify_map_cases neq) apply (simp add: mdb_next_unfold m'_def n_def modify_map_cases neq) apply clarsimp apply (drule prev_src) apply (clarsimp simp: mdb_next_unfold) apply (case_tac z) apply clarsimp apply (clarsimp simp: mdb_next_unfold m'_def n_def modify_map_cases) apply (cases "mdbNext src_node = p") apply (clarsimp) apply (case_tac z) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto> p' = (if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0 else m \<turnstile> p \<leadsto> p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node)\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' = (if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0 else m \<turnstile> p \<leadsto> p') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); m' \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0 else m \<turnstile> p \<leadsto> p'
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0 else m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0 else m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0 else m \<turnstile> p \<leadsto> p'; p = 0\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p'
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0 else m \<turnstile> p \<leadsto> p'; p \<noteq> 0\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); if p = src then p' = 0 else if p = dest then m \<turnstile> src \<leadsto> p' else if p = mdbPrev src_node then p' = dest \<and> p \<noteq> 0 else m \<turnstile> p \<leadsto> p'; p \<noteq> 0\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = src; p' = 0\<rbrakk> \<Longrightarrow> m' \<turnstile> src \<leadsto> 0
 2. \<lbrakk>dest \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = dest; m \<turnstile> src \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> dest \<leadsto> p'
 3. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = mdbPrev src_node; p' = dest \<and> mdbPrev src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m' \<turnstile> mdbPrev src_node \<leadsto> dest
 4. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = dest; m \<turnstile> src \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> dest \<leadsto> p'
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = mdbPrev src_node; p' = dest \<and> mdbPrev src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m' \<turnstile> mdbPrev src_node \<leadsto> dest
 3. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = mdbPrev src_node; p' = dest \<and> mdbPrev src_node \<noteq> 0\<rbrakk> \<Longrightarrow> m' \<turnstile> mdbPrev src_node \<leadsto> dest
 2. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = mdbPrev src_node; p' = dest \<and> mdbPrev src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbPrev src_node) = Some (CTE cap node) \<and> CTE cap (mdbNext_update (\<lambda>_. dest) node) = z) \<and> dest = mdbNext (cteMDBNode z)
 2. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = mdbPrev src_node; p' = dest; mdbPrev src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbPrev src_node) = Some (CTE cap node) \<and> CTE cap (mdbNext_update (\<lambda>_. dest) node) = z) \<and> dest = mdbNext (cteMDBNode z)
 2. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = mdbPrev src_node; p' = dest; m \<turnstile> mdbPrev src_node \<leadsto> src\<rbrakk> \<Longrightarrow> \<exists>z. (\<exists>cap node. m (mdbPrev src_node) = Some (CTE cap node) \<and> CTE cap (mdbNext_update (\<lambda>_. dest) node) = z) \<and> dest = mdbNext (cteMDBNode z)
 2. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m (mdbNext (cteMDBNode z)) = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = mdbPrev src_node; p' = dest; m (mdbPrev src_node) = Some z; src = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> \<exists>za. (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbNext_update (\<lambda>_. dest) node) = za) \<and> dest = mdbNext (cteMDBNode za)
 2. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>z x1 x2. \<lbrakk>m (mdbNext (cteMDBNode z)) = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p = mdbPrev src_node; p' = dest; m (mdbPrev src_node) = Some z; src = mdbNext (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>za. (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbNext_update (\<lambda>_. dest) node) = za) \<and> dest = mdbNext (cteMDBNode za)
 2. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m p = Some z; p' = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> \<exists>za. (mdbNext src_node \<noteq> p \<longrightarrow> z = za) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = za)) \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m p = Some z; p' = mdbNext (cteMDBNode z); mdbNext src_node = p\<rbrakk> \<Longrightarrow> \<exists>za. (mdbNext src_node \<noteq> p \<longrightarrow> z = za) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = za)) \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za)
 2. \<And>z. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m p = Some z; p' = mdbNext (cteMDBNode z); mdbNext src_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>za. (mdbNext src_node \<noteq> p \<longrightarrow> z = za) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = za)) \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>mdbNext src_node \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); m (mdbNext src_node) = Some z; p' = mdbNext (cteMDBNode z); p = mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>za. (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = za) \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za)
 2. \<And>z. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m p = Some z; p' = mdbNext (cteMDBNode z); mdbNext src_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>za. (mdbNext src_node \<noteq> p \<longrightarrow> z = za) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = za)) \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal (2 subgoals):
 1. \<And>z x1 x2. \<lbrakk>mdbNext src_node \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); m (mdbNext src_node) = Some z; p' = mdbNext (cteMDBNode z); p = mdbNext src_node; z = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>za. (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = za) \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za)
 2. \<And>z. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m p = Some z; p' = mdbNext (cteMDBNode z); mdbNext src_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>za. (mdbNext src_node \<noteq> p \<longrightarrow> z = za) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = za)) \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>p \<noteq> 0; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); p \<noteq> src; p \<noteq> dest; p \<noteq> mdbPrev src_node; m p = Some z; p' = mdbNext (cteMDBNode z); mdbNext src_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>za. (mdbNext src_node \<noteq> p \<longrightarrow> z = za) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>cap node. z = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>_. dest) node) = za)) \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal:
No subgoals!