theory Word_Lemmas

lemma is_aligned_shiftr_add:
 "\<lbrakk>is_aligned a n; is_aligned b m; b < 2^n; m \<le> n; n < LENGTH('a)\<rbrakk>
  \<Longrightarrow> a + b >> m = (a >> m) + (b >> m)" for a :: "'a::len word" apply(simp add: shiftr_div_2n_w word_size) apply (rule word_unat_eq_iff[THEN iffD2]) apply (subst unat_plus_simple[THEN iffD1]) apply (subst shiftr_div_2n_w[symmetric])+ apply (rule is_aligned_no_wrap') apply (rule is_aligned_shiftr[where n = "n - m"]) apply simp apply (rule shiftr_less_t2n) apply simp apply (simp add:unat_div) apply (subst unat_plus_simple[THEN iffD1]) apply (erule is_aligned_no_wrap') apply simp by (meson div_plus_div_distrib_dvd_left is_aligned_iff_dvd_nat is_aligned_weaken)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a + b >> m = (a >> m) + (b >> m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (a + b) div 2 ^ m = a div 2 ^ m + b div 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a + b) div 2 ^ m) = unat (a div 2 ^ m + b div 2 ^ m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a div 2 ^ m \<le> a div 2 ^ m + b div 2 ^ m
 2. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a + b) div 2 ^ m) = unat (a div 2 ^ m) + unat (b div 2 ^ m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a >> m \<le> (a >> m) + (b >> m)
 2. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a + b) div 2 ^ m) = unat (a div 2 ^ m) + unat (b div 2 ^ m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (a >> m) ?sz9
 2. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> b >> m < 2 ^ ?sz9
 3. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a + b) div 2 ^ m) = unat (a div 2 ^ m) + unat (b div 2 ^ m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned a (n - m + m)
 2. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> b >> m < 2 ^ (n - m)
 3. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a + b) div 2 ^ m) = unat (a div 2 ^ m) + unat (b div 2 ^ m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> b >> m < 2 ^ (n - m)
 2. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a + b) div 2 ^ m) = unat (a div 2 ^ m) + unat (b div 2 ^ m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> b < 2 ^ (m + (n - m))
 2. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a + b) div 2 ^ m) = unat (a div 2 ^ m) + unat (b div 2 ^ m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a + b) div 2 ^ m) = unat (a div 2 ^ m) + unat (b div 2 ^ m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (a + b) div 2 ^ m = unat a div 2 ^ m + unat b div 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a \<le> a + b
 2. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (unat a + unat b) div 2 ^ m = unat a div 2 ^ m + unat b div 2 ^ m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> b < 2 ^ n
 2. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (unat a + unat b) div 2 ^ m = unat a div 2 ^ m + unat b div 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b m; b < 2 ^ n; m \<le> n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (unat a + unat b) div 2 ^ m = unat a div 2 ^ m + unat b div 2 ^ m