theory Retype_R

lemma pspace_no_overlap_base':
  "\<lbrakk>pspace_aligned' s;pspace_no_overlap' x n s; is_aligned x n \<rbrakk> \<Longrightarrow> ksPSpace s x = None" apply (drule(1) pspace_no_overlap_disjoint') apply (drule equals0D[where a=x]) apply (rule ccontr, clarsimp) apply (erule is_aligned_get_word_bits) apply (erule impE) apply (frule mask_out_add_aligned[where q = 0,simplified,symmetric]) apply (fastforce simp add: is_aligned_no_overflow) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_no_overlap' x n s; is_aligned x n\<rbrakk> \<Longrightarrow> ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' x n s; is_aligned x n; {x..(x && ~~ mask n) + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' x n s; is_aligned x n; x \<notin> {x..(x && ~~ mask n) + 2 ^ n - 1} \<inter> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>pspace_no_overlap' x n s; is_aligned x n; x \<le> x + 2 ^ n - 1 \<longrightarrow> x \<notin> dom (ksPSpace s); ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>pspace_no_overlap' x n s; x \<le> x + 2 ^ n - 1 \<longrightarrow> x \<notin> dom (ksPSpace s); ksPSpace s x = Some y; is_aligned x n; n < LENGTH(32)\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>pspace_no_overlap' x n s; x \<le> x + 2 ^ n - 1 \<longrightarrow> x \<notin> dom (ksPSpace s); ksPSpace s x = Some y; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>pspace_no_overlap' x n s; ksPSpace s x = Some y; is_aligned x n; n < LENGTH(32)\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n - 1
 2. \<And>y. \<lbrakk>pspace_no_overlap' x n s; ksPSpace s x = Some y; is_aligned x n; n < LENGTH(32); x \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 3. \<And>y. \<lbrakk>pspace_no_overlap' x n s; x \<le> x + 2 ^ n - 1 \<longrightarrow> x \<notin> dom (ksPSpace s); ksPSpace s x = Some y; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>pspace_no_overlap' x n s; ksPSpace s x = Some y; is_aligned x n; n < LENGTH(32); x && ~~ mask n = x\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n - 1
 2. \<And>y. \<lbrakk>pspace_no_overlap' x n s; ksPSpace s x = Some y; is_aligned x n; n < LENGTH(32); x \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 3. \<And>y. \<lbrakk>pspace_no_overlap' x n s; x \<le> x + 2 ^ n - 1 \<longrightarrow> x \<notin> dom (ksPSpace s); ksPSpace s x = Some y; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>pspace_no_overlap' x n s; ksPSpace s x = Some y; is_aligned x n; n < LENGTH(32); x \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>pspace_no_overlap' x n s; x \<le> x + 2 ^ n - 1 \<longrightarrow> x \<notin> dom (ksPSpace s); ksPSpace s x = Some y; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!