theory CSpace1_R

lemma derived_sameRegionAs:
  "\<lbrakk> is_derived' m p cap' cap; s \<turnstile>' cap' \<rbrakk>
       \<Longrightarrow> sameRegionAs cap cap'" unfolding is_derived'_def badge_derived'_def apply (simp add: sameRegionAs_def3) apply (cases "isUntypedCap cap \<or> isArchPageCap cap") apply (rule disjI2, rule disjI1) apply (erule disjE) apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def
                          is_aligned_no_overflow capRange_def
          split:capability.splits arch_capability.splits option.splits) apply (clarsimp simp: isCap_simps valid_cap'_def capAligned_def
                          is_aligned_no_overflow capRange_def
          split:capability.splits arch_capability.splits option.splits) apply (clarsimp simp: isCap_simps valid_cap'_def
                          is_aligned_no_overflow capRange_def
          split:capability.splits arch_capability.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived' m p cap' cap; valid_cap' cap' s\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> (capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False) \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<or> isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> capASID cap \<noteq> None); valid_cap' cap' s\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; isUntypedCap cap \<or> isArchPageCap cap\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap'
 2. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; \<not> (isUntypedCap cap \<or> isArchPageCap cap)\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; isUntypedCap cap \<or> isArchPageCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap')
 2. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; \<not> (isUntypedCap cap \<or> isArchPageCap cap)\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; isUntypedCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap')
 2. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; isArchPageCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap')
 3. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; \<not> (isUntypedCap cap \<or> isArchPageCap cap)\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; isArchPageCap cap\<rbrakk> \<Longrightarrow> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap')
 2. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; \<not> (isUntypedCap cap \<or> isArchPageCap cap)\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isIRQControlCap cap' \<and> capMasterCap cap = capMasterCap cap' \<and> (capBadge cap, capBadge cap') \<in> capBadge_ordering False \<and> (isUntypedCap cap \<longrightarrow> descendants_of' p m = {}) \<and> isReplyCap cap = isReplyCap cap' \<and> (isReplyCap cap \<longrightarrow> capReplyMaster cap) \<and> (isReplyCap cap' \<longrightarrow> \<not> capReplyMaster cap') \<and> (vsCapRef cap = vsCapRef cap' \<or> isArchCap isPageCap cap') \<and> (isArchCap isPageTableCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)) \<and> (isArchCap isPageDirectoryCap cap \<longrightarrow> capASID cap = capASID cap' \<and> (\<exists>y. capASID cap = Some y)); valid_cap' cap' s; \<not> (isUntypedCap cap \<or> isArchPageCap cap)\<rbrakk> \<Longrightarrow> cap \<noteq> capability.NullCap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap' proof (prove)
goal:
No subgoals!