theory Finalise_R

lemma n_parent_of:
  "\<lbrakk> n \<turnstile> p parentOf p'; p \<noteq> slot; p' \<noteq> slot \<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf p'" apply (clarsimp simp: parentOf_def) apply (case_tac cte, case_tac cte') apply clarsimp apply (frule_tac p=p in n_cap) apply (frule_tac p=p in n_badged) apply (drule_tac p=p in n_revokable) apply (clarsimp) apply (frule_tac p=p' in n_cap) apply (frule_tac p=p' in n_badged) apply (drule_tac p=p' in n_revokable) apply (clarsimp 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>n \<turnstile> p parentOf p'; p \<noteq> slot; p' \<noteq> slot\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf p' proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte. \<lbrakk>p \<noteq> slot; p' \<noteq> slot; n p' = Some cte; n p = Some cte'; isMDBParentOf cte' cte\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m p' = Some cte \<and> m 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; n p' = Some cte; n p = Some cte'; isMDBParentOf cte' cte; cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m p' = Some cte \<and> m 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; n p' = Some (CTE x1 x2); n p = Some (CTE x1a x2a); isMDBParentOf (CTE x1a x2a) (CTE x1 x2)\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m p' = Some cte \<and> m 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; n p' = Some (CTE x1 x2); n p = Some (CTE x1a x2a); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then x1a = capability.NullCap else cap' = x1a)\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m p' = Some cte \<and> m 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; n p' = Some (CTE x1 x2); n p = Some (CTE x1a x2a); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then x1a = capability.NullCap else cap' = x1a); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged x2a else if p = mdbNext s_node then mdbFirstBadged x2a = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2a = mdbFirstBadged node')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m p' = Some cte \<and> m 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; n p' = Some (CTE x1 x2); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then x1a = capability.NullCap else cap' = x1a); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbFirstBadged x2a else if p = mdbNext s_node then mdbFirstBadged x2a = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2a = mdbFirstBadged node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable x2a else mdbRevocable x2a = mdbRevocable node')\<rbrakk> \<Longrightarrow> \<exists>cte' cte. m p' = Some cte \<and> m 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; n p' = Some (CTE x1 x2); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged x2a = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2a = mdbFirstBadged node'; m p = Some (CTE x1a node'); mdbRevocable x2a = mdbRevocable node'\<rbrakk> \<Longrightarrow> \<exists>cte. m 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; n p' = Some (CTE x1 x2); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged x2a = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2a = mdbFirstBadged node'; m p = Some (CTE x1a node'); mdbRevocable x2a = mdbRevocable node'; \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then x1 = capability.NullCap else cap' = x1)\<rbrakk> \<Longrightarrow> \<exists>cte. m 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; n p' = Some (CTE x1 x2); isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged x2a = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2a = mdbFirstBadged node'; m p = Some (CTE x1a node'); mdbRevocable x2a = mdbRevocable node'; \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then x1 = capability.NullCap else cap' = x1); \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then \<not> mdbFirstBadged x2 else if p' = mdbNext s_node then mdbFirstBadged x2 = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2 = mdbFirstBadged node')\<rbrakk> \<Longrightarrow> \<exists>cte. m 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; isMDBParentOf (CTE x1a x2a) (CTE x1 x2); if p = mdbNext s_node then mdbFirstBadged x2a = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2a = mdbFirstBadged node'; m p = Some (CTE x1a node'); mdbRevocable x2a = mdbRevocable node'; \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then x1 = capability.NullCap else cap' = x1); \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then \<not> mdbFirstBadged x2 else if p' = mdbNext s_node then mdbFirstBadged x2 = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) else mdbFirstBadged x2 = mdbFirstBadged node'); \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then \<not> mdbRevocable x2 else mdbRevocable x2 = mdbRevocable node')\<rbrakk> \<Longrightarrow> \<exists>cte. m p' = Some cte \<and> isMDBParentOf (CTE x1a node') cte proof (prove)
goal:
No subgoals!