theory ArchADT_AI

lemma VSRef_AASIDPool_in_vs_refs:
  "(VSRef (asid && mask asid_low_bits) (Some AASIDPool), r) \<in> vs_refs_arch ko =
   (\<exists>apool. ko = arch_kernel_obj.ASIDPool apool \<and>
            apool (ucast (asid && mask asid_low_bits)) = Some r)" apply simp apply (case_tac ko, simp_all add: image_def graph_of_def) apply (rename_tac arch_kernel_obj) apply (rule iffI) apply clarsimp apply (subst ucast_up_ucast_id, simp add: is_up, assumption) apply (intro exI conjI, assumption) apply (rule sym, rule ucast_ucast_len) apply (cut_tac and_mask_less'[of asid_low_bits asid]) apply (simp_all add: asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), r) \<in> vs_refs_arch ko) = (\<exists>apool. ko = ASIDPool apool \<and> apool (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r) proof (prove)
goal (1 subgoal):
 1. ((VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), r) \<in> (case ko of ASIDPool pool \<Rightarrow> (\<lambda>(r, p). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), p)) ` graph_of pool | PageDirectory pd \<Rightarrow> (\<lambda>(r, p). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), p)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | _ \<Rightarrow> {})) = (\<exists>apool. ko = ASIDPool apool \<and> apool (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r) proof (prove)
goal (1 subgoal):
 1. \<And>x1. ko = ASIDPool x1 \<Longrightarrow> (\<exists>a. x1 a = Some r \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a) = (x1 (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj. ko = ASIDPool arch_kernel_obj \<Longrightarrow> (\<exists>a. arch_kernel_obj a = Some r \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a) = (arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r) proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj. \<lbrakk>ko = ASIDPool arch_kernel_obj; \<exists>a. arch_kernel_obj a = Some r \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r
 2. \<And>arch_kernel_obj. \<lbrakk>ko = ASIDPool arch_kernel_obj; arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r\<rbrakk> \<Longrightarrow> \<exists>a. arch_kernel_obj a = Some r \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj a. \<lbrakk>ko = ASIDPool arch_kernel_obj; arch_kernel_obj a = Some r; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> arch_kernel_obj (UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) a)) = Some r
 2. \<And>arch_kernel_obj. \<lbrakk>ko = ASIDPool arch_kernel_obj; arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r\<rbrakk> \<Longrightarrow> \<exists>a. arch_kernel_obj a = Some r \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj. \<lbrakk>ko = ASIDPool arch_kernel_obj; arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r\<rbrakk> \<Longrightarrow> \<exists>a. arch_kernel_obj a = Some r \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj. \<lbrakk>ko = ASIDPool arch_kernel_obj; arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r\<rbrakk> \<Longrightarrow> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj. \<lbrakk>ko = ASIDPool arch_kernel_obj; arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r\<rbrakk> \<Longrightarrow> asid && mask local.asid_low_bits < 2 ^ LENGTH(10) proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_obj. \<lbrakk>ko = ASIDPool arch_kernel_obj; arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r; asid && mask local.asid_low_bits < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> asid && mask local.asid_low_bits < 2 ^ LENGTH(10)
 2. \<And>arch_kernel_obj. \<lbrakk>ko = ASIDPool arch_kernel_obj; arch_kernel_obj (UCAST(32 \<rightarrow> 10) (asid && mask local.asid_low_bits)) = Some r\<rbrakk> \<Longrightarrow> local.asid_low_bits < LENGTH(32) proof (prove)
goal:
No subgoals!