[STATEMENT]
lemma word_ctz_unfold':
  \<open>word_ctz w = Min (insert LENGTH('a) {n. bit w n})\<close> for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
proof (cases \<open>\<exists>n. bit w n\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
 2. \<nexists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>n. bit w n

goal (2 subgoals):
 1. \<exists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
 2. \<nexists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. bit w n
[PROOF STEP]
obtain n where \<open>bit w n\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>n. bit w n

goal (1 subgoal):
 1. (\<And>n. bit w n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
bit w n

goal (2 subgoals):
 1. \<exists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
 2. \<nexists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
from \<open>bit w n\<close>
[PROOF STATE]
proof (chain)
picking this:
bit w n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bit w n

goal (1 subgoal):
 1. word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
apply (simp add: word_ctz_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w n \<Longrightarrow> length (takeWhile (Not \<circ> bit w) [0..<LENGTH('a)]) = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
apply (subst Min_eq_length_takeWhile [symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>bit w n; bit w m\<rbrakk> \<Longrightarrow> m < LENGTH('a)
 2. bit w n \<Longrightarrow> Ex (bit w)
 3. bit w n \<Longrightarrow> Min (Collect (bit w)) = Min (insert LENGTH('a) (Collect (bit w)))
[PROOF STEP]
apply (auto simp add: bit_imp_le_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w n \<Longrightarrow> Min (Collect (bit w)) = Min (insert LENGTH('a) (Collect (bit w)))
[PROOF STEP]
apply (subst Min_insert)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. bit w n \<Longrightarrow> finite (Collect (bit w))
 2. bit w n \<Longrightarrow> Collect (bit w) \<noteq> {}
 3. bit w n \<Longrightarrow> Min (Collect (bit w)) = min LENGTH('a) (Min (Collect (bit w)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w n \<Longrightarrow> Min (Collect (bit w)) = min LENGTH('a) (Min (Collect (bit w)))
[PROOF STEP]
apply (subst min.absorb2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bit w n \<Longrightarrow> Min (Collect (bit w)) \<le> LENGTH('a)
 2. bit w n \<Longrightarrow> Min (Collect (bit w)) = Min (Collect (bit w))
[PROOF STEP]
apply (subst Min_le_iff)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. bit w n \<Longrightarrow> finite (Collect (bit w))
 2. bit w n \<Longrightarrow> Collect (bit w) \<noteq> {}
 3. bit w n \<Longrightarrow> \<exists>a\<in>Collect (bit w). a \<le> LENGTH('a)
 4. bit w n \<Longrightarrow> Min (Collect (bit w)) = Min (Collect (bit w))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w n \<Longrightarrow> \<exists>a. bit w a \<and> a \<le> LENGTH('a)
[PROOF STEP]
apply (meson bit_imp_le_length order_less_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
word_ctz w = Min (insert LENGTH('a) {n. bit w n})

goal (1 subgoal):
 1. \<nexists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>n. bit w n

goal (1 subgoal):
 1. \<nexists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>n. bit w n
[PROOF STEP]
have \<open>bit w = bot\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>n. bit w n

goal (1 subgoal):
 1. bit w = bot
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bit w = bot

goal (1 subgoal):
 1. \<nexists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bit w = bot
[PROOF STEP]
have \<open>word_ctz w = LENGTH('a)\<close>
[PROOF STATE]
proof (prove)
using this:
bit w = bot

goal (1 subgoal):
 1. word_ctz w = LENGTH('a)
[PROOF STEP]
by (simp add: word_ctz_def rev_to_bl_eq bot_fun_def map_replicate_const)
[PROOF STATE]
proof (state)
this:
word_ctz w = LENGTH('a)

goal (1 subgoal):
 1. \<nexists>n. bit w n \<Longrightarrow> word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
with \<open>bit w = bot\<close>
[PROOF STATE]
proof (chain)
picking this:
bit w = bot
word_ctz w = LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bit w = bot
word_ctz w = LENGTH('a)

goal (1 subgoal):
 1. word_ctz w = Min (insert LENGTH('a) {n. bit w n})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
word_ctz w = Min (insert LENGTH('a) {n. bit w n})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_ctz_le:
  "word_ctz (w :: ('a::len word)) \<le> LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_ctz w \<le> LENGTH('a)
[PROOF STEP]
apply (clarsimp simp: word_ctz_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (rev (to_bl w))) \<le> LENGTH('a)
[PROOF STEP]
using length_takeWhile_le
[PROOF STATE]
proof (prove)
using this:
length (takeWhile ?P ?xs) \<le> length ?xs

goal (1 subgoal):
 1. length (takeWhile Not (rev (to_bl w))) \<le> LENGTH('a)
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (rev (to_bl w)) \<le> LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_ctz_less:
  "w \<noteq> 0 \<Longrightarrow> word_ctz (w :: ('a::len word)) < LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_ctz w < LENGTH('a)
[PROOF STEP]
apply (clarsimp simp: word_ctz_def eq_zero_set_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<in> set (to_bl w) \<Longrightarrow> length (takeWhile Not (rev (to_bl w))) < LENGTH('a)
[PROOF STEP]
using length_takeWhile_less
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>set ?xs. \<not> ?P x \<Longrightarrow> length (takeWhile ?P ?xs) < length ?xs

goal (1 subgoal):
 1. True \<in> set (to_bl w) \<Longrightarrow> length (takeWhile Not (rev (to_bl w))) < LENGTH('a)
[PROOF STEP]
apply (rule less_le_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True \<in> set (to_bl w) \<Longrightarrow> \<exists>x\<in>set (rev (to_bl w)). \<not> \<not> x
 2. True \<in> set (to_bl w) \<Longrightarrow> length (rev (to_bl w)) \<le> LENGTH('a)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma take_bit_word_ctz_eq [simp]:
  \<open>take_bit LENGTH('a) (word_ctz w) = word_ctz w\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit LENGTH('a) (word_ctz w) = word_ctz w
[PROOF STEP]
apply (simp add: take_bit_nat_eq_self_iff word_ctz_def to_bl_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (map (bit w) [0..<LENGTH('a)])) < 2 ^ LENGTH('a)
[PROOF STEP]
using length_takeWhile_le
[PROOF STATE]
proof (prove)
using this:
length (takeWhile ?P ?xs) \<le> length ?xs

goal (1 subgoal):
 1. length (takeWhile Not (map (bit w) [0..<LENGTH('a)])) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule le_less_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (bit w) [0..<LENGTH('a)]) < 2 ^ LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_ctz_not_minus_1:
  \<open>word_of_nat (word_ctz (w :: 'a :: len word)) \<noteq> (- 1 :: 'a::len word)\<close> if \<open>1 < LENGTH('a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
note word_ctz_le
[PROOF STATE]
proof (state)
this:
word_ctz ?w \<le> LENGTH(?'a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
word_ctz ?w \<le> LENGTH(?'a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
1 < LENGTH('a)
[PROOF STEP]
have \<open>LENGTH('a) < mask LENGTH('a)\<close>
[PROOF STATE]
proof (prove)
using this:
1 < LENGTH('a)

goal (1 subgoal):
 1. LENGTH('a) < mask LENGTH('a)
[PROOF STEP]
by (simp add: less_mask)
[PROOF STATE]
proof (state)
this:
LENGTH('a) < mask LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
word_ctz ?w1 < mask LENGTH('a)
[PROOF STEP]
have \<open>word_ctz w < mask LENGTH('a)\<close>
[PROOF STATE]
proof (prove)
using this:
word_ctz ?w1 < mask LENGTH('a)

goal (1 subgoal):
 1. word_ctz w < mask LENGTH('a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
word_ctz w < mask LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
word_ctz w < mask LENGTH('a)
[PROOF STEP]
have \<open>word_of_nat (word_ctz w) < (word_of_nat (mask LENGTH('a)) :: 'a word)\<close>
[PROOF STATE]
proof (prove)
using this:
word_ctz w < mask LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (word_ctz w) < word_of_nat (mask LENGTH('a))
[PROOF STEP]
by (simp add: of_nat_word_less_iff)
[PROOF STATE]
proof (state)
this:
word_of_nat (word_ctz w) < word_of_nat (mask LENGTH('a))

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
word_of_nat (word_ctz w) < word_of_nat (mask LENGTH('a))

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
have \<open>\<dots> = - 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_of_nat (mask LENGTH('a)) = - 1
[PROOF STEP]
by (rule bit_word_eqI) (simp add: bit_simps)
[PROOF STATE]
proof (state)
this:
word_of_nat (mask LENGTH('a)) = - 1

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
word_of_nat (word_ctz w) < - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
word_of_nat (word_ctz w) < - 1

goal (1 subgoal):
 1. word_of_nat (word_ctz w) \<noteq> - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
word_of_nat (word_ctz w) \<noteq> - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unat_of_nat_ctz_mw:
  "unat (of_nat (word_ctz (w :: 'a :: len word)) :: 'a :: len word) = word_ctz w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat (word_ctz w)) = word_ctz w
[PROOF STEP]
by (simp add: unsigned_of_nat)


[STATEMENT]
lemma unat_of_nat_ctz_smw:
  "unat (of_nat (word_ctz (w :: 'a :: len word)) :: 'a :: len signed word) = word_ctz w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat (word_ctz w)) = word_ctz w
[PROOF STEP]
by (simp add: unsigned_of_nat)


[STATEMENT]
lemma sign_extend_eq_signed_take_bit:
  \<open>sign_extend = signed_take_bit\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_extend = signed_take_bit
[PROOF STEP]
proof (rule ext)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. sign_extend x xa = signed_take_bit x xa
[PROOF STEP]
fix n and w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. sign_extend x xa = signed_take_bit x xa
[PROOF STEP]
show \<open>sign_extend n w = signed_take_bit n w\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_extend n w = signed_take_bit n w
[PROOF STEP]
proof (rule bit_word_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (sign_extend n w) na = bit (signed_take_bit n w) na
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (sign_extend n w) na = bit (signed_take_bit n w) na
[PROOF STEP]
assume \<open>q < LENGTH('a)\<close>
[PROOF STATE]
proof (state)
this:
q < LENGTH('a)

goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (sign_extend n w) na = bit (signed_take_bit n w) na
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q < LENGTH('a)
[PROOF STEP]
show \<open>bit (sign_extend n w) q \<longleftrightarrow> bit (signed_take_bit n w) q\<close>
[PROOF STATE]
proof (prove)
using this:
q < LENGTH('a)

goal (1 subgoal):
 1. bit (sign_extend n w) q = bit (signed_take_bit n w) q
[PROOF STEP]
by (auto simp add: bit_signed_take_bit_iff
        sign_extend_def bit_and_iff bit_or_iff bit_not_iff bit_mask_iff not_less
        exp_eq_0_imp_not_bit not_le min_def)
[PROOF STATE]
proof (state)
this:
bit (sign_extend n w) q = bit (signed_take_bit n w) q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sign_extend n w = signed_take_bit n w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ptr_add_0 [simp]:
  "ptr_add ref 0 = ref "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptr_add ref 0 = ref
[PROOF STEP]
unfolding ptr_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref + word_of_nat 0 = ref
[PROOF STEP]
by simp


[STATEMENT]
lemma pop_count_0[simp]:
  "pop_count 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pop_count 0 = 0
[PROOF STEP]
by (clarsimp simp:pop_count_def)


[STATEMENT]
lemma pop_count_1[simp]:
  "pop_count 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pop_count 1 = 1
[PROOF STEP]
by (clarsimp simp:pop_count_def to_bl_1)


[STATEMENT]
lemma pop_count_0_imp_0:
  "(pop_count w = 0) = (w = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pop_count w = 0) = (w = 0)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pop_count w = 0 \<Longrightarrow> w = 0
 2. w = 0 \<Longrightarrow> pop_count w = 0
[PROOF STEP]
apply (clarsimp simp:pop_count_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. filter id (to_bl w) = [] \<Longrightarrow> w = 0
 2. w = 0 \<Longrightarrow> pop_count w = 0
[PROOF STEP]
apply (subst (asm) filter_empty_conv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set (to_bl w). \<not> id x \<Longrightarrow> w = 0
 2. w = 0 \<Longrightarrow> pop_count w = 0
[PROOF STEP]
apply (clarsimp simp:eq_zero_set_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set (to_bl w). \<not> x; True \<in> set (to_bl w)\<rbrakk> \<Longrightarrow> False
 2. w = 0 \<Longrightarrow> pop_count w = 0
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = 0 \<Longrightarrow> pop_count w = 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_log2_zero_eq [simp]:
  \<open>word_log2 0 = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_log2 0 = 0
[PROOF STEP]
by (simp add: word_log2_def word_clz_def word_size)


[STATEMENT]
lemma word_log2_unfold:
  \<open>word_log2 w = (if w = 0 then 0 else Max {n. bit w n})\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
proof (cases \<open>w = 0\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w = 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
 2. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w = 0

goal (2 subgoals):
 1. w = 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
 2. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w = 0

goal (1 subgoal):
 1. word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
word_log2 w = (if w = 0 then 0 else Max {n. bit w n})

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
w \<noteq> 0

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> 0
[PROOF STEP]
obtain r where \<open>bit w r\<close>
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0

goal (1 subgoal):
 1. (\<And>r. bit w r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: bit_eq_iff)
[PROOF STATE]
proof (state)
this:
bit w r

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bit w r
[PROOF STEP]
have \<open>Max {m. bit w m} = LENGTH('a) - Suc (length
    (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)])))\<close>
[PROOF STATE]
proof (prove)
using this:
bit w r

goal (1 subgoal):
 1. Max {m. bit w m} = LENGTH('a) - Suc (length (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)])))
[PROOF STEP]
by (subst Max_eq_length_takeWhile [of _ \<open>LENGTH('a)\<close>])
      (auto simp add: bit_imp_le_length)
[PROOF STATE]
proof (state)
this:
Max {m. bit w m} = LENGTH('a) - Suc (length (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)])))

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Max {m. bit w m} = LENGTH('a) - Suc (length (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)])))
[PROOF STEP]
have \<open>word_log2 w = Max {x. bit w x}\<close>
[PROOF STATE]
proof (prove)
using this:
Max {m. bit w m} = LENGTH('a) - Suc (length (takeWhile (Not \<circ> bit w) (rev [0..<LENGTH('a)])))

goal (1 subgoal):
 1. word_log2 w = Max {x. bit w x}
[PROOF STEP]
by (simp add: word_log2_def word_clz_def word_size to_bl_unfold rev_map takeWhile_map)
[PROOF STATE]
proof (state)
this:
word_log2 w = Max {x. bit w x}

goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
with \<open>w \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> 0
word_log2 w = Max {x. bit w x}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0
word_log2 w = Max {x. bit w x}

goal (1 subgoal):
 1. word_log2 w = (if w = 0 then 0 else Max {n. bit w n})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
word_log2 w = (if w = 0 then 0 else Max {n. bit w n})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_log2_eqI:
  \<open>word_log2 w = n\<close>
  if \<open>w \<noteq> 0\<close> \<open>bit w n\<close> \<open>\<And>m. bit w m \<Longrightarrow> m \<le> n\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_log2 w = n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_log2 w = n
[PROOF STEP]
from \<open>w \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> 0
[PROOF STEP]
have \<open>word_log2 w = Max {n. bit w n}\<close>
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0

goal (1 subgoal):
 1. word_log2 w = Max {n. bit w n}
[PROOF STEP]
by (simp add: word_log2_unfold)
[PROOF STATE]
proof (state)
this:
word_log2 w = Max {n. bit w n}

goal (1 subgoal):
 1. word_log2 w = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
word_log2 w = Max {n. bit w n}

goal (1 subgoal):
 1. word_log2 w = n
[PROOF STEP]
have \<open>Max {n. bit w n} = n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max {n. bit w n} = n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0
bit w n
bit w ?m \<Longrightarrow> ?m \<le> n

goal (1 subgoal):
 1. Max {n. bit w n} = n
[PROOF STEP]
by (auto intro: Max_eqI)
[PROOF STATE]
proof (state)
this:
Max {n. bit w n} = n

goal (1 subgoal):
 1. word_log2 w = n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
word_log2 w = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
word_log2 w = n

goal (1 subgoal):
 1. word_log2 w = n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
word_log2 w = n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bit_word_log2:
  \<open>bit w (word_log2 w)\<close> if \<open>w \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w (word_log2 w)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bit w (word_log2 w)
[PROOF STEP]
from \<open>w \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> 0
[PROOF STEP]
have \<open>\<exists>r. bit w r\<close>
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0

goal (1 subgoal):
 1. \<exists>r. bit w r
[PROOF STEP]
by (auto intro: bit_eqI)
[PROOF STATE]
proof (state)
this:
\<exists>r. bit w r

goal (1 subgoal):
 1. bit w (word_log2 w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r. bit w r
[PROOF STEP]
obtain r where \<open>bit w r\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>r. bit w r

goal (1 subgoal):
 1. (\<And>r. bit w r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
bit w r

goal (1 subgoal):
 1. bit w (word_log2 w)
[PROOF STEP]
from \<open>w \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> 0
[PROOF STEP]
have \<open>word_log2 w = Max {n. bit w n}\<close>
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0

goal (1 subgoal):
 1. word_log2 w = Max {n. bit w n}
[PROOF STEP]
by (simp add: word_log2_unfold)
[PROOF STATE]
proof (state)
this:
word_log2 w = Max {n. bit w n}

goal (1 subgoal):
 1. bit w (word_log2 w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
word_log2 w = Max {n. bit w n}

goal (1 subgoal):
 1. bit w (word_log2 w)
[PROOF STEP]
have \<open>Max {n. bit w n} \<in> {n. bit w n}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max {n. bit w n} \<in> {n. bit w n}
[PROOF STEP]
using \<open>bit w r\<close>
[PROOF STATE]
proof (prove)
using this:
bit w r

goal (1 subgoal):
 1. Max {n. bit w n} \<in> {n. bit w n}
[PROOF STEP]
by (subst Max_in) auto
[PROOF STATE]
proof (state)
this:
Max {n. bit w n} \<in> {n. bit w n}

goal (1 subgoal):
 1. bit w (word_log2 w)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
word_log2 w \<in> {n. bit w n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
word_log2 w \<in> {n. bit w n}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_log2_maximum:
  \<open>n \<le> word_log2 w\<close> if \<open>bit w n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> word_log2 w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<le> word_log2 w
[PROOF STEP]
have \<open>n \<le> Max {n. bit w n}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> Max {n. bit w n}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
bit w n

goal (1 subgoal):
 1. n \<le> Max {n. bit w n}
[PROOF STEP]
by (auto intro: Max_ge)
[PROOF STATE]
proof (state)
this:
n \<le> Max {n. bit w n}

goal (1 subgoal):
 1. n \<le> word_log2 w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n \<le> Max {n. bit w n}

goal (1 subgoal):
 1. n \<le> word_log2 w
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
bit w n
[PROOF STEP]
have \<open>w \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
bit w n

goal (1 subgoal):
 1. w \<noteq> 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
w \<noteq> 0

goal (1 subgoal):
 1. n \<le> word_log2 w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> 0
[PROOF STEP]
have \<open>Max {n. bit w n} = word_log2 w\<close>
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0

goal (1 subgoal):
 1. Max {n. bit w n} = word_log2 w
[PROOF STEP]
by (simp add: word_log2_unfold)
[PROOF STATE]
proof (state)
this:
Max {n. bit w n} = word_log2 w

goal (1 subgoal):
 1. n \<le> word_log2 w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n \<le> word_log2 w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<le> word_log2 w

goal (1 subgoal):
 1. n \<le> word_log2 w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
n \<le> word_log2 w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_log2_nth_same:
  "w \<noteq> 0 \<Longrightarrow> bit w (word_log2 w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> bit w (word_log2 w)
[PROOF STEP]
by (drule bit_word_log2) simp


[STATEMENT]
lemma word_log2_nth_not_set:
  "\<lbrakk> word_log2 w < i ; i < size w \<rbrakk> \<Longrightarrow> \<not> bit w i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_log2 w < i; i < size w\<rbrakk> \<Longrightarrow> \<not> bit w i
[PROOF STEP]
using word_log2_maximum [of w i]
[PROOF STATE]
proof (prove)
using this:
bit w i \<Longrightarrow> i \<le> word_log2 w

goal (1 subgoal):
 1. \<lbrakk>word_log2 w < i; i < size w\<rbrakk> \<Longrightarrow> \<not> bit w i
[PROOF STEP]
by auto


[STATEMENT]
lemma word_log2_highest:
  assumes a: "bit w i"
  shows "i \<le> word_log2 w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> word_log2 w
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
bit w i

goal (1 subgoal):
 1. i \<le> word_log2 w
[PROOF STEP]
by (simp add: word_log2_maximum)


[STATEMENT]
lemma word_log2_max:
  "word_log2 w < size w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_log2 w < size w
[PROOF STEP]
apply (cases \<open>w = 0\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. w = 0 \<Longrightarrow> word_log2 w < size w
 2. w \<noteq> 0 \<Longrightarrow> word_log2 w < size w
[PROOF STEP]
apply (simp_all add: word_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_log2 w < LENGTH('a)
[PROOF STEP]
apply (drule bit_word_log2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w (word_log2 w) \<Longrightarrow> word_log2 w < LENGTH('a)
[PROOF STEP]
apply (fact bit_imp_le_length)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_clz_0[simp]:
  "word_clz (0::'a::len word) = LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_clz 0 = LENGTH('a)
[PROOF STEP]
unfolding word_clz_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (to_bl 0)) = LENGTH('a)
[PROOF STEP]
by simp


[STATEMENT]
lemma word_clz_minus_one[simp]:
  "word_clz (-1::'a::len word) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_clz (- 1) = 0
[PROOF STEP]
unfolding word_clz_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (to_bl (- 1))) = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma is_aligned_alignUp[simp]:
  "is_aligned (alignUp p n) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (alignUp p n) n
[PROOF STEP]
by (simp add: alignUp_def is_aligned_mask mask_eq_decr_exp word_bw_assocs)


[STATEMENT]
lemma alignUp_le[simp]:
  "alignUp p n \<le> p + 2 ^ n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp p n \<le> p + 2 ^ n - 1
[PROOF STEP]
unfolding alignUp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p + 2 ^ n - 1 AND NOT (2 ^ n - 1) \<le> p + 2 ^ n - 1
[PROOF STEP]
by (rule word_and_le2)


[STATEMENT]
lemma alignUp_idem:
  fixes a :: "'a::len word"
  assumes "is_aligned a n" "n < LENGTH('a)"
  shows "alignUp a n = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a n = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_aligned a n
n < LENGTH('a)

goal (1 subgoal):
 1. alignUp a n = a
[PROOF STEP]
unfolding alignUp_def
[PROOF STATE]
proof (prove)
using this:
is_aligned a n
n < LENGTH('a)

goal (1 subgoal):
 1. a + 2 ^ n - 1 AND NOT (2 ^ n - 1) = a
[PROOF STEP]
by (metis add_cancel_right_right add_diff_eq and_mask_eq_iff_le_mask mask_eq_decr_exp mask_out_add_aligned order_refl word_plus_and_or_coroll2)


[STATEMENT]
lemma alignUp_not_aligned_eq:
  fixes a :: "'a :: len word"
  assumes al: "\<not> is_aligned a n"
  and     sz: "n < LENGTH('a)"
  shows   "alignUp a n = (a div 2 ^ n + 1) * 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
have anz: "a mod 2 ^ n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n \<noteq> 0
[PROOF STEP]
by (rule not_aligned_mod_nz) fact+
[PROOF STATE]
proof (state)
this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod 2 ^ n \<noteq> 0
[PROOF STEP]
have um: "unat (a mod 2 ^ n - 1) div 2 ^ n = 0"
[PROOF STATE]
proof (prove)
using this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. unat (a mod 2 ^ n - 1) div 2 ^ n = 0
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
a mod 2 ^ n \<noteq> 0
n < LENGTH('a)

goal (1 subgoal):
 1. unat (a mod 2 ^ n - 1) div 2 ^ n = 0
[PROOF STEP]
by (meson Euclidean_Division.div_eq_0_iff le_m1_iff_lt measure_unat order_less_trans
              unat_less_power word_less_sub_le word_mod_less_divisor)
[PROOF STATE]
proof (state)
this:
unat (a mod 2 ^ n - 1) div 2 ^ n = 0

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
have "a + 2 ^ n - 1 = (a div 2 ^ n) * 2 ^ n + (a mod 2 ^ n) + 2 ^ n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + 2 ^ n - 1 = a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1
[PROOF STEP]
by (simp add: word_mod_div_equality)
[PROOF STATE]
proof (state)
this:
a + 2 ^ n - 1 = a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a + 2 ^ n - 1 = a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
have "\<dots> = (a mod 2 ^ n - 1) + (a div 2 ^ n + 1) * 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
a div 2 ^ n * 2 ^ n + a mod 2 ^ n + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
show "alignUp a n = (a div 2 ^ n + 1) * 2 ^ n"
[PROOF STATE]
proof (prove)
using this:
a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n
n < LENGTH('a)

goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
unfolding alignUp_def
[PROOF STATE]
proof (prove)
using this:
a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n
n < LENGTH('a)

goal (1 subgoal):
 1. a + 2 ^ n - 1 AND NOT (2 ^ n - 1) = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
apply (subst mask_eq_decr_exp [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + 2 ^ n - 1 = a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a + 2 ^ n - 1 AND NOT (mask n) = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
apply (erule ssubst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n AND NOT (mask n) = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
apply (subst neg_mask_is_div)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> (a mod 2 ^ n - 1 + (a div 2 ^ n + 1) * 2 ^ n) div 2 ^ n * 2 ^ n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
apply (simp add: word_arith_nat_div)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (unat (a mod 2 ^ n - 1 + (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst unat_word_ariths(1) unat_word_ariths(2))+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + (unat (word_of_nat (unat a div 2 ^ n)) + unat 1) mod 2 ^ LENGTH('a) * unat (2 ^ n) mod 2 ^ LENGTH('a)) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst uno_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + (unat a div 2 ^ n + unat 1) mod 2 ^ LENGTH('a) * unat (2 ^ n) mod 2 ^ LENGTH('a)) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst unat_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + (unat a div 2 ^ n + 1) mod 2 ^ LENGTH('a) * unat (2 ^ n) mod 2 ^ LENGTH('a)) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst mod_add_right_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + (unat a div 2 ^ n + 1) mod 2 ^ LENGTH('a) * unat (2 ^ n)) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) * 2 ^ n) mod 2 ^ LENGTH('a) div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst power_mod_div)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((unat (a mod 2 ^ n - 1) + Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) * 2 ^ n) div 2 ^ n mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst div_mult_self1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n \<noteq> 0
 2. n < LENGTH('a) \<Longrightarrow> word_of_nat ((Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) + unat (a mod 2 ^ n - 1) div 2 ^ n) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) + unat (a mod 2 ^ n - 1) div 2 ^ n) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst um)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat ((Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) + 0) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) mod 2 ^ LENGTH('a) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst mod_mod_power)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) mod 2 ^ min LENGTH('a) (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) mod 2 ^ (LENGTH('a) - n)) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst word_unat_power, subst Abs_fnat_hom_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) mod 2 ^ (LENGTH('a) - n) * 2 ^ n) = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst mult_mod_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) * 2 ^ n mod (2 ^ (LENGTH('a) - n) * 2 ^ n)) = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst power_add [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> word_of_nat (Suc (unat a div 2 ^ n) * 2 ^ n mod 2 ^ (LENGTH('a) - n + n)) = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + 1) * 2 ^ n
[PROOF STEP]
apply (subst Abs_fnat_hom_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n) * 2 ^ n = (word_of_nat (unat a div 2 ^ n) + word_of_nat (Suc 0)) * 2 ^ n
[PROOF STEP]
apply (subst Abs_fnat_hom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n) * 2 ^ n = word_of_nat (unat a div 2 ^ n + Suc 0) * 2 ^ n
[PROOF STEP]
apply (subst word_unat_power, subst Abs_fnat_hom_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n * 2 ^ n) = word_of_nat (unat a div 2 ^ n + Suc 0) * 2 ^ n
[PROOF STEP]
apply (subst word_unat.Rep_inverse[symmetric], subst Abs_fnat_hom_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> 2 ^ n + word_of_nat (unat a div 2 ^ n * 2 ^ n) = word_of_nat ((unat a div 2 ^ n + Suc 0) * unat (2 ^ n))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
alignUp a n = (a div 2 ^ n + 1) * 2 ^ n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alignUp_ge:
  fixes a :: "'a :: len word"
  assumes sz: "n < LENGTH('a)"
  and nowrap: "alignUp a n \<noteq> 0"
  shows "a \<le> alignUp a n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> alignUp a n
[PROOF STEP]
proof (cases "is_aligned a n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> a \<le> alignUp a n
 2. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_aligned a n

goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> a \<le> alignUp a n
 2. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_aligned a n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_aligned a n

goal (1 subgoal):
 1. a \<le> alignUp a n
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
is_aligned a n
n < LENGTH('a)

goal (1 subgoal):
 1. a \<le> alignUp a n
[PROOF STEP]
by (subst alignUp_idem, simp_all)
[PROOF STATE]
proof (state)
this:
a \<le> alignUp a n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_aligned a n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
have lt0: "unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
by (metis le_add_diff_inverse2 less_mult_imp_div_less order_less_imp_le power_add unsigned_less)
[PROOF STATE]
proof (state)
this:
unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
have"2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
[PROOF STEP]
by (metis One_nat_def Suc_leI add.right_neutral add_Suc_right lt0 nat_le_power_trans nat_less_le)
[PROOF STATE]
proof (state)
this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
have "2 ^ n * (unat a div 2 ^ n + 1) \<noteq> 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) \<noteq> 2 ^ LENGTH('a)
[PROOF STEP]
using nowrap sz
[PROOF STATE]
proof (prove)
using this:
alignUp a n \<noteq> 0
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) \<noteq> 2 ^ LENGTH('a)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alignUp a n \<noteq> 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n * (unat a div 2 ^ n + 1) \<noteq> 2 ^ LENGTH('a)
[PROOF STEP]
apply (erule contrapos_nn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> alignUp a n = 0
[PROOF STEP]
apply (subst alignUp_not_aligned_eq [OF False sz])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (a div 2 ^ n + 1) * 2 ^ n = 0
[PROOF STEP]
apply (subst unat_arith_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ((a div 2 ^ n + 1) * 2 ^ n) = unat 0
[PROOF STEP]
apply (subst unat_word_ariths)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (a div 2 ^ n + 1) * unat (2 ^ n) mod 2 ^ LENGTH('a) = unat 0
[PROOF STEP]
apply (subst unat_word_ariths)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> (unat (a div 2 ^ n) + unat 1) mod 2 ^ LENGTH('a) * unat (2 ^ n) mod 2 ^ LENGTH('a) = unat 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) = 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> Suc (unat (a div 2 ^ n)) mod 2 ^ LENGTH('a) * 2 ^ n mod 2 ^ LENGTH('a) = 0
[PROOF STEP]
apply (subst mult_mod_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) = 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> Suc (unat (a div 2 ^ n)) * 2 ^ n mod (2 ^ LENGTH('a) * 2 ^ n) mod 2 ^ LENGTH('a) = 0
[PROOF STEP]
apply (simp add: unat_div field_simps power_add[symmetric] mod_mod_power)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
2 ^ n * (unat a div 2 ^ n + 1) \<noteq> 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
2 ^ n * (unat a div 2 ^ n + 1) \<noteq> 2 ^ LENGTH('a)
[PROOF STEP]
have lt: "2 ^ n * (unat a div 2 ^ n + 1) < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
using this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
2 ^ n * (unat a div 2 ^ n + 1) \<noteq> 2 ^ LENGTH('a)

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

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
have "a = a div 2 ^ n * 2 ^ n + a mod 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = a div 2 ^ n * 2 ^ n + a mod 2 ^ n
[PROOF STEP]
by (rule word_mod_div_equality [symmetric])
[PROOF STATE]
proof (state)
this:
a = a div 2 ^ n * 2 ^ n + a mod 2 ^ n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a = a div 2 ^ n * 2 ^ n + a mod 2 ^ n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
have "\<dots> < (a div 2 ^ n + 1) * 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div 2 ^ n * 2 ^ n + a mod 2 ^ n < (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
using sz lt
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)
2 ^ n * (unat a div 2 ^ n + 1) < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. a div 2 ^ n * 2 ^ n + a mod 2 ^ n < (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
apply (simp add: field_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> a mod 2 ^ n + 2 ^ n * (a div 2 ^ n) < 2 ^ n + 2 ^ n * (a div 2 ^ n)
[PROOF STEP]
apply (rule word_add_less_mono1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> a mod 2 ^ n < 2 ^ n
 2. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) + unat (2 ^ n * (a div 2 ^ n)) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule word_mod_less_divisor)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> 0 < 2 ^ n
 2. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) + unat (2 ^ n * (a div 2 ^ n)) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (simp add: word_less_nat_alt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) + unat (2 ^ n * (a div 2 ^ n)) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst unat_word_ariths)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); 2 ^ n + 2 ^ n * (unat a div 2 ^ n) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) + unat (2 ^ n) * unat (a div 2 ^ n) mod 2 ^ LENGTH('a) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (simp add: unat_div)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
a div 2 ^ n * 2 ^ n + a mod 2 ^ n < (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a div 2 ^ n * 2 ^ n + a mod 2 ^ n < (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
have "\<dots> =  alignUp a n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a div 2 ^ n + 1) * 2 ^ n = alignUp a n
[PROOF STEP]
by (rule alignUp_not_aligned_eq [symmetric]) fact+
[PROOF STATE]
proof (state)
this:
(a div 2 ^ n + 1) * 2 ^ n = alignUp a n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> a \<le> alignUp a n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a < alignUp a n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a < alignUp a n

goal (1 subgoal):
 1. a \<le> alignUp a n
[PROOF STEP]
by (rule order_less_imp_le)
[PROOF STATE]
proof (state)
this:
a \<le> alignUp a n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alignUp_le_greater_al:
  fixes x :: "'a :: len word"
  assumes le: "a \<le> x"
  and     sz: "n < LENGTH('a)"
  and     al: "is_aligned x n"
  shows   "alignUp a n \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a n \<le> x
[PROOF STEP]
proof (cases "is_aligned a n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> alignUp a n \<le> x
 2. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_aligned a n

goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> alignUp a n \<le> x
 2. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_aligned a n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_aligned a n

goal (1 subgoal):
 1. alignUp a n \<le> x
[PROOF STEP]
using sz le
[PROOF STATE]
proof (prove)
using this:
is_aligned a n
n < LENGTH('a)
a \<le> x

goal (1 subgoal):
 1. alignUp a n \<le> x
[PROOF STEP]
by (simp add: alignUp_idem)
[PROOF STATE]
proof (state)
this:
alignUp a n \<le> x

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_aligned a n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> is_aligned a n
[PROOF STEP]
have anz: "a mod 2 ^ n \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> is_aligned a n

goal (1 subgoal):
 1. a mod 2 ^ n \<noteq> 0
[PROOF STEP]
by (rule not_aligned_mod_nz)
[PROOF STATE]
proof (state)
this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
is_aligned x n
[PROOF STEP]
obtain k where xk: "x = 2 ^ n * of_nat k" and kv: "k < 2 ^ (LENGTH('a) - n)"
[PROOF STATE]
proof (prove)
using this:
is_aligned x n

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

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 2 ^ n * word_of_nat k
k < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
have kn: "unat (of_nat k :: 'a word) * unat ((2::'a word) ^ n) < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
using this:
x = 2 ^ n * word_of_nat k
k < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. unat (word_of_nat k) * unat (2 ^ n) < 2 ^ LENGTH('a)
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
x = 2 ^ n * word_of_nat k
k < 2 ^ (LENGTH('a) - n)
n < LENGTH('a)

goal (1 subgoal):
 1. unat (word_of_nat k) * unat (2 ^ n) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst unat_of_nat_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k < 2 ^ LENGTH('a)
 2. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k * unat (2 ^ n) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (erule order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH('a) - n) \<le> 2 ^ LENGTH('a)
 2. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k * unat (2 ^ n) < 2 ^ LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k * unat (2 ^ n) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst mult.commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ n) * k < 2 ^ LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ n * k < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule nat_less_power_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> k < 2 ^ (LENGTH('a) - n)
 2. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> n \<le> LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 2 ^ n * word_of_nat k; k < 2 ^ (LENGTH('a) - n); n < LENGTH('a)\<rbrakk> \<Longrightarrow> n \<le> LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat (word_of_nat k) * unat (2 ^ n) < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
have au: "alignUp a n = (a div 2 ^ n + 1) * 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
by (rule alignUp_not_aligned_eq) fact+
[PROOF STATE]
proof (state)
this:
alignUp a n = (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
alignUp a n = (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
have "\<dots> \<le> of_nat k * 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a div 2 ^ n + 1) * 2 ^ n \<le> word_of_nat k * 2 ^ n
[PROOF STEP]
proof (rule word_mult_le_mono1 [OF inc_le _ kn])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a div 2 ^ n < word_of_nat k
 2. 0 < 2 ^ n
[PROOF STEP]
show "a div 2 ^ n < of_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k
[PROOF STEP]
using kv xk le sz anz
[PROOF STATE]
proof (prove)
using this:
k < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat k
a \<le> x
n < LENGTH('a)
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k
[PROOF STEP]
by (simp add: alignUp_div_helper)
[PROOF STATE]
proof (state)
this:
a div 2 ^ n < word_of_nat k

goal (1 subgoal):
 1. 0 < 2 ^ n
[PROOF STEP]
show "(0:: 'a word) < 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ n
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. 0 < 2 ^ n
[PROOF STEP]
by (simp add: p2_gt_0 sz)
[PROOF STATE]
proof (state)
this:
0 < 2 ^ n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a div 2 ^ n + 1) * 2 ^ n \<le> word_of_nat k * 2 ^ n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<le> x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
alignUp a n \<le> word_of_nat k * 2 ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
alignUp a n \<le> word_of_nat k * 2 ^ n

goal (1 subgoal):
 1. alignUp a n \<le> x
[PROOF STEP]
using xk
[PROOF STATE]
proof (prove)
using this:
alignUp a n \<le> word_of_nat k * 2 ^ n
x = 2 ^ n * word_of_nat k

goal (1 subgoal):
 1. alignUp a n \<le> x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
alignUp a n \<le> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alignUp_is_aligned_nz:
  fixes a :: "'a :: len word"
  assumes al: "is_aligned x n"
  and     sz: "n < LENGTH('a)"
  and     ax: "a \<le> x"
  and     az: "a \<noteq> 0"
  shows   "alignUp (a::'a :: len word) n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a n \<noteq> 0
[PROOF STEP]
proof (cases "is_aligned a n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
 2. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_aligned a n

goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
 2. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_aligned a n
[PROOF STEP]
have "alignUp a n = a"
[PROOF STATE]
proof (prove)
using this:
is_aligned a n

goal (1 subgoal):
 1. alignUp a n = a
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
is_aligned a n
n < LENGTH('a)

goal (1 subgoal):
 1. alignUp a n = a
[PROOF STEP]
by (simp add: alignUp_idem)
[PROOF STATE]
proof (state)
this:
alignUp a n = a

goal (2 subgoals):
 1. is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
 2. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alignUp a n = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
alignUp a n = a

goal (1 subgoal):
 1. alignUp a n \<noteq> 0
[PROOF STEP]
using az
[PROOF STATE]
proof (prove)
using this:
alignUp a n = a
a \<noteq> 0

goal (1 subgoal):
 1. alignUp a n \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
alignUp a n \<noteq> 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_aligned a n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> is_aligned a n
[PROOF STEP]
have anz: "a mod 2 ^ n \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> is_aligned a n

goal (1 subgoal):
 1. a mod 2 ^ n \<noteq> 0
[PROOF STEP]
by (rule not_aligned_mod_nz)
[PROOF STATE]
proof (state)
this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
assume asm: "alignUp a n = 0"
[PROOF STATE]
proof (state)
this:
alignUp a n = 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
have lt0: "unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
by (metis le_add_diff_inverse2 less_mult_imp_div_less order_less_imp_le power_add unsigned_less)
[PROOF STATE]
proof (state)
this:
unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
have leq: "2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
[PROOF STEP]
by (metis One_nat_def Suc_leI add.right_neutral add_Suc_right lt0 nat_le_power_trans
                order_less_imp_le)
[PROOF STATE]
proof (state)
this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
is_aligned x n
[PROOF STEP]
obtain k where  kv: "k < 2 ^ (LENGTH('a) - n)" and xk: "x = 2 ^ n * of_nat k"
[PROOF STATE]
proof (prove)
using this:
is_aligned x n

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

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat k
[PROOF STEP]
have "a div 2 ^ n < of_nat k"
[PROOF STATE]
proof (prove)
using this:
k < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat k

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k
[PROOF STEP]
using ax sz anz
[PROOF STATE]
proof (prove)
using this:
k < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat k
a \<le> x
n < LENGTH('a)
a mod 2 ^ n \<noteq> 0

goal (1 subgoal):
 1. a div 2 ^ n < word_of_nat k
[PROOF STEP]
by (rule alignUp_div_helper)
[PROOF STATE]
proof (state)
this:
a div 2 ^ n < word_of_nat k

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a div 2 ^ n < word_of_nat k
[PROOF STEP]
have r: "unat a div 2 ^ n < k"
[PROOF STATE]
proof (prove)
using this:
a div 2 ^ n < word_of_nat k

goal (1 subgoal):
 1. unat a div 2 ^ n < k
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
a div 2 ^ n < word_of_nat k
n < LENGTH('a)

goal (1 subgoal):
 1. unat a div 2 ^ n < k
[PROOF STEP]
by (simp flip: drop_bit_eq_div unat_drop_bit_eq) (metis leI le_unat_uoi unat_mono)
[PROOF STATE]
proof (state)
this:
unat a div 2 ^ n < k

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
have "alignUp a n = (a div 2 ^ n + 1) * 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
by (rule alignUp_not_aligned_eq) fact+
[PROOF STATE]
proof (state)
this:
alignUp a n = (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
using this:
alignUp a n = (a div 2 ^ n + 1) * 2 ^ n

goal (1 subgoal):
 1. (a div 2 ^ n + 1) * 2 ^ n = 0
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
alignUp a n = (a div 2 ^ n + 1) * 2 ^ n
alignUp a n = 0

goal (1 subgoal):
 1. (a div 2 ^ n + 1) * 2 ^ n = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a div 2 ^ n + 1) * 2 ^ n = 0

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a div 2 ^ n + 1) * 2 ^ n = 0
[PROOF STEP]
have "2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)"
[PROOF STATE]
proof (prove)
using this:
(a div 2 ^ n + 1) * 2 ^ n = 0

goal (1 subgoal):
 1. 2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
(a div 2 ^ n + 1) * 2 ^ n = 0
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)
[PROOF STEP]
by (simp add: unat_arith_simps ac_simps)
                  (simp add: unat_word_ariths mod_simps mod_eq_0_iff_dvd)
[PROOF STATE]
proof (state)
this:
2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
with leq
[PROOF STATE]
proof (chain)
picking this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)
[PROOF STEP]
have "2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
using this:
2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)
2 ^ LENGTH('a) dvd 2 ^ n * (unat a div 2 ^ n + 1)

goal (1 subgoal):
 1. 2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)
[PROOF STEP]
by (force elim!: le_SucE)
[PROOF STATE]
proof (state)
this:
2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)
[PROOF STEP]
have "unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1"
[PROOF STATE]
proof (prove)
using this:
2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1
[PROOF STEP]
by (metis (no_types, opaque_lifting) Groups.add_ac(2) add.right_neutral
                add_diff_cancel_left' div_le_dividend div_mult_self4 gr_implies_not0
                le_neq_implies_less power_eq_0_iff zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1
[PROOF STEP]
have "unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1"
[PROOF STATE]
proof (prove)
using this:
unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1

goal (1 subgoal):
 1. unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1
[PROOF STEP]
using sz
[PROOF STATE]
proof (prove)
using this:
unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1
n < LENGTH('a)

goal (1 subgoal):
 1. unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1
[PROOF STEP]
by (simp add: power_sub)
[PROOF STATE]
proof (state)
this:
unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1
[PROOF STEP]
have "2 ^ (LENGTH('a) - n) - 1 < k"
[PROOF STATE]
proof (prove)
using this:
unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1

goal (1 subgoal):
 1. 2 ^ (LENGTH('a) - n) - 1 < k
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1
unat a div 2 ^ n < k

goal (1 subgoal):
 1. 2 ^ (LENGTH('a) - n) - 1 < k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (LENGTH('a) - n) - 1 < k

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ (LENGTH('a) - n) - 1 < k
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
2 ^ (LENGTH('a) - n) - 1 < k

goal (1 subgoal):
 1. False
[PROOF STEP]
using kv
[PROOF STATE]
proof (prove)
using this:
2 ^ (LENGTH('a) - n) - 1 < k
k < 2 ^ (LENGTH('a) - n)

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

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
alignUp a n = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> is_aligned a n \<Longrightarrow> alignUp a n \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alignUp a n = 0 \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
alignUp a n = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. alignUp a n \<noteq> 0
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
alignUp a n \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alignUp_ar_helper:
  fixes a :: "'a :: len word"
  assumes al: "is_aligned x n"
  and     sz: "n < LENGTH('a)"
  and    sub: "{x..x + 2 ^ n - 1} \<subseteq> {a..b}"
  and    anz: "a \<noteq> 0"
  shows "a \<le> alignUp a n \<and> alignUp a n + 2 ^ n - 1 \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> alignUp a n \<and> alignUp a n + 2 ^ n - 1 \<le> b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<le> alignUp a n
 2. alignUp a n + 2 ^ n - 1 \<le> b
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
is_aligned x n
[PROOF STEP]
have xl: "x \<le> x + 2 ^ n - 1"
[PROOF STATE]
proof (prove)
using this:
is_aligned x n

goal (1 subgoal):
 1. x \<le> x + 2 ^ n - 1
[PROOF STEP]
by (simp add: is_aligned_no_overflow)
[PROOF STATE]
proof (state)
this:
x \<le> x + 2 ^ n - 1

goal (2 subgoals):
 1. a \<le> alignUp a n
 2. alignUp a n + 2 ^ n - 1 \<le> b
[PROOF STEP]
from xl sub
[PROOF STATE]
proof (chain)
picking this:
x \<le> x + 2 ^ n - 1
{x..x + 2 ^ n - 1} \<subseteq> {a..b}
[PROOF STEP]
have ax: "a \<le> x"
[PROOF STATE]
proof (prove)
using this:
x \<le> x + 2 ^ n - 1
{x..x + 2 ^ n - 1} \<subseteq> {a..b}

goal (1 subgoal):
 1. a \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> x

goal (2 subgoals):
 1. a \<le> alignUp a n
 2. alignUp a n + 2 ^ n - 1 \<le> b
[PROOF STEP]
show "a \<le> alignUp a n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> alignUp a n
[PROOF STEP]
proof (rule alignUp_ge)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n < LENGTH('a)
 2. alignUp a n \<noteq> 0
[PROOF STEP]
show "alignUp a n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a n \<noteq> 0
[PROOF STEP]
using al sz ax anz
[PROOF STATE]
proof (prove)
using this:
is_aligned x n
n < LENGTH('a)
a \<le> x
a \<noteq> 0

goal (1 subgoal):
 1. alignUp a n \<noteq> 0
[PROOF STEP]
by (rule alignUp_is_aligned_nz)
[PROOF STATE]
proof (state)
this:
alignUp a n \<noteq> 0

goal (1 subgoal):
 1. n < LENGTH('a)
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
a \<le> alignUp a n

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> b
[PROOF STEP]
show "alignUp a n + 2 ^ n - 1 \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> b
[PROOF STEP]
proof (rule order_trans)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. alignUp a n + 2 ^ n - 1 \<le> ?y
 2. ?y \<le> b
[PROOF STEP]
from xl
[PROOF STATE]
proof (chain)
picking this:
x \<le> x + 2 ^ n - 1
[PROOF STEP]
show tp: "x + 2 ^ n - 1 \<le> b"
[PROOF STATE]
proof (prove)
using this:
x \<le> x + 2 ^ n - 1

goal (1 subgoal):
 1. x + 2 ^ n - 1 \<le> b
[PROOF STEP]
using sub
[PROOF STATE]
proof (prove)
using this:
x \<le> x + 2 ^ n - 1
{x..x + 2 ^ n - 1} \<subseteq> {a..b}

goal (1 subgoal):
 1. x + 2 ^ n - 1 \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x + 2 ^ n - 1 \<le> b

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1
[PROOF STEP]
from ax
[PROOF STATE]
proof (chain)
picking this:
a \<le> x
[PROOF STEP]
have "alignUp a n \<le> x"
[PROOF STATE]
proof (prove)
using this:
a \<le> x

goal (1 subgoal):
 1. alignUp a n \<le> x
[PROOF STEP]
by (rule alignUp_le_greater_al) fact+
[PROOF STATE]
proof (state)
this:
alignUp a n \<le> x

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alignUp a n \<le> x
[PROOF STEP]
have "alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)"
[PROOF STATE]
proof (prove)
using this:
alignUp a n \<le> x

goal (1 subgoal):
 1. alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)
[PROOF STEP]
using xl al is_aligned_no_overflow' olen_add_eqv word_plus_mcs_3
[PROOF STATE]
proof (prove)
using this:
alignUp a n \<le> x
x \<le> x + 2 ^ n - 1
is_aligned x n
is_aligned ?p ?n \<Longrightarrow> ?p \<le> ?p + (2 ^ ?n - 1)
(?y \<le> ?y + ?x) = (?x \<le> ?y + ?x)
\<lbrakk>?v \<le> ?w; ?x \<le> ?w + ?x\<rbrakk> \<Longrightarrow> ?v + ?x \<le> ?w + ?x

goal (1 subgoal):
 1. alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)
[PROOF STEP]
show "alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1"
[PROOF STATE]
proof (prove)
using this:
alignUp a n + (2 ^ n - 1) \<le> x + (2 ^ n - 1)

goal (1 subgoal):
 1. alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
alignUp a n + 2 ^ n - 1 \<le> x + 2 ^ n - 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
alignUp a n + 2 ^ n - 1 \<le> b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alignUp_def2:
  "alignUp a sz = a + 2 ^ sz - 1 AND NOT (mask sz)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a sz = a + 2 ^ sz - 1 AND NOT (mask sz)
[PROOF STEP]
by (simp add: alignUp_def flip: mask_eq_decr_exp)


[STATEMENT]
lemma alignUp_def3:
  "alignUp a sz = 2^ sz + (a - 1 AND NOT (mask sz))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp a sz = 2 ^ sz + (a - 1 AND NOT (mask sz))
[PROOF STEP]
by (simp add: alignUp_def2 is_aligned_triv field_simps mask_out_add_aligned)


[STATEMENT]
lemma  alignUp_plus:
  "is_aligned w us \<Longrightarrow> alignUp (w + a) us  = w + alignUp a us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w us \<Longrightarrow> alignUp (w + a) us = w + alignUp a us
[PROOF STEP]
by (clarsimp simp: alignUp_def2 mask_out_add_aligned field_simps)


[STATEMENT]
lemma alignUp_distance:
  "alignUp (q :: 'a :: len word) sz - q \<le> mask sz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alignUp q sz - q \<le> mask sz
[PROOF STEP]
by (metis (no_types) add.commute add_diff_cancel_left alignUp_def2 diff_add_cancel
                       mask_2pm1 subtract_mask(2) word_and_le1 word_sub_le_iff)


[STATEMENT]
lemma is_aligned_diff_neg_mask:
  "is_aligned p sz \<Longrightarrow> (p - q AND NOT (mask sz)) = (p - ((alignUp q sz) AND NOT (mask sz)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> p - q AND NOT (mask sz) = p - (alignUp q sz AND NOT (mask sz))
[PROOF STEP]
apply (clarsimp simp only:word_and_le2 diff_conv_add_uminus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> p + - q AND NOT (mask sz) = p + - (alignUp q sz AND NOT (mask sz))
[PROOF STEP]
apply (subst mask_out_add_aligned[symmetric]; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> - q AND NOT (mask sz) = - (alignUp q sz AND NOT (mask sz))
[PROOF STEP]
apply (simp add: eq_neg_iff_add_eq_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> (- q AND NOT (mask sz)) + (alignUp q sz AND NOT (mask sz)) = 0
[PROOF STEP]
apply (subst add.commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p sz \<Longrightarrow> (alignUp q sz AND NOT (mask sz)) + (- q AND NOT (mask sz)) = 0
[PROOF STEP]
apply (simp add: alignUp_distance is_aligned_neg_mask_eq mask_out_add_aligned and_mask_eq_iff_le_mask flip: mask_eq_x_eq_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_clz_max:
  "word_clz w \<le> size (w::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_clz w \<le> size w
[PROOF STEP]
unfolding word_clz_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (to_bl w)) \<le> size w
[PROOF STEP]
by (metis length_takeWhile_le word_size_bl)


[STATEMENT]
lemma word_clz_nonzero_max:
  fixes w :: "'a::len word"
  assumes nz: "w \<noteq> 0"
  shows "word_clz w < size (w::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
assume a: "word_clz w = size (w::'a::len word)"
[PROOF STATE]
proof (state)
this:
word_clz w = size w

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
hence "length (takeWhile Not (to_bl w)) = length (to_bl w)"
[PROOF STATE]
proof (prove)
using this:
word_clz w = size w

goal (1 subgoal):
 1. length (takeWhile Not (to_bl w)) = length (to_bl w)
[PROOF STEP]
by (simp add: word_clz_def word_size)
[PROOF STATE]
proof (state)
this:
length (takeWhile Not (to_bl w)) = length (to_bl w)

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
hence allj: "\<forall>j\<in>set(to_bl w). \<not> j"
[PROOF STATE]
proof (prove)
using this:
length (takeWhile Not (to_bl w)) = length (to_bl w)

goal (1 subgoal):
 1. \<forall>j\<in>set (to_bl w). \<not> j
[PROOF STEP]
by (metis a length_takeWhile_less less_irrefl_nat word_clz_def)
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>set (to_bl w). \<not> j

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
hence "to_bl w = replicate (length (to_bl w)) False"
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>set (to_bl w). \<not> j

goal (1 subgoal):
 1. to_bl w = replicate (length (to_bl w)) False
[PROOF STEP]
using eq_zero_set_bl nz
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>set (to_bl w). \<not> j
(?w = 0) = (True \<notin> set (to_bl ?w))
w \<noteq> 0

goal (1 subgoal):
 1. to_bl w = replicate (length (to_bl w)) False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
to_bl w = replicate (length (to_bl w)) False

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
hence "w = 0"
[PROOF STATE]
proof (prove)
using this:
to_bl w = replicate (length (to_bl w)) False

goal (1 subgoal):
 1. w = 0
[PROOF STEP]
by (metis to_bl_0 word_bl.Rep_eqD word_bl_Rep')
[PROOF STATE]
proof (state)
this:
w = 0

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
with nz
[PROOF STATE]
proof (chain)
picking this:
w \<noteq> 0
w = 0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0
w = 0

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

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
word_clz w = size w \<Longrightarrow> False

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
word_clz w = size w \<Longrightarrow> False

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
using word_clz_max
[PROOF STATE]
proof (prove)
using this:
word_clz w = size w \<Longrightarrow> False
word_clz ?w \<le> size ?w

goal (1 subgoal):
 1. word_clz w < size w
[PROOF STEP]
by (fastforce intro: le_neq_trans)
[PROOF STATE]
proof (state)
this:
word_clz w < size w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bin_sign_extend_iff [bit_simps]:
  \<open>bit (sign_extend e w) i \<longleftrightarrow> bit w (min e i)\<close>
  if \<open>i < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (sign_extend e w) i = bit w (min e i)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < LENGTH('a)

goal (1 subgoal):
 1. bit (sign_extend e w) i = bit w (min e i)
[PROOF STEP]
by (simp add: sign_extend_def bit_simps min_def)


[STATEMENT]
lemma sign_extend_bitwise_if:
  "i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (if i < e then bit w i else bit w e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < size w \<Longrightarrow> bit (sign_extend e w) i = (if i < e then bit w i else bit w e)
[PROOF STEP]
by (simp add: word_size bit_simps)


[STATEMENT]
lemma sign_extend_bitwise_if'  [word_eqI_simps]:
  \<open>i < LENGTH('a) \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (if i < e then bit w i else bit w e)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < LENGTH('a) \<Longrightarrow> bit (sign_extend e w) i = (if i < e then bit w i else bit w e)
[PROOF STEP]
using sign_extend_bitwise_if [of i w e]
[PROOF STATE]
proof (prove)
using this:
i < size w \<Longrightarrow> bit (sign_extend e w) i = (if i < e then bit w i else bit w e)

goal (1 subgoal):
 1. i < LENGTH('a) \<Longrightarrow> bit (sign_extend e w) i = (if i < e then bit w i else bit w e)
[PROOF STEP]
by (simp add: word_size)


[STATEMENT]
lemma sign_extend_bitwise_disj:
  "i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> i \<le> e \<and> bit w i \<or> e \<le> i \<and> bit w e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < size w \<Longrightarrow> bit (sign_extend e w) i = (i \<le> e \<and> bit w i \<or> e \<le> i \<and> bit w e)
[PROOF STEP]
by (auto simp: sign_extend_bitwise_if)


[STATEMENT]
lemma sign_extend_bitwise_cases:
  "i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (i \<le> e \<longrightarrow> bit w i) \<and> (e \<le> i \<longrightarrow> bit w e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < size w \<Longrightarrow> bit (sign_extend e w) i = ((i \<le> e \<longrightarrow> bit w i) \<and> (e \<le> i \<longrightarrow> bit w e))
[PROOF STEP]
by (auto simp: sign_extend_bitwise_if)


[STATEMENT]
lemma sign_extend_def':
  "sign_extend n w = (if bit w n then w OR NOT (mask (Suc n)) else w AND mask (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_extend n w = (if bit w n then w OR NOT (mask (Suc n)) else w AND mask (Suc n))
[PROOF STEP]
by (rule bit_word_eqI) (auto simp add: bit_simps sign_extend_eq_signed_take_bit min_def less_Suc_eq_le)


[STATEMENT]
lemma sign_extended_sign_extend:
  "sign_extended n (sign_extend n w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_extended n (sign_extend n w)
[PROOF STEP]
by (clarsimp simp: sign_extended_def word_size sign_extend_bitwise_if)


[STATEMENT]
lemma sign_extended_iff_sign_extend:
  "sign_extended n w \<longleftrightarrow> sign_extend n w = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_extended n w = (sign_extend n w = w)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sign_extended n w \<Longrightarrow> sign_extend n w = w
 2. sign_extend n w = w \<Longrightarrow> sign_extended n w
[PROOF STEP]
apply (auto simp add: bit_eq_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>sign_extended n w; na < LENGTH('a); bit (sign_extend n w) na\<rbrakk> \<Longrightarrow> bit w na
 2. \<And>na. \<lbrakk>sign_extended n w; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> bit (sign_extend n w) na
 3. \<forall>na<LENGTH('a). bit (sign_extend n w) na = bit w na \<Longrightarrow> sign_extended n w
[PROOF STEP]
apply (simp_all add: bit_simps sign_extend_eq_signed_take_bit not_le min_def sign_extended_def word_size split: if_splits)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i; na < LENGTH('a); n \<le> na; bit w n\<rbrakk> \<Longrightarrow> bit w na
 2. \<And>na. \<lbrakk>\<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i = bit w n; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> n \<le> na \<longrightarrow> bit w n
 3. \<forall>na<LENGTH('a). na < n \<or> bit w n = bit w na \<Longrightarrow> \<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i = bit w n
[PROOF STEP]
using le_imp_less_or_eq
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x < ?y \<or> ?x = ?y

goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i; na < LENGTH('a); n \<le> na; bit w n\<rbrakk> \<Longrightarrow> bit w na
 2. \<And>na. \<lbrakk>\<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i = bit w n; na < LENGTH('a); bit w na\<rbrakk> \<Longrightarrow> n \<le> na \<longrightarrow> bit w n
 3. \<forall>na<LENGTH('a). na < n \<or> bit w n = bit w na \<Longrightarrow> \<forall>i>n. i < LENGTH('a) \<longrightarrow> bit w i = bit w n
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sign_extended_weaken:
  "sign_extended n w \<Longrightarrow> n \<le> m \<Longrightarrow> sign_extended m w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sign_extended n w; n \<le> m\<rbrakk> \<Longrightarrow> sign_extended m w
[PROOF STEP]
unfolding sign_extended_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i>n. i < size w \<longrightarrow> bit w i = bit w n; n \<le> m\<rbrakk> \<Longrightarrow> \<forall>i>m. i < size w \<longrightarrow> bit w i = bit w m
[PROOF STEP]
by (cases "n < m") auto


[STATEMENT]
lemma sign_extend_sign_extend_eq:
  "sign_extend m (sign_extend n w) = sign_extend (min m n) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_extend m (sign_extend n w) = sign_extend (min m n) w
[PROOF STEP]
by (rule bit_word_eqI) (simp add: sign_extend_eq_signed_take_bit bit_simps)


[STATEMENT]
lemma sign_extended_high_bits:
  "\<lbrakk> sign_extended e p; j < size p; e \<le> i; i < j \<rbrakk> \<Longrightarrow> bit p i = bit p j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sign_extended e p; j < size p; e \<le> i; i < j\<rbrakk> \<Longrightarrow> bit p i = bit p j
[PROOF STEP]
by (drule (1) sign_extended_weaken; simp add: sign_extended_def)


[STATEMENT]
lemma sign_extend_eq:
  "w AND mask (Suc n) = v AND mask (Suc n) \<Longrightarrow> sign_extend n w = sign_extend n v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w AND mask (Suc n) = v AND mask (Suc n) \<Longrightarrow> sign_extend n w = sign_extend n v
[PROOF STEP]
by (simp flip: take_bit_eq_mask add: sign_extend_eq_signed_take_bit signed_take_bit_eq_iff_take_bit_eq)


[STATEMENT]
lemma sign_extended_add:
  assumes p: "is_aligned p n"
  assumes f: "f < 2 ^ n"
  assumes e: "n \<le> e"
  assumes "sign_extended e p"
  shows "sign_extended e (p + f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_extended e (p + f)
[PROOF STEP]
proof (cases "e < size p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
e < size p

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
note and_or = is_aligned_add_or[OF p f]
[PROOF STATE]
proof (state)
this:
p + f = p OR f

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
have "\<not> bit f e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit f e
[PROOF STEP]
using True e less_2p_is_upper_bits_unset[THEN iffD1, OF f]
[PROOF STATE]
proof (prove)
using this:
e < size p
n \<le> e
n < LENGTH('a) \<and> (\<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit f n')

goal (1 subgoal):
 1. \<not> bit f e
[PROOF STEP]
by (fastforce simp: word_size)
[PROOF STATE]
proof (state)
this:
\<not> bit f e

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
hence i: "bit (p + f) e = bit p e"
[PROOF STATE]
proof (prove)
using this:
\<not> bit f e

goal (1 subgoal):
 1. bit (p + f) e = bit p e
[PROOF STEP]
by (simp add: and_or bit_simps)
[PROOF STATE]
proof (state)
this:
bit (p + f) e = bit p e

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
have fm: "f AND mask e = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f AND mask e = f
[PROOF STEP]
by (fastforce intro: subst[where P="\<lambda>f. f AND mask e = f", OF less_mask_eq[OF f]]
                  simp: mask_twice e)
[PROOF STATE]
proof (state)
this:
f AND mask e = f

goal (2 subgoals):
 1. e < size p \<Longrightarrow> sign_extended e (p + f)
 2. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sign_extended e (p + f)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_aligned p n
f < 2 ^ n
n \<le> e
sign_extended e p

goal (1 subgoal):
 1. sign_extended e (p + f)
[PROOF STEP]
apply (simp add: sign_extended_iff_sign_extend sign_extend_def i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; f < 2 ^ n; n \<le> e; (if bit p e then p OR NOT (mask e) else p AND mask e) = p\<rbrakk> \<Longrightarrow> (bit p e \<longrightarrow> p + f OR NOT (mask e) = p + f) \<and> (\<not> bit p e \<longrightarrow> p + f AND mask e = p + f)
[PROOF STEP]
apply (simp add: and_or word_bw_comms[of p f])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; f < 2 ^ n; n \<le> e; (if bit p e then p OR NOT (mask e) else p AND mask e) = p\<rbrakk> \<Longrightarrow> (bit p e \<longrightarrow> (f OR p) OR NOT (mask e) = f OR p) \<and> (\<not> bit p e \<longrightarrow> (f OR p) AND mask e = f OR p)
[PROOF STEP]
apply (clarsimp simp: word_ao_dist fm word_bw_assocs split: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sign_extended e (p + f)

goal (1 subgoal):
 1. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> e < size p

goal (1 subgoal):
 1. \<not> e < size p \<Longrightarrow> sign_extended e (p + f)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> e < size p

goal (1 subgoal):
 1. sign_extended e (p + f)
[PROOF STEP]
by (simp add: sign_extended_def word_size)
[PROOF STATE]
proof (state)
this:
sign_extended e (p + f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sign_extended_neq_mask:
  "\<lbrakk>sign_extended n ptr; m \<le> n\<rbrakk> \<Longrightarrow> sign_extended n (ptr AND NOT (mask m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sign_extended n ptr; m \<le> n\<rbrakk> \<Longrightarrow> sign_extended n (ptr AND NOT (mask m))
[PROOF STEP]
by (fastforce simp: sign_extended_def word_size neg_mask_test_bit bit_simps)


[STATEMENT]
lemma limited_and_eq_0:
  "\<lbrakk> limited_and x z; y AND NOT z = y \<rbrakk> \<Longrightarrow> x AND y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>limited_and x z; y AND NOT z = y\<rbrakk> \<Longrightarrow> x AND y = 0
[PROOF STEP]
unfolding limited_and_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> x AND y = 0
[PROOF STEP]
apply (subst arg_cong2[where f="(AND)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> x = ?b
 2. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> y = ?d
 3. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> ?b AND ?d = 0
[PROOF STEP]
apply (erule sym)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND z = x; y AND NOT z = y\<rbrakk> \<Longrightarrow> (x AND z) AND y AND NOT z = 0
[PROOF STEP]
apply (simp(no_asm) add: word_bw_assocs word_bw_comms word_bw_lcs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma limited_and_eq_id:
  "\<lbrakk> limited_and x z; y AND z = z \<rbrakk> \<Longrightarrow> x AND y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>limited_and x z; y AND z = z\<rbrakk> \<Longrightarrow> x AND y = x
[PROOF STEP]
unfolding limited_and_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x AND z = x; y AND z = z\<rbrakk> \<Longrightarrow> x AND y = x
[PROOF STEP]
by (erule subst, fastforce simp: word_bw_lcs word_bw_assocs word_bw_comms)


[STATEMENT]
lemma lshift_limited_and:
  "limited_and x z \<Longrightarrow> limited_and (x << n) (z << n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limited_and x z \<Longrightarrow> limited_and (x << n) (z << n)
[PROOF STEP]
using push_bit_and [of n x z]
[PROOF STATE]
proof (prove)
using this:
push_bit n (x AND z) = push_bit n x AND push_bit n z

goal (1 subgoal):
 1. limited_and x z \<Longrightarrow> limited_and (x << n) (z << n)
[PROOF STEP]
by (simp add: limited_and_def shiftl_def)


[STATEMENT]
lemma rshift_limited_and:
  "limited_and x z \<Longrightarrow> limited_and (x >> n) (z >> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limited_and x z \<Longrightarrow> limited_and (x >> n) (z >> n)
[PROOF STEP]
using drop_bit_and [of n x z]
[PROOF STATE]
proof (prove)
using this:
drop_bit n (x AND z) = drop_bit n x AND drop_bit n z

goal (1 subgoal):
 1. limited_and x z \<Longrightarrow> limited_and (x >> n) (z >> n)
[PROOF STEP]
by (simp add: limited_and_def shiftr_def)


[STATEMENT]
lemma from_bool_eq:
  \<open>from_bool = of_bool\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_bool = of_bool
[PROOF STEP]
by (simp add: fun_eq_iff from_bool_def)


[STATEMENT]
lemma from_bool_0:
  "(from_bool x = 0) = (\<not> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (from_bool x = 0) = (\<not> x)
[PROOF STEP]
by (simp add: from_bool_def split: bool.split)


[STATEMENT]
lemma from_bool_eq_if':
  "((if P then 1 else 0) = from_bool Q) = (P = Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if P then 1 else 0) = from_bool Q) = (P = Q)
[PROOF STEP]
by (cases Q) (simp_all add: from_bool_def)


[STATEMENT]
lemma to_bool_and_1:
  "to_bool (x AND 1) \<longleftrightarrow> bit x 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bool (x AND 1) = bit x 0
[PROOF STEP]
by (simp add: to_bool_def word_and_1)


[STATEMENT]
lemma to_bool_from_bool [simp]:
  "to_bool (from_bool r) = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bool (from_bool r) = r
[PROOF STEP]
unfolding from_bool_def to_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<noteq> (case r of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0)) = r
[PROOF STEP]
by (simp split: bool.splits)


[STATEMENT]
lemma from_bool_neq_0 [simp]:
  "(from_bool b \<noteq> 0) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (from_bool b \<noteq> 0) = b
[PROOF STEP]
by (simp add: from_bool_def split: bool.splits)


[STATEMENT]
lemma from_bool_mask_simp [simp]:
  "(from_bool r :: 'a::len word) AND 1 = from_bool r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_bool r AND 1 = from_bool r
[PROOF STEP]
unfolding from_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case r of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0) AND 1 = (case r of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0)
[PROOF STEP]
by (clarsimp split: bool.splits)


[STATEMENT]
lemma from_bool_1 [simp]:
  "(from_bool P = 1) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (from_bool P = 1) = P
[PROOF STEP]
by (simp add: from_bool_def split: bool.splits)


[STATEMENT]
lemma ge_0_from_bool [simp]:
  "(0 < from_bool P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < from_bool P) = P
[PROOF STEP]
by (simp add: from_bool_def split: bool.splits)


[STATEMENT]
lemma limited_and_from_bool:
  "limited_and (from_bool b) 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limited_and (from_bool b) 1
[PROOF STEP]
by (simp add: from_bool_def limited_and_def split: bool.split)


[STATEMENT]
lemma to_bool_1 [simp]: "to_bool 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bool 1
[PROOF STEP]
by (simp add: to_bool_def)


[STATEMENT]
lemma to_bool_0 [simp]: "\<not>to_bool 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> to_bool 0
[PROOF STEP]
by (simp add: to_bool_def)


[STATEMENT]
lemma from_bool_eq_if:
  "(from_bool Q = (if P then 1 else 0)) = (P = Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (from_bool Q = (if P then 1 else 0)) = (P = Q)
[PROOF STEP]
by (cases Q) (simp_all add: from_bool_def)


[STATEMENT]
lemma to_bool_eq_0:
  "(\<not> to_bool x) = (x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> to_bool x) = (x = 0)
[PROOF STEP]
by (simp add: to_bool_def)


[STATEMENT]
lemma to_bool_neq_0:
  "(to_bool x) = (x \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bool x = (x \<noteq> 0)
[PROOF STEP]
by (simp add: to_bool_def)


[STATEMENT]
lemma from_bool_all_helper:
  "(\<forall>bool. from_bool bool = val \<longrightarrow> P bool)
      = ((\<exists>bool. from_bool bool = val) \<longrightarrow> P (val \<noteq> 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>bool. from_bool bool = val \<longrightarrow> P bool) = ((\<exists>bool. from_bool bool = val) \<longrightarrow> P (val \<noteq> 0))
[PROOF STEP]
by (auto simp: from_bool_0)


[STATEMENT]
lemma fold_eq_0_to_bool:
  "(v = 0) = (\<not> to_bool v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v = 0) = (\<not> to_bool v)
[PROOF STEP]
by (simp add: to_bool_def)


[STATEMENT]
lemma from_bool_to_bool_iff:
  "w = from_bool b \<longleftrightarrow> to_bool w = b \<and> (w = 0 \<or> w = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w = from_bool b) = (to_bool w = b \<and> (w = 0 \<or> w = 1))
[PROOF STEP]
by (cases b) (auto simp: from_bool_def to_bool_def)


[STATEMENT]
lemma from_bool_eqI:
  "from_bool x = from_bool y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_bool x = from_bool y \<Longrightarrow> x = y
[PROOF STEP]
unfolding from_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case x of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0) = (case y of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0) \<Longrightarrow> x = y
[PROOF STEP]
by (auto split: bool.splits)