theory Finalise_R

lemma m_parent_of:
  "\<lbrakk> m \<turnstile> p parentOf p'; p \<noteq> slot; p' \<noteq> slot; p\<noteq>p'; p'\<noteq>mdbNext s_node \<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf p'" apply (clarsimp simp add: parentOf_def) apply (case_tac cte, case_tac cte') apply clarsimp apply (frule_tac p=p in m_cap) apply (frule_tac p=p in m_badged) apply (drule_tac p=p in m_revokable) apply clarsimp apply (frule_tac p=p' in m_cap) apply (frule_tac p=p' in m_badged) apply (drule_tac p=p' in m_revokable) apply clarsimp apply (simp split: if_split_asm;
         clarsimp simp: isMDBParentOf_def isCap_simps split: if_split_asm cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p parentOf p'; p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node\<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf p' proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some cte; m p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n p' = Some cte \<and> n p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte x1 x2 x1a x2a. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some cte; m p = Some cte'; isMDBParentOf cte' cte; cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n p' = Some cte \<and> n p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some (CTE x1 x2); m p = Some (CTE x1a x2a); isMDBParentOf (CTE x1a x2a) (CTE x1 x2)\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n p' = Some cte \<and> n p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some (CTE x1 x2); m p = Some (CTE x1a x2a); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then cap' = capability.NullCap else cap' = x1a)\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n p' = Some cte \<and> n p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some (CTE x1 x2); m p = Some (CTE x1a x2a); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then cap' = capability.NullCap else cap' = x1a); \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node' else if p = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2a)\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n p' = Some cte \<and> n p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some (CTE x1 x2); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then cap' = capability.NullCap else cap' = x1a); \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged node' else if p = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2a); \<exists>cap' node'. n p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable node' else mdbRevocable node' = mdbRevocable x2a)\<rbrakk> \<Longrightarrow> \<exists>cte' cte. n p' = Some cte \<and> n p = Some cte' \<and> isMDBParentOf cte' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a node'. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some (CTE x1 x2); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2a; n p = Some (CTE x1a node'); mdbRevocable node' = mdbRevocable x2a\<rbrakk> \<Longrightarrow> \<exists>cte. n p' = Some cte \<and> isMDBParentOf (CTE x1a node') cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a node'. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some (CTE x1 x2); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2a; n p = Some (CTE x1a node'); mdbRevocable node' = mdbRevocable x2a; \<exists>cap' node'. n p' = Some (CTE cap' node') \<and> (if p' = slot then cap' = capability.NullCap else cap' = x1)\<rbrakk> \<Longrightarrow> \<exists>cte. n p' = Some cte \<and> isMDBParentOf (CTE x1a node') cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a node'. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; m p' = Some (CTE x1 x2); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2a; n p = Some (CTE x1a node'); mdbRevocable node' = mdbRevocable x2a; \<exists>cap' node'. n p' = Some (CTE cap' node') \<and> (if p' = slot then cap' = capability.NullCap else cap' = x1); \<exists>cap' node'. n p' = Some (CTE cap' node') \<and> (if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2)\<rbrakk> \<Longrightarrow> \<exists>cte. n p' = Some cte \<and> isMDBParentOf (CTE x1a node') cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a node'. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2a; n p = Some (CTE x1a node'); mdbRevocable node' = mdbRevocable x2a; \<exists>cap' node'. n p' = Some (CTE cap' node') \<and> (if p' = slot then cap' = capability.NullCap else cap' = x1); \<exists>cap' node'. n p' = Some (CTE cap' node') \<and> (if p' = slot then \<not> mdbFirstBadged node' else if p' = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2 \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2); \<exists>cap' node'. n p' = Some (CTE cap' node') \<and> (if p' = slot then \<not> mdbRevocable node' else mdbRevocable node' = mdbRevocable x2)\<rbrakk> \<Longrightarrow> \<exists>cte. n p' = Some cte \<and> isMDBParentOf (CTE x1a node') cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a node' node'a. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; p \<noteq> p'; p' \<noteq> mdbNext s_node; isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged node' = (mdbFirstBadged x2a \<or> mdbFirstBadged s_node) else mdbFirstBadged node' = mdbFirstBadged x2a; n p = Some (CTE x1a node'); mdbRevocable node' = mdbRevocable x2a; mdbFirstBadged node'a = mdbFirstBadged x2; n p' = Some (CTE x1 node'a); mdbRevocable node'a = mdbRevocable x2\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1a node') (CTE x1 node'a) proof (prove)
goal:
No subgoals!