theory More_Word_Operations

lemma neg_mask_in_mask_range:
  "is_aligned ptr bits \<Longrightarrow> (ptr' AND NOT(mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)" apply (erule is_aligned_get_word_bits) apply (rule iffI) apply (drule sym) apply (simp add: word_and_le2) apply (subst word_plus_and_or_coroll, word_eqI_solve) apply (metis bit.disj_ac(2) bit.disj_conj_distrib2 le_word_or2 word_and_max word_or_not) apply clarsimp apply (smt add.right_neutral eq_iff is_aligned_neg_mask_eq mask_out_add_aligned neg_mask_mono_le
              word_and_not) apply (simp add: power_overflow mask_eq_decr_exp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr bits \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a)\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits)
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' AND NOT (mask bits) = ptr\<rbrakk> \<Longrightarrow> ptr' \<in> mask_range ptr bits
 2. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 3. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr = ptr' AND NOT (mask bits)\<rbrakk> \<Longrightarrow> ptr' \<in> mask_range ptr bits
 2. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 3. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bits < LENGTH('a); ptr = ptr' AND NOT (mask bits)\<rbrakk> \<Longrightarrow> ptr' \<le> (ptr' AND NOT (mask bits)) + mask bits
 2. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 3. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bits < LENGTH('a); ptr = ptr' AND NOT (mask bits)\<rbrakk> \<Longrightarrow> ptr' \<le> ptr' AND NOT (mask bits) OR mask bits
 2. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 3. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr' \<in> mask_range ptr bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a); ptr \<le> ptr'; ptr' \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr' AND NOT (mask bits) = ptr
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr = 0; LENGTH('a) \<le> bits\<rbrakk> \<Longrightarrow> (ptr' AND NOT (mask bits) = ptr) = (ptr' \<in> mask_range ptr bits) proof (prove)
goal:
No subgoals!