theory More_Word_Operations

lemma aligned_mask_ranges_disjoint2:
  "\<lbrakk> is_aligned p n; is_aligned ptr bits; n \<ge> m; n < size p; m \<le> bits;
     (\<forall>y < 2 ^ (n - m). p + (y << m) \<notin> mask_range ptr bits) \<rbrakk>
   \<Longrightarrow> mask_range p n \<inter> mask_range ptr bits = {}" apply safe apply (simp only: flip: neg_mask_in_mask_range) apply (drule_tac x="x AND mask n >> m" in spec) apply (erule notE[OF mp]) apply (simp flip: take_bit_eq_mask add: shiftr_def drop_bit_take_bit) apply transfer apply simp apply (simp add: word_size and_mask_less_size) apply (subst disjunctive_add) apply (auto simp add: bit_simps word_size intro!: bit_eqI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; \<forall>y<2 ^ (n - m). p + (y << m) \<notin> mask_range ptr bits\<rbrakk> \<Longrightarrow> mask_range p n \<inter> mask_range ptr bits = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; \<forall>y<2 ^ (n - m). p + (y << m) \<notin> mask_range ptr bits; x \<in> mask_range p n; x \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> x \<in> {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; \<forall>y<2 ^ (n - m). p + (y << m) AND NOT (mask bits) \<noteq> ptr; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> x \<in> {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr; x AND mask n >> m < 2 ^ (n - m) \<longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) \<noteq> ptr\<rbrakk> \<Longrightarrow> x \<in> {} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> x AND mask n >> m < 2 ^ (n - m)
 2. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> take_bit (n - m) (drop_bit m x) < 2 ^ (n - m)
 2. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr proof (prove)
goal (2 subgoals):
 1. \<And>x p n ptr bits m. \<lbrakk>2 ^ n dvd take_bit LENGTH('a) p; 2 ^ bits dvd take_bit LENGTH('a) ptr; m \<le> n; n < LENGTH('a); m \<le> bits; take_bit LENGTH('a) (x AND NOT (mask n)) = take_bit LENGTH('a) p; take_bit LENGTH('a) (x AND NOT (mask bits)) = take_bit LENGTH('a) ptr\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) (take_bit (min LENGTH('a) (n - m)) ((drop_bit m \<circ> take_bit LENGTH('a)) x)) < take_bit LENGTH('a) (2 ^ (n - m))
 2. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < size p; m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < LENGTH('a); m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> p + (x AND mask n >> m << m) AND NOT (mask bits) = ptr proof (prove)
goal (2 subgoals):
 1. \<And>x na. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < LENGTH('a); m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> \<not> bit p na \<or> \<not> bit (x AND mask n >> m << m) na
 2. \<And>x. \<lbrakk>is_aligned p n; is_aligned ptr bits; m \<le> n; n < LENGTH('a); m \<le> bits; x AND NOT (mask n) = p; x AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> (p OR (x AND mask n >> m << m)) AND NOT (mask bits) = ptr proof (prove)
goal:
No subgoals!