theory Finalise_DR

lemma and_mask_plus:
  "\<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^m\<rbrakk>
   \<Longrightarrow> (ptr::word32) + a && mask n = (ptr && 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 && mask n) && ~~ mask m
     = (ptr + a && ~~ mask m ) && 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; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> ptr + a && mask n = (ptr && mask n) + a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && mask m = (ptr && mask n) + a && mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> ptr + a && mask m = (ptr && mask n) + a && mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = (ptr && mask n) + a && mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask n) m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 4. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> m \<le> n
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 4. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 3. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m; (ptr + a && mask n) && ~~ mask m = (ptr + a && ~~ mask m) && mask n\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr && mask n) + a && ~~ mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr + a && ~~ mask m) && mask n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m; (ptr + a && mask n) && ~~ mask m = ptr && mask n\<rbrakk> \<Longrightarrow> ptr && mask n = (ptr && mask n) + a && ~~ mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr + a && ~~ mask m) && mask n proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m; (ptr + a && mask n) && ~~ mask m = ptr && mask n\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask n) m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m; (ptr + a && mask n) && ~~ mask m = ptr && mask n\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m; (ptr + a && mask n) && ~~ mask m = ptr && mask n\<rbrakk> \<Longrightarrow> ptr && mask n = ptr && mask n
 4. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr + a && ~~ mask m) && mask n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m; (ptr + a && mask n) && ~~ mask m = ptr && mask n\<rbrakk> \<Longrightarrow> a < 2 ^ m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m; (ptr + a && mask n) && ~~ mask m = ptr && mask n\<rbrakk> \<Longrightarrow> ptr && mask n = ptr && mask n
 3. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr + a && ~~ mask m) && mask n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m; (ptr + a && mask n) && ~~ mask m = ptr && mask n\<rbrakk> \<Longrightarrow> ptr && mask n = ptr && mask n
 2. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr + a && ~~ mask m) && mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a && mask n) && ~~ mask m = (ptr + a && ~~ mask m) && mask n proof (prove)
goal:
No subgoals!