theory Tcb_R

lemma sameObject_corres2:
  "\<lbrakk> cap_relation c c'; cap_relation d d' \<rbrakk>
     \<Longrightarrow> same_object_as c d = sameObjectAs c' d'" apply (frule(1) sameRegion_corres2[symmetric, where c=c and d=d]) apply (case_tac c; simp add: sameObjectAs_def same_object_as_def
                               isCap_simps is_cap_simps bits_of_def) apply (case_tac d; simp) apply (case_tac d'; simp) apply (rename_tac arch_cap) apply clarsimp apply (case_tac d, (simp_all split: arch_cap.split)[11]) apply (rename_tac arch_capa) apply (clarsimp simp add: ARM_H.sameObjectAs_def Let_def) apply (intro conjI impI) apply (case_tac arch_cap; simp add: isCap_simps del: not_ex) apply (case_tac arch_capa; clarsimp simp del: not_ex) apply fastforce apply (case_tac arch_cap; simp add: sameRegionAs_def isCap_simps) apply (case_tac arch_capa; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'\<rbrakk> \<Longrightarrow> same_object_as c d = global.sameObjectAs c' d' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'; global.sameRegionAs c' d' = same_region_as c d\<rbrakk> \<Longrightarrow> same_object_as c d = global.sameObjectAs c' d' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' = capability.IRQControlCap; cap_relation d d'; global.sameRegionAs capability.IRQControlCap d' = (d = cap.IRQControlCap \<or> (\<exists>n. d = cap.IRQHandlerCap n)); c = cap.IRQControlCap\<rbrakk> \<Longrightarrow> (case d of cap.IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as cap.IRQControlCap d) = (case d' of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)
 2. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; cap_relation d d'; global.sameRegionAs c' d' = (case d of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False); c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case d of cap.ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (cap.ArchObjectCap x12) d) = (case c' of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` d' | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` d' | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` d' | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` d' | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` d' | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` d' | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` d' | capability.ArchObjectCap a \<Rightarrow> case d' of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` d' | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` d' | capability.IRQControlCap \<Rightarrow> case d' of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap) proof (prove)
goal (2 subgoals):
 1. \<And>x12. \<lbrakk>c' = capability.IRQControlCap; \<exists>a'. acap_relation x12 a' \<and> d' = capability.ArchObjectCap a'; \<not> global.sameRegionAs capability.IRQControlCap d'; c = cap.IRQControlCap; d = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<not> (case d' of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap)
 2. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; cap_relation d d'; global.sameRegionAs c' d' = (case d of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False); c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case d of cap.ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (cap.ArchObjectCap x12) d) = (case c' of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` d' | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` d' | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` d' | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` d' | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` d' | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` d' | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` d' | capability.ArchObjectCap a \<Rightarrow> case d' of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` d' | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` d' | capability.IRQControlCap \<Rightarrow> case d' of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap) proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>\<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; cap_relation d d'; global.sameRegionAs c' d' = (case d of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as x12 x | _ \<Rightarrow> False); c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case d of cap.ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (cap.ArchObjectCap x12) d) = (case c' of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` d' | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` d' | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` d' | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` d' | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` d' | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` d' | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` d' | capability.ArchObjectCap a \<Rightarrow> case d' of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` d' | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` d' | capability.IRQControlCap \<Rightarrow> case d' of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>\<exists>a'. acap_relation arch_cap a' \<and> c' = capability.ArchObjectCap a'; cap_relation d d'; global.sameRegionAs c' d' = (case d of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as arch_cap x | _ \<Rightarrow> False); c = cap.ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> (case d of cap.ArchObjectCap x \<Rightarrow> same_aobject_as arch_cap x | _ \<Rightarrow> same_region_as (cap.ArchObjectCap arch_cap) d) = (case c' of capability.ThreadCap word \<Rightarrow> capability.ThreadCap word `~global.sameRegionAs~` d' | capability.NullCap \<Rightarrow> capability.NullCap `~global.sameRegionAs~` d' | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.NotificationCap word1 word2 bool1 bool2 `~global.sameRegionAs~` d' | capability.IRQHandlerCap word \<Rightarrow> capability.IRQHandlerCap word `~global.sameRegionAs~` d' | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 `~global.sameRegionAs~` d' | capability.DomainCap \<Rightarrow> capability.DomainCap `~global.sameRegionAs~` d' | capability.Zombie word zombie_type nat \<Rightarrow> capability.Zombie word zombie_type nat `~global.sameRegionAs~` d' | capability.ArchObjectCap a \<Rightarrow> case d' of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a `~global.sameRegionAs~` capability.IRQControlCap | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ReplyCap word bool1 bool2 `~global.sameRegionAs~` d' | capability.UntypedCap x xa xb xc \<Rightarrow> False | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.CNodeCap word1 nat1 word2 nat2 `~global.sameRegionAs~` d' | capability.IRQControlCap \<Rightarrow> case d' of capability.ThreadCap word \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap x \<Rightarrow> False | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap arch_capability \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ArchObjectCap arch_capability | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.IRQControlCap `~global.sameRegionAs~` capability.IRQControlCap) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap a'. \<lbrakk>cap_relation d d'; global.sameRegionAs (capability.ArchObjectCap a') d' = (case d of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as arch_cap x | _ \<Rightarrow> False); c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> (case d of cap.ArchObjectCap x \<Rightarrow> same_aobject_as arch_cap x | _ \<Rightarrow> same_region_as (cap.ArchObjectCap arch_cap) d) = (case d' of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a' `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.IRQControlCap) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap a' x12. \<lbrakk>cap_relation d d'; global.sameRegionAs (capability.ArchObjectCap a') d' = (case d of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as arch_cap x | _ \<Rightarrow> False); c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'; d = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case d of cap.ArchObjectCap x \<Rightarrow> same_aobject_as arch_cap x | _ \<Rightarrow> same_region_as (cap.ArchObjectCap arch_cap) d) = (case d' of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a' `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.IRQControlCap) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap a' arch_capa. \<lbrakk>cap_relation d d'; global.sameRegionAs (capability.ArchObjectCap a') d' = (case d of cap.ArchObjectCap x \<Rightarrow> arch_same_region_as arch_cap x | _ \<Rightarrow> False); c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'; d = cap.ArchObjectCap arch_capa\<rbrakk> \<Longrightarrow> (case d of cap.ArchObjectCap x \<Rightarrow> same_aobject_as arch_cap x | _ \<Rightarrow> same_region_as (cap.ArchObjectCap arch_cap) d) = (case d' of capability.ThreadCap word \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.ThreadCap word | capability.NullCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.NullCap | capability.NotificationCap word1 word2 bool1 bool2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.NotificationCap word1 word2 bool1 bool2 | capability.IRQHandlerCap word \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.IRQHandlerCap word | capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.EndpointCap word1 word2 bool1 bool2 bool3 bool4 | capability.DomainCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.DomainCap | capability.Zombie word zombie_type nat \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.Zombie word zombie_type nat | capability.ArchObjectCap x \<Rightarrow> a' `~Arch.sameObjectAs~` x | capability.ReplyCap word bool1 bool2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.ReplyCap word bool1 bool2 | capability.UntypedCap bool word nat1 nat2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.UntypedCap bool word nat1 nat2 | capability.CNodeCap word1 nat1 word2 nat2 \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.CNodeCap word1 nat1 word2 nat2 | capability.IRQControlCap \<Rightarrow> capability.ArchObjectCap a' `~global.sameRegionAs~` capability.IRQControlCap) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap a' arch_capa a'a. \<lbrakk>global.sameRegionAs (capability.ArchObjectCap a') (capability.ArchObjectCap a'a) = arch_same_region_as arch_cap arch_capa; c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'; d = cap.ArchObjectCap arch_capa; acap_relation arch_capa a'a; d' = capability.ArchObjectCap a'a\<rbrakk> \<Longrightarrow> (isPageCap a' \<and> isPageCap a'a \<longrightarrow> (case arch_cap of arch_cap.PageCap dev ref x pgsz xa \<Rightarrow> case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = (capVPBasePtr a' = capVPBasePtr a'a \<and> capVPSize a' = capVPSize a'a \<and> capVPBasePtr a' \<le> capVPBasePtr a' + 2 ^ pageBitsForSize (capVPSize a') - 1 \<and> capVPIsDevice a' = capVPIsDevice a'a)) \<and> ((isPageCap a' \<longrightarrow> \<not> isPageCap a'a) \<longrightarrow> (case arch_cap of arch_cap.PageCap dev ref x pgsz xa \<Rightarrow> case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = Arch.sameRegionAs a' a'a) proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap a' arch_capa a'a. \<lbrakk>global.sameRegionAs (capability.ArchObjectCap a') (capability.ArchObjectCap a'a) = arch_same_region_as arch_cap arch_capa; c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'; d = cap.ArchObjectCap arch_capa; acap_relation arch_capa a'a; d' = capability.ArchObjectCap a'a; isPageCap a' \<and> isPageCap a'a\<rbrakk> \<Longrightarrow> (case arch_cap of arch_cap.PageCap dev ref x pgsz xa \<Rightarrow> case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = (capVPBasePtr a' = capVPBasePtr a'a \<and> capVPSize a' = capVPSize a'a \<and> capVPBasePtr a' \<le> capVPBasePtr a' + 2 ^ pageBitsForSize (capVPSize a') - 1 \<and> capVPIsDevice a' = capVPIsDevice a'a)
 2. \<And>arch_cap a' arch_capa a'a. \<lbrakk>global.sameRegionAs (capability.ArchObjectCap a') (capability.ArchObjectCap a'a) = arch_same_region_as arch_cap arch_capa; c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'; d = cap.ArchObjectCap arch_capa; acap_relation arch_capa a'a; d' = capability.ArchObjectCap a'a; isPageCap a' \<longrightarrow> \<not> isPageCap a'a\<rbrakk> \<Longrightarrow> (case arch_cap of arch_cap.PageCap dev ref x pgsz xa \<Rightarrow> case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = Arch.sameRegionAs a' a'a proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap a' arch_capa a'a x31 x32 x33 x34 x35. \<lbrakk>global.sameRegionAs (capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35)) (capability.ArchObjectCap a'a) = arch_same_region_as (arch_cap.PageCap x31 x32 x33 x34 x35) arch_capa; c = cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35); a' = arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35; c' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35); d = cap.ArchObjectCap arch_capa; acap_relation arch_capa a'a; d' = capability.ArchObjectCap a'a; \<exists>d v0 v1 v2 v3. a'a = arch_capability.PageCap d v0 v1 v2 v3; arch_cap = arch_cap.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = (x32 = capVPBasePtr a'a \<and> x34 = capVPSize a'a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = capVPIsDevice a'a)
 2. \<And>arch_cap a' arch_capa a'a. \<lbrakk>global.sameRegionAs (capability.ArchObjectCap a') (capability.ArchObjectCap a'a) = arch_same_region_as arch_cap arch_capa; c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'; d = cap.ArchObjectCap arch_capa; acap_relation arch_capa a'a; d' = capability.ArchObjectCap a'a; isPageCap a' \<longrightarrow> \<not> isPageCap a'a\<rbrakk> \<Longrightarrow> (case arch_cap of arch_cap.PageCap dev ref x pgsz xa \<Rightarrow> case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = Arch.sameRegionAs a' a'a proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x31a x32a x33a x34a x35a. \<lbrakk>global.sameRegionAs (capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35)) (capability.ArchObjectCap (arch_capability.PageCap x31a x32a (vmrights_map x33a) x34a x35a)) = (let topB = x32a + 2 ^ pageBitsForSize x34a - 1 in x32 \<le> x32a \<and> topB \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x32a \<le> topB); c = cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35); c' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35); d = cap.ArchObjectCap (arch_cap.PageCap x31a x32a x33a x34a x35a); d' = capability.ArchObjectCap (arch_capability.PageCap x31a x32a (vmrights_map x33a) x34a x35a)\<rbrakk> \<Longrightarrow> (x31 = x31a \<and> x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1) = (x32 = x32a \<and> x34 = x34a \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 \<and> x31 = x31a)
 2. \<And>arch_cap a' arch_capa a'a. \<lbrakk>global.sameRegionAs (capability.ArchObjectCap a') (capability.ArchObjectCap a'a) = arch_same_region_as arch_cap arch_capa; c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'; d = cap.ArchObjectCap arch_capa; acap_relation arch_capa a'a; d' = capability.ArchObjectCap a'a; isPageCap a' \<longrightarrow> \<not> isPageCap a'a\<rbrakk> \<Longrightarrow> (case arch_cap of arch_cap.PageCap dev ref x pgsz xa \<Rightarrow> case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = Arch.sameRegionAs a' a'a proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap a' arch_capa a'a. \<lbrakk>global.sameRegionAs (capability.ArchObjectCap a') (capability.ArchObjectCap a'a) = arch_same_region_as arch_cap arch_capa; c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'; d = cap.ArchObjectCap arch_capa; acap_relation arch_capa a'a; d' = capability.ArchObjectCap a'a; isPageCap a' \<longrightarrow> \<not> isPageCap a'a\<rbrakk> \<Longrightarrow> (case arch_cap of arch_cap.PageCap dev ref x pgsz xa \<Rightarrow> case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = Arch.sameRegionAs a' a'a proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap a' arch_capa a'a x31 x32 x33 x34 x35. \<lbrakk>Arch.sameRegionAs (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35) a'a = arch_same_region_as (arch_cap.PageCap x31 x32 x33 x34 x35) arch_capa; c = cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35); a' = arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35; c' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35); d = cap.ArchObjectCap arch_capa; acap_relation arch_capa a'a; d' = capability.ArchObjectCap a'a; \<forall>d v0 v1 v2 v3. a'a \<noteq> arch_capability.PageCap d v0 v1 v2 v3; arch_cap = arch_cap.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (case arch_capa of arch_cap.PageCap dev' ref' xb pgsz' xc \<Rightarrow> (x31, x32, x34) = (dev', ref', pgsz') \<and> x32 \<le> x32 + 2 ^ pageBitsForSize x34 - 1 | _ \<Rightarrow> arch_same_region_as arch_cap arch_capa) = arch_same_region_as (arch_cap.PageCap x31 x32 x33 x34 x35) arch_capa proof (prove)
goal:
No subgoals!