theory Aligned

lemma aligned_offset_non_zero:
  "\<lbrakk> is_aligned x n; y < 2 ^ n; x \<noteq> 0 \<rbrakk> \<Longrightarrow> x + y \<noteq> 0" apply (cases "y = 0") apply simp apply (subst word_neq_0_conv) apply (subst gt0_iff_gem1) apply (erule is_aligned_get_word_bits) apply (subst field_simps[symmetric], subst plus_le_left_cancel_nowrap) apply (rule is_aligned_no_wrap') apply simp apply (rule word_leq_le_minus_one) apply simp apply assumption apply (erule (1) is_aligned_no_wrap') apply (simp add: gt0_iff_gem1 [symmetric] word_neq_0_conv) apply simp done

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