theory Arch_C

lemma cap_get_tag_PageDirectoryCap:
  "ccap_relation cap cap' \<Longrightarrow>
     (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) =
     (cap = ArchObjectCap
        (PageDirectoryCap (capPDBasePtr_CL (cap_page_directory_cap_lift cap'))
                          (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap'))
                           then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap'))
                           else None)))" apply (rule iffI) apply (erule ccap_relationE) apply (clarsimp simp: cap_lifts cap_to_H_def) apply (simp add: cap_get_tag_isCap_unfolded_H_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = (cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL (cap_page_directory_cap_lift cap')) (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap')) else None))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL (cap_page_directory_cap_lift cap')) (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap')) else None))
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL (cap_page_directory_cap_lift cap')) (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap')) else None))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap; cap_lift cap' = Some vl; cap = cap_to_H vl; c_valid_cap cap'\<rbrakk> \<Longrightarrow> cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL (cap_page_directory_cap_lift cap')) (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap')) else None))
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL (cap_page_directory_cap_lift cap')) (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap')) else None))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL (cap_page_directory_cap_lift cap')) (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap')) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift cap')) else None))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap proof (prove)
goal:
No subgoals!