theory Finalise_R

lemma m_prev:
  "m p = Some (CTE cap node) \<Longrightarrow>
  \<exists>cap' node'. n p = Some (CTE cap' node') \<and>
              (if p = slot
               then mdbPrev node' = 0
               else if p = mdbNext s_node
               then mdbPrev node' = mdbPrev s_node
               else mdbPrev node' = mdbPrev node)" apply (subgoal_tac "p \<noteq> 0") prefer 2 apply clarsimp apply (cases "p = slot") apply (clarsimp simp: n_def modify_map_if) apply (cases "p = mdbPrev s_node") apply (simp add: n_def modify_map_if) apply simp apply (simp add: n_def modify_map_if) apply (cases "mdbNext s_node = p") apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node)
 2. m p = Some (CTE cap node) \<Longrightarrow> p \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. m p = Some (CTE cap node) \<Longrightarrow> p \<noteq> 0
 2. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p = slot\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node)
 2. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot; p = mdbPrev s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node)
 2. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then mdbPrev node' = 0 else if p = mdbNext s_node then mdbPrev node' = mdbPrev s_node else mdbPrev node' = mdbPrev node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (p = mdbNext s_node \<longrightarrow> n (mdbNext s_node) = Some (CTE cap' node') \<and> mdbPrev node' = mdbPrev s_node) \<and> (p \<noteq> mdbNext s_node \<longrightarrow> n p = Some (CTE cap' node') \<and> mdbPrev node' = mdbPrev node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (p = mdbNext s_node \<longrightarrow> (mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<and> ((mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<longrightarrow> (\<exists>node. m (mdbNext s_node) = Some (CTE cap' node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) \<and> mdbPrev node' = mdbPrev s_node) \<and> (p \<noteq> mdbNext s_node \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbPrev node' = mdbPrev node) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot; p \<noteq> mdbPrev s_node; mdbNext s_node = p\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (p = mdbNext s_node \<longrightarrow> (mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<and> ((mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<longrightarrow> (\<exists>node. m (mdbNext s_node) = Some (CTE cap' node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) \<and> mdbPrev node' = mdbPrev s_node) \<and> (p \<noteq> mdbNext s_node \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbPrev node' = mdbPrev node)
 2. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot; p \<noteq> mdbPrev s_node; mdbNext s_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (p = mdbNext s_node \<longrightarrow> (mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<and> ((mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<longrightarrow> (\<exists>node. m (mdbNext s_node) = Some (CTE cap' node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) \<and> mdbPrev node' = mdbPrev s_node) \<and> (p \<noteq> mdbNext s_node \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbPrev node' = mdbPrev node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> 0; p \<noteq> slot; p \<noteq> mdbPrev s_node; mdbNext s_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (p = mdbNext s_node \<longrightarrow> (mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<and> ((mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<longrightarrow> (\<exists>node. m (mdbNext s_node) = Some (CTE cap' node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) \<and> mdbPrev node' = mdbPrev s_node) \<and> (p \<noteq> mdbNext s_node \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbPrev node' = mdbPrev node) proof (prove)
goal:
No subgoals!