theory Finalise_R

lemma m_cap:
  "m p = Some (CTE cap node) \<Longrightarrow>
  \<exists>cap' node'. n p = Some (CTE cap' node') \<and>
              (if p = slot
               then cap' = NullCap
               else cap' = cap)" apply (clarsimp simp: n_def modify_map_cases initMDBNode_def) apply (cases node) apply clarsimp apply (cases "p=slot", simp) apply clarsimp apply (cases "mdbNext s_node = p", simp) apply fastforce apply simp apply (cases "mdbPrev s_node = p", simp) 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 cap' = capability.NullCap else cap' = cap) proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap'. (p = slot \<longrightarrow> capability.NullCap = cap' \<and> cap' = capability.NullCap) \<and> (p \<noteq> slot \<longrightarrow> (\<exists>node'. (mdbNext s_node \<noteq> p \<longrightarrow> (mdbPrev s_node \<noteq> p \<longrightarrow> cap = cap' \<and> node = node') \<and> (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node')) \<and> (mdbNext s_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev s_node \<noteq> p \<longrightarrow> cap = cap' \<and> node = nodea) \<and> (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. p) node = nodea) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged nodea \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) nodea) = node')) \<and> cap' = cap)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap node); node = MDB x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<exists>cap'. (p = slot \<longrightarrow> capability.NullCap = cap' \<and> cap' = capability.NullCap) \<and> (p \<noteq> slot \<longrightarrow> (\<exists>node'. (mdbNext s_node \<noteq> p \<longrightarrow> (mdbPrev s_node \<noteq> p \<longrightarrow> cap = cap' \<and> node = node') \<and> (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. mdbNext s_node) node = node')) \<and> (mdbNext s_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev s_node \<noteq> p \<longrightarrow> cap = cap' \<and> node = nodea) \<and> (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> mdbNext_update (\<lambda>_. p) node = nodea) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged nodea \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) nodea) = node')) \<and> cap' = cap)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap (MDB x1 x2 x3 x4)); node = MDB x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<exists>cap'. (p = slot \<longrightarrow> capability.NullCap = cap' \<and> cap' = capability.NullCap) \<and> (p \<noteq> slot \<longrightarrow> (\<exists>node'. (mdbNext s_node \<noteq> p \<longrightarrow> (mdbPrev s_node \<noteq> p \<longrightarrow> cap = cap' \<and> MDB x1 x2 x3 x4 = node') \<and> (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> MDB (mdbNext s_node) x2 x3 x4 = node')) \<and> (mdbNext s_node = p \<longrightarrow> (\<exists>node. (mdbPrev s_node \<noteq> p \<longrightarrow> cap = cap' \<and> MDB x1 x2 x3 x4 = node) \<and> (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> MDB p x2 x3 x4 = node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) \<and> cap' = cap)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap (MDB x1 x2 x3 x4)); node = MDB x1 x2 x3 x4; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cap'. (p = slot \<longrightarrow> capability.NullCap = cap' \<and> cap' = capability.NullCap) \<and> (p \<noteq> slot \<longrightarrow> (\<exists>node'. (mdbNext s_node \<noteq> p \<longrightarrow> (mdbPrev s_node \<noteq> p \<longrightarrow> cap = cap' \<and> MDB x1 x2 x3 x4 = node') \<and> (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> MDB (mdbNext s_node) x2 x3 x4 = node')) \<and> (mdbNext s_node = p \<longrightarrow> (\<exists>node. (mdbPrev s_node \<noteq> p \<longrightarrow> cap = cap' \<and> MDB x1 x2 x3 x4 = node) \<and> (mdbPrev s_node = p \<longrightarrow> cap = cap' \<and> MDB p x2 x3 x4 = node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) \<and> cap' = cap)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap (MDB x1 x2 x3 x4)); node = MDB x1 x2 x3 x4; p \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>node'. (mdbNext s_node \<noteq> p \<longrightarrow> (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node') \<and> (mdbPrev s_node = p \<longrightarrow> MDB (mdbNext s_node) x2 x3 x4 = node')) \<and> (mdbNext s_node = p \<longrightarrow> (\<exists>node. (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node) \<and> (mdbPrev s_node = p \<longrightarrow> MDB p x2 x3 x4 = node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap (MDB x1 x2 x3 x4)); node = MDB x1 x2 x3 x4; p \<noteq> slot; mdbNext s_node = p\<rbrakk> \<Longrightarrow> \<exists>node. (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node) \<and> (mdbPrev s_node = p \<longrightarrow> MDB p x2 x3 x4 = node)
 2. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap (MDB x1 x2 x3 x4)); node = MDB x1 x2 x3 x4; p \<noteq> slot; mdbNext s_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node'. (mdbNext s_node \<noteq> p \<longrightarrow> (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node') \<and> (mdbPrev s_node = p \<longrightarrow> MDB (mdbNext s_node) x2 x3 x4 = node')) \<and> (mdbNext s_node = p \<longrightarrow> (\<exists>node. (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node) \<and> (mdbPrev s_node = p \<longrightarrow> MDB p x2 x3 x4 = node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap (MDB x1 x2 x3 x4)); node = MDB x1 x2 x3 x4; p \<noteq> slot; mdbNext s_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node'. (mdbNext s_node \<noteq> p \<longrightarrow> (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node') \<and> (mdbPrev s_node = p \<longrightarrow> MDB (mdbNext s_node) x2 x3 x4 = node')) \<and> (mdbNext s_node = p \<longrightarrow> (\<exists>node. (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node) \<and> (mdbPrev s_node = p \<longrightarrow> MDB p x2 x3 x4 = node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = node')) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap (MDB x1 x2 x3 x4)); node = MDB x1 x2 x3 x4; p \<noteq> slot; mdbNext s_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node'. (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node') \<and> (mdbPrev s_node = p \<longrightarrow> MDB (mdbNext s_node) x2 x3 x4 = node') proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>m p = Some (CTE cap (MDB x1 x2 x3 x4)); node = MDB x1 x2 x3 x4; p \<noteq> slot; mdbNext s_node \<noteq> p; mdbPrev s_node \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>node'. (mdbPrev s_node \<noteq> p \<longrightarrow> MDB x1 x2 x3 x4 = node') \<and> (mdbPrev s_node = p \<longrightarrow> MDB (mdbNext s_node) x2 x3 x4 = node') proof (prove)
goal:
No subgoals!