[STATEMENT]
lemma is_aligned_no_wrap_le:
  fixes ptr::"'a::len word"
  assumes al: "is_aligned ptr sz"
  and    szv: "sz < LENGTH('a)"
  and    off: "off \<le> 2 ^ sz"
  shows  "unat ptr + off \<le> 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
is_aligned ptr sz
[PROOF STEP]
obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and
    qv: "q < 2 ^ (LENGTH('a) - sz)"
[PROOF STATE]
proof (prove)
using this:
is_aligned ptr sz

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>ptr = 2 ^ sz * word_of_nat q; q < 2 ^ (LENGTH('a) - sz)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_alignedE)
[PROOF STATE]
proof (state)
this:
ptr = 2 ^ sz * word_of_nat q
q < 2 ^ (LENGTH('a) - sz)

goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
proof (cases "sz = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sz = 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
 2. sz \<noteq> 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
sz = 0

goal (2 subgoals):
 1. sz = 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
 2. sz \<noteq> 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sz = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sz = 0

goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
using off ptrq qv
[PROOF STATE]
proof (prove)
using this:
sz = 0
off \<le> 2 ^ sz
ptr = 2 ^ sz * word_of_nat q
q < 2 ^ (LENGTH('a) - sz)

goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
by (auto simp add: le_Suc_eq Suc_le_eq) (simp add: le_less)
[PROOF STATE]
proof (state)
this:
unat ptr + off \<le> 2 ^ LENGTH('a)

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
sz \<noteq> 0

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sz \<noteq> 0
[PROOF STEP]
have sne: "0 < sz"
[PROOF STATE]
proof (prove)
using this:
sz \<noteq> 0

goal (1 subgoal):
 1. 0 < sz
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
0 < sz

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
have uq: "unat (of_nat q :: 'a word) = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat q) = q
[PROOF STEP]
apply (subst unat_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q mod 2 ^ LENGTH('a) = q
[PROOF STEP]
apply (rule mod_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule order_less_trans [OF qv])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (LENGTH('a) - sz) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule power_strict_increasing [OF diff_less [OF sne]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < LENGTH('a)
 2. 1 < 2
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat (word_of_nat q) = q

goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
have uptr: "unat ptr = 2 ^ sz * q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr = 2 ^ sz * q
[PROOF STEP]
apply (subst ptrq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz * word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (subst iffD1 [OF unat_mult_lem])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. unat (2 ^ sz) * unat (word_of_nat q) < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (subst unat_power_lower [OF szv])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 2 ^ sz * unat (word_of_nat q) < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (subst uq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 2 ^ sz * q < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (subst uq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz) * q = 2 ^ sz * q
[PROOF STEP]
apply (subst unat_power_lower [OF szv])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ sz * q = 2 ^ sz * q
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat ptr = 2 ^ sz * q

goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
show "unat ptr + off \<le> 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
using szv
[PROOF STATE]
proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. unat ptr + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst uptr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz * q + off \<le> 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst mult.commute, rule nat_add_offset_le [OF off qv])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = LENGTH('a) - sz + sz
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat ptr + off \<le> 2 ^ LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unat ptr + off \<le> 2 ^ LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unat ptr + off \<le> 2 ^ LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_neg_mask:
  "m \<le> n \<Longrightarrow> is_aligned (x AND NOT (mask n)) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> is_aligned (x AND NOT (mask n)) m
[PROOF STEP]
by (rule is_aligned_bitI) (simp add: bit_simps)


[STATEMENT]
lemma unat_minus:
  "unat (- (x :: 'a :: len word)) = (if x = 0 then 0 else 2 ^ size x - unat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (- x) = (if x = 0 then 0 else 2 ^ size x - unat x)
[PROOF STEP]
using unat_sub_if_size[where x="2 ^ size x" and y=x]
[PROOF STATE]
proof (prove)
using this:
unat (2 ^ size x - x) = (if unat x \<le> unat (2 ^ size x) then unat (2 ^ size x) - unat x else unat (2 ^ size x) + 2 ^ size (2 ^ size x) - unat x)

goal (1 subgoal):
 1. unat (- x) = (if x = 0 then 0 else 2 ^ size x - unat x)
[PROOF STEP]
by (simp add: unat_eq_0 word_size)


[STATEMENT]
lemma is_aligned_minus:
  \<open>is_aligned (- p) n\<close> if \<open>is_aligned p n\<close> for p :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (- p) n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
is_aligned p n

goal (1 subgoal):
 1. is_aligned (- p) n
[PROOF STEP]
apply (cases \<open>n < LENGTH('a)\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (- p) n
 2. \<lbrakk>is_aligned p n; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (- p) n
[PROOF STEP]
apply (simp_all add: not_less is_aligned_beyond_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (- p) n
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>2 ^ n dvd take_bit LENGTH('a) p; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n dvd take_bit LENGTH('a) (- p)
[PROOF STEP]
apply (simp flip: take_bit_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>take_bit n p = 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit n (- p) = 0
[PROOF STEP]
apply (subst take_bit_minus [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>take_bit n p = 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit n (- take_bit n p) = 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma add_mask_lower_bits:
  "\<lbrakk>is_aligned (x :: 'a :: len word) n;
    \<forall>n' \<ge> n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x + p AND NOT (mask n) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x + p AND NOT (mask n) = x
[PROOF STEP]
apply (subst word_plus_and_or_coroll)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x AND p = 0
 2. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x
[PROOF STEP]
apply (rule word_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> na < size (x AND p) \<longrightarrow> bit (x AND p) na = bit 0 na
 2. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x
[PROOF STEP]
apply (clarsimp simp: word_size is_aligned_nth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit x na; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'; na < LENGTH('a); bit (x AND p) na\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x
[PROOF STEP]
apply (erule_tac x=na in allE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>na < LENGTH('a); bit (x AND p) na; na < n \<longrightarrow> \<not> bit x na; n \<le> na \<longrightarrow> na < LENGTH('a) \<longrightarrow> \<not> bit p na\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x
[PROOF STEP]
apply (simp add: bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> (x OR p) AND NOT (mask n) = x
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit ((x OR p) AND NOT (mask n)) na = bit x na
[PROOF STEP]
apply (auto simp add: bit_simps not_less word_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned x n; \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'; na < LENGTH('a); bit x na\<rbrakk> \<Longrightarrow> n \<le> na
[PROOF STEP]
apply (metis is_aligned_nth not_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_andI1:
  "is_aligned x n \<Longrightarrow> is_aligned (x AND y) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned x n \<Longrightarrow> is_aligned (x AND y) n
[PROOF STEP]
by (simp add: is_aligned_nth bit_simps)


[STATEMENT]
lemma is_aligned_andI2:
  "is_aligned y n \<Longrightarrow> is_aligned (x AND y) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned y n \<Longrightarrow> is_aligned (x AND y) n
[PROOF STEP]
by (simp add: is_aligned_nth bit_simps)


[STATEMENT]
lemma is_aligned_shiftl:
  "is_aligned w (n - m) \<Longrightarrow> is_aligned (w << m) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w (n - m) \<Longrightarrow> is_aligned (w << m) n
[PROOF STEP]
by (simp add: is_aligned_nth bit_simps)


[STATEMENT]
lemma is_aligned_shiftr:
  "is_aligned w (n + m) \<Longrightarrow> is_aligned (w >> m) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w (n + m) \<Longrightarrow> is_aligned (w >> m) n
[PROOF STEP]
by (simp add: is_aligned_nth bit_simps)


[STATEMENT]
lemma is_aligned_shiftl_self:
  "is_aligned (p << n) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (p << n) n
[PROOF STEP]
by (rule is_aligned_shift)


[STATEMENT]
lemma is_aligned_neg_mask_eq:
  "is_aligned p n \<Longrightarrow> p AND NOT (mask n) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p n \<Longrightarrow> p AND NOT (mask n) = p
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned p n; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (p AND NOT (mask n)) na = bit p na
[PROOF STEP]
apply (auto simp add: bit_simps is_aligned_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_shiftr_shiftl:
  "is_aligned w n \<Longrightarrow> w >> n << n = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w n \<Longrightarrow> w >> n << n = w
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned w n; na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (w >> n << n) na = bit w na
[PROOF STEP]
apply (auto simp add: bit_simps is_aligned_nth intro: ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit w na; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> bit w (n + (na - n))
[PROOF STEP]
apply (subst add_diff_inverse_nat)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit w na; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> \<not> na < n
 2. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit w na; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> bit w na
[PROOF STEP]
apply (auto intro: ccontr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_shiftr_mask_shiftl:
  "is_aligned x n \<Longrightarrow> ((x >> n) AND mask v) << n = x AND mask (v + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned x n \<Longrightarrow> (x >> n) AND mask v << n = x AND mask (v + n)
[PROOF STEP]
apply (rule word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. is_aligned x n \<Longrightarrow> na < size ((x >> n) AND mask v << n) \<longrightarrow> bit ((x >> n) AND mask v << n) na = bit (x AND mask (v + n)) na
[PROOF STEP]
apply (simp add: word_size bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. is_aligned x n \<Longrightarrow> na < LENGTH('a) \<longrightarrow> (n \<le> na \<and> bit x (n + (na - n)) \<and> na - n < LENGTH('a) \<and> na - n < v) = (bit x na \<and> na < v + n)
[PROOF STEP]
apply (subgoal_tac "\<forall>m. bit x m \<longrightarrow> m \<ge> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x n; \<forall>m. bit x m \<longrightarrow> n \<le> m\<rbrakk> \<Longrightarrow> na < LENGTH('a) \<longrightarrow> (n \<le> na \<and> bit x (n + (na - n)) \<and> na - n < LENGTH('a) \<and> na - n < v) = (bit x na \<and> na < v + n)
 2. \<And>na. is_aligned x n \<Longrightarrow> \<forall>m. bit x m \<longrightarrow> n \<le> m
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. is_aligned x n \<Longrightarrow> \<forall>m. bit x m \<longrightarrow> n \<le> m
[PROOF STEP]
apply (clarsimp simp: is_aligned_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>x AND mask n = 0; bit x m\<rbrakk> \<Longrightarrow> n \<le> m
[PROOF STEP]
apply (drule_tac x=m in word_eqD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>bit x m; bit (x AND mask n) m = bit 0 m\<rbrakk> \<Longrightarrow> n \<le> m
[PROOF STEP]
apply (frule test_bit_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>bit x m; bit (x AND mask n) m = bit 0 m; m < size x\<rbrakk> \<Longrightarrow> n \<le> m
[PROOF STEP]
apply (simp add: word_size bit_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mask_zero:
  "is_aligned x a \<Longrightarrow> x AND mask a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned x a \<Longrightarrow> x AND mask a = 0
[PROOF STEP]
by (metis is_aligned_mask)


[STATEMENT]
lemma is_aligned_neg_mask_eq_concrete:
  "\<lbrakk> is_aligned p n; msk AND NOT (mask n) = NOT (mask n) \<rbrakk>
   \<Longrightarrow> p AND msk = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; msk AND NOT (mask n) = NOT (mask n)\<rbrakk> \<Longrightarrow> p AND msk = p
[PROOF STEP]
by (metis word_bw_assocs(1) word_bw_comms(1) is_aligned_neg_mask_eq)


[STATEMENT]
lemma is_aligned_and_not_zero:
  "\<lbrakk> is_aligned n k; n \<noteq> 0 \<rbrakk> \<Longrightarrow> 2 ^ k \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned n k; n \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ k \<le> n
[PROOF STEP]
using is_aligned_less_sz leI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_aligned ?a ?sz; ?a \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> ?a < 2 ^ ?sz
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x

goal (1 subgoal):
 1. \<lbrakk>is_aligned n k; n \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ k \<le> n
[PROOF STEP]
by blast


[STATEMENT]
lemma is_aligned_and_2_to_k:
  "(n AND 2 ^ k - 1) = 0 \<Longrightarrow> is_aligned (n :: 'a :: len word) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n AND 2 ^ k - 1 = 0 \<Longrightarrow> is_aligned n k
[PROOF STEP]
by (simp add: is_aligned_mask mask_eq_decr_exp)


[STATEMENT]
lemma is_aligned_power2:
  "b \<le> a \<Longrightarrow> is_aligned (2 ^ a) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> is_aligned (2 ^ a) b
[PROOF STEP]
by (metis is_aligned_triv is_aligned_weaken)


[STATEMENT]
lemma is_aligned_neg_mask_weaken:
  "\<lbrakk> is_aligned p n; m \<le> n \<rbrakk> \<Longrightarrow> p AND NOT (mask m) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; m \<le> n\<rbrakk> \<Longrightarrow> p AND NOT (mask m) = p
[PROOF STEP]
using is_aligned_neg_mask_eq is_aligned_weaken
[PROOF STATE]
proof (prove)
using this:
is_aligned ?p ?n \<Longrightarrow> ?p AND NOT (mask ?n) = ?p
\<lbrakk>is_aligned ?w ?x; ?y \<le> ?x\<rbrakk> \<Longrightarrow> is_aligned ?w ?y

goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; m \<le> n\<rbrakk> \<Longrightarrow> p AND NOT (mask m) = p
[PROOF STEP]
by blast


[STATEMENT]
lemma is_aligned_neg_mask2 [simp]:
  "is_aligned (a AND NOT (mask n)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (a AND NOT (mask n)) n
[PROOF STEP]
by (rule is_aligned_bitI) (simp add: bit_simps)


[STATEMENT]
lemma is_aligned_0':
  "is_aligned 0 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned 0 n
[PROOF STEP]
by (fact is_aligned_0)


[STATEMENT]
lemma aligned_add_offset_no_wrap:
  fixes off :: "('a::len) word"
  and     x :: "'a word"
  assumes al: "is_aligned x sz"
  and   offv: "off < 2 ^ sz"
  shows  "unat x + unat off < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
 2. \<not> ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
assume szv: "sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
 2. \<not> ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
is_aligned x sz
[PROOF STEP]
obtain k where xv: "x = 2 ^ sz * (of_nat k)"
    and kl: "k < 2 ^ (LENGTH('a) - sz)"
[PROOF STATE]
proof (prove)
using this:
is_aligned x sz

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>x = 2 ^ sz * word_of_nat k; k < 2 ^ (LENGTH('a) - sz)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_alignedE)
[PROOF STATE]
proof (state)
this:
x = 2 ^ sz * word_of_nat k
k < 2 ^ (LENGTH('a) - sz)

goal (2 subgoals):
 1. ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
 2. \<not> ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
using szv
[PROOF STATE]
proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst xv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz * word_of_nat k) + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst unat_mult_power_lem[OF kl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz * k + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst mult.commute, rule nat_add_offset_less)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat off < 2 ^ sz
 2. sz < LENGTH('a) \<Longrightarrow> k < 2 ^ ?m1
 3. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = ?m1 + sz
[PROOF STEP]
apply (rule less_le_trans[OF unat_mono[OF offv, simplified]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz) \<le> 2 ^ sz
 2. sz < LENGTH('a) \<Longrightarrow> k < 2 ^ ?m1
 3. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = ?m1 + sz
[PROOF STEP]
apply (erule eq_imp_le[OF unat_power_lower])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> k < 2 ^ ?m1
 2. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = ?m1 + sz
[PROOF STEP]
apply (rule kl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = LENGTH('a) - sz + sz
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat x + unat off < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
assume "\<not> sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
with offv
[PROOF STATE]
proof (chain)
picking this:
off < 2 ^ sz
\<not> sz < LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
off < 2 ^ sz
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
by (simp add: not_less power_overflow )
[PROOF STATE]
proof (state)
this:
unat x + unat off < 2 ^ LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aligned_add_offset_mod:
  fixes x :: "('a::len) word"
  assumes al: "is_aligned x sz"
  and     kv: "k < 2 ^ sz"
  shows   "(x + k) mod 2 ^ sz = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + k) mod 2 ^ sz = k
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
 2. \<not> ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
[PROOF STEP]
assume szv: "sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
 2. \<not> ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
[PROOF STEP]
have ux: "unat x + unat k < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat x + unat k < 2 ^ LENGTH('a)
[PROOF STEP]
by (rule aligned_add_offset_no_wrap) fact+
[PROOF STATE]
proof (state)
this:
unat x + unat k < 2 ^ LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
 2. \<not> ?P \<Longrightarrow> (x + k) mod 2 ^ sz = k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + k) mod 2 ^ sz = k
[PROOF STEP]
using al szv
[PROOF STATE]
proof (prove)
using this:
is_aligned x sz
sz < LENGTH('a)

goal (1 subgoal):
 1. (x + k) mod 2 ^ sz = k
[PROOF STEP]
apply (simp flip: take_bit_eq_mod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit sz (x + k) = k
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (take_bit sz (x + k)) n = bit k n
[PROOF STEP]
apply (auto simp add: bit_simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < sz; bit (x + k) n\<rbrakk> \<Longrightarrow> bit k n
 2. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> n < sz
 3. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> bit (x + k) n
[PROOF STEP]
apply (metis assms(2) bit_or_iff is_aligned_mask is_aligned_nth leD less_mask_eq word_and_le1 word_bw_lcs(1) word_neq_0_conv word_plus_and_or_coroll)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> n < sz
 2. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> bit (x + k) n
[PROOF STEP]
apply (meson assms(2) leI less_2p_is_upper_bits_unset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>is_aligned x sz; sz < LENGTH('a); n < LENGTH('a); bit k n\<rbrakk> \<Longrightarrow> bit (x + k) n
[PROOF STEP]
apply (metis assms(2) bit_disjunctive_add_iff bit_imp_le_length bit_push_bit_iff is_alignedE' less_2p_is_upper_bits_unset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(x + k) mod 2 ^ sz = k

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> (x + k) mod 2 ^ sz = k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> (x + k) mod 2 ^ sz = k
[PROOF STEP]
assume "\<not> sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> (x + k) mod 2 ^ sz = k
[PROOF STEP]
with al
[PROOF STATE]
proof (chain)
picking this:
is_aligned x sz
\<not> sz < LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_aligned x sz
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. (x + k) mod 2 ^ sz = k
[PROOF STEP]
by (simp add: not_less power_overflow is_aligned_mask mask_eq_decr_exp
                  word_mod_by_0)
[PROOF STATE]
proof (state)
this:
(x + k) mod 2 ^ sz = k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aligned_neq_into_no_overlap:
  fixes x :: "'a::len word"
  assumes neq: "x \<noteq> y"
  and     alx: "is_aligned x sz"
  and     aly: "is_aligned y sz"
  shows  "{x .. x + (2 ^ sz - 1)} \<inter> {y .. y + (2 ^ sz - 1)} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
 2. \<not> ?P \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
assume szv: "sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
 2. \<not> ?P \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
proof (rule equals0I, clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume xb: "x \<le> z" and xt: "z \<le> x + (2 ^ sz - 1)"
      and yb: "y \<le> z" and yt: "z \<le> y + (2 ^ sz - 1)"
[PROOF STATE]
proof (state)
this:
x \<le> z
z \<le> x + (2 ^ sz - 1)
y \<le> z
z \<le> y + (2 ^ sz - 1)

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have rl: "\<And>(p::'a word) k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; w \<le> p + (2 ^ sz - 1) \<rbrakk>
      \<Longrightarrow> k < 2 ^ sz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; w \<le> p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> k < 2 ^ sz
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; w \<le> p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> k < 2 ^ sz
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; p + k \<le> p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> k < 2 ^ sz
[PROOF STEP]
apply (subst (asm) add.commute, subst (asm) add.commute, drule word_plus_mcs_4)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k\<rbrakk> \<Longrightarrow> p \<le> k + p
 2. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; k \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz
[PROOF STEP]
apply (subst add.commute, subst no_plus_overflow_uint_size)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k\<rbrakk> \<Longrightarrow> uint p + uint k < 2 ^ size p
 2. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; k \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p k w. \<lbrakk>take_bit LENGTH('a) p + take_bit LENGTH('a) k < 2 ^ LENGTH('a); take_bit LENGTH('a) w = take_bit LENGTH('a) (p + k)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) p + take_bit LENGTH('a) k < 2 ^ LENGTH('a)
 2. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; k \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p k w. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); w = p + k; k \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz
[PROOF STEP]
apply (auto simp add: le_less power_2_ge_iff szv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p k. \<lbrakk>uint p + uint k < 2 ^ LENGTH('a); k < 2 ^ sz - 1\<rbrakk> \<Longrightarrow> k < 2 ^ sz
[PROOF STEP]
apply (metis le_less_trans mask_eq_decr_exp mask_lt_2pn order_less_imp_le szv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>uint ?p + uint ?k < 2 ^ LENGTH('a); ?w = ?p + ?k; ?w \<le> ?p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> ?k < 2 ^ sz

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from xb
[PROOF STATE]
proof (chain)
picking this:
x \<le> z
[PROOF STEP]
obtain kx where
      kx: "z = x + kx" and
      kxl: "uint x + uint kx < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
using this:
x \<le> z

goal (1 subgoal):
 1. (\<And>kx. \<lbrakk>z = x + kx; uint x + uint kx < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (clarsimp dest!: word_le_exists')
[PROOF STATE]
proof (state)
this:
z = x + kx
uint x + uint kx < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from yb
[PROOF STATE]
proof (chain)
picking this:
y \<le> z
[PROOF STEP]
obtain ky where
      ky: "z = y + ky" and
      kyl: "uint y + uint ky < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
using this:
y \<le> z

goal (1 subgoal):
 1. (\<And>ky. \<lbrakk>z = y + ky; uint y + uint ky < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (clarsimp dest!: word_le_exists')
[PROOF STATE]
proof (state)
this:
z = y + ky
uint y + uint ky < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "kx = z mod 2 ^ sz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kx = z mod 2 ^ sz
[PROOF STEP]
proof (subst kx, rule sym, rule aligned_add_offset_mod)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_aligned x sz
 2. kx < 2 ^ sz
[PROOF STEP]
show "kx < 2 ^ sz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kx < 2 ^ sz
[PROOF STEP]
by (rule rl) fact+
[PROOF STATE]
proof (state)
this:
kx < 2 ^ sz

goal (1 subgoal):
 1. is_aligned x sz
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
kx = z mod 2 ^ sz

goal (1 subgoal):
 1. x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
kx = z mod 2 ^ sz

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "\<dots> = ky"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z mod 2 ^ sz = ky
[PROOF STEP]
proof (subst ky, rule aligned_add_offset_mod)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_aligned y sz
 2. ky < 2 ^ sz
[PROOF STEP]
show "ky < 2 ^ sz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ky < 2 ^ sz
[PROOF STEP]
using kyl ky yt
[PROOF STATE]
proof (prove)
using this:
uint y + uint ky < 2 ^ LENGTH('a)
z = y + ky
z \<le> y + (2 ^ sz - 1)

goal (1 subgoal):
 1. ky < 2 ^ sz
[PROOF STEP]
by (rule rl)
[PROOF STATE]
proof (state)
this:
ky < 2 ^ sz

goal (1 subgoal):
 1. is_aligned y sz
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
z mod 2 ^ sz = ky

goal (1 subgoal):
 1. x = y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
kx = ky
[PROOF STEP]
have kxky: "kx = ky"
[PROOF STATE]
proof (prove)
using this:
kx = ky

goal (1 subgoal):
 1. kx = ky
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
kx = ky

goal (1 subgoal):
 1. x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
kx = ky

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have "x + kx = y + ky"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + kx = y + ky
[PROOF STEP]
by (simp add: kx [symmetric] ky [symmetric])
[PROOF STATE]
proof (state)
this:
x + kx = y + ky

goal (1 subgoal):
 1. x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
kx = ky
x + kx = y + ky
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
kx = ky
x + kx = y + ky

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>x \<le> ya; y \<le> ya; ya \<le> x + (2 ^ sz - 1); ya \<le> y + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. False
[PROOF STEP]
using neq
[PROOF STATE]
proof (prove)
using this:
x = y
x \<noteq> y

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
assume "\<not> sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
with neq alx aly
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
is_aligned x sz
is_aligned y sz
\<not> sz < LENGTH('a)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
is_aligned x sz
is_aligned y sz
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: is_aligned_mask mask_eq_decr_exp power_overflow)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. {x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
{x..x + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ sz - 1)} = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_add_helper:
  "\<lbrakk> is_aligned p n; d < 2 ^ n \<rbrakk>
     \<Longrightarrow> (p + d AND mask n = d) \<and> (p + d AND (NOT (mask n)) = p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d AND mask n = d \<and> p + d AND NOT (mask n) = p
[PROOF STEP]
apply (subst (asm) is_aligned_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p AND mask n = 0; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d AND mask n = d \<and> p + d AND NOT (mask n) = p
[PROOF STEP]
apply (drule less_mask_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p AND mask n = 0; d AND mask n = d\<rbrakk> \<Longrightarrow> p + d AND mask n = d \<and> p + d AND NOT (mask n) = p
[PROOF STEP]
apply (rule context_conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p AND mask n = 0; d AND mask n = d\<rbrakk> \<Longrightarrow> p + d AND mask n = d
 2. \<lbrakk>p AND mask n = 0; d AND mask n = d; p + d AND mask n = d\<rbrakk> \<Longrightarrow> p + d AND NOT (mask n) = p
[PROOF STEP]
apply (subst word_plus_and_or_coroll)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p AND mask n = 0; d AND mask n = d\<rbrakk> \<Longrightarrow> p AND d = 0
 2. \<lbrakk>p AND mask n = 0; d AND mask n = d\<rbrakk> \<Longrightarrow> (p OR d) AND mask n = d
 3. \<lbrakk>p AND mask n = 0; d AND mask n = d; p + d AND mask n = d\<rbrakk> \<Longrightarrow> p + d AND NOT (mask n) = p
[PROOF STEP]
apply (simp_all flip: take_bit_eq_mask)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>take_bit n p = 0; take_bit n d = d\<rbrakk> \<Longrightarrow> p AND d = 0
 2. \<lbrakk>take_bit n p = 0; take_bit n d = d; take_bit n (p + d) = d\<rbrakk> \<Longrightarrow> p + d AND NOT (mask n) = p
[PROOF STEP]
apply (metis take_bit_eq_mask word_bw_lcs(1) word_log_esimps(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_bit n p = 0; take_bit n d = d; take_bit n (p + d) = d\<rbrakk> \<Longrightarrow> p + d AND NOT (mask n) = p
[PROOF STEP]
apply (metis add.commute add_left_imp_eq take_bit_eq_mask word_plus_and_or_coroll2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mask_add_aligned:
  "is_aligned p n \<Longrightarrow> (p + q) AND mask n = q AND mask n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p n \<Longrightarrow> p + q AND mask n = q AND mask n
[PROOF STEP]
apply (simp add: is_aligned_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p AND mask n = 0 \<Longrightarrow> p + q AND mask n = q AND mask n
[PROOF STEP]
apply (subst mask_inner_mask [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p AND mask n = 0 \<Longrightarrow> (p AND mask n) + q AND mask n = q AND mask n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mask_out_add_aligned:
  assumes al: "is_aligned p n"
  shows "p + (q AND NOT (mask n)) = (p + q) AND NOT (mask n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p + (q AND NOT (mask n)) = p + q AND NOT (mask n)
[PROOF STEP]
using mask_add_aligned [OF al]
[PROOF STATE]
proof (prove)
using this:
p + ?q AND mask n = ?q AND mask n

goal (1 subgoal):
 1. p + (q AND NOT (mask n)) = p + q AND NOT (mask n)
[PROOF STEP]
by (simp add: mask_out_sub_mask)


[STATEMENT]
lemma is_aligned_add_or:
  "\<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d = p OR d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d = p OR d
[PROOF STEP]
apply (subst disjunctive_add, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> bit p na \<longrightarrow> \<not> bit d na
[PROOF STEP]
apply (clarsimp simp: is_aligned_nth less_2p_is_upper_bits_unset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>na<n. \<not> bit p na; n < LENGTH('a); \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit d n'; bit p na; bit d na\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>na<n. \<not> bit p na; n < LENGTH('a); \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit d n'; bit p m; bit d m\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases \<open>m < n\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>na<n. \<not> bit p na; n < LENGTH('a); \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit d n'; bit p m; bit d m; m < n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>na<n. \<not> bit p na; n < LENGTH('a); \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit d n'; bit p m; bit d m; \<not> m < n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp add: not_less dest: bit_imp_possible_bit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_greatest_aligned:
  "\<lbrakk> x < y; is_aligned x n; is_aligned y n \<rbrakk> \<Longrightarrow> x + 2 ^ n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < y; is_aligned x n; is_aligned y n\<rbrakk> \<Longrightarrow> x + 2 ^ n \<noteq> 0
[PROOF STEP]
by (metis NOT_mask add_diff_cancel_right' diff_0 is_aligned_neg_mask_eq not_le word_and_le1)


[STATEMENT]
lemma neg_mask_mono_le:
  "x \<le> y \<Longrightarrow> x AND NOT(mask n) \<le> y AND NOT(mask n)" for x :: "'a :: len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x AND NOT (mask n) \<le> y AND NOT (mask n)
[PROOF STEP]
proof (rule ccontr, simp add: linorder_not_le, cases "n < LENGTH('a)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n < LENGTH('a)

goal (2 subgoals):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> n < LENGTH('a)
[PROOF STEP]
show "y AND NOT(mask n) < x AND NOT(mask n) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> False
[PROOF STEP]
by (simp add: mask_eq_decr_exp linorder_not_less power_overflow)
[PROOF STATE]
proof (state)
this:
y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume a: "x \<le> y" and b: "y AND NOT(mask n) < x AND NOT(mask n)"
[PROOF STATE]
proof (state)
this:
x \<le> y
y AND NOT (mask n) < x AND NOT (mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have word_bits: "n < LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "y \<le> (y AND NOT(mask n)) + (y AND mask n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> (y AND NOT (mask n)) + (y AND mask n)
[PROOF STEP]
by (simp add: word_plus_and_or_coroll2 add.commute)
[PROOF STATE]
proof (state)
this:
y \<le> (y AND NOT (mask n)) + (y AND mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y \<le> (y AND NOT (mask n)) + (y AND mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> (y AND NOT(mask n)) + 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y AND NOT (mask n)) + (y AND mask n) \<le> (y AND NOT (mask n)) + 2 ^ n
[PROOF STEP]
apply (rule word_plus_mono_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. y AND mask n \<le> 2 ^ n
 2. y AND NOT (mask n) \<le> (y AND NOT (mask n)) + 2 ^ n
[PROOF STEP]
apply (rule order_less_imp_le, rule and_mask_less_size)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n < size y
 2. y AND NOT (mask n) \<le> (y AND NOT (mask n)) + 2 ^ n
[PROOF STEP]
apply (simp add: word_size word_bits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y AND NOT (mask n) \<le> (y AND NOT (mask n)) + 2 ^ n
[PROOF STEP]
apply (rule is_aligned_no_overflow'', simp add: is_aligned_neg_mask word_bits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y AND NOT (mask n)) + 2 ^ n \<noteq> 0
[PROOF STEP]
apply (rule not_greatest_aligned, rule b; simp add: is_aligned_neg_mask)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(y AND NOT (mask n)) + (y AND mask n) \<le> (y AND NOT (mask n)) + 2 ^ n

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y AND NOT (mask n)) + (y AND mask n) \<le> (y AND NOT (mask n)) + 2 ^ n

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> x AND NOT(mask n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y AND NOT (mask n)) + 2 ^ n \<le> x AND NOT (mask n)
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
y AND NOT (mask n) < x AND NOT (mask n)

goal (1 subgoal):
 1. (y AND NOT (mask n)) + 2 ^ n \<le> x AND NOT (mask n)
[PROOF STEP]
apply (subst add.commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> 2 ^ n + (y AND NOT (mask n)) \<le> x AND NOT (mask n)
[PROOF STEP]
apply (rule le_plus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> y AND NOT (mask n) \<le> (x AND NOT (mask n)) - 2 ^ n
 2. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> 2 ^ n \<le> x AND NOT (mask n)
[PROOF STEP]
apply (rule aligned_at_least_t2n_diff; simp add: is_aligned_neg_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y AND NOT (mask n) < x AND NOT (mask n) \<Longrightarrow> 2 ^ n \<le> x AND NOT (mask n)
[PROOF STEP]
apply (rule ccontr, simp add: linorder_not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y AND NOT (mask n) < x AND NOT (mask n); x AND NOT (mask n) < 2 ^ n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule aligned_small_is_0[rotated]; simp add: is_aligned_neg_mask)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(y AND NOT (mask n)) + 2 ^ n \<le> x AND NOT (mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y AND NOT (mask n)) + 2 ^ n \<le> x AND NOT (mask n)

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND NOT (mask n) \<le> x
[PROOF STEP]
by (rule word_and_le2)
[PROOF STATE]
proof (state)
this:
x AND NOT (mask n) \<le> x

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x AND NOT (mask n) \<le> x

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y AND NOT (mask n) < x AND NOT (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y = x
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
y = x

goal (1 subgoal):
 1. False
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
y = x
y AND NOT (mask n) < x AND NOT (mask n)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma and_neg_mask_eq_iff_not_mask_le:
  "w AND NOT(mask n) = NOT(mask n) \<longleftrightarrow> NOT(mask n) \<le> w"
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w AND NOT (mask n) = NOT (mask n)) = (NOT (mask n) \<le> w)
[PROOF STEP]
by (metis eq_iff neg_mask_mono_le word_and_le1 word_and_le2 word_bw_same(1))


[STATEMENT]
lemma neg_mask_le_high_bits:
  \<open>NOT (mask n) \<le> w \<longleftrightarrow> (\<forall>i \<in> {n ..< size w}. bit w i)\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (NOT (mask n) \<le> w) = (\<forall>i\<in>{n..<size w}. bit w i)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
 2. \<forall>i\<in>{n..<size w}. bit w i \<Longrightarrow> NOT (mask n) \<le> w
[PROOF STEP]
assume ?Q
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{n..<size w}. bit w i

goal (2 subgoals):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
 2. \<forall>i\<in>{n..<size w}. bit w i \<Longrightarrow> NOT (mask n) \<le> w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>{n..<size w}. bit w i
[PROOF STEP]
have \<open>w AND NOT (mask n) = NOT (mask n)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{n..<size w}. bit w i

goal (1 subgoal):
 1. w AND NOT (mask n) = NOT (mask n)
[PROOF STEP]
by (auto simp add: bit_simps word_size intro: bit_word_eqI)
[PROOF STATE]
proof (state)
this:
w AND NOT (mask n) = NOT (mask n)

goal (2 subgoals):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
 2. \<forall>i\<in>{n..<size w}. bit w i \<Longrightarrow> NOT (mask n) \<le> w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w AND NOT (mask n) = NOT (mask n)
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
using this:
w AND NOT (mask n) = NOT (mask n)

goal (1 subgoal):
 1. NOT (mask n) \<le> w
[PROOF STEP]
by (simp add: and_neg_mask_eq_iff_not_mask_le)
[PROOF STATE]
proof (state)
this:
NOT (mask n) \<le> w

goal (1 subgoal):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
[PROOF STEP]
assume ?P
[PROOF STATE]
proof (state)
this:
NOT (mask n) \<le> w

goal (1 subgoal):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
NOT (mask n) \<le> w
[PROOF STEP]
have *: \<open>w AND NOT (mask n) = NOT (mask n)\<close>
[PROOF STATE]
proof (prove)
using this:
NOT (mask n) \<le> w

goal (1 subgoal):
 1. w AND NOT (mask n) = NOT (mask n)
[PROOF STEP]
by (simp add: and_neg_mask_eq_iff_not_mask_le)
[PROOF STATE]
proof (state)
this:
w AND NOT (mask n) = NOT (mask n)

goal (1 subgoal):
 1. NOT (mask n) \<le> w \<Longrightarrow> \<forall>i\<in>{n..<size w}. bit w i
[PROOF STEP]
show \<open>?Q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{n..<size w}. bit w i
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>i\<in>{n..<size w}. bit w i) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> (\<forall>i\<in>{n..<size w}. bit w i)\<close>
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>i\<in>{n..<size w}. bit w i)

goal (1 subgoal):
 1. \<not> (\<forall>i\<in>{n..<size w}. bit w i) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>i\<in>{n..<size w}. bit w i)
[PROOF STEP]
obtain m where m: \<open>\<not> bit w m\<close> \<open>n \<le> m\<close> \<open>m < LENGTH('a)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i\<in>{n..<size w}. bit w i)

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>\<not> bit w m; n \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: word_size)
[PROOF STATE]
proof (state)
this:
\<not> bit w m
n \<le> m
m < LENGTH('a)

goal (1 subgoal):
 1. \<not> (\<forall>i\<in>{n..<size w}. bit w i) \<Longrightarrow> False
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
w AND NOT (mask n) = NOT (mask n)
[PROOF STEP]
have \<open>bit (w AND NOT (mask n)) m \<longleftrightarrow> bit (NOT (mask n :: 'a word)) m\<close>
[PROOF STATE]
proof (prove)
using this:
w AND NOT (mask n) = NOT (mask n)

goal (1 subgoal):
 1. bit (w AND NOT (mask n)) m = bit (NOT (mask n)) m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bit (w AND NOT (mask n)) m = bit (NOT (mask n)) m

goal (1 subgoal):
 1. \<not> (\<forall>i\<in>{n..<size w}. bit w i) \<Longrightarrow> False
[PROOF STEP]
with m
[PROOF STATE]
proof (chain)
picking this:
\<not> bit w m
n \<le> m
m < LENGTH('a)
bit (w AND NOT (mask n)) m = bit (NOT (mask n)) m
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> bit w m
n \<le> m
m < LENGTH('a)
bit (w AND NOT (mask n)) m = bit (NOT (mask n)) m

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp add: bit_simps)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{n..<size w}. bit w i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_add_less_t2n:
  "\<lbrakk>is_aligned (p::'a::len word) n; d < 2^n; n \<le> m; p < 2^m\<rbrakk> \<Longrightarrow> p + d < 2^m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply (case_tac "m < LENGTH('a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply (subst mask_eq_iff_w2p[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> m < size (p + d)
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d AND mask m = p + d
 3. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply (simp add: word_size)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d AND mask m = p + d
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply (simp add: is_aligned_add_or word_ao_dist less_mask_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p OR d AND mask m = p OR d
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply (subst less_mask_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> d < 2 ^ m
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p OR d = p OR d
 3. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply (erule order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n \<le> 2 ^ m
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p OR d = p OR d
 3. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply (erule(1) two_power_increasing)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> p OR d = p OR d
 2. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d < 2 ^ n; n \<le> m; p < 2 ^ m; \<not> m < LENGTH('a)\<rbrakk> \<Longrightarrow> p + d < 2 ^ m
[PROOF STEP]
apply (simp add: power_overflow)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_offset_non_zero:
  "\<lbrakk> is_aligned x n; y < 2 ^ n; x \<noteq> 0 \<rbrakk> \<Longrightarrow> x + y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y < 2 ^ n; x \<noteq> 0\<rbrakk> \<Longrightarrow> x + y \<noteq> 0
[PROOF STEP]
apply (cases "y = 0")
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply (subst word_neq_0_conv)
[PROOF STATE]
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 STEP]
apply (subst gt0_iff_gem1)
[PROOF STATE]
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 STEP]
apply (erule is_aligned_get_word_bits)
[PROOF STATE]
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 STEP]
apply (subst field_simps[symmetric], subst plus_le_left_cancel_nowrap)
[PROOF STATE]
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 STEP]
apply (rule is_aligned_no_wrap')
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply (rule word_leq_le_minus_one)
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
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 STEP]
apply assumption
[PROOF STATE]
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 STEP]
apply (erule (1) is_aligned_no_wrap')
[PROOF STATE]
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 STEP]
apply (simp add: gt0_iff_gem1 [symmetric] word_neq_0_conv)
[PROOF STATE]
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 STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_over_length:
  "\<lbrakk> is_aligned p n; LENGTH('a) \<le> n \<rbrakk> \<Longrightarrow> (p::'a::len word) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p = 0
[PROOF STEP]
by (simp add: is_aligned_mask mask_over_length)


[STATEMENT]
lemma is_aligned_no_overflow_mask:
  "is_aligned x n \<Longrightarrow> x \<le> x + mask n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned x n \<Longrightarrow> x \<le> x + mask n
[PROOF STEP]
by (simp add: mask_eq_decr_exp) (erule is_aligned_no_overflow')


[STATEMENT]
lemma aligned_mask_step:
  "\<lbrakk> n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n' \<rbrakk> \<Longrightarrow>
   (p'::'a::len word) + mask n' \<le> p + mask n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
[PROOF STEP]
apply (cases "LENGTH('a) \<le> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
 2. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
[PROOF STEP]
apply (frule (1) is_aligned_over_length)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; LENGTH('a) \<le> n; p = 0\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
 2. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
[PROOF STEP]
apply (drule mask_over_length)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; p = 0; mask n = - 1\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
 2. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
[PROOF STEP]
apply (simp add: not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; p' \<le> p + mask n; is_aligned p n; is_aligned p' n'; n < LENGTH('a)\<rbrakk> \<Longrightarrow> p' + mask n' \<le> p + mask n
[PROOF STEP]
apply (simp add: word_le_nat_alt unat_plus_simple)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; unat p' \<le> unat (p + mask n); is_aligned p n; is_aligned p' n'; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (p' + mask n') \<le> unat (p + mask n)
[PROOF STEP]
apply (subst unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; unat p' \<le> unat (p + mask n); is_aligned p n; is_aligned p' n'; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat p' + unat (mask n') \<le> unat p + unat (mask n)
[PROOF STEP]
apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' \<le> n; unat p' \<le> unat p + unat (mask n); is_aligned p n; is_aligned p' n'; n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat p' + unat (mask n') \<le> unat p + unat (mask n)
[PROOF STEP]
apply (clarsimp simp: dvd_def is_aligned_iff_dvd_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k ka. \<lbrakk>n' \<le> n; 2 ^ n' * ka \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a); unat p = 2 ^ n * k; unat p' = 2 ^ n' * ka\<rbrakk> \<Longrightarrow> 2 ^ n' * ka + unat (mask n') \<le> 2 ^ n * k + unat (mask n)
[PROOF STEP]
apply (rename_tac k k')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; 2 ^ n' * k' \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a); unat p = 2 ^ n * k; unat p' = 2 ^ n' * k'\<rbrakk> \<Longrightarrow> 2 ^ n' * k' + unat (mask n') \<le> 2 ^ n * k + unat (mask n)
[PROOF STEP]
apply (thin_tac "unat p = x" for p x)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; 2 ^ n' * k' \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n' * k' + unat (mask n') \<le> 2 ^ n * k + unat (mask n)
[PROOF STEP]
apply (subst Suc_le_mono[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; 2 ^ n' * k' \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> Suc (2 ^ n' * k' + unat (mask n')) \<le> Suc (2 ^ n * k + unat (mask n))
[PROOF STEP]
apply (simp only: Suc_2p_unat_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; 2 ^ n' * k' \<le> 2 ^ n * k + unat (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * (k + 1)
[PROOF STEP]
apply (drule le_imp_less_Suc, subst (asm) Suc_2p_unat_mask, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k k'. \<lbrakk>n' \<le> n; n < LENGTH('a); 2 ^ n' * k' < 2 ^ n * (k + 1)\<rbrakk> \<Longrightarrow> 2 ^ n' * (k' + 1) \<le> 2 ^ n * (k + 1)
[PROOF STEP]
apply (erule (1) power_2_mult_step_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_mask_offset_unat:
  fixes off :: "('a::len) word"
  and     x :: "'a word"
  assumes al: "is_aligned x sz"
  and   offv: "off \<le> mask sz"
  shows  "unat x + unat off < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
 2. \<not> ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
assume szv: "sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
 2. \<not> ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
is_aligned x sz
[PROOF STEP]
obtain k where xv: "x = 2 ^ sz * (of_nat k)"
    and kl: "k < 2 ^ (LENGTH('a) - sz)"
[PROOF STATE]
proof (prove)
using this:
is_aligned x sz

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>x = 2 ^ sz * word_of_nat k; k < 2 ^ (LENGTH('a) - sz)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_alignedE)
[PROOF STATE]
proof (state)
this:
x = 2 ^ sz * word_of_nat k
k < 2 ^ (LENGTH('a) - sz)

goal (2 subgoals):
 1. ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
 2. \<not> ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
from offv szv
[PROOF STATE]
proof (chain)
picking this:
off \<le> mask sz
sz < LENGTH('a)
[PROOF STEP]
have offv': "unat off < 2 ^ sz"
[PROOF STATE]
proof (prove)
using this:
off \<le> mask sz
sz < LENGTH('a)

goal (1 subgoal):
 1. unat off < 2 ^ sz
[PROOF STEP]
by (simp add: mask_2pm1 unat_less_power)
[PROOF STATE]
proof (state)
this:
unat off < 2 ^ sz

goal (2 subgoals):
 1. ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
 2. \<not> ?P \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
using szv
[PROOF STATE]
proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
using al is_aligned_no_wrap''' offv'
[PROOF STATE]
proof (prove)
using this:
sz < LENGTH('a)
is_aligned x sz
\<lbrakk>is_aligned ?ptr ?sz; ?sz < LENGTH(?'a); ?off < 2 ^ ?sz\<rbrakk> \<Longrightarrow> unat ?ptr + ?off < 2 ^ LENGTH(?'a)
unat off < 2 ^ sz

goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
unat x + unat off < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
assume "\<not> sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
with al
[PROOF STATE]
proof (chain)
picking this:
is_aligned x sz
\<not> sz < LENGTH('a)
[PROOF STEP]
have "x = 0"
[PROOF STATE]
proof (prove)
using this:
is_aligned x sz
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. x = 0
[PROOF STEP]
by (meson is_aligned_get_word_bits)
[PROOF STATE]
proof (state)
this:
x = 0

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. unat x + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
unat x + unat off < 2 ^ LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aligned_less_plus_1:
  "\<lbrakk> is_aligned x n; n > 0 \<rbrakk> \<Longrightarrow> x < x + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 0 < n\<rbrakk> \<Longrightarrow> x < x + 1
[PROOF STEP]
apply (rule plus_one_helper2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; 0 < n\<rbrakk> \<Longrightarrow> x \<le> x
 2. \<lbrakk>is_aligned x n; 0 < n\<rbrakk> \<Longrightarrow> x + 1 \<noteq> 0
[PROOF STEP]
apply (rule order_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 0 < n\<rbrakk> \<Longrightarrow> x + 1 \<noteq> 0
[PROOF STEP]
apply (clarsimp simp: field_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 0 < n; 1 + x = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule arg_cong[where f="\<lambda>x. x - 1"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 0 < n; 1 + x - 1 = 0 - 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp simp: is_aligned_mask)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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


[STATEMENT]
lemma gap_between_aligned:
  "\<lbrakk>a < (b :: 'a ::len word); is_aligned a n; is_aligned b n; n < LENGTH('a) \<rbrakk>
  \<Longrightarrow> a + (2^n - 1) < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; is_aligned a n; is_aligned b n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a + (2 ^ n - 1) < b
[PROOF STEP]
by (simp add: aligned_add_offset_less)


[STATEMENT]
lemma is_aligned_add_step_le:
  "\<lbrakk> is_aligned (a::'a::len word) n; is_aligned b n; a < b; b \<le> a + mask n \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; a < b; b \<le> a + mask n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp flip: not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; \<not> b \<le> a; b \<le> a + mask n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n\<rbrakk> \<Longrightarrow> b \<le> a
[PROOF STEP]
apply (cases "LENGTH('a) \<le> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a
 2. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a
[PROOF STEP]
apply (drule (1) is_aligned_over_length)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<le> a + mask n; LENGTH('a) \<le> n; a = 0; b = 0\<rbrakk> \<Longrightarrow> b \<le> a
 2. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a
[PROOF STEP]
apply (drule mask_over_length)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<le> a + mask n; a = 0; b = 0; mask n = - 1\<rbrakk> \<Longrightarrow> b \<le> a
 2. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; b \<le> a + mask n; \<not> LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> b \<le> a
[PROOF STEP]
apply (clarsimp simp: word_le_nat_alt not_less not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; unat b \<le> unat (a + mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat b \<le> unat a
[PROOF STEP]
apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; unat b \<le> unat a + unat (mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat b \<le> unat a
[PROOF STEP]
apply (subst (asm) unat_add_lem' [symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); is_aligned a n; is_aligned b n\<rbrakk> \<Longrightarrow> unat a + unat (mask n) < 2 ^ LENGTH('a)
 2. \<lbrakk>is_aligned a n; is_aligned b n; unat b \<le> unat (a + mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat b \<le> unat a
[PROOF STEP]
apply (simp add: is_aligned_mask_offset_unat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; is_aligned b n; unat b \<le> unat (a + mask n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat b \<le> unat a
[PROOF STEP]
apply (metis gap_between_aligned linorder_not_less mask_eq_decr_exp unat_arith_simps(2))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_add_mask_lessD:
  "\<lbrakk> x + mask n < y; is_aligned x n \<rbrakk> \<Longrightarrow> x < y" for y::"'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x + mask n < y; is_aligned x n\<rbrakk> \<Longrightarrow> x < y
[PROOF STEP]
by (metis is_aligned_no_overflow' mask_2pm1 order_le_less_trans)


[STATEMENT]
lemma aligned_add_mask_less_eq:
  "\<lbrakk> is_aligned x n; is_aligned y n;  n < LENGTH('a) \<rbrakk> \<Longrightarrow> (x + mask n < y) = (x < y)"
  for y::"'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x + mask n < y) = (x < y)
[PROOF STEP]
using aligned_add_mask_lessD is_aligned_add_step_le word_le_not_less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x + mask ?n < ?y; is_aligned ?x ?n\<rbrakk> \<Longrightarrow> ?x < ?y
\<lbrakk>is_aligned ?a ?n; is_aligned ?b ?n; ?a < ?b; ?b \<le> ?a + mask ?n\<rbrakk> \<Longrightarrow> False
(?b \<le> ?a) = (\<not> ?a < ?b)

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (x + mask n < y) = (x < y)
[PROOF STEP]
by blast