theory CSpace1_R

lemma n'_prev:
  "n' p = Some (CTE cap node) \<Longrightarrow>
  if p = mdbNext src_node then mdbPrev node = dest
  else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbPrev node = mdbPrev node'" apply (simp add: n'_def) apply (rule conjI) apply clarsimp apply (simp add: modify_map_cases) apply clarsimp apply clarsimp by (auto simp add: modify_map_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> if p = mdbNext src_node then mdbPrev node = dest else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbPrev node = mdbPrev node' proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some (CTE cap node) \<Longrightarrow> (p = mdbNext src_node \<longrightarrow> mdbPrev node = dest) \<and> (p \<noteq> mdbNext src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbPrev node = mdbPrev node')) proof (prove)
goal (2 subgoals):
 1. modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some (CTE cap node) \<Longrightarrow> p = mdbNext src_node \<longrightarrow> mdbPrev node = dest
 2. modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some (CTE cap node) \<Longrightarrow> p \<noteq> mdbNext src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbPrev node = mdbPrev node') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) (mdbNext src_node) = Some (CTE cap node); p = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbPrev node = dest
 2. modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some (CTE cap node) \<Longrightarrow> p \<noteq> mdbNext src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbPrev node = mdbPrev node') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<exists>nodea. ((mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (dest \<noteq> mdbNext src_node \<longrightarrow> m (mdbNext src_node) = Some (CTE cap nodea)) \<and> (dest = mdbNext src_node \<longrightarrow> (\<exists>cap. m (mdbNext src_node) = Some (CTE cap nodea)) \<and> scap = cap)) \<and> (mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node; p = mdbNext src_node\<rbrakk> \<Longrightarrow> mdbPrev node = dest
 2. modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some (CTE cap node) \<Longrightarrow> p \<noteq> mdbNext src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbPrev node = mdbPrev node') proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some (CTE cap node) \<Longrightarrow> p \<noteq> mdbNext src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbPrev node = mdbPrev node') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some (CTE cap node); p \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbPrev node = mdbPrev node'