theory ArchVSpace_AI

lemma vs_lookup_typI:
  "\<lbrakk>(r \<rhd> p) s; valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s\<rbrakk>
   \<Longrightarrow> page_table_at p s
    \<or> page_directory_at p s
    \<or> asid_pool_at p s" apply (erule (1) vs_lookupE_alt) apply (clarsimp simp: ran_def) apply (drule (2) valid_asid_tableD) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(r \<rhd> p) s; valid_vspace_objs s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s
 2. \<And>a. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s
 3. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s proof (prove)
goal (4 subgoals):
 1. \<And>p a. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) p s
 2. \<And>a. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s
 3. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s
 4. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p; typ_at (AArch AASIDPool) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s
 2. \<And>a p\<^sub>1 ap b. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p; typ_at (AArch APageDirectory) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s
 3. \<And>a p\<^sub>1 ap b p\<^sub>2 pd c. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; asid_table s a = Some p\<^sub>1; kheap s p\<^sub>1 = Some (ArchObj (ASIDPool ap)); ap b = Some p\<^sub>2; kheap s p\<^sub>2 = Some (ArchObj (PageDirectory pd)); c \<notin> kernel_mapping_slots; pde_ref (pd c) = Some p; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) p s \<or> typ_at (AArch APageDirectory) p s \<or> typ_at (AArch AASIDPool) p s proof (prove)
goal:
No subgoals!