theory ArchAcc_AI

lemma valid_vspace_objs_arch_update:
  "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) \<Longrightarrow>
  valid_vspace_objs (arch_state_update f s) = valid_vspace_objs s" apply (rule iffI) apply (erule valid_vspace_objs_stateI) apply (clarsimp simp: obj_at_def) apply simp apply simp apply (erule valid_vspace_objs_stateI) apply (clarsimp simp: obj_at_def) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> valid_vspace_objs (arch_state_update f s) = valid_vspace_objs s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; valid_vspace_objs (arch_state_update f s)\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> valid_vspace_objs (arch_state_update f s) proof (prove)
goal (4 subgoals):
 1. \<And>ko p. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; ko_at ko p s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p (arch_state_update f s)
 2. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (arch_state_update f s))
 3. \<And>p ref ao'. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; (ref \<rhd> p) (arch_state_update f s); (ref \<rhd> p) s; \<forall>ao. ako_at ao p (arch_state_update f s) \<longrightarrow> valid_vspace_obj ao (arch_state_update f s); ako_at ao' p s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao' s
 4. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> valid_vspace_objs (arch_state_update f s) proof (prove)
goal (3 subgoals):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (arch_state_update f s))
 2. \<And>p ref ao'. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; (ref \<rhd> p) (arch_state_update f s); (ref \<rhd> p) s; \<forall>ao. ako_at ao p (arch_state_update f s) \<longrightarrow> valid_vspace_obj ao (arch_state_update f s); ako_at ao' p s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao' s
 3. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> valid_vspace_objs (arch_state_update f s) proof (prove)
goal (2 subgoals):
 1. \<And>p ref ao'. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; (ref \<rhd> p) (arch_state_update f s); (ref \<rhd> p) s; \<forall>ao. ako_at ao p (arch_state_update f s) \<longrightarrow> valid_vspace_obj ao (arch_state_update f s); ako_at ao' p s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao' s
 2. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> valid_vspace_objs (arch_state_update f s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> valid_vspace_objs (arch_state_update f s) proof (prove)
goal (3 subgoals):
 1. \<And>ko p. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; ko_at ko p (arch_state_update f s)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s
 2. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> graph_of (asid_table (arch_state_update f s)) \<subseteq> graph_of (asid_table s)
 3. \<And>p ref ao'. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; (ref \<rhd> p) s; (ref \<rhd> p) (arch_state_update f s); \<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s; ako_at ao' p (arch_state_update f s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao' (arch_state_update f s) proof (prove)
goal (2 subgoals):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> graph_of (asid_table (arch_state_update f s)) \<subseteq> graph_of (asid_table s)
 2. \<And>p ref ao'. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; (ref \<rhd> p) s; (ref \<rhd> p) (arch_state_update f s); \<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s; ako_at ao' p (arch_state_update f s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao' (arch_state_update f s) proof (prove)
goal (1 subgoal):
 1. \<And>p ref ao'. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; (ref \<rhd> p) s; (ref \<rhd> p) (arch_state_update f s); \<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s; ako_at ao' p (arch_state_update f s)\<rbrakk> \<Longrightarrow> valid_vspace_obj ao' (arch_state_update f s) proof (prove)
goal:
No subgoals!