theory Detype_R

lemma not_in_new_cap_addrs:
  "\<lbrakk>is_aligned ptr (objBitsKO obj + us);
    objBitsKO obj + us < word_bits;
    pspace_no_overlap' ptr (objBitsKO obj + us) s;
    ksPSpace s dest = Some ko;pspace_aligned' s\<rbrakk>
   \<Longrightarrow> dest \<notin> set (new_cap_addrs (2 ^ us) ptr obj)" supply
    is_aligned_neg_mask_eq[simp del]
    is_aligned_neg_mask_weaken[simp del] apply (rule ccontr) apply simp apply (drule(1) pspace_no_overlapD'[rotated]) apply (erule_tac x = dest in in_empty_interE) apply (clarsimp) apply (erule(1) is_aligned_no_overflow[OF pspace_alignedD']) apply (erule subsetD[rotated]) apply (simp add:p_assoc_help) apply (rule new_cap_addrs_subset[unfolded ptr_add_def,simplified]) apply (rule range_cover_rel[OF range_cover_full]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> dest \<notin> set (new_cap_addrs (2 ^ us) ptr obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> dest \<notin> set (new_cap_addrs (2 ^ us) ptr obj) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; ksPSpace s dest = Some ko; pspace_aligned' s; \<not> dest \<notin> set (new_cap_addrs (2 ^ us) ptr obj)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; ksPSpace s dest = Some ko; pspace_aligned' s; dest \<in> set (new_cap_addrs (2 ^ us) ptr obj)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s; dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); {dest..dest + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask (objBitsKO obj + us)) + 2 ^ (objBitsKO obj + us) - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s; dest \<in> set (new_cap_addrs (2 ^ us) ptr obj)\<rbrakk> \<Longrightarrow> dest \<in> {dest..dest + 2 ^ objBitsKO ko - 1}
 2. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s; dest \<in> set (new_cap_addrs (2 ^ us) ptr obj)\<rbrakk> \<Longrightarrow> dest \<in> {ptr..(ptr && ~~ mask (objBitsKO obj + us)) + 2 ^ (objBitsKO obj + us) - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s; dest \<in> set (new_cap_addrs (2 ^ us) ptr obj)\<rbrakk> \<Longrightarrow> dest \<le> dest + 2 ^ objBitsKO ko - 1
 2. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s; dest \<in> set (new_cap_addrs (2 ^ us) ptr obj)\<rbrakk> \<Longrightarrow> dest \<in> {ptr..(ptr && ~~ mask (objBitsKO obj + us)) + 2 ^ (objBitsKO obj + us) - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s; dest \<in> set (new_cap_addrs (2 ^ us) ptr obj)\<rbrakk> \<Longrightarrow> dest \<in> {ptr..(ptr && ~~ mask (objBitsKO obj + us)) + 2 ^ (objBitsKO obj + us) - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) ptr obj) \<subseteq> {ptr..(ptr && ~~ mask (objBitsKO obj + us)) + 2 ^ (objBitsKO obj + us) - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) ptr obj) \<subseteq> up_aligned_area ptr (objBitsKO obj + us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> range_cover ptr (objBitsKO obj + us) (objBitsKO obj) (2 ^ us) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> is_aligned ptr (objBitsKO obj + us)
 2. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> objBitsKO obj + us < word_bits
 3. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> objBitsKO obj \<le> objBitsKO obj + us
 4. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; ksPSpace s dest = Some ko; pspace_aligned' s\<rbrakk> \<Longrightarrow> 2 ^ us = 2 ^ (objBitsKO obj + us - objBitsKO obj) * Suc 0 proof (prove)
goal:
No subgoals!