theory CSpace1_R

lemma isMDBParentOf1:
  assumes "\<not>isReplyCap cap"
  assumes "\<not>isEndpointCap cap"
  assumes "\<not>isNotificationCap cap"
  shows "isMDBParentOf c (CTE cap' m) = isMDBParentOf c (CTE cap m)" proof - from assms have c':
    "\<not>isReplyCap cap'" "\<not>isEndpointCap cap'"
    "\<not>isNotificationCap cap'" by auto note isReplyCap [simp del] isEndpointCap [simp del] isNotificationCap [simp del] from c' assms show ?thesis apply (cases c, clarsimp) apply (simp add: isMDBParentOf_CTE) apply (rule iffI) apply clarsimp apply (clarsimp simp: capBadge_ordering_def capBadge_def isCap_simps sameRegionAs_def3
                   split: if_split_asm) apply clarsimp apply (clarsimp simp: capBadge_ordering_def capBadge_def isCap_simps sameRegionAs_def3
                  split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf c (CTE cap' m) = isMDBParentOf c (CTE cap m) proof (state)
goal (1 subgoal):
 1. isMDBParentOf c (CTE cap' m) = isMDBParentOf c (CTE cap m) proof (chain)
picking this:
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap proof (prove)
using this:
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap

goal (1 subgoal):
 1. \<not> isReplyCap cap' &&& \<not> isEndpointCap cap' &&& \<not> isNotificationCap cap' proof (state)
this:
\<not> isReplyCap cap'
\<not> isEndpointCap cap'
\<not> isNotificationCap cap'

goal (1 subgoal):
 1. isMDBParentOf c (CTE cap' m) = isMDBParentOf c (CTE cap m) proof (state)
this:
isReplyCap cap' = isReplyCap cap
isEndpointCap cap' = isEndpointCap cap
isNotificationCap cap' = isNotificationCap cap

goal (1 subgoal):
 1. isMDBParentOf c (CTE cap' m) = isMDBParentOf c (CTE cap m) proof (chain)
picking this:
\<not> isReplyCap cap'
\<not> isEndpointCap cap'
\<not> isNotificationCap cap'
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap proof (prove)
using this:
\<not> isReplyCap cap'
\<not> isEndpointCap cap'
\<not> isNotificationCap cap'
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap

goal (1 subgoal):
 1. isMDBParentOf c (CTE cap' m) = isMDBParentOf c (CTE cap m) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1 x2) (CTE cap' m) = isMDBParentOf (CTE x1 x2) (CTE cap m) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap\<rbrakk> \<Longrightarrow> (global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged m)) = (global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged m)) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap; global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged m)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged m)
 2. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap; global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged m)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged m) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap; global.sameRegionAs x1 cap; mdbRevocable x2; (capBadge x1, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged m)\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged m)
 2. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap; global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged m)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged m) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap; global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged m)\<rbrakk> \<Longrightarrow> global.sameRegionAs x1 cap \<and> mdbRevocable x2 \<and> (capBadge x1, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged m) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>c = CTE x1 x2; \<not> isReplyCap cap'; \<not> isEndpointCap cap'; \<not> isNotificationCap cap'; \<not> isReplyCap cap; \<not> isEndpointCap cap; \<not> isNotificationCap cap; global.sameRegionAs x1 cap; mdbRevocable x2; (capBadge x1, capBadge cap) \<in> capBadge_ordering (mdbFirstBadged m)\<rbrakk> \<Longrightarrow> (capBadge x1, capBadge cap') \<in> capBadge_ordering (mdbFirstBadged m) proof (prove)
goal:
No subgoals! proof (state)
this:
isMDBParentOf c (CTE cap' m) = isMDBParentOf c (CTE cap m)

goal:
No subgoals!