theory CSpace1_R

lemma capASID_update [simp]:
  "capASID (RetypeDecls_H.updateCapData P x c) = capASID c" unfolding capASID_def apply (cases c, simp_all add: updateCapData_def isCap_simps Let_def) apply (rename_tac arch_capability) apply (case_tac arch_capability,
         simp_all add: updateCapData_def
                       ARM_H.updateCapData_def
                       isCap_simps Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capASID (global.updateCapData P x c) = capASID c proof (prove)
goal (1 subgoal):
 1. (case global.updateCapData P 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 (asid, xd))) \<Rightarrow> Some asid | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (Some (asid, xa))) \<Rightarrow> Some asid | capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some asid)) \<Rightarrow> Some asid | 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 (asid, xd))) \<Rightarrow> Some asid | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (Some (asid, xa))) \<Rightarrow> Some asid | capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some asid)) \<Rightarrow> Some asid | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>x8. c = capability.ArchObjectCap x8 \<Longrightarrow> (case Arch.updateCapData P 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 (asid, xd))) \<Rightarrow> Some asid | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (Some (asid, xa))) \<Rightarrow> Some asid | capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some asid)) \<Rightarrow> Some asid | 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 (asid, xd)) \<Rightarrow> Some asid | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, xa)) \<Rightarrow> Some asid | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some xb) \<Rightarrow> Some xb | _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. c = capability.ArchObjectCap arch_capability \<Longrightarrow> (case Arch.updateCapData P 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 (asid, xd))) \<Rightarrow> Some asid | capability.ArchObjectCap (arch_capability.PageTableCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageTableCap x (Some (asid, xa))) \<Rightarrow> Some asid | capability.ArchObjectCap (arch_capability.PageDirectoryCap x None) \<Rightarrow> None | capability.ArchObjectCap (arch_capability.PageDirectoryCap x (Some asid)) \<Rightarrow> Some asid | 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 (asid, xd)) \<Rightarrow> Some asid | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, xa)) \<Rightarrow> Some asid | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some xb) \<Rightarrow> Some xb | _ \<Rightarrow> None) proof (prove)
goal:
No subgoals!