theory CSpace1_R

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> if p = mdbPrev src_node then mdbNext node = dest else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext 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 = mdbPrev src_node \<longrightarrow> mdbNext node = dest) \<and> (p \<noteq> mdbPrev src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext 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 = mdbPrev src_node \<longrightarrow> mdbNext 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> mdbPrev src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext 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))) (mdbPrev src_node) = Some (CTE cap node); p = mdbPrev src_node\<rbrakk> \<Longrightarrow> mdbNext 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> mdbPrev src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>((mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0) \<longrightarrow> (\<exists>nodea. (dest \<noteq> mdbPrev src_node \<longrightarrow> m (mdbPrev src_node) = Some (CTE cap nodea)) \<and> (dest = mdbPrev src_node \<longrightarrow> (\<exists>cap. m (mdbPrev src_node) = Some (CTE cap nodea)) \<and> scap = cap) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)) \<and> (mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0); p = mdbPrev src_node\<rbrakk> \<Longrightarrow> mdbNext 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> mdbPrev src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext 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> mdbPrev src_node \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext 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> mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbNext node = mdbNext node' proof (prove)
goal:
No subgoals!