theory TcbAcc_R

lemma pspace_dom_dom:
  "dom ps \<subseteq> pspace_dom ps" unfolding pspace_dom_def apply clarsimp apply (rule rev_bexI [OF domI], assumption) apply (simp add: obj_relation_cuts_def2 image_Collect cte_map_def range_composition [symmetric]
    split: Structures_A.kernel_object.splits arch_kernel_obj.splits cong: arch_kernel_obj.case_cong) apply safe apply (drule wf_cs_0) apply clarsimp apply (rule_tac x = n in exI) apply (clarsimp simp: of_bl_def) apply (rule range_eqI [where x = 0], simp)+ apply (rename_tac vmpage_size) apply (rule exI [where x = 0]) apply (case_tac vmpage_size, simp_all add: pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom ps \<subseteq> pspace_dom ps proof (prove)
goal (1 subgoal):
 1. dom ps \<subseteq> (\<Union>x\<in>dom ps. fst ` obj_relation_cuts (the (ps x)) x) proof (prove)
goal (1 subgoal):
 1. \<And>x y. ps x = Some y \<Longrightarrow> \<exists>xa\<in>dom ps. x \<in> fst ` obj_relation_cuts (the (ps xa)) xa proof (prove)
goal (1 subgoal):
 1. \<And>x y. ps x = Some y \<Longrightarrow> x \<in> fst ` obj_relation_cuts (the (ps x)) x proof (prove)
goal (1 subgoal):
 1. \<And>x y. ps x = Some y \<Longrightarrow> (\<forall>x11 x12. well_formed_cnode_n x11 x12 \<longrightarrow> y = CNode x11 x12 \<longrightarrow> (\<exists>y. of_bl y * 2 ^ cte_level_bits = 0 \<and> y \<in> dom x12)) \<and> (\<forall>x5. (\<forall>x2. x5 = PageTable x2 \<longrightarrow> y = ArchObj (PageTable x2) \<longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(8 \<rightarrow> 32) xa << 2))) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> y = ArchObj (PageDirectory x3) \<longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(12 \<rightarrow> 32) xa << 2))) \<and> (\<forall>x41 x42. x5 = DataPage x41 x42 \<longrightarrow> y = ArchObj (DataPage x41 x42) \<longrightarrow> (\<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (pageBitsForSize x42 - pageBits)))) proof (prove)
goal (4 subgoals):
 1. \<And>x y x11 x12. \<lbrakk>ps x = Some (CNode x11 x12); well_formed_cnode_n x11 x12\<rbrakk> \<Longrightarrow> \<exists>y. of_bl y * 2 ^ cte_level_bits = 0 \<and> y \<in> dom x12
 2. \<And>x y x5 x2. ps x = Some (ArchObj (PageTable x2)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(8 \<rightarrow> 32) xa << 2))
 3. \<And>x y x5 x3. ps x = Some (ArchObj (PageDirectory x3)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(12 \<rightarrow> 32) xa << 2))
 4. \<And>x y x5 x41 x42. ps x = Some (ArchObj (DataPage x41 x42)) \<Longrightarrow> \<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (pageBitsForSize x42 - pageBits) proof (prove)
goal (4 subgoals):
 1. \<And>x y x11 x12. \<lbrakk>ps x = Some (CNode x11 x12); \<exists>n. n \<in> dom x12 \<and> bl_to_bin n = 0\<rbrakk> \<Longrightarrow> \<exists>y. of_bl y * 2 ^ cte_level_bits = 0 \<and> y \<in> dom x12
 2. \<And>x y x5 x2. ps x = Some (ArchObj (PageTable x2)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(8 \<rightarrow> 32) xa << 2))
 3. \<And>x y x5 x3. ps x = Some (ArchObj (PageDirectory x3)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(12 \<rightarrow> 32) xa << 2))
 4. \<And>x y x5 x41 x42. ps x = Some (ArchObj (DataPage x41 x42)) \<Longrightarrow> \<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (pageBitsForSize x42 - pageBits) proof (prove)
goal (4 subgoals):
 1. \<And>x x11 x12 n y. \<lbrakk>ps x = Some (CNode x11 x12); bl_to_bin n = 0; x12 n = Some y\<rbrakk> \<Longrightarrow> \<exists>y. of_bl y * 2 ^ cte_level_bits = 0 \<and> y \<in> dom x12
 2. \<And>x y x5 x2. ps x = Some (ArchObj (PageTable x2)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(8 \<rightarrow> 32) xa << 2))
 3. \<And>x y x5 x3. ps x = Some (ArchObj (PageDirectory x3)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(12 \<rightarrow> 32) xa << 2))
 4. \<And>x y x5 x41 x42. ps x = Some (ArchObj (DataPage x41 x42)) \<Longrightarrow> \<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (pageBitsForSize x42 - pageBits) proof (prove)
goal (4 subgoals):
 1. \<And>x x11 x12 n y. \<lbrakk>ps x = Some (CNode x11 x12); bl_to_bin n = 0; x12 n = Some y\<rbrakk> \<Longrightarrow> of_bl n * 2 ^ cte_level_bits = 0 \<and> n \<in> dom x12
 2. \<And>x y x5 x2. ps x = Some (ArchObj (PageTable x2)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(8 \<rightarrow> 32) xa << 2))
 3. \<And>x y x5 x3. ps x = Some (ArchObj (PageDirectory x3)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(12 \<rightarrow> 32) xa << 2))
 4. \<And>x y x5 x41 x42. ps x = Some (ArchObj (DataPage x41 x42)) \<Longrightarrow> \<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (pageBitsForSize x42 - pageBits) proof (prove)
goal (3 subgoals):
 1. \<And>x y x5 x2. ps x = Some (ArchObj (PageTable x2)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(8 \<rightarrow> 32) xa << 2))
 2. \<And>x y x5 x3. ps x = Some (ArchObj (PageDirectory x3)) \<Longrightarrow> x \<in> range (\<lambda>xa. x + (UCAST(12 \<rightarrow> 32) xa << 2))
 3. \<And>x y x5 x41 x42. ps x = Some (ArchObj (DataPage x41 x42)) \<Longrightarrow> \<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (pageBitsForSize x42 - pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x y x5 x41 x42. ps x = Some (ArchObj (DataPage x41 x42)) \<Longrightarrow> \<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (pageBitsForSize x42 - pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x y x5 x41 vmpage_size. ps x = Some (ArchObj (DataPage x41 vmpage_size)) \<Longrightarrow> \<exists>n. n * 2 ^ pageBits = 0 \<and> n < 2 ^ (pageBitsForSize vmpage_size - pageBits) proof (prove)
goal (1 subgoal):
 1. \<And>x y x5 x41 vmpage_size. ps x = Some (ArchObj (DataPage x41 vmpage_size)) \<Longrightarrow> 0 * 2 ^ pageBits = 0 \<and> 0 < 2 ^ (pageBitsForSize vmpage_size - pageBits) proof (prove)
goal:
No subgoals!