theory Detype_R

lemma obj_relation_cuts_eqv_base_in_detype_range:
  "\<lbrakk> (y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko;
      valid_objs s; pspace_aligned s;
      valid_untyped (cap.UntypedCap d base bits idx) s \<rbrakk>
    \<Longrightarrow> (x \<in> {base .. base + 2 ^ bits - 1}) = (y \<in> {base .. base + 2 ^ bits - 1})" apply (simp add: valid_untyped_def del: atLeastAtMost_iff) apply (subgoal_tac "x \<in> obj_range x ko") apply (subgoal_tac "y \<in> obj_range x ko") apply blast apply (erule(4) obj_relation_cuts_in_obj_range) apply (simp add: obj_range_def) apply (rule is_aligned_no_overflow) apply (erule(1) pspace_alignedD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; valid_untyped (cap.UntypedCap d base bits idx) s\<rbrakk> \<Longrightarrow> (x \<in> {base..base + 2 ^ bits - 1}) = (y \<in> {base..base + 2 ^ bits - 1}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> (x \<in> {base..base + 2 ^ bits - 1}) = (y \<in> {base..base + 2 ^ bits - 1}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}; x \<in> obj_range x ko\<rbrakk> \<Longrightarrow> (x \<in> {base..base + 2 ^ bits - 1}) = (y \<in> {base..base + 2 ^ bits - 1})
 2. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> x \<in> obj_range x ko proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}; x \<in> obj_range x ko; y \<in> obj_range x ko\<rbrakk> \<Longrightarrow> (x \<in> {base..base + 2 ^ bits - 1}) = (y \<in> {base..base + 2 ^ bits - 1})
 2. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}; x \<in> obj_range x ko\<rbrakk> \<Longrightarrow> y \<in> obj_range x ko
 3. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> x \<in> obj_range x ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}; x \<in> obj_range x ko\<rbrakk> \<Longrightarrow> y \<in> obj_range x ko
 2. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> x \<in> obj_range x ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {base..base + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {base..base + 2 ^ bits - 1} \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> x \<in> obj_range x ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> p \<le> base + 2 ^ bits - 1 \<and> base \<le> p + 2 ^ obj_bits obj - 1 \<and> p \<le> p + 2 ^ obj_bits obj - 1 \<and> base \<le> base + 2 ^ bits - 1 \<longrightarrow> base \<le> p \<and> p + 2 ^ obj_bits obj - 1 \<le> base + 2 ^ bits - 1 \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> {p..p + 2 ^ obj_bits obj - 1} = {}\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ obj_bits ko - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; \<forall>p obj. kheap s p = Some obj \<longrightarrow> p \<le> base + 2 ^ bits - 1 \<and> base \<le> p + 2 ^ obj_bits obj - 1 \<and> p \<le> p + 2 ^ obj_bits obj - 1 \<and> base \<le> base + 2 ^ bits - 1 \<longrightarrow> base \<le> p \<and> p + 2 ^ obj_bits obj - 1 \<le> base + 2 ^ bits - 1 \<and> (if idx < 2 ^ bits then {base + word_of_nat idx..base + 2 ^ bits - 1} else {}) \<inter> {p..p + 2 ^ obj_bits obj - 1} = {}\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits ko) proof (prove)
goal:
No subgoals!