theory CSpace_R

lemma capAligned_master:
  "\<lbrakk>capAligned cap; capMasterCap cap = capMasterCap ncap\<rbrakk> \<Longrightarrow> capAligned ncap" apply (case_tac cap) apply (clarsimp simp:capAligned_def)+ apply (rename_tac arch_capability) apply (case_tac arch_capability) apply (clarsimp simp:capAligned_def)+ done

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