theory CSpace_I

lemma capMasterCap_simps[simp]:
  "capMasterCap (EndpointCap ref bdg s r g gr) = EndpointCap ref 0 True True True True"
  "capMasterCap (NotificationCap ref bdg s r) = NotificationCap ref 0 True True"
  "capMasterCap (CNodeCap ref bits gd gs) = CNodeCap ref bits 0 0"
  "capMasterCap (ThreadCap ref) = ThreadCap ref"
  "capMasterCap capability.NullCap = capability.NullCap"
  "capMasterCap capability.DomainCap = capability.DomainCap"
  "capMasterCap (capability.IRQHandlerCap irq) = capability.IRQHandlerCap irq"
  "capMasterCap (capability.Zombie word zombie_type n) = capability.Zombie word zombie_type n"
  "capMasterCap (capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 word2)) =
            capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 0)"
  "capMasterCap (capability.ArchObjectCap arch_capability.ASIDControlCap) =
         capability.ArchObjectCap arch_capability.ASIDControlCap"
  "capMasterCap (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size pdata)) =
            capability.ArchObjectCap (arch_capability.PageCap d word VMReadWrite vmpage_size None)"
  "capMasterCap (capability.ArchObjectCap (arch_capability.PageTableCap word ptdata)) =
            capability.ArchObjectCap (arch_capability.PageTableCap word None)"
  "capMasterCap (capability.ArchObjectCap (arch_capability.PageDirectoryCap word pddata)) =
            capability.ArchObjectCap (arch_capability.PageDirectoryCap word None)"
  "capMasterCap (capability.UntypedCap d word n f) = capability.UntypedCap d word n 0"
  "capMasterCap capability.IRQControlCap = capability.IRQControlCap"
  "capMasterCap (capability.ReplyCap word m g) = capability.ReplyCap word True True" by (simp_all add: capMasterCap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((capMasterCap (capability.EndpointCap ref bdg s r g gr) = capability.EndpointCap ref 0 True True True True &&& capMasterCap (capability.NotificationCap ref bdg s r) = capability.NotificationCap ref 0 True True) &&& capMasterCap (capability.CNodeCap ref bits gd gs) = capability.CNodeCap ref bits 0 0 &&& capMasterCap (capability.ThreadCap ref) = capability.ThreadCap ref) &&& (capMasterCap capability.NullCap = capability.NullCap &&& capMasterCap capability.DomainCap = capability.DomainCap) &&& capMasterCap (capability.IRQHandlerCap irq) = capability.IRQHandlerCap irq &&& capMasterCap (capability.Zombie word zombie_type n) = capability.Zombie word zombie_type n) &&& ((capMasterCap (capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 word2)) = capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 0) &&& capMasterCap (capability.ArchObjectCap arch_capability.ASIDControlCap) = capability.ArchObjectCap arch_capability.ASIDControlCap) &&& capMasterCap (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size pdata)) = capability.ArchObjectCap (arch_capability.PageCap d word VMReadWrite vmpage_size None) &&& capMasterCap (capability.ArchObjectCap (arch_capability.PageTableCap word ptdata)) = capability.ArchObjectCap (arch_capability.PageTableCap word None)) &&& (capMasterCap (capability.ArchObjectCap (arch_capability.PageDirectoryCap word pddata)) = capability.ArchObjectCap (arch_capability.PageDirectoryCap word None) &&& capMasterCap (capability.UntypedCap d word n f) = capability.UntypedCap d word n 0) &&& capMasterCap capability.IRQControlCap = capability.IRQControlCap &&& capMasterCap (capability.ReplyCap word m g) = capability.ReplyCap word True True