theory ArchDetype_AI

lemma valid_global_objs_detype[detype_invs_proofs]: "valid_global_objs (detype (untyped_range cap) s)" using valid_global_objs valid_global_refsD [OF globals cap] apply (simp add: valid_global_objs_def valid_vso_at_def arch_state_det) apply (elim conjE, intro conjI) apply (simp add: global_refs_def cap_range_def arch_state_det) apply (erule exEI) apply (insert pd_at_global_pd)[1] subgoal by (clarsimp simp: obj_at_def a_type_simps empty_table_def arch_state_det) apply (simp add: global_refs_def cap_range_def) apply (clarsimp elim!: global_pts) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_objs (detype (untyped_range cap) s) proof (prove)
using this:
valid_global_objs s
?r \<in> global_refs s \<Longrightarrow> ?r \<notin> cap_range cap

goal (1 subgoal):
 1. valid_global_objs (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s) \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s \<and> (\<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))); \<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> untyped_range cap \<and> (\<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao (detype (untyped_range cap) s)) \<and> arm_global_pd (arch_state s) \<notin> untyped_range cap \<and> (\<forall>p\<in>set (arm_global_pts (arch_state s)). p \<notin> untyped_range cap) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> untyped_range cap
 2. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao (detype (untyped_range cap) s)
 3. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> untyped_range cap
 4. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (arm_global_pts (arch_state s)). p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao (detype (untyped_range cap) s)
 2. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> untyped_range cap
 3. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (arm_global_pts (arch_state s)). p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at x (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj x s\<rbrakk> \<Longrightarrow> ako_at x (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj x (detype (untyped_range cap) s)
 2. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> untyped_range cap
 3. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (arm_global_pts (arch_state s)). p \<notin> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at x (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj x s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s\<rbrakk> \<Longrightarrow> ako_at x (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj x (detype (untyped_range cap) s)
 2. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> untyped_range cap
 3. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (arm_global_pts (arch_state s)). p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x)); ako_at x_ (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj x_ s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s\<rbrakk> \<Longrightarrow> ako_at x_ (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj x_ (detype (untyped_range cap) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<notin> untyped_range cap
 2. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (arm_global_pts (arch_state s)). p \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. r \<in> global_refs s \<Longrightarrow> r \<notin> cap_range cap; \<exists>ao. ako_at ao (arm_global_pd (arch_state s)) s \<and> valid_vspace_obj ao s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (arm_global_pts (arch_state s)). p \<notin> untyped_range cap proof (prove)
goal:
No subgoals!