theory CSpace_I

lemma capMasterCap_maskCapRights[simp]:
  "capMasterCap (maskCapRights msk cap)
    = capMasterCap cap" apply (cases cap;
         simp add: maskCapRights_def Let_def isCap_simps capMasterCap_def) apply (rename_tac arch_capability) apply (case_tac arch_capability;
         simp add: ARM_H.maskCapRights_def Let_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capMasterCap (global.maskCapRights msk cap) = capMasterCap cap proof (prove)
goal (1 subgoal):
 1. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> (case Arch.maskCapRights msk x8 of capability.ThreadCap ref \<Rightarrow> capability.ThreadCap ref | capability.NotificationCap ref bdg s r \<Rightarrow> capability.NotificationCap ref 0 True True | capability.EndpointCap ref bdg s r g gr \<Rightarrow> capability.EndpointCap ref 0 True True True True | capability.ArchObjectCap acap \<Rightarrow> capability.ArchObjectCap (case acap of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> acap | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) | capability.ReplyCap ref master g \<Rightarrow> capability.ReplyCap ref True True | capability.UntypedCap d ref n f \<Rightarrow> capability.UntypedCap d ref n 0 | capability.CNodeCap ref bits gd gs \<Rightarrow> capability.CNodeCap ref bits 0 0 | _ \<Rightarrow> Arch.maskCapRights msk x8) = capability.ArchObjectCap (case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> x8 | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. cap = capability.ArchObjectCap arch_capability \<Longrightarrow> (case Arch.maskCapRights msk arch_capability of capability.ThreadCap ref \<Rightarrow> capability.ThreadCap ref | capability.NotificationCap ref bdg s r \<Rightarrow> capability.NotificationCap ref 0 True True | capability.EndpointCap ref bdg s r g gr \<Rightarrow> capability.EndpointCap ref 0 True True True True | capability.ArchObjectCap acap \<Rightarrow> capability.ArchObjectCap (case acap of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> acap | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) | capability.ReplyCap ref master g \<Rightarrow> capability.ReplyCap ref True True | capability.UntypedCap d ref n f \<Rightarrow> capability.UntypedCap d ref n 0 | capability.CNodeCap ref bits gd gs \<Rightarrow> capability.CNodeCap ref bits 0 0 | _ \<Rightarrow> Arch.maskCapRights msk arch_capability) = capability.ArchObjectCap (case arch_capability of arch_capability.ASIDPoolCap pool asid \<Rightarrow> arch_capability.ASIDPoolCap pool 0 | arch_capability.ASIDControlCap \<Rightarrow> arch_capability | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> arch_capability.PageCap d ref VMReadWrite sz None | arch_capability.PageTableCap ptr data \<Rightarrow> arch_capability.PageTableCap ptr None | arch_capability.PageDirectoryCap ptr data \<Rightarrow> arch_capability.PageDirectoryCap ptr None) proof (prove)
goal:
No subgoals!