theory Retype_R

lemma pspace_no_overlap_disjoint':
  "\<lbrakk>pspace_aligned' s;pspace_no_overlap' x n s\<rbrakk>
   \<Longrightarrow> {x .. (x && ~~ mask n) + 2 ^ n  - 1} \<inter> dom (ksPSpace s) = {}" unfolding pspace_no_overlap'_def apply (rule disjointI) apply (rule ccontr) apply clarsimp apply (elim allE impE notE) apply (simp add:field_simps)+ apply (erule(2) order_trans[OF _ is_aligned_no_overflow,OF _ pspace_alignedD']) apply (erule(1) is_aligned_no_overflow[OF pspace_alignedD']) apply (erule order_trans) apply (simp add:p_assoc_help) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_no_overlap' x n s\<rbrakk> \<Longrightarrow> {x..(x && ~~ mask n) + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; \<forall>xa ko. ksPSpace s xa = Some ko \<longrightarrow> {xa..xa + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area x n = {}\<rbrakk> \<Longrightarrow> {x..(x && ~~ mask n) + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>pspace_aligned' s; \<forall>xa ko. ksPSpace s xa = Some ko \<longrightarrow> {xa..xa + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area x n = {}; xa \<in> {x..(x && ~~ mask n) + 2 ^ n - 1}; y \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> xa \<noteq> y proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>pspace_aligned' s; \<forall>xa ko. ksPSpace s xa = Some ko \<longrightarrow> {xa..xa + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area x n = {}; xa \<in> {x..(x && ~~ mask n) + 2 ^ n - 1}; y \<in> dom (ksPSpace s); \<not> xa \<noteq> y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>pspace_aligned' s; \<forall>xa ko. ksPSpace s xa = Some ko \<longrightarrow> xa \<le> (x && ~~ mask n) + (2 ^ n - 1) \<longrightarrow> x \<le> xa + 2 ^ objBitsKO ko - 1 \<longrightarrow> xa \<le> xa + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> x \<le> (x && ~~ mask n) + (2 ^ n - 1); ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ksPSpace s (?x12 y ya) = Some (?ko13 y ya)
 2. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ?x12 y ya \<le> (x && ~~ mask n) + (2 ^ n - 1)
 3. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> x \<le> ?x12 y ya + 2 ^ objBitsKO (?ko13 y ya) - 1
 4. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ?x12 y ya \<le> ?x12 y ya + 2 ^ objBitsKO (?ko13 y ya) - 1
 5. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> x \<le> (x && ~~ mask n) + (2 ^ n - 1) proof (prove)
goal (3 subgoals):
 1. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> x \<le> y + 2 ^ objBitsKO ya - 1
 2. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> y \<le> y + 2 ^ objBitsKO ya - 1
 3. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> x \<le> (x && ~~ mask n) + (2 ^ n - 1) proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> y \<le> y + 2 ^ objBitsKO ya - 1
 2. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> x \<le> (x && ~~ mask n) + (2 ^ n - 1) proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; x \<le> y; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> x \<le> (x && ~~ mask n) + (2 ^ n - 1) proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>pspace_aligned' s; ksPSpace s y = Some ya; y \<le> (x && ~~ mask n) + 2 ^ n - 1\<rbrakk> \<Longrightarrow> y \<le> (x && ~~ mask n) + (2 ^ n - 1) proof (prove)
goal:
No subgoals!