theory ArchInvariants_AI

lemma vs_lookup_pages_vs_lookupI: "(ref \<rhd> p) s \<Longrightarrow> (ref \<unrhd> p) s" apply (clarsimp simp: vs_lookup_pages_def vs_lookup_def Image_def
                 elim!: bexEI) apply (erule rtrancl.induct, simp_all) apply (rename_tac a b c) apply (subgoal_tac "(b \<unrhd>1 c) s", erule (1) rtrancl_into_rtrancl) apply (thin_tac "x : rtrancl r" for x r)+ apply (simp add: vs_lookup1_def vs_lookup_pages1_def split_def) apply (erule exEI) apply clarsimp apply (case_tac x, simp_all add: vs_refs_def vs_refs_pages_def
                            split: arch_kernel_obj.splits) apply (clarsimp simp: split_def graph_of_def image_def  split: if_split_asm) apply (intro exI conjI impI, assumption) apply (simp add: pde_ref_def pde_ref_pages_def
             split: pde.splits) apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ref \<rhd> p) s \<Longrightarrow> (ref \<unrhd> p) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); ((a, b), ref, p) \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> ((a, b), ref, p) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba c. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); (aa, ba) \<in> (vs_lookup1 s)\<^sup>*; (aa, ba) \<in> (vs_lookup_pages1 s)\<^sup>*; (ba, c) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (aa, c) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>aa ba a b c. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); (a, b) \<in> (vs_lookup1 s)\<^sup>*; (a, b) \<in> (vs_lookup_pages1 s)\<^sup>*; (b, c) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (a, c) \<in> (vs_lookup_pages1 s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>aa ba a b c. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); (a, b) \<in> (vs_lookup1 s)\<^sup>*; (a, b) \<in> (vs_lookup_pages1 s)\<^sup>*; (b, c) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (b, c) \<in> vs_lookup_pages1 s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba a b c. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); (b, c) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (b, c) \<in> vs_lookup_pages1 s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba b c. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); \<exists>ko. ko_at ko (snd b) s \<and> (\<exists>r. fst c = r # fst b \<and> (r, snd c) \<in> vs_refs ko)\<rbrakk> \<Longrightarrow> \<exists>ko. ko_at ko (snd b) s \<and> (\<exists>r. fst c = r # fst b \<and> (r, snd c) \<in> vs_refs_pages ko) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba b c x. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ko_at x (snd b) s \<and> (\<exists>r. fst c = r # fst b \<and> (r, snd c) \<in> vs_refs x)\<rbrakk> \<Longrightarrow> ko_at x (snd b) s \<and> (\<exists>r. fst c = r # fst b \<and> (r, snd c) \<in> vs_refs_pages x) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba b bb x r. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ko_at x b s; (r, bb) \<in> vs_refs x\<rbrakk> \<Longrightarrow> (r, bb) \<in> vs_refs_pages x proof (prove)
goal (1 subgoal):
 1. \<And>aa ba b bb x r x5 x3. \<lbrakk>x = ArchObj (PageDirectory x3); (aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (PageDirectory x3) b s; x5 = PageDirectory x3; (r, bb) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x))\<rbrakk> \<Longrightarrow> (r, bb) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba b bb x3 a. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (PageDirectory x3) b s; a \<notin> kernel_mapping_slots; pde_ref (x3 a) = Some bb\<rbrakk> \<Longrightarrow> \<exists>aa. aa \<notin> kernel_mapping_slots \<and> (aa \<notin> kernel_mapping_slots \<longrightarrow> pde_ref_pages (x3 aa) = Some bb \<and> UCAST(12 \<rightarrow> 32) a = UCAST(12 \<rightarrow> 32) aa) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba b bb x3 a. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (PageDirectory x3) b s; a \<notin> kernel_mapping_slots; pde_ref (x3 a) = Some bb; a \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> pde_ref_pages (x3 a) = Some bb
 2. \<And>aa ba b bb x3 a. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (PageDirectory x3) b s; a \<notin> kernel_mapping_slots; pde_ref (x3 a) = Some bb; a \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) a = UCAST(12 \<rightarrow> 32) a proof (prove)
goal (1 subgoal):
 1. \<And>aa ba b bb x3 a. \<lbrakk>(aa, ba) \<in> vs_asid_refs (asid_table s); ako_at (PageDirectory x3) b s; a \<notin> kernel_mapping_slots; pde_ref (x3 a) = Some bb; a \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) a = UCAST(12 \<rightarrow> 32) a proof (prove)
goal:
No subgoals!