theory ArchInvariants_AI

lemma valid_vspace_objs_stateI:
  assumes 1: "valid_vspace_objs s"
  assumes ko: "\<And>ko p. ko_at ko p s' \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s"
  assumes arch: "graph_of (arm_asid_table (arch_state s')) \<subseteq> graph_of (arm_asid_table (arch_state s))"
  assumes vao: "\<And>p ref ao'.
                \<lbrakk> (ref \<rhd> p) s; (ref \<rhd> p) s'; \<forall>ao. ko_at (ArchObj ao) p s \<longrightarrow> valid_vspace_obj ao s;
                  ko_at (ArchObj ao') p s' \<rbrakk> \<Longrightarrow> valid_vspace_obj ao' s'"
  shows "valid_vspace_objs s'" using 1 unfolding valid_vspace_objs_def apply clarsimp apply (frule vs_lookup_stateI) apply (erule ko) apply (rule arch) apply (erule allE, erule impE, fastforce) apply (erule (3) vao) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs s' proof (prove)
using this:
valid_vspace_objs s

goal (1 subgoal):
 1. valid_vspace_objs s' proof (prove)
using this:
\<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ako_at ao p s \<longrightarrow> valid_vspace_obj ao s

goal (1 subgoal):
 1. \<forall>p rs ao. (rs \<rhd> p) s' \<longrightarrow> ako_at ao p s' \<longrightarrow> valid_vspace_obj ao s' proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (rs \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
goal (3 subgoals):
 1. \<And>p rs ao ko pa. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (rs \<rhd> p) s'; ako_at ao p s'; ko_at ko pa s'\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') pa (?s'10 p rs ao)
 2. \<And>p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (rs \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> graph_of (asid_table s') \<subseteq> graph_of (asid_table (?s'10 p rs ao))
 3. \<And>p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (rs \<rhd> p) s'; ako_at ao p s'; (rs \<rhd> p) (?s'10 p rs ao)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
goal (2 subgoals):
 1. \<And>p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (rs \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> graph_of (asid_table s') \<subseteq> graph_of (asid_table s)
 2. \<And>p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (rs \<rhd> p) s'; ako_at ao p s'; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (rs \<rhd> p) s'; ako_at ao p s'; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao. \<lbrakk>(rs \<rhd> p) s'; ako_at ao p s'; (rs \<rhd> p) s; \<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
goal:
No subgoals!