theory ArchVSpace_AI

lemma vs_lookup_pages_eq_ap:
  "[VSRef b (Some AASIDPool), VSRef a None] \<rhd> pd =
   [VSRef b (Some AASIDPool), 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 rtranclE) apply (clarsimp simp: vs_asid_refs_def graph_of_def image_def) apply (rule converse_rtrancl_into_rtrancl[OF _ rtrancl_refl]) apply (fastforce simp: vs_refs_pages_def graph_of_def image_def
                          vs_lookup_pages1_def) 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) apply (erule rtranclE) apply (clarsimp simp: vs_asid_refs_def graph_of_def image_def) apply (rule converse_rtrancl_into_rtrancl[OF _ rtrancl_refl]) apply (fastforce simp: vs_refs_def graph_of_def image_def
                         vs_lookup1_def) 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 b (Some AASIDPool), VSRef a None] \<rhd> pd = [VSRef b (Some AASIDPool), VSRef a None] \<unrhd> pd proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>*) = (\<lambda>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), 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 b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>*) = (\<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), 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 b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), 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 b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), 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 b (Some AASIDPool), VSRef a None], pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba p x1 aaa. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ((aa, ba), [VSRef a None], p) \<in> (vs_lookup1 s)\<^sup>*; ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>s aa ba p x1 aaa. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; (aa, ba) = ([VSRef a None], p)\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s aa ba p x1 aaa y. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; ((aa, ba), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef a None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>s ba x1 aa ab. \<lbrakk>ako_at (ASIDPool x1) ba s; x1 aa = Some pd; b = UCAST(10 \<rightarrow> 32) aa; asid_table s ab = Some ba; a = UCAST(7 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s aa ba p x1 aaa y. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; ((aa, ba), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef a None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>s ba x1 aa ab. \<lbrakk>ako_at (ASIDPool x1) ba s; x1 aa = Some pd; b = UCAST(10 \<rightarrow> 32) aa; asid_table s ab = Some ba; a = UCAST(7 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], pd) \<in> vs_lookup_pages1 s
 2. \<And>s aa ba p x1 aaa y. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; ((aa, ba), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef a None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 3. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba p x1 aaa y. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; ((aa, ba), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef a None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*
 2. \<And>s. \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), 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 b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>* \<Longrightarrow> \<exists>x\<in>vs_asid_refs (asid_table s). (x, [VSRef b (Some AASIDPool), 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 b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, [VSRef b (Some AASIDPool), 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 b (Some AASIDPool), VSRef a None], pd) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> (x, [VSRef b (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba p x1 aaa. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ((aa, ba), [VSRef a None], p) \<in> (vs_lookup_pages1 s)\<^sup>*; ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba p x1 aaa. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; (aa, ba) = ([VSRef a None], p)\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>s aa ba p x1 aaa y. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; ((aa, ba), y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, [VSRef a None], p) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s ba x1 aa ab. \<lbrakk>ako_at (ASIDPool x1) ba s; x1 aa = Some pd; b = UCAST(10 \<rightarrow> 32) aa; asid_table s ab = Some ba; a = UCAST(7 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], pd) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>s aa ba p x1 aaa y. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; ((aa, ba), y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, [VSRef a None], p) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>s ba x1 aa ab. \<lbrakk>ako_at (ASIDPool x1) ba s; x1 aa = Some pd; b = UCAST(10 \<rightarrow> 32) aa; asid_table s ab = Some ba; a = UCAST(7 \<rightarrow> 32) ab\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], ba), [VSRef (UCAST(10 \<rightarrow> 32) aa) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) ab) None], pd) \<in> vs_lookup1 s
 2. \<And>s aa ba p x1 aaa y. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; ((aa, ba), y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, [VSRef a None], p) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba p x1 aaa y. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (ASIDPool x1) p s; x1 aaa = Some pd; b = UCAST(10 \<rightarrow> 32) aaa; ((aa, ba), y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, [VSRef a None], p) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> ((aa, ba), [VSRef (UCAST(10 \<rightarrow> 32) aaa) (Some AASIDPool), VSRef a None], pd) \<in> (vs_lookup1 s)\<^sup>* proof (prove)
goal:
No subgoals!