theory Aligned

lemma aligned_add_offset_less:
  "\<lbrakk>is_aligned x n; is_aligned y n; x < y; z < 2 ^ n\<rbrakk> \<Longrightarrow> x + z < y" apply (cases "y = 0") apply simp apply (erule is_aligned_get_word_bits[where p=y], simp_all) apply (cases "z = 0", simp_all) apply (drule(2) aligned_at_least_t2n_diff[rotated -1]) apply (drule plus_one_helper2) apply (rule less_is_non_zero_p1) apply (rule aligned_less_plus_1) apply (erule aligned_sub_aligned[OF _ _ order_refl],
           simp_all add: is_aligned_triv)[1] apply (cases n, simp_all)[1] apply (simp only: trans[OF diff_add_eq diff_diff_eq2[symmetric]]) apply (drule word_less_add_right) apply (rule ccontr, simp add: linorder_not_le) apply (drule aligned_small_is_0, erule order_less_trans) apply (clarsimp simp: power_overflow) apply simp apply (erule order_le_less_trans[rotated],
         rule word_plus_mono_right) apply (erule word_le_minus_one_leq) apply (simp add: is_aligned_no_wrap' is_aligned_no_overflow field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; x < y; z < 2 ^ n\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; is_aligned y n; x < y; z < 2 ^ n; y = 0\<rbrakk> \<Longrightarrow> x + z < y
 2. \<lbrakk>is_aligned x n; is_aligned y n; x < y; z < 2 ^ n; y \<noteq> 0\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; x < y; z < 2 ^ n; y \<noteq> 0\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x < y; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x < y; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x \<le> y - 2 ^ n\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> y - 2 ^ n + 1 \<noteq> 0
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x < y - 2 ^ n + 1\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> y - 2 ^ n < ?k12
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x < y - 2 ^ n + 1\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (y - 2 ^ n) ?n14
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < ?n14
 3. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x < y - 2 ^ n + 1\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < n
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x < y - 2 ^ n + 1\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x < y - 2 ^ n + 1\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x < y - (2 ^ n - 1)\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ n - 1 \<le> y
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x + (2 ^ n - 1) < y\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; y < 2 ^ n - 1\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x + (2 ^ n - 1) < y\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ n - 1 < 2 ^ n
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; n < LENGTH('a); z \<noteq> 0; y < 2 ^ n - 1; y = 0\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x + (2 ^ n - 1) < y\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; n < LENGTH('a); z \<noteq> 0; y < 2 ^ n - 1; y = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x + (2 ^ n - 1) < y\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0; x + (2 ^ n - 1) < y\<rbrakk> \<Longrightarrow> x + z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> z \<le> 2 ^ n - 1
 2. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ n - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; z < 2 ^ n; y \<noteq> 0; is_aligned y n; n < LENGTH('a); z \<noteq> 0\<rbrakk> \<Longrightarrow> x \<le> x + (2 ^ n - 1) proof (prove)
goal:
No subgoals!