theory CSpace1_R

lemma cap_vptr_mask' [simp]:
  "cap_vptr' (maskCapRights x c) = cap_vptr' c" unfolding cap_vptr'_def apply (cases c, simp_all add: maskCapRights_def isCap_simps Let_def) apply (rename_tac arch_capability) apply (case_tac arch_capability,
         simp_all add: maskCapRights_def ARM_H.maskCapRights_def isCap_simps Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_vptr' (global.maskCapRights x c) = cap_vptr' c proof (prove)
goal (1 subgoal):
 1. (case global.maskCapRights x c of capability.ArchObjectCap (arch_capability.PageCap x xa xb xc None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb xc (Some (xd, vptr))) \<Rightarrow> Some vptr | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (Some (xa, vptr))) \<Rightarrow> Some vptr | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case c of capability.ArchObjectCap (arch_capability.PageCap x xa xb xc None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb xc (Some (xd, vptr))) \<Rightarrow> Some vptr | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (Some (xa, vptr))) \<Rightarrow> Some vptr | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>x8. c = capability.ArchObjectCap x8 \<Longrightarrow> (case Arch.maskCapRights x x8 of capability.ArchObjectCap (arch_capability.PageCap x xa xb xc None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb xc (Some (xd, vptr))) \<Rightarrow> Some vptr | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (Some (xa, vptr))) \<Rightarrow> Some vptr | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case x8 of arch_capability.PageCap x xa xb xc None \<Rightarrow> None | arch_capability.PageCap x xa xb xc (Some (xd, xf)) \<Rightarrow> Some xf | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (xa, xc)) \<Rightarrow> Some xc | _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. c = capability.ArchObjectCap arch_capability \<Longrightarrow> (case Arch.maskCapRights x arch_capability of capability.ArchObjectCap (arch_capability.PageCap x xa xb xc None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageCap x xa xb xc (Some (xd, vptr))) \<Rightarrow> Some vptr | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (Some (xa, vptr))) \<Rightarrow> Some vptr | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case arch_capability of arch_capability.PageCap x xa xb xc None \<Rightarrow> None | arch_capability.PageCap x xa xb xc (Some (xd, xf)) \<Rightarrow> Some xf | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (xa, xc)) \<Rightarrow> Some xc | _ \<Rightarrow> None) proof (prove)
goal:
No subgoals!