theory More_Word_Operations

lemma aligned_offset_in_range:
  "\<lbrakk> is_aligned (x :: 'a :: len word) m; y < 2 ^ m; is_aligned p n; n \<ge> m; n < LENGTH('a) \<rbrakk>
   \<Longrightarrow> (x + y \<in> {p .. p + mask n}) = (x \<in> mask_range p n)" apply (subst disjunctive_add) apply (simp add: bit_simps) apply (erule is_alignedE') apply (auto simp add: bit_simps not_le)[1] apply (metis less_2p_is_upper_bits_unset) apply (simp only: is_aligned_add_or word_ao_dist flip: neg_mask_in_mask_range) apply (subgoal_tac \<open>y AND NOT (mask n) = 0\<close>) apply simp apply (metis (full_types) is_aligned_mask is_aligned_neg_mask less_mask_eq word_bw_comms(1) word_bw_lcs(1)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x + y \<in> mask_range p n) = (x \<in> mask_range p n) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> bit x na \<or> \<not> bit y na
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit x na \<longrightarrow> \<not> bit y na
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n) proof (prove)
goal (2 subgoals):
 1. \<And>na q. \<lbrakk>y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a); x = push_bit m (word_of_nat q); q < 2 ^ (LENGTH('a) - m)\<rbrakk> \<Longrightarrow> bit x na \<longrightarrow> \<not> bit y na
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n) proof (prove)
goal (2 subgoals):
 1. \<And>na q. \<lbrakk>y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a); x = push_bit m (word_of_nat q); q < 2 ^ (LENGTH('a) - m); m \<le> na; na < LENGTH('a); na - m < LENGTH('a); bit q (na - m); bit y na\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x OR y \<in> mask_range p n) = (x \<in> mask_range p n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x AND NOT (mask n) OR y AND NOT (mask n) = p) = (x AND NOT (mask n) = p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a); y AND NOT (mask n) = 0\<rbrakk> \<Longrightarrow> (x AND NOT (mask n) OR y AND NOT (mask n) = p) = (x AND NOT (mask n) = p)
 2. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> y AND NOT (mask n) = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x m; y < 2 ^ m; is_aligned p n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> y AND NOT (mask n) = 0 proof (prove)
goal:
No subgoals!