theory Finalise_R

lemma m_revokable:
  "m p = Some (CTE cap node) \<Longrightarrow>
  (\<exists>cap' node'. n p = Some (CTE cap' node') \<and>
              (if p = slot
               then \<not> mdbRevocable node'
               else mdbRevocable node' = mdbRevocable node))" apply (clarsimp simp add: n_def modify_map_if nullMDBNode_def split: if_split_asm) apply (cases "p=slot", simp) apply (cases "p=mdbNext s_node", simp) apply (cases "p=mdbPrev s_node", simp) apply clarsimp apply simp apply (cases "p=mdbPrev s_node", simp) apply simp 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 \<not> mdbRevocable node' else mdbRevocable node' = mdbRevocable node) proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. p) (mdbNext_update (\<lambda>_. p) node)) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node' \<and> mdbRevocable node' = mdbRevocable node))) \<and> (mdbPrev s_node \<noteq> p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbRevocable node' = mdbRevocable node))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. p) (mdbNext_update (\<lambda>_. p) node)) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node' \<and> mdbRevocable node' = mdbRevocable node))) \<and> (mdbPrev s_node \<noteq> p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbRevocable node' = mdbRevocable node))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbNext s_node) = Some (CTE cap node); p = mdbNext s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = 0 \<and> mdbNext s_node = 0 \<longrightarrow> cap = cap' \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. 0) (mdbNext_update (\<lambda>_. 0) node)) = node' \<and> mdbRevocable node' = mdbRevocable node) \<and> ((mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<longrightarrow> cap' = cap \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node' \<and> mdbRevocable node' = mdbRevocable node)
 2. \<lbrakk>m p = Some (CTE cap node); p \<noteq> slot; p \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. p) (mdbNext_update (\<lambda>_. p) node)) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node' \<and> mdbRevocable node' = mdbRevocable node))) \<and> (mdbPrev s_node \<noteq> p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbRevocable node' = mdbRevocable node))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbNext s_node) = Some (CTE cap node); p = mdbNext s_node; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = 0 \<and> mdbNext s_node = 0 \<longrightarrow> cap = cap' \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. 0) (mdbNext_update (\<lambda>_. 0) node)) = node' \<and> mdbRevocable node' = mdbRevocable node) \<and> ((mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0) \<longrightarrow> cap' = cap \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node' \<and> mdbRevocable node' = mdbRevocable node)
 2. \<lbrakk>m p = Some (CTE cap node); p \<noteq> slot; p \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. p) (mdbNext_update (\<lambda>_. p) node)) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node' \<and> mdbRevocable node' = mdbRevocable node))) \<and> (mdbPrev s_node \<noteq> p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbRevocable node' = mdbRevocable node))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> slot; p \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. p) (mdbNext_update (\<lambda>_. p) node)) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node' \<and> mdbRevocable node' = mdbRevocable node))) \<and> (mdbPrev s_node \<noteq> p \<longrightarrow> (mdbNext s_node = p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node' \<and> mdbRevocable node' = mdbRevocable node)) \<and> (mdbNext s_node \<noteq> p \<longrightarrow> (p = slot \<longrightarrow> capability.NullCap = cap' \<and> MDB nullPointer nullPointer False False = node' \<and> \<not> mdbRevocable node') \<and> (p \<noteq> slot \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbRevocable node' = mdbRevocable node))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> slot; p \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node' \<and> mdbRevocable node' = mdbRevocable node) \<and> (mdbPrev s_node \<noteq> p \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbRevocable node' = mdbRevocable node) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); p \<noteq> slot; p \<noteq> mdbNext s_node; p \<noteq> mdbPrev s_node\<rbrakk> \<Longrightarrow> \<exists>cap' node'. (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node' \<and> mdbRevocable node' = mdbRevocable node) \<and> (mdbPrev s_node \<noteq> p \<longrightarrow> cap' = cap \<and> node' = node \<and> mdbRevocable node' = mdbRevocable node) proof (prove)
goal:
No subgoals!