theory CNodeInv_R

lemma m'_nextD:
  "m' \<turnstile> p \<leadsto> p' \<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')" using src dest src_0 dest_0 dlist neq src_neq_prev apply (simp add: m'_def n_def) apply (simp add: mdb_next_unfold) apply (elim exE conjE) apply (case_tac z) apply simp apply (simp add: modify_map_cases) apply (cases "mdbPrev src_node = p") apply clarsimp apply simp apply (cases "p=src", simp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto> p' \<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' proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE capability.NullCap old_dest_node)
src \<noteq> 0
dest \<noteq> 0
valid_dlist m
src \<noteq> dest
src \<noteq> mdbPrev src_node

goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto> p' \<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' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) \<turnstile> p \<leadsto> p'; m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> p' = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> (p = dest \<longrightarrow> m \<turnstile> src \<leadsto> p') \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> m \<turnstile> p \<leadsto> p'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>z. modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some z \<and> p' = mdbNext (cteMDBNode z); m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> p' = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> (p = dest \<longrightarrow> p' = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> p' = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some z; p' = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> p' = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> (p = dest \<longrightarrow> p' = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> p' = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some z; p' = mdbNext (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> p' = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> (p = dest \<longrightarrow> p' = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> p' = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> p' = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))) p = Some (CTE x1 x2); p' = mdbNext x2; z = CTE x1 x2\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> mdbNext x2 = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> (p = dest \<longrightarrow> mdbNext x2 = mdbNext src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbNext x2 = 0) \<and> (p \<noteq> src \<longrightarrow> (\<exists>z. m p = Some z \<and> mdbNext x2 = mdbNext (cteMDBNode z))))) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 x2)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = x2)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = node) \<and> nullMDBNode = x2))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = nodea) \<and> nullMDBNode = node)) \<and> mdbNext_update (\<lambda>_. dest) node = x2)); p' = mdbNext x2; z = CTE x1 x2\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> mdbNext x2 = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext x2 = 0) proof (prove)
goal (2 subgoals):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 x2)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = x2)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = node) \<and> nullMDBNode = x2))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = nodea) \<and> nullMDBNode = node)) \<and> mdbNext_update (\<lambda>_. dest) node = x2)); p' = mdbNext x2; z = CTE x1 x2; mdbPrev src_node = p\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> mdbNext x2 = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext x2 = 0)
 2. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 x2)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = x2)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = node) \<and> nullMDBNode = x2))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = nodea) \<and> nullMDBNode = node)) \<and> mdbNext_update (\<lambda>_. dest) node = x2)); p' = mdbNext x2; z = CTE x1 x2; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> mdbNext x2 = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext x2 = 0) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 x2)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = x2)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = node) \<and> nullMDBNode = x2))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = nodea) \<and> nullMDBNode = node)) \<and> mdbNext_update (\<lambda>_. dest) node = x2)); p' = mdbNext x2; z = CTE x1 x2; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> (p = mdbPrev src_node \<longrightarrow> mdbNext x2 = dest \<and> mdbPrev src_node \<noteq> 0) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext x2 = 0) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 x2)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = x2)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = node) \<and> nullMDBNode = x2)); p' = mdbNext x2; z = CTE x1 x2; mdbPrev src_node \<noteq> p\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext x2 = 0 proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); dest \<noteq> 0; valid_dlist m; src \<noteq> dest; (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE x1 x2)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = x1 \<and> src_node = x2)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = x1) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE x1 node)) \<and> src_node = node) \<and> nullMDBNode = x2)); p' = mdbNext x2; z = CTE x1 x2; mdbPrev src_node \<noteq> p; p \<noteq> src\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> p = src \<longrightarrow> mdbNext x2 = 0 proof (prove)
goal:
No subgoals!