theory ArchRetype_AI

lemma valid_global_objs:
  "valid_global_objs s \<Longrightarrow> valid_global_objs s'" apply (simp add: valid_global_objs_def valid_vso_at_def) apply (elim conjE, intro conjI ballI) apply (erule exEI) apply (simp add: obj_at_pres valid_vspace_obj_pres) apply (simp add: obj_at_pres) apply (rule exEI, erule(1) bspec) apply (simp add: obj_at_pres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_objs s \<Longrightarrow> valid_global_objs s' proof (prove)
goal (1 subgoal):
 1. (\<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))) \<Longrightarrow> (\<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))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<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 s'
 2. \<lbrakk>\<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> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s'
 3. \<And>p. \<lbrakk>\<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)); p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p s' \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>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 s'
 2. \<lbrakk>\<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> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s'
 3. \<And>p. \<lbrakk>\<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)); p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p s' \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<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> obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s'
 2. \<And>p. \<lbrakk>\<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)); p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p s' \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<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)); p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p s' \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal (1 subgoal):
 1. \<And>p x. \<lbrakk>\<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)); p \<in> set (arm_global_pts (arch_state s)); ako_at (PageTable x) p s \<and> (\<forall>xa. aligned_pte (x xa))\<rbrakk> \<Longrightarrow> ako_at (PageTable x) p s' \<and> (\<forall>xa. aligned_pte (x xa)) proof (prove)
goal:
No subgoals!