theory CSpace_I

lemma capMasterCap_eqDs1:
  "capMasterCap cap = EndpointCap ref bdg s r g gr
     \<Longrightarrow> bdg = 0 \<and> s \<and> r \<and> g \<and> gr
          \<and> (\<exists>bdg s r g gr. cap = EndpointCap ref bdg s r g gr)"
  "capMasterCap cap = NotificationCap ref bdg s r
     \<Longrightarrow> bdg = 0 \<and> s \<and> r
          \<and> (\<exists>bdg s r. cap = NotificationCap ref bdg s r)"
  "capMasterCap cap = CNodeCap ref bits gd gs
     \<Longrightarrow> gd = 0 \<and> gs = 0 \<and> (\<exists>gd gs. cap = CNodeCap ref bits gd gs)"
  "capMasterCap cap = ThreadCap ref
     \<Longrightarrow> cap = ThreadCap ref"
  "capMasterCap cap = NullCap
     \<Longrightarrow> cap = NullCap"
  "capMasterCap cap = DomainCap
     \<Longrightarrow> cap = DomainCap"
  "capMasterCap cap = IRQControlCap
     \<Longrightarrow> cap = IRQControlCap"
  "capMasterCap cap = IRQHandlerCap irq
     \<Longrightarrow> cap = IRQHandlerCap irq"
  "capMasterCap cap = Zombie ref tp n
     \<Longrightarrow> cap = Zombie ref tp n"
  "capMasterCap cap = UntypedCap d ref bits 0
     \<Longrightarrow> \<exists>f. cap = UntypedCap d ref bits f"
  "capMasterCap cap = ReplyCap ref master g
     \<Longrightarrow> master \<and> g \<and> (\<exists>master g. cap = ReplyCap ref master g)"
  "capMasterCap cap = ArchObjectCap (PageCap d ref rghts sz mapdata)
     \<Longrightarrow> rghts = VMReadWrite \<and> mapdata = None
          \<and> (\<exists>rghts mapdata. cap = ArchObjectCap (PageCap d ref rghts sz mapdata))"
  "capMasterCap cap = ArchObjectCap ASIDControlCap
     \<Longrightarrow> cap = ArchObjectCap ASIDControlCap"
  "capMasterCap cap = ArchObjectCap (ASIDPoolCap pool asid)
     \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = ArchObjectCap (ASIDPoolCap pool asid))"
  "capMasterCap cap = ArchObjectCap (PageTableCap ptr data)
     \<Longrightarrow> data = None \<and> (\<exists>data. cap = ArchObjectCap (PageTableCap ptr data))"
  "capMasterCap cap = ArchObjectCap (PageDirectoryCap ptr data2)
     \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = ArchObjectCap (PageDirectoryCap ptr data2))" by (clarsimp simp: capMasterCap_def
              split: capability.split_asm arch_capability.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((((capMasterCap cap = capability.EndpointCap ref bdg s r g gr \<Longrightarrow> bdg = 0 \<and> s \<and> r \<and> g \<and> gr \<and> (\<exists>bdg s r g gr. cap = capability.EndpointCap ref bdg s r g gr)) &&& (capMasterCap cap = capability.NotificationCap ref bdg s r \<Longrightarrow> bdg = 0 \<and> s \<and> r \<and> (\<exists>bdg s r. cap = capability.NotificationCap ref bdg s r))) &&& (capMasterCap cap = capability.CNodeCap ref bits gd gs \<Longrightarrow> gd = 0 \<and> gs = 0 \<and> (\<exists>gd gs. cap = capability.CNodeCap ref bits gd gs)) &&& (capMasterCap cap = capability.ThreadCap ref \<Longrightarrow> cap = capability.ThreadCap ref)) &&& ((capMasterCap cap = capability.NullCap \<Longrightarrow> cap = capability.NullCap) &&& (capMasterCap cap = capability.DomainCap \<Longrightarrow> cap = capability.DomainCap)) &&& (capMasterCap cap = capability.IRQControlCap \<Longrightarrow> cap = capability.IRQControlCap) &&& (capMasterCap cap = capability.IRQHandlerCap irq \<Longrightarrow> cap = capability.IRQHandlerCap irq)) &&& (((capMasterCap cap = capability.Zombie ref tp n \<Longrightarrow> cap = capability.Zombie ref tp n) &&& (capMasterCap cap = capability.UntypedCap d ref bits 0 \<Longrightarrow> \<exists>f. cap = capability.UntypedCap d ref bits f)) &&& (capMasterCap cap = capability.ReplyCap ref master g \<Longrightarrow> master \<and> g \<and> (\<exists>master g. cap = capability.ReplyCap ref master g)) &&& (capMasterCap cap = capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz mapdata) \<Longrightarrow> rghts = VMReadWrite \<and> mapdata = None \<and> (\<exists>rghts mapdata. cap = capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz mapdata)))) &&& ((capMasterCap cap = capability.ArchObjectCap arch_capability.ASIDControlCap \<Longrightarrow> cap = capability.ArchObjectCap arch_capability.ASIDControlCap) &&& (capMasterCap cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap pool asid) \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = capability.ArchObjectCap (arch_capability.ASIDPoolCap pool asid)))) &&& (capMasterCap cap = capability.ArchObjectCap (arch_capability.PageTableCap ptr data) \<Longrightarrow> data = None \<and> (\<exists>data. cap = capability.ArchObjectCap (arch_capability.PageTableCap ptr data))) &&& (capMasterCap cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap ptr data2) \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap ptr data2)))