theory Aligned

lemma and_mask_plus:
  "\<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk>
   \<Longrightarrow> ptr + a AND mask n = (ptr AND mask n) + a" apply (rule mask_eqI[where n = m]) apply (simp add:mask_twice min_def) apply (simp add:is_aligned_add_helper) apply (subst is_aligned_add_helper[THEN conjunct1]) apply (erule is_aligned_after_mask) apply simp apply simp apply simp apply (subgoal_tac "(ptr + a AND mask n) AND NOT (mask m)
     = (ptr + a AND NOT (mask m) ) AND mask n") apply (simp add:is_aligned_add_helper) apply (subst is_aligned_add_helper[THEN conjunct2]) apply (simp add:is_aligned_after_mask) apply simp apply simp apply (simp add:word_bw_comms word_bw_lcs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> ptr + a AND mask n = (ptr AND mask n) + a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND mask m = (ptr AND mask n) + a AND mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> ptr + a AND mask m = (ptr AND mask n) + a AND mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = (ptr AND mask n) + a AND mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> is_aligned (ptr AND mask n) m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 4. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> m \<le> n
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 4. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> ptr AND mask n = (ptr AND mask n) + a AND NOT (mask m)
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> is_aligned (ptr AND mask n) m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> ptr AND mask n = ptr AND mask n
 4. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> a < 2 ^ m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> ptr AND mask n = ptr AND mask n
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> ptr AND mask n = ptr AND mask n
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n proof (prove)
goal:
No subgoals!