theory ArchMove_C

lemma cap_case_isPageDirectoryCap:
  "(case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd ( Some asid))  \<Rightarrow> fn pd asid
                | _ => g)
    = (if ( if (isArchObjectCap cap) then if (isPageDirectoryCap (capCap cap)) then capPDMappedASID (capCap cap) \<noteq> None else False else False)
                then fn (capPDBasePtr (capCap cap)) (the ( capPDMappedASID (capCap cap))) else g)" apply (cases cap; simp add: isArchObjectCap_def) apply (rename_tac arch_capability) apply (case_tac arch_capability, simp_all add: isPageDirectoryCap_def) apply (rename_tac option) apply (case_tac option; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> g | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> fn pd asid | capability.ArchObjectCap _ \<Rightarrow> g | _ \<Rightarrow> g) = (if if isArchObjectCap cap then if isPageDirectoryCap (capCap cap) then capPDMappedASID (capCap cap) \<noteq> None else False else False then fn (capPDBasePtr (capCap cap)) (the (capPDMappedASID (capCap cap))) else g) proof (prove)
goal (1 subgoal):
 1. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> (isPageDirectoryCap x8 \<longrightarrow> ((\<exists>y. capPDMappedASID x8 = Some y) \<longrightarrow> (case x8 of arch_capability.PageDirectoryCap pd None \<Rightarrow> g | arch_capability.PageDirectoryCap pd (Some xa) \<Rightarrow> fn pd xa | _ \<Rightarrow> g) = fn (capPDBasePtr x8) (the (capPDMappedASID x8))) \<and> (capPDMappedASID x8 = None \<longrightarrow> (case x8 of arch_capability.PageDirectoryCap pd None \<Rightarrow> g | arch_capability.PageDirectoryCap pd (Some xa) \<Rightarrow> fn pd xa | _ \<Rightarrow> g) = g)) \<and> (\<not> isPageDirectoryCap x8 \<longrightarrow> (case x8 of arch_capability.PageDirectoryCap pd None \<Rightarrow> g | arch_capability.PageDirectoryCap pd (Some xa) \<Rightarrow> fn pd xa | _ \<Rightarrow> g) = g) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. cap = capability.ArchObjectCap arch_capability \<Longrightarrow> (isPageDirectoryCap arch_capability \<longrightarrow> ((\<exists>y. capPDMappedASID arch_capability = Some y) \<longrightarrow> (case arch_capability of arch_capability.PageDirectoryCap pd None \<Rightarrow> g | arch_capability.PageDirectoryCap pd (Some xa) \<Rightarrow> fn pd xa | _ \<Rightarrow> g) = fn (capPDBasePtr arch_capability) (the (capPDMappedASID arch_capability))) \<and> (capPDMappedASID arch_capability = None \<longrightarrow> (case arch_capability of arch_capability.PageDirectoryCap pd None \<Rightarrow> g | arch_capability.PageDirectoryCap pd (Some xa) \<Rightarrow> fn pd xa | _ \<Rightarrow> g) = g)) \<and> (\<not> isPageDirectoryCap arch_capability \<longrightarrow> (case arch_capability of arch_capability.PageDirectoryCap pd None \<Rightarrow> g | arch_capability.PageDirectoryCap pd (Some xa) \<Rightarrow> fn pd xa | _ \<Rightarrow> g) = g) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability x51 x52. \<lbrakk>cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> (\<exists>y. x52 = Some y) \<longrightarrow> (case x52 of None \<Rightarrow> g | Some x \<Rightarrow> fn x51 x) = fn x51 (the x52) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability x51 option. \<lbrakk>cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 option); arch_capability = arch_capability.PageDirectoryCap x51 option\<rbrakk> \<Longrightarrow> (\<exists>y. option = Some y) \<longrightarrow> (case option of None \<Rightarrow> g | Some x \<Rightarrow> fn x51 x) = fn x51 (the option) proof (prove)
goal:
No subgoals!