theory ArchKHeap_AI

lemma valid_table_caps_ptD:
  "\<lbrakk> (caps_of_state s) p = Some (ArchObjectCap (arch_cap.PageTableCap p' None));
     page_table_at p' s; valid_table_caps s \<rbrakk> \<Longrightarrow>
    \<exists>pt. ko_at (ArchObj (PageTable pt)) p' s \<and> valid_vspace_obj (PageTable pt) s" apply (clarsimp simp: valid_table_caps_def simp del: split_paired_All) apply (erule allE)+ apply (erule (1) impE) apply (clarsimp simp add: is_pt_cap_def cap_asid_def) apply (erule impE, rule refl) apply (clarsimp simp: obj_at_def empty_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap p' None)); typ_at (AArch APageTable) p' s; valid_table_caps s\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p' s \<and> valid_vspace_obj (PageTable pt) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap p' None)); typ_at (AArch APageTable) p' s; \<forall>r p cap. caps_of_state s p = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p' s \<and> (\<forall>x. valid_pte (pt x) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap p' None)); typ_at (AArch APageTable) p' s; caps_of_state s ?p5 = Some ?cap7 \<longrightarrow> (is_pd_cap ?cap7 \<longrightarrow> cap_asid ?cap7 = None \<longrightarrow> ?r3 \<in> obj_refs ?cap7 \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s) \<and> (is_pt_cap ?cap7 \<longrightarrow> cap_asid ?cap7 = None \<longrightarrow> ?r3 \<in> obj_refs ?cap7 \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s)\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p' s \<and> (\<forall>x. valid_pte (pt x) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap p' None)); typ_at (AArch APageTable) p' s; (is_pd_cap (ArchObjectCap (PageTableCap p' None)) \<longrightarrow> cap_asid (ArchObjectCap (PageTableCap p' None)) = None \<longrightarrow> ?r3 \<in> obj_refs (ArchObjectCap (PageTableCap p' None)) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s) \<and> (is_pt_cap (ArchObjectCap (PageTableCap p' None)) \<longrightarrow> cap_asid (ArchObjectCap (PageTableCap p' None)) = None \<longrightarrow> ?r3 \<in> obj_refs (ArchObjectCap (PageTableCap p' None)) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s)\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p' s \<and> (\<forall>x. valid_pte (pt x) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap p' None)); typ_at (AArch APageTable) p' s; is_pd_cap (ArchObjectCap (PageTableCap p' None)) \<longrightarrow> ?r3 = p' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s; ?r3 = p' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?r3 s\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p' s \<and> (\<forall>x. valid_pte (pt x) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap p' None)); typ_at (AArch APageTable) p' s; is_pd_cap (ArchObjectCap (PageTableCap p' None)) \<longrightarrow> p' = p' \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p' s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p' s\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p' s \<and> (\<forall>x. valid_pte (pt x) s) proof (prove)
goal:
No subgoals!