theory Ipc_R

lemma isIRQControlCap_mask [simp]:
  "isIRQControlCap (maskCapRights R c) = isIRQControlCap c" apply (case_tac c) apply (clarsimp simp: isCap_simps maskCapRights_def Let_def)+ apply (rename_tac arch_capability) apply (case_tac arch_capability) apply (clarsimp simp: isCap_simps ARM_H.maskCapRights_def
                                maskCapRights_def Let_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c proof (prove)
goal (12 subgoals):
 1. \<And>x1. c = capability.ThreadCap x1 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 2. c = capability.NullCap \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 3. \<And>x31 x32 x33 x34. c = capability.NotificationCap x31 x32 x33 x34 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 4. \<And>x4. c = capability.IRQHandlerCap x4 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 5. \<And>x51 x52 x53 x54 x55 x56. c = capability.EndpointCap x51 x52 x53 x54 x55 x56 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 6. c = capability.DomainCap \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 7. \<And>x71 x72 x73. c = capability.Zombie x71 x72 x73 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 8. \<And>x8. c = capability.ArchObjectCap x8 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 9. \<And>x91 x92 x93. c = capability.ReplyCap x91 x92 x93 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 10. \<And>x101 x102 x103 x104. c = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
A total of 12 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>x8. \<lbrakk>c = capability.ArchObjectCap x8; Arch.maskCapRights R x8 = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 2. \<And>x91 x92 x93. c = capability.ReplyCap x91 x92 x93 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 3. \<And>x101 x102 x103 x104. c = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 4. \<And>x111 x112 x113 x114. c = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 5. c = capability.IRQControlCap \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c proof (prove)
goal (5 subgoals):
 1. \<And>arch_capability. \<lbrakk>c = capability.ArchObjectCap arch_capability; Arch.maskCapRights R arch_capability = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 2. \<And>x91 x92 x93. c = capability.ReplyCap x91 x92 x93 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 3. \<And>x101 x102 x103 x104. c = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 4. \<And>x111 x112 x113 x114. c = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 5. c = capability.IRQControlCap \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c proof (prove)
goal (9 subgoals):
 1. \<And>arch_capability x11 x12. \<lbrakk>c = capability.ArchObjectCap arch_capability; Arch.maskCapRights R arch_capability = capability.IRQControlCap; arch_capability = arch_capability.ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> False
 2. \<And>arch_capability. \<lbrakk>c = capability.ArchObjectCap arch_capability; Arch.maskCapRights R arch_capability = capability.IRQControlCap; arch_capability = arch_capability.ASIDControlCap\<rbrakk> \<Longrightarrow> False
 3. \<And>arch_capability x31 x32 x33 x34 x35. \<lbrakk>c = capability.ArchObjectCap arch_capability; Arch.maskCapRights R arch_capability = capability.IRQControlCap; arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> False
 4. \<And>arch_capability x41 x42. \<lbrakk>c = capability.ArchObjectCap arch_capability; Arch.maskCapRights R arch_capability = capability.IRQControlCap; arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> False
 5. \<And>arch_capability x51 x52. \<lbrakk>c = capability.ArchObjectCap arch_capability; Arch.maskCapRights R arch_capability = capability.IRQControlCap; arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> False
 6. \<And>x91 x92 x93. c = capability.ReplyCap x91 x92 x93 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 7. \<And>x101 x102 x103 x104. c = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 8. \<And>x111 x112 x113 x114. c = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c
 9. c = capability.IRQControlCap \<Longrightarrow> isIRQControlCap (global.maskCapRights R c) = isIRQControlCap c proof (prove)
goal:
No subgoals!