theory ArchFinalise_AI

lemma page_directory_at_def2:
  "page_directory_at p s = (\<exists>pd. ko_at (ArchObj (PageDirectory pd)) p s)" apply (simp add: a_type_def obj_at_def) apply (rule iffI) apply (erule exE) apply (case_tac ko, simp_all add: if_split_eq1) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj, simp_all split: if_splits) apply (erule exE) apply (rule_tac x="ArchObj (PageDirectory pd)" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at (AArch APageDirectory) p s = (\<exists>pd. ako_at (PageDirectory pd) p s) proof (prove)
goal (1 subgoal):
 1. (\<exists>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory) = (\<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd))) proof (prove)
goal (2 subgoals):
 1. \<exists>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory \<Longrightarrow> \<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd))
 2. \<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)) \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory proof (prove)
goal (2 subgoals):
 1. \<And>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory \<Longrightarrow> \<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd))
 2. \<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)) \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory proof (prove)
goal (2 subgoals):
 1. \<And>ko x5. \<lbrakk>kheap s p = Some (ArchObj x5) \<and> (case x5 of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) = APageDirectory; ko = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>pd. x5 = PageDirectory pd
 2. \<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)) \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory proof (prove)
goal (2 subgoals):
 1. \<And>ko arch_kernel_obj. \<lbrakk>kheap s p = Some (ArchObj arch_kernel_obj) \<and> (case arch_kernel_obj of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) = APageDirectory; ko = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> \<exists>pd. arch_kernel_obj = PageDirectory pd
 2. \<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)) \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory proof (prove)
goal (1 subgoal):
 1. \<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)) \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory proof (prove)
goal (1 subgoal):
 1. \<And>pd. kheap s p = Some (ArchObj (PageDirectory pd)) \<Longrightarrow> \<exists>ko. kheap s p = Some ko \<and> (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory proof (prove)
goal (1 subgoal):
 1. \<And>pd. kheap s p = Some (ArchObj (PageDirectory pd)) \<Longrightarrow> kheap s p = Some (ArchObj (PageDirectory pd)) \<and> (case ArchObj (PageDirectory pd) of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory proof (prove)
goal:
No subgoals!