theory ArchVSpace_AI

lemma vs_lookup_pages_eq_at:
  "[VSRef a None] \<rhd> pd = [VSRef a None] \<unrhd> pd" apply (simp add: vs_lookup_pages_def vs_lookup_def Image_def) apply (rule ext) apply (rule iffI) apply (erule bexEI) apply (erule rtranclE, simp) apply (clarsimp simp: vs_refs_def graph_of_def image_def
                  dest!: vs_lookup1D
                  split: Structures_A.kernel_object.splits
                         arch_kernel_obj.splits) apply (erule bexEI) apply (erule rtranclE, simp) apply (clarsimp simp: vs_refs_pages_def graph_of_def image_def
                 dest!: vs_lookup_pages1D
                 split: Structures_A.kernel_object.splits
                        arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [VSRef a None] \<rhd> pd = [VSRef a None] \<unrhd> pd proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>*) = (\<lambda>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>*) = (\<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>x \<in> vs_asid_refs (asid_table s); (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s x y. \<lbrakk>x \<in> vs_asid_refs (asid_table s); (x, y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef a None], pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>x \<in> vs_asid_refs (asid_table s); (x, [VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>x \<in> vs_asid_refs (asid_table s); (x, y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, [VSRef a None], pd) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> (x, [VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal:
No subgoals!