[STATEMENT]
lemma of_bl_drop':
  "lend = length bl - LENGTH('a::len) \<Longrightarrow>
    of_bl (drop lend bl) = (of_bl bl :: 'a word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lend = length bl - LENGTH('a) \<Longrightarrow> of_bl (drop lend bl) = of_bl bl
[PROOF STEP]
by transfer (simp flip: trunc_bl2bin)


[STATEMENT]
lemma test_bit_of_bl:
  "bit (of_bl bl::'a::len word) n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (of_bl bl) n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)
[PROOF STEP]
by transfer (simp add: bin_nth_of_bl ac_simps)


[STATEMENT]
lemma no_of_bl: "(numeral bin ::'a::len word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. numeral bin = of_bl (bin_to_bl LENGTH('a) (numeral bin))
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = bin_to_bl (size w) (uint w)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (to_bl w) = uint w
[PROOF STEP]
by (simp add: uint_bl word_size)


[STATEMENT]
lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len word) = bin_to_bl (LENGTH('a)) bin"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (word_of_int bin) = bin_to_bl LENGTH('a) bin
[PROOF STEP]
by (auto simp: uint_bl word_ubin.eq_norm word_size)


[STATEMENT]
lemma to_bl_numeral [simp]:
  "to_bl (numeral bin::'a::len word) =
    bin_to_bl (LENGTH('a)) (numeral bin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (numeral bin) = bin_to_bl LENGTH('a) (numeral bin)
[PROOF STEP]
unfolding word_numeral_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (word_of_int (numeral bin)) = bin_to_bl LENGTH('a) (numeral bin)
[PROOF STEP]
by (rule to_bl_of_bin)


[STATEMENT]
lemma to_bl_neg_numeral [simp]:
  "to_bl (- numeral bin::'a::len word) =
    bin_to_bl (LENGTH('a)) (- numeral bin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (- numeral bin) = bin_to_bl LENGTH('a) (- numeral bin)
[PROOF STEP]
unfolding word_neg_numeral_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (word_of_int (- numeral bin)) = bin_to_bl LENGTH('a) (- numeral bin)
[PROOF STEP]
by (rule to_bl_of_bin)


[STATEMENT]
lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (to_bl w) = uint w
[PROOF STEP]
by (simp add: uint_bl word_size)


[STATEMENT]
lemma uint_bl_bin: "bl_to_bin (bin_to_bl (LENGTH('a)) (uint x)) = uint x"
  for x :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bin_to_bl LENGTH('a) (uint x)) = uint x
[PROOF STEP]
by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])


[STATEMENT]
lemma ucast_bl: "ucast w = of_bl (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ucast w = of_bl (to_bl w)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma ucast_down_bl:
  \<open>(ucast :: 'a::len word \<Rightarrow> 'b::len word) (of_bl bl) = of_bl bl\<close>
    if \<open>is_down (ucast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ucast (of_bl bl) = of_bl bl
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
is_down ucast

goal (1 subgoal):
 1. ucast (of_bl bl) = of_bl bl
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (X @ to_bl w) = w
[PROOF STEP]
by transfer (simp add: bl_to_bin_app_cat)


[STATEMENT]
lemma ucast_of_bl_up:
  \<open>ucast (of_bl bl :: 'a::len word) = of_bl bl\<close>
  if \<open>size bl \<le> size (of_bl bl :: 'a::len word)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ucast (of_bl bl) = of_bl bl
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
length bl \<le> size (of_bl bl)

goal (1 subgoal):
 1. ucast (of_bl bl) = of_bl bl
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>bl. length bl \<le> LENGTH('a) \<Longrightarrow> take_bit LENGTH('b) (take_bit LENGTH('a) (bl_to_bin bl)) = take_bit LENGTH('b) (bl_to_bin bl)
[PROOF STEP]
apply (rule bit_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>bl n. \<lbrakk>length bl \<le> LENGTH('a); possible_bit TYPE(int) n\<rbrakk> \<Longrightarrow> bit (take_bit LENGTH('b) (take_bit LENGTH('a) (bl_to_bin bl))) n = bit (take_bit LENGTH('b) (bl_to_bin bl)) n
[PROOF STEP]
apply (auto simp add: bit_take_bit_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>bl n. \<lbrakk>length bl \<le> LENGTH('a); n < LENGTH('b); bit (bl_to_bin bl) n\<rbrakk> \<Longrightarrow> n < LENGTH('a)
[PROOF STEP]
apply (subst (asm) trunc_bl2bin_len [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>bl n. \<lbrakk>length bl \<le> LENGTH('a); n < LENGTH('b); bit (take_bit (length bl) (bl_to_bin bl)) n\<rbrakk> \<Longrightarrow> n < LENGTH('a)
[PROOF STEP]
apply (auto simp only: bit_take_bit_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_rev_tf:
  "to_bl (of_bl bl::'a::len word) =
    rev (takefill False (LENGTH('a)) (rev bl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl bl) = rev (takefill False LENGTH('a) (rev bl))
[PROOF STEP]
by transfer (simp add: bl_bin_bl_rtf)


[STATEMENT]
lemma word_rep_drop:
  "to_bl (of_bl bl::'a::len word) =
    replicate (LENGTH('a) - length bl) False @
    drop (length bl - LENGTH('a)) bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl bl) = replicate (LENGTH('a) - length bl) False @ drop (length bl - LENGTH('a)) bl
[PROOF STEP]
by (simp add: word_rev_tf takefill_alt rev_take)


[STATEMENT]
lemma to_bl_ucast:
  "to_bl (ucast (w::'b::len word) ::'a::len word) =
    replicate (LENGTH('a) - LENGTH('b)) False @
    drop (LENGTH('b) - LENGTH('a)) (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (ucast w) = replicate (LENGTH('a) - LENGTH('b)) False @ drop (LENGTH('b) - LENGTH('a)) (to_bl w)
[PROOF STEP]
apply (unfold ucast_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl (to_bl w)) = replicate (LENGTH('a) - LENGTH('b)) False @ drop (LENGTH('b) - LENGTH('a)) (to_bl w)
[PROOF STEP]
apply (rule trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. to_bl (of_bl (to_bl w)) = ?s
 2. ?s = replicate (LENGTH('a) - LENGTH('b)) False @ drop (LENGTH('b) - LENGTH('a)) (to_bl w)
[PROOF STEP]
apply (rule word_rep_drop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replicate (LENGTH('a) - length (to_bl w)) False @ drop (length (to_bl w) - LENGTH('a)) (to_bl w) = replicate (LENGTH('a) - LENGTH('b)) False @ drop (LENGTH('b) - LENGTH('a)) (to_bl w)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ucast_up_app:
  \<open>to_bl (ucast w :: 'b::len word) = replicate n False @ (to_bl w)\<close>
    if \<open>source_size (ucast :: 'a word \<Rightarrow> 'b word) + n = target_size (ucast :: 'a word \<Rightarrow> 'b word)\<close>
    for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (ucast w) = replicate n False @ to_bl w
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
source_size ucast + n = target_size ucast

goal (1 subgoal):
 1. to_bl (ucast w) = replicate n False @ to_bl w
[PROOF STEP]
by (auto simp add : source_size target_size to_bl_ucast)


[STATEMENT]
lemma ucast_down_drop [OF refl]:
  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
    to_bl (uc w) = drop n (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uc = ucast; source_size uc = target_size uc + n\<rbrakk> \<Longrightarrow> to_bl (uc w) = drop n (to_bl w)
[PROOF STEP]
by (auto simp add : source_size target_size to_bl_ucast)


[STATEMENT]
lemma scast_down_drop [OF refl]:
  "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow>
    to_bl (sc w) = drop n (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sc = scast; source_size sc = target_size sc + n\<rbrakk> \<Longrightarrow> to_bl (sc w) = drop n (to_bl w)
[PROOF STEP]
apply (subgoal_tac "sc = ucast")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sc = scast; source_size sc = target_size sc + n; sc = ucast\<rbrakk> \<Longrightarrow> to_bl (sc w) = drop n (to_bl w)
 2. \<lbrakk>sc = scast; source_size sc = target_size sc + n\<rbrakk> \<Longrightarrow> sc = ucast
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>source_size scast = target_size scast + n; scast = ucast; sc = scast\<rbrakk> \<Longrightarrow> to_bl (scast w) = drop n (to_bl w)
 2. \<lbrakk>source_size scast = target_size scast + n; sc = scast\<rbrakk> \<Longrightarrow> scast = ucast
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>source_size ucast = target_size ucast + n; scast = ucast; sc = ucast\<rbrakk> \<Longrightarrow> to_bl (ucast w) = drop n (to_bl w)
 2. \<lbrakk>source_size scast = target_size scast + n; sc = scast\<rbrakk> \<Longrightarrow> scast = ucast
[PROOF STEP]
apply (erule ucast_down_drop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>source_size scast = target_size scast + n; sc = scast\<rbrakk> \<Longrightarrow> scast = ucast
[PROOF STEP]
apply (rule down_cast_same [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>source_size scast = target_size scast + n; sc = scast\<rbrakk> \<Longrightarrow> is_down ucast
[PROOF STEP]
apply (simp add : source_size target_size is_down)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_0_bl [simp]: "of_bl [] = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl [] = 0
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma word_1_bl: "of_bl [True] = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl [True] = 1
[PROOF STEP]
by transfer (simp add: bl_to_bin_def)


[STATEMENT]
lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (replicate n False) = 0
[PROOF STEP]
by transfer (simp add: bl_to_bin_rep_False)


[STATEMENT]
lemma to_bl_0 [simp]: "to_bl (0::'a::len word) = replicate (LENGTH('a)) False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl 0 = replicate LENGTH('a) False
[PROOF STEP]
by (simp add: uint_bl word_size bin_to_bl_zero)

\<comment> \<open>links with \<open>rbl\<close> operations\<close>


[STATEMENT]
lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))
[PROOF STEP]
by transfer (simp add: rbl_succ)


[STATEMENT]
lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))
[PROOF STEP]
by transfer (simp add: rbl_pred)


[STATEMENT]
lemma word_add_rbl:
  "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
    to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>to_bl v = vbl; to_bl w = wbl\<rbrakk> \<Longrightarrow> to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>bin_to_bl LENGTH('a) v = vbl; bin_to_bl LENGTH('a) w = wbl\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v + w) = rev (rbl_add (rev vbl) (rev wbl))
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>bin_to_bl LENGTH('a) w = wbl; vbl = bin_to_bl LENGTH('a) v\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v + w) = rev (rbl_add (rev vbl) (rev wbl))
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>vbl = bin_to_bl LENGTH('a) v; wbl = bin_to_bl LENGTH('a) w\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v + w) = rev (rbl_add (rev vbl) (rev wbl))
[PROOF STEP]
apply (simp add: rbl_add)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_mult_rbl:
  "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
    to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>to_bl v = vbl; to_bl w = wbl\<rbrakk> \<Longrightarrow> to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>bin_to_bl LENGTH('a) v = vbl; bin_to_bl LENGTH('a) w = wbl\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v * w) = rev (rbl_mult (rev vbl) (rev wbl))
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>bin_to_bl LENGTH('a) w = wbl; vbl = bin_to_bl LENGTH('a) v\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v * w) = rev (rbl_mult (rev vbl) (rev wbl))
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v vbl w wbl. \<lbrakk>vbl = bin_to_bl LENGTH('a) v; wbl = bin_to_bl LENGTH('a) w\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (v * w) = rev (rbl_mult (rev vbl) (rev wbl))
[PROOF STEP]
apply (simp add: rbl_mult)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rtb_rbl_ariths:
  "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
  "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
  "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
  "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys) &&& (rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys)) &&& (\<lbrakk>rev (to_bl v) = ys; rev (to_bl w) = xs\<rbrakk> \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs) &&& (\<lbrakk>rev (to_bl v) = ys; rev (to_bl w) = xs\<rbrakk> \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs)
[PROOF STEP]
by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl)


[STATEMENT]
lemma of_bl_length_less:
  \<open>(of_bl x :: 'a::len word) < 2 ^ k\<close>
    if \<open>length x = k\<close> \<open>k < LENGTH('a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl x < 2 ^ k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_bl x < 2 ^ k
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
length x = k
k < LENGTH('a)
[PROOF STEP]
have \<open>length x < LENGTH('a)\<close>
[PROOF STATE]
proof (prove)
using this:
length x = k
k < LENGTH('a)

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

goal (1 subgoal):
 1. of_bl x < 2 ^ k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length x < LENGTH('a)
[PROOF STEP]
have \<open>(of_bl x :: 'a::len word) < 2 ^ length x\<close>
[PROOF STATE]
proof (prove)
using this:
length x < LENGTH('a)

goal (1 subgoal):
 1. of_bl x < 2 ^ length x
[PROOF STEP]
apply (simp add: of_bl_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length x < LENGTH('a) \<Longrightarrow> horner_sum of_bool 2 (rev x) < 2 ^ length x
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. length x < LENGTH('a) \<Longrightarrow> take_bit LENGTH('a) (horner_sum of_bool 2 (rev x)) < take_bit LENGTH('a) (2 ^ length x)
[PROOF STEP]
apply (simp add: take_bit_horner_sum_bit_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. length x < LENGTH('a) \<Longrightarrow> horner_sum of_bool 2 (rev x) < 2 ^ length x
[PROOF STEP]
apply (subst length_rev [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. length x < LENGTH('a) \<Longrightarrow> horner_sum of_bool 2 (rev x) < 2 ^ length (rev x)
[PROOF STEP]
apply (simp only: horner_sum_of_bool_2_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
of_bl x < 2 ^ length x

goal (1 subgoal):
 1. of_bl x < 2 ^ k
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
length x = k
k < LENGTH('a)
of_bl x < 2 ^ length x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length x = k
k < LENGTH('a)
of_bl x < 2 ^ length x

goal (1 subgoal):
 1. of_bl x < 2 ^ k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_bl x < 2 ^ k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (NOT w) = map Not (to_bl w)
[PROOF STEP]
by transfer (simp add: bl_not_bin)


[STATEMENT]
lemma bl_word_xor: "to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)
[PROOF STEP]
by transfer (simp flip: bl_xor_bin)


[STATEMENT]
lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)
[PROOF STEP]
by transfer (simp flip: bl_or_bin)


[STATEMENT]
lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)
[PROOF STEP]
by transfer (simp flip: bl_and_bin)


[STATEMENT]
lemma bin_nth_uint': "bit (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w)
[PROOF STEP]
apply (unfold word_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (uint w) n = (rev (bin_to_bl LENGTH('a) (uint w)) ! n \<and> n < LENGTH('a))
[PROOF STEP]
apply (safe elim!: bin_nth_uint_imp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bit (uint w) n \<Longrightarrow> rev (bin_to_bl LENGTH('a) (uint w)) ! n
 2. \<lbrakk>rev (bin_to_bl LENGTH('a) (uint w)) ! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (uint w) n
[PROOF STEP]
apply (frule bin_nth_uint_imp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bit (uint w) n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> rev (bin_to_bl LENGTH('a) (uint w)) ! n
 2. \<lbrakk>rev (bin_to_bl LENGTH('a) (uint w)) ! n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (uint w) n
[PROOF STEP]
apply (fast dest!: bin_nth_bl)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma test_bit_bl: "bit w n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit w n = (rev (to_bl w) ! n \<and> n < size w)
[PROOF STEP]
by transfer (auto simp add: bin_nth_bl)


[STATEMENT]
lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = bit w (size w - Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < size w \<Longrightarrow> to_bl w ! n = bit w (size w - Suc n)
[PROOF STEP]
by (simp add: word_size rev_nth test_bit_bl)


[STATEMENT]
lemma map_bit_interval_eq:
  \<open>map (bit w) [0..<n] = takefill False n (rev (to_bl w))\<close> for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (bit w) [0..<n] = takefill False n (rev (to_bl w))
[PROOF STEP]
proof (rule nth_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (map (bit w) [0..<n]) = length (takefill False n (rev (to_bl w)))
 2. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i
[PROOF STEP]
show \<open>length (map (bit w) [0..<n]) =
    length (takefill False n (rev (to_bl w)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (bit w) [0..<n]) = length (takefill False n (rev (to_bl w)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (map (bit w) [0..<n]) = length (takefill False n (rev (to_bl w)))

goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i
[PROOF STEP]
assume \<open>m < length (map (bit w) [0..<n])\<close>
[PROOF STATE]
proof (state)
this:
m < length (map (bit w) [0..<n])

goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m < length (map (bit w) [0..<n])
[PROOF STEP]
have \<open>m < n\<close>
[PROOF STATE]
proof (prove)
using this:
m < length (map (bit w) [0..<n])

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

goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m < n
[PROOF STEP]
have \<open>bit w m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. bit w m = takefill False n (rev (to_bl w)) ! m
[PROOF STEP]
by (auto simp add: nth_takefill not_less rev_nth to_bl_nth word_size dest: bit_imp_le_length)
[PROOF STATE]
proof (state)
this:
bit w m = takefill False n (rev (to_bl w)) ! m

goal (1 subgoal):
 1. \<And>i. i < length (map (bit w) [0..<n]) \<Longrightarrow> map (bit w) [0..<n] ! i = takefill False n (rev (to_bl w)) ! i
[PROOF STEP]
with \<open>m < n \<close>
[PROOF STATE]
proof (chain)
picking this:
m < n
bit w m = takefill False n (rev (to_bl w)) ! m
[PROOF STEP]
show \<open>map (bit w) [0..<n] ! m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
[PROOF STATE]
proof (prove)
using this:
m < n
bit w m = takefill False n (rev (to_bl w)) ! m

goal (1 subgoal):
 1. map (bit w) [0..<n] ! m = takefill False n (rev (to_bl w)) ! m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (bit w) [0..<n] ! m = takefill False n (rev (to_bl w)) ! m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_bl_unfold:
  \<open>to_bl w = rev (map (bit w) [0..<LENGTH('a)])\<close> for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = rev (map (bit w) [0..<LENGTH('a)])
[PROOF STEP]
by (simp add: map_bit_interval_eq takefill_bintrunc to_bl_def flip: bin_to_bl_def)


[STATEMENT]
lemma nth_rev_to_bl:
  \<open>rev (to_bl w) ! n \<longleftrightarrow> bit w n\<close>
  if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (to_bl w) ! n = bit w n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. rev (to_bl w) ! n = bit w n
[PROOF STEP]
by (simp add: to_bl_unfold)


[STATEMENT]
lemma nth_to_bl:
  \<open>to_bl w ! n \<longleftrightarrow> bit w (LENGTH('a) - Suc n)\<close>
  if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w ! n = bit w (LENGTH('a) - Suc n)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. to_bl w ! n = bit w (LENGTH('a) - Suc n)
[PROOF STEP]
by (simp add: to_bl_unfold rev_nth)


[STATEMENT]
lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (replicate n False @ bs) = of_bl bs
[PROOF STEP]
by (auto simp: of_bl_def bl_to_bin_rep_F)


[STATEMENT]
lemma [code abstract]:
  \<open>Word.the_int (of_bl bs :: 'a word) = horner_sum of_bool 2 (take LENGTH('a::len) (rev bs))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Word.the_int (of_bl bs) = horner_sum of_bool 2 (take LENGTH('a) (rev bs))
[PROOF STEP]
apply (simp add: of_bl_eq flip: take_bit_horner_sum_bit_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uint (horner_sum of_bool 2 (rev bs)) = take_bit LENGTH('a) (horner_sum of_bool 2 (rev bs))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>bs. take_bit LENGTH('a) (horner_sum of_bool 2 (rev bs)) = take_bit LENGTH('a) (horner_sum of_bool 2 (rev bs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code]:
  \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a::len)])\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = map (bit w) (rev [0..<LENGTH('a)])
[PROOF STEP]
by (fact to_bl_eq_rev)


[STATEMENT]
lemma word_reverse_eq_of_bl_rev_to_bl:
  \<open>word_reverse w = of_bl (rev (to_bl w))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_reverse w = of_bl (rev (to_bl w))
[PROOF STEP]
by (rule bit_word_eqI)
    (auto simp add: bit_word_reverse_iff bit_of_bl_iff nth_to_bl)


[STATEMENT]
lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (word_reverse w) = rev (to_bl w)
[PROOF STEP]
by (rule nth_equalityI) (simp_all add: nth_rev_to_bl word_reverse_def word_rep_drop flip: of_bl_eq)


[STATEMENT]
lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (- 1) = replicate LENGTH('a) True
[PROOF STEP]
apply (rule word_bl.Abs_inverse')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. replicate LENGTH('a) True \<in> {bl. length bl = LENGTH('a)}
 2. of_bl (replicate LENGTH('a) True) = - 1
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (replicate LENGTH('a) True) = - 1
[PROOF STEP]
apply (rule word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size (of_bl (replicate LENGTH('a) True)) \<longrightarrow> bit (of_bl (replicate LENGTH('a) True)) n = bit (- 1) n
[PROOF STEP]
apply (clarsimp simp add: word_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (of_bl (replicate LENGTH('a) True)) n
[PROOF STEP]
apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))
[PROOF STEP]
by (simp add: zip_rev bl_word_or rev_map)


[STATEMENT]
lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))
[PROOF STEP]
by (simp add: zip_rev bl_word_and rev_map)


[STATEMENT]
lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))
[PROOF STEP]
by (simp add: zip_rev bl_word_xor rev_map)


[STATEMENT]
lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (to_bl (NOT x)) = map Not (rev (to_bl x))
[PROOF STEP]
by (simp add: bl_word_not rev_map)


[STATEMENT]
lemma bshiftr1_numeral [simp]:
  \<open>bshiftr1 b (numeral w :: 'a word) = of_bl (b # butlast (bin_to_bl LENGTH('a::len) (numeral w)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. numeral w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b) = of_bl (b # butlast (bin_to_bl LENGTH('a) (numeral w)))
[PROOF STEP]
by (rule bit_word_eqI) (auto simp add: bit_simps rev_nth nth_append nth_butlast nth_bin_to_bl simp flip: bit_Suc)


[STATEMENT]
lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b)) = b # butlast (to_bl w)
[PROOF STEP]
unfolding bshiftr1_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl (b # butlast (to_bl w))) = b # butlast (to_bl w)
[PROOF STEP]
by (rule word_bl.Abs_inverse) simp


[STATEMENT]
lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shiftl1 (of_bl bl) = of_bl (bl @ [False])
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftl1 (of_bl bl)) n = bit (of_bl (bl @ [False])) n
[PROOF STEP]
apply (simp add: bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> (0 < n \<and> rev bl ! (n - Suc 0) \<and> n - Suc 0 < LENGTH('a) \<and> n - Suc 0 < length bl) = ((False # rev bl) ! n \<and> n < Suc (length bl))
[PROOF STEP]
subgoal for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> (0 < n \<and> rev bl ! (n - Suc 0) \<and> n - Suc 0 < LENGTH('a) \<and> n - Suc 0 < length bl) = ((False # rev bl) ! n \<and> n < Suc (length bl))
[PROOF STEP]
apply (cases n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); n = 0\<rbrakk> \<Longrightarrow> (0 < n \<and> rev bl ! (n - Suc 0) \<and> n - Suc 0 < LENGTH('a) \<and> n - Suc 0 < length bl) = ((False # rev bl) ! n \<and> n < Suc (length bl))
 2. \<And>nat. \<lbrakk>n < LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> (0 < n \<and> rev bl ! (n - Suc 0) \<and> n - Suc 0 < LENGTH('a) \<and> n - Suc 0 < length bl) = ((False # rev bl) ! n \<and> n < Suc (length bl))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shiftl1 w = of_bl (to_bl w @ [False])
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftl1 w) n = bit (of_bl (to_bl w @ [False])) n
[PROOF STEP]
apply (simp add: bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> (0 < n \<and> bit w (n - Suc 0)) = (False # rev (to_bl w)) ! n
[PROOF STEP]
subgoal for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> (0 < n \<and> bit w (n - Suc 0)) = (False # rev (to_bl w)) ! n
[PROOF STEP]
apply (cases n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); n = 0\<rbrakk> \<Longrightarrow> (0 < n \<and> bit w (n - Suc 0)) = (False # rev (to_bl w)) ! n
 2. \<And>nat. \<lbrakk>n < LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> (0 < n \<and> bit w (n - Suc 0)) = (False # rev (to_bl w)) ! n
[PROOF STEP]
apply (simp_all add: nth_rev_to_bl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
  for w :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (shiftl1 w) = tl (to_bl w) @ [False]
[PROOF STEP]
by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)


[STATEMENT]
lemma to_bl_double_eq:
  \<open>to_bl (2 * w) = tl (to_bl w) @ [False]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (2 * w) = tl (to_bl w) @ [False]
[PROOF STEP]
using bl_shiftl1 [of w]
[PROOF STATE]
proof (prove)
using this:
to_bl (shiftl1 w) = tl (to_bl w) @ [False]

goal (1 subgoal):
 1. to_bl (2 * w) = tl (to_bl w) @ [False]
[PROOF STEP]
by (simp add: shiftl1_def ac_simps)

\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>


[STATEMENT]
lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (shiftl1 w) = tl (to_bl w @ [False])
[PROOF STEP]
by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)


[STATEMENT]
lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)"
  for w :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (shiftr1 w) = False # butlast (to_bl w)
[PROOF STEP]
by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])

\<comment> \<open>Generalized version of \<open>bl_shiftr1\<close>. Maybe this one should replace it?\<close>


[STATEMENT]
lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (shiftr1 w) = butlast (False # to_bl w)
[PROOF STEP]
apply (rule word_bl.Abs_inverse')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. butlast (False # to_bl w) \<in> {bl. length bl = LENGTH('a)}
 2. of_bl (butlast (False # to_bl w)) = shiftr1 w
[PROOF STEP]
apply (simp del: butlast.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (butlast (False # to_bl w)) = shiftr1 w
[PROOF STEP]
apply (simp add: shiftr1_bl of_bl_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)"
  for w :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)
[PROOF STEP]
proof (rule nth_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
 2. \<And>i. i < length (to_bl (sshiftr1 w)) \<Longrightarrow> to_bl (sshiftr1 w) ! i = (hd (to_bl w) # butlast (to_bl w)) ! i
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
 2. \<And>i. i < length (to_bl (sshiftr1 w)) \<Longrightarrow> to_bl (sshiftr1 w) ! i = (hd (to_bl w) # butlast (to_bl w)) ! i
[PROOF STEP]
assume \<open>n < length (to_bl (sshiftr1 w))\<close>
[PROOF STATE]
proof (state)
this:
n < length (to_bl (sshiftr1 w))

goal (2 subgoals):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
 2. \<And>i. i < length (to_bl (sshiftr1 w)) \<Longrightarrow> to_bl (sshiftr1 w) ! i = (hd (to_bl w) # butlast (to_bl w)) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < length (to_bl (sshiftr1 w))
[PROOF STEP]
have \<open>n < LENGTH('a)\<close>
[PROOF STATE]
proof (prove)
using this:
n < length (to_bl (sshiftr1 w))

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

goal (2 subgoals):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
 2. \<And>i. i < length (to_bl (sshiftr1 w)) \<Longrightarrow> to_bl (sshiftr1 w) ! i = (hd (to_bl w) # butlast (to_bl w)) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < LENGTH('a)
[PROOF STEP]
show \<open>to_bl (sshiftr1 w) ! n \<longleftrightarrow> (hd (to_bl w) # butlast (to_bl w)) ! n\<close>
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. to_bl (sshiftr1 w) ! n = (hd (to_bl w) # butlast (to_bl w)) ! n
[PROOF STEP]
apply (cases n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); n = 0\<rbrakk> \<Longrightarrow> to_bl (sshiftr1 w) ! n = (hd (to_bl w) # butlast (to_bl w)) ! n
 2. \<And>nat. \<lbrakk>n < LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> to_bl (sshiftr1 w) ! n = (hd (to_bl w) # butlast (to_bl w)) ! n
[PROOF STEP]
apply (simp_all add: to_bl_nth word_size hd_conv_nth bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
to_bl (sshiftr1 w) ! n = (hd (to_bl w) # butlast (to_bl w)) ! n

goal (1 subgoal):
 1. length (to_bl (sshiftr1 w)) = length (hd (to_bl w) # butlast (to_bl w))
[PROOF STEP]
qed simp


[STATEMENT]
lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
  for w :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (drop n (to_bl (w >> n))) = length (take (size w - n) (to_bl w))
 2. \<And>i. i < length (drop n (to_bl (w >> n))) \<Longrightarrow> drop n (to_bl (w >> n)) ! i = take (size w - n) (to_bl w) ! i
[PROOF STEP]
apply (simp_all add: word_size to_bl_nth bit_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
  for w :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (drop n (to_bl (w >>> n))) = length (take (size w - n) (to_bl w))
 2. \<And>i. i < length (drop n (to_bl (w >>> n))) \<Longrightarrow> drop n (to_bl (w >>> n)) ! i = take (size w - n) (to_bl w) ! i
[PROOF STEP]
apply (simp_all add: word_size nth_to_bl bit_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n \<le> size w \<Longrightarrow> length (take n (to_bl (w >> n))) = length (replicate n False)
 2. \<And>i. \<lbrakk>n \<le> size w; i < length (take n (to_bl (w >> n)))\<rbrakk> \<Longrightarrow> take n (to_bl (w >> n)) ! i = replicate n False ! i
[PROOF STEP]
apply (auto simp add: word_size to_bl_nth bit_simps dest: bit_imp_le_length)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma take_sshiftr':
  "n \<le> size w \<Longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
    take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
  for w :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> size w \<Longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and> take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))
[PROOF STEP]
apply (cases n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> size w; n = 0\<rbrakk> \<Longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and> take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))
 2. \<And>nat. \<lbrakk>n \<le> size w; n = Suc nat\<rbrakk> \<Longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and> take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))
[PROOF STEP]
apply (auto simp add: hd_to_bl_iff bit_simps not_less word_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>Suc nat \<le> LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> take (Suc nat) (to_bl (w >>> Suc nat)) = bit w (LENGTH('a) - Suc 0) # replicate nat (bit w (LENGTH('a) - Suc 0))
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>Suc nat \<le> LENGTH('a); n = Suc nat\<rbrakk> \<Longrightarrow> length (take (Suc nat) (to_bl (w >>> Suc nat))) = length (bit w (LENGTH('a) - Suc 0) # replicate nat (bit w (LENGTH('a) - Suc 0)))
 2. \<And>nat i. \<lbrakk>Suc nat \<le> LENGTH('a); n = Suc nat; i < length (take (Suc nat) (to_bl (w >>> Suc nat)))\<rbrakk> \<Longrightarrow> take (Suc nat) (to_bl (w >>> Suc nat)) ! i = (bit w (LENGTH('a) - Suc 0) # replicate nat (bit w (LENGTH('a) - Suc 0))) ! i
[PROOF STEP]
apply (auto simp add: nth_to_bl bit_simps nth_Cons split: nat.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take n xs = t; drop n xs = d\<rbrakk> \<Longrightarrow> xs = t @ d
[PROOF STEP]
by (auto intro: append_take_drop_id [symmetric])


[STATEMENT]
lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl bl << n = of_bl (bl @ replicate n False)
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (of_bl bl << n) na = bit (of_bl (bl @ replicate n False)) na
[PROOF STEP]
apply (auto simp add: bit_simps nth_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
  for w :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w << n = of_bl (to_bl w @ replicate n False)
[PROOF STEP]
by (simp flip: shiftl_of_bl)


[STATEMENT]
lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False
[PROOF STEP]
by (simp add: shiftl_bl word_rep_drop word_size)


[STATEMENT]
lemma shiftr1_bl_of:
  "length bl \<le> LENGTH('a) \<Longrightarrow>
    shiftr1 (of_bl bl::'a::len word) = of_bl (butlast bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl \<le> LENGTH('a) \<Longrightarrow> shiftr1 (of_bl bl) = of_bl (butlast bl)
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>length bl \<le> LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (shiftr1 (of_bl bl)) n = bit (of_bl (butlast bl)) n
[PROOF STEP]
apply (simp add: bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>length bl \<le> LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> (rev bl ! Suc n \<and> Suc n < LENGTH('a) \<and> Suc n < length bl) = (rev (butlast bl) ! n \<and> n < length bl - Suc 0)
[PROOF STEP]
apply (cases bl rule: rev_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>length bl \<le> LENGTH('a); n < LENGTH('a); bl = []\<rbrakk> \<Longrightarrow> (rev bl ! Suc n \<and> Suc n < LENGTH('a) \<and> Suc n < length bl) = (rev (butlast bl) ! n \<and> n < length bl - Suc 0)
 2. \<And>n ys y. \<lbrakk>length bl \<le> LENGTH('a); n < LENGTH('a); bl = ys @ [y]\<rbrakk> \<Longrightarrow> (rev bl ! Suc n \<and> Suc n < LENGTH('a) \<and> Suc n < length bl) = (rev (butlast bl) ! n \<and> n < length bl - Suc 0)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma shiftr_bl_of:
  "length bl \<le> LENGTH('a) \<Longrightarrow>
     (of_bl bl::'a::len word) >> n = of_bl (take (length bl - n) bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl \<le> LENGTH('a) \<Longrightarrow> of_bl bl >> n = of_bl (take (length bl - n) bl)
[PROOF STEP]
by (rule bit_word_eqI) (auto simp add: bit_simps rev_nth)


[STATEMENT]
lemma shiftr_bl: "x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))"
  for x :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))
[PROOF STEP]
using shiftr_bl_of [where 'a='a, of "to_bl x"]
[PROOF STATE]
proof (prove)
using this:
length (to_bl x) \<le> LENGTH('a) \<Longrightarrow> of_bl (to_bl x) >> ?n = of_bl (take (length (to_bl x) - ?n) (to_bl x))

goal (1 subgoal):
 1. x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))
[PROOF STEP]
by simp


[STATEMENT]
lemma aligned_bl_add_size [OF refl]:
  "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
    take m (to_bl y) = replicate m False \<Longrightarrow>
    to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)" for x :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply (subgoal_tac "x AND y = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> x AND y = 0
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> x AND y = 0
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply (rule word_bl.Rep_eqD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> to_bl (x AND y) = to_bl 0
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply (simp add: bl_word_and)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> map2 (\<and>) (to_bl x) (to_bl y) = replicate LENGTH('a) False
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply (rule align_lem_and [THEN trans])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> length (to_bl x) = ?n4 + ?m4
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> length (to_bl y) = ?n4 + ?m4
 3. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> drop ?m4 (to_bl x) = replicate ?n4 False
 4. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> take ?m4 (to_bl y) = replicate ?m4 False
 5. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> replicate (?n4 + ?m4) False = replicate LENGTH('a) False
 6. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply (simp_all add: word_size)[5]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>LENGTH('a) - n = m; n \<le> LENGTH('a); drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> n + m = LENGTH('a)
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply (subst word_plus_and_or [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl ((x AND y) + (x OR y)) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply (simp add : bl_word_or)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> map2 (\<or>) (to_bl x) (to_bl y) = take m (to_bl x) @ drop m (to_bl y)
[PROOF STEP]
apply (rule align_lem_or)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> length (to_bl x) = ?n88 + m
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> length (to_bl y) = ?n88 + m
 3. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> drop m (to_bl x) = replicate ?n88 False
 4. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> take m (to_bl y) = replicate m False
[PROOF STEP]
apply (simp_all add: word_size)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mask_bl: "mask n = of_bl (replicate n True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mask n = of_bl (replicate n True)
[PROOF STEP]
by (auto simp add: bit_simps intro!: word_eqI)


[STATEMENT]
lemma bl_and_mask':
  "to_bl (w AND mask n :: 'a::len word) =
    replicate (LENGTH('a) - n) False @
    drop (LENGTH('a) - n) (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w)
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (to_bl (w AND mask n)) = length (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w))
 2. \<And>i. i < length (to_bl (w AND mask n)) \<Longrightarrow> to_bl (w AND mask n) ! i = (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w)) ! i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (to_bl (w AND mask n)) \<Longrightarrow> to_bl (w AND mask n) ! i = (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w)) ! i
[PROOF STEP]
apply (clarsimp simp add: to_bl_nth word_size bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < LENGTH('a) \<Longrightarrow> (bit w (LENGTH('a) - Suc i) \<and> LENGTH('a) - Suc i < n) = (replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w)) ! i
[PROOF STEP]
apply (auto simp add: word_size test_bit_bl nth_append rev_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma slice1_eq_of_bl:
  \<open>(slice1 n w :: 'b::len word) = of_bl (takefill False n (to_bl w))\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice1 n w = of_bl (takefill False n (to_bl w))
[PROOF STEP]
proof (rule bit_word_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('b) \<Longrightarrow> bit (slice1 n w) na = bit (of_bl (takefill False n (to_bl w))) na
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('b) \<Longrightarrow> bit (slice1 n w) na = bit (of_bl (takefill False n (to_bl w))) na
[PROOF STEP]
assume \<open>m < LENGTH('b)\<close>
[PROOF STATE]
proof (state)
this:
m < LENGTH('b)

goal (1 subgoal):
 1. \<And>na. na < LENGTH('b) \<Longrightarrow> bit (slice1 n w) na = bit (of_bl (takefill False n (to_bl w))) na
[PROOF STEP]
show \<open>bit (slice1 n w :: 'b::len word) m \<longleftrightarrow> bit (of_bl (takefill False n (to_bl w)) :: 'b word) m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (slice1 n w) m = bit (of_bl (takefill False n (to_bl w))) m
[PROOF STEP]
by (cases \<open>m \<ge> n\<close>; cases \<open>LENGTH('a) \<ge> n\<close>)
      (auto simp add: bit_slice1_iff bit_of_bl_iff not_less rev_nth not_le nth_takefill nth_to_bl algebra_simps)
[PROOF STATE]
proof (state)
this:
bit (slice1 n w) m = bit (of_bl (takefill False n (to_bl w))) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma slice1_no_bin [simp]:
  "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len)) (numeral w)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice1 n (numeral w) = of_bl (takefill False n (bin_to_bl LENGTH('b) (numeral w)))
[PROOF STEP]
by (simp add: slice1_eq_of_bl)


[STATEMENT]
lemma slice_no_bin [simp]:
  "slice n (numeral w :: 'b word) = of_bl (takefill False (LENGTH('b::len) - n)
    (bin_to_bl (LENGTH('b::len)) (numeral w)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice n (numeral w) = of_bl (takefill False (LENGTH('b) - n) (bin_to_bl LENGTH('b) (numeral w)))
[PROOF STEP]
by (simp add: slice_def)


[STATEMENT]
lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice n w = of_bl (take (size w - n) (to_bl w))
[PROOF STEP]
by (simp add: slice_def word_size slice1_eq_of_bl takefill_alt)


[STATEMENT]
lemma slice1_down_alt':
  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
    to_bl sl = takefill False fs (drop k (to_bl w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sl = slice1 n w; fs = size sl; fs + k = n\<rbrakk> \<Longrightarrow> to_bl sl = takefill False fs (drop k (to_bl w))
[PROOF STEP]
apply (simp add: slice1_eq_of_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sl = of_bl (takefill False n (to_bl w)); fs = size (of_bl (takefill False n (to_bl w))); size (of_bl (takefill False n (to_bl w))) + k = n\<rbrakk> \<Longrightarrow> to_bl (of_bl (takefill False n (to_bl w))) = takefill False (size (of_bl (takefill False n (to_bl w)))) (drop k (to_bl w))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sl n w fs k. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); fs = LENGTH('a); LENGTH('a) + k = n\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))) = takefill False LENGTH('a) (drop k (bin_to_bl LENGTH('b) w))
[PROOF STEP]
apply (simp add: bl_bin_bl_rep_drop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sl n w fs k. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); fs = LENGTH('a); LENGTH('a) + k = n\<rbrakk> \<Longrightarrow> drop (n - LENGTH('a)) (takefill False n (bin_to_bl LENGTH('b) w)) = takefill False LENGTH('a) (drop k (bin_to_bl LENGTH('b) w))
[PROOF STEP]
using drop_takefill
[PROOF STATE]
proof (prove)
using this:
drop ?k (takefill ?fill (?m + ?k) ?w) = takefill ?fill ?m (drop ?k ?w)

goal (1 subgoal):
 1. \<And>sl n w fs k. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); fs = LENGTH('a); LENGTH('a) + k = n\<rbrakk> \<Longrightarrow> drop (n - LENGTH('a)) (takefill False n (bin_to_bl LENGTH('b) w)) = takefill False LENGTH('a) (drop k (bin_to_bl LENGTH('b) w))
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma slice1_up_alt':
  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
    to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sl = slice1 n w; fs = size sl; fs = n + k\<rbrakk> \<Longrightarrow> to_bl sl = takefill False fs (replicate k False @ to_bl w)
[PROOF STEP]
apply (simp add: slice1_eq_of_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sl = of_bl (takefill False n (to_bl w)); n + k = size (of_bl (takefill False n (to_bl w))); fs = size (of_bl (takefill False n (to_bl w)))\<rbrakk> \<Longrightarrow> to_bl (of_bl (takefill False n (to_bl w))) = takefill False (size (of_bl (takefill False n (to_bl w)))) (replicate k False @ to_bl w)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sl n w k fs. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); n + k = LENGTH('a); fs = LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))) = takefill False LENGTH('a) (replicate k False @ bin_to_bl LENGTH('b) w)
[PROOF STEP]
apply (simp add: bl_bin_bl_rep_drop flip: takefill_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>sl n w k fs. \<lbrakk>take_bit LENGTH('a) sl = take_bit LENGTH('a) (bl_to_bin (takefill False n (bin_to_bl LENGTH('b) w))); n + k = LENGTH('a); fs = LENGTH('a)\<rbrakk> \<Longrightarrow> takefill False LENGTH('a) (replicate (LENGTH('a) - n) False @ bin_to_bl LENGTH('b) w) = takefill False LENGTH('a) (replicate k False @ bin_to_bl LENGTH('b) w)
[PROOF STEP]
apply (metis diff_add_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma slice1_tf_tf':
  "to_bl (slice1 n w :: 'a::len word) =
    rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (slice1 n w) = rev (takefill False LENGTH('a) (rev (takefill False n (to_bl w))))
[PROOF STEP]
unfolding slice1_eq_of_bl
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl (takefill False n (to_bl w))) = rev (takefill False LENGTH('a) (rev (takefill False n (to_bl w))))
[PROOF STEP]
by (rule word_rev_tf)


[STATEMENT]
lemma revcast_eq_of_bl:
  \<open>(revcast w :: 'b::len word) = of_bl (takefill False (LENGTH('b)) (to_bl w))\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revcast w = of_bl (takefill False LENGTH('b) (to_bl w))
[PROOF STEP]
by (simp add: revcast_def slice1_eq_of_bl)


[STATEMENT]
lemma to_bl_revcast:
  "to_bl (revcast w :: 'a::len word) = takefill False (LENGTH('a)) (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (revcast w) = takefill False LENGTH('a) (to_bl w)
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (to_bl (revcast w)) = length (takefill False LENGTH('a) (to_bl w))
 2. \<And>i. i < length (to_bl (revcast w)) \<Longrightarrow> to_bl (revcast w) ! i = takefill False LENGTH('a) (to_bl w) ! i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (to_bl (revcast w)) \<Longrightarrow> to_bl (revcast w) ! i = takefill False LENGTH('a) (to_bl w) ! i
[PROOF STEP]
apply (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < length (to_bl (revcast w)); LENGTH('a) \<le> LENGTH('b)\<rbrakk> \<Longrightarrow> to_bl (revcast w) ! i = takefill False LENGTH('a) (to_bl w) ! i
 2. \<And>i. \<lbrakk>i < length (to_bl (revcast w)); \<not> LENGTH('a) \<le> LENGTH('b)\<rbrakk> \<Longrightarrow> to_bl (revcast w) ! i = takefill False LENGTH('a) (to_bl w) ! i
[PROOF STEP]
apply (auto simp add: nth_to_bl nth_takefill bit_revcast_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_cat a b = of_bl (to_bl a @ to_bl b)
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (word_cat a b) n = bit (of_bl (to_bl a @ to_bl b)) n
[PROOF STEP]
apply (simp add: bit_word_cat_iff bit_of_bl_iff nth_append not_less nth_rev_to_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> LENGTH('c) \<le> n \<longrightarrow> bit a (n - LENGTH('c)) = (rev (to_bl a) ! (n - LENGTH('c)) \<and> n < LENGTH('b) + LENGTH('c))
[PROOF STEP]
apply (meson bit_word.rep_eq less_diff_conv2 nth_rev_to_bl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma of_bl_append:
  "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (xs @ ys) = of_bl xs * 2 ^ length ys + of_bl ys
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs ys. take_bit LENGTH('a) (bl_to_bin (xs @ ys)) = take_bit LENGTH('a) (bl_to_bin xs * 2 ^ length ys + bl_to_bin ys)
[PROOF STEP]
apply (simp add: bl_to_bin_app_cat bin_cat_num)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (False # xs) = of_bl xs
[PROOF STEP]
by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)


[STATEMENT]
lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (True # xs) = 2 ^ length xs + of_bl xs
[PROOF STEP]
by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)


[STATEMENT]
lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (x # xs) = of_bool x * 2 ^ length xs + of_bl xs
[PROOF STEP]
by (cases x) simp_all


[STATEMENT]
lemma word_split_bl':
  "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
    (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>std = size c - size b; word_split c = (a, b)\<rbrakk> \<Longrightarrow> a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))
[PROOF STEP]
apply (simp add: word_split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>std = size c - size b; ucast (drop_bit LENGTH('b) c) = a \<and> ucast c = b\<rbrakk> \<Longrightarrow> a = of_bl (take (size c - size b) (to_bl c)) \<and> b = of_bl (drop (size c - size b) (to_bl c))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>std c b a. \<lbrakk>std = LENGTH('a) - LENGTH('b); take_bit LENGTH('c) (take_bit LENGTH('a) ((drop_bit LENGTH('b) \<circ> take_bit LENGTH('a)) c)) = take_bit LENGTH('c) a \<and> take_bit LENGTH('b) (take_bit LENGTH('a) c) = take_bit LENGTH('b) b\<rbrakk> \<Longrightarrow> take_bit LENGTH('c) a = take_bit LENGTH('c) (bl_to_bin (take (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c))) \<and> take_bit LENGTH('b) b = take_bit LENGTH('b) (bl_to_bin (drop (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c)))
[PROOF STEP]
apply (cases \<open>LENGTH('b) \<le> LENGTH('a)\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>std c b a. \<lbrakk>std = LENGTH('a) - LENGTH('b); take_bit LENGTH('c) (take_bit LENGTH('a) ((drop_bit LENGTH('b) \<circ> take_bit LENGTH('a)) c)) = take_bit LENGTH('c) a \<and> take_bit LENGTH('b) (take_bit LENGTH('a) c) = take_bit LENGTH('b) b; LENGTH('b) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('c) a = take_bit LENGTH('c) (bl_to_bin (take (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c))) \<and> take_bit LENGTH('b) b = take_bit LENGTH('b) (bl_to_bin (drop (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c)))
 2. \<And>std c b a. \<lbrakk>std = LENGTH('a) - LENGTH('b); take_bit LENGTH('c) (take_bit LENGTH('a) ((drop_bit LENGTH('b) \<circ> take_bit LENGTH('a)) c)) = take_bit LENGTH('c) a \<and> take_bit LENGTH('b) (take_bit LENGTH('a) c) = take_bit LENGTH('b) b; \<not> LENGTH('b) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('c) a = take_bit LENGTH('c) (bl_to_bin (take (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c))) \<and> take_bit LENGTH('b) b = take_bit LENGTH('b) (bl_to_bin (drop (LENGTH('a) - LENGTH('b)) (bin_to_bl LENGTH('a) c)))
[PROOF STEP]
apply (auto simp add: drop_bit_take_bit drop_bin2bl bin_to_bl_drop_bit [symmetric, of \<open>LENGTH('a)\<close> \<open>LENGTH('a) - LENGTH('b)\<close> \<open>LENGTH('b)\<close>] min_absorb2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_split_bl: "std = size c - size b \<Longrightarrow>
    (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
    word_split c = (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. std = size c - size b \<Longrightarrow> (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) = (word_split c = (a, b))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>std = size c - size b; a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (a, b)
 2. \<lbrakk>std = size c - size b; word_split c = (a, b)\<rbrakk> \<Longrightarrow> a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>std = size c - size b; word_split c = (a, b)\<rbrakk> \<Longrightarrow> a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))
 2. \<lbrakk>std = size c - size b; a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (a, b)
[PROOF STEP]
apply (erule (1) word_split_bl')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>std = size c - size b; a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (a, b)
[PROOF STEP]
apply (case_tac "word_split c")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>std = size c - size b; a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)); word_split c = (aa, ba)\<rbrakk> \<Longrightarrow> word_split c = (a, b)
[PROOF STEP]
apply (auto simp add: word_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>std = LENGTH('a) - LENGTH('b); word_split c = (aa, ba); a = of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)); b = of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)), of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c)))
[PROOF STEP]
apply (frule word_split_bl' [rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>std = LENGTH('a) - LENGTH('b); word_split c = (aa, ba); a = of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)); b = of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c))\<rbrakk> \<Longrightarrow> ?std8 aa ba = size c - size ba
 2. \<And>aa ba. \<lbrakk>std = LENGTH('a) - LENGTH('b); word_split c = (aa, ba); a = of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)); b = of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c)); aa = of_bl (take (?std8 aa ba) (to_bl c)) \<and> ba = of_bl (drop (?std8 aa ba) (to_bl c))\<rbrakk> \<Longrightarrow> word_split c = (of_bl (take (LENGTH('a) - LENGTH('b)) (to_bl c)), of_bl (drop (LENGTH('a) - LENGTH('b)) (to_bl c)))
[PROOF STEP]
apply (auto simp add: word_size)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_split_bl_eq:
  "(word_split c :: ('c::len word \<times> 'd::len word)) =
    (of_bl (take (LENGTH('a::len) - LENGTH('d::len)) (to_bl c)),
     of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))"
  for c :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_split c = (of_bl (take (LENGTH('a) - LENGTH('d)) (to_bl c)), of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))
[PROOF STEP]
apply (rule word_split_bl [THEN iffD1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?std1 = size c - size (of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))
 2. of_bl (take (LENGTH('a) - LENGTH('d)) (to_bl c)) = of_bl (take ?std1 (to_bl c)) \<and> of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)) = of_bl (drop ?std1 (to_bl c))
[PROOF STEP]
apply (unfold word_size)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?std1 = LENGTH('a) - LENGTH('d)
 2. of_bl (take (LENGTH('a) - LENGTH('d)) (to_bl c)) = of_bl (take ?std1 (to_bl c)) \<and> of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)) = of_bl (drop ?std1 (to_bl c))
[PROOF STEP]
apply (rule refl conjI)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_rcat_bl:
  \<open>word_rcat wl = of_bl (concat (map to_bl wl))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl))
[PROOF STEP]
define ws where \<open>ws = rev wl\<close>
[PROOF STATE]
proof (state)
this:
ws = rev wl

goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ws = rev wl

goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl))
[PROOF STEP]
have \<open>word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))
[PROOF STEP]
apply (simp add: word_rcat_def of_bl_eq rev_concat rev_map comp_def rev_to_bl_eq flip: horner_sum_of_bool_2_concat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_of_int (horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('b)]) ws))) = horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('b)]) ws))
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ws. take_bit LENGTH('c) (horner_sum of_bool 2 (concat (map (\<lambda>x. map (\<lambda>n. n < LENGTH('b) \<and> bit x n) [0..<LENGTH('b)]) ws))) = take_bit LENGTH('c) (horner_sum of_bool 2 (concat (map (\<lambda>x. map (\<lambda>n. n < LENGTH('b) \<and> bit x n) [0..<LENGTH('b)]) ws)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))

goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ws = rev wl
word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ws = rev wl
word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))

goal (1 subgoal):
 1. word_rcat wl = of_bl (concat (map to_bl wl))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
word_rcat wl = of_bl (concat (map to_bl wl))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (concat (map to_bl wl)) = length wl * size (hd wl)
[PROOF STEP]
by (induct wl) (auto simp: word_size)


[STATEMENT]
lemma nth_rcat_lem:
  "n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow>
    rev (concat (map to_bl wl)) ! n =
    rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))
[PROOF STEP]
apply (induct wl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n < length [] * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl [])) ! n = rev (to_bl (rev [] ! (n div LENGTH('a)))) ! (n mod LENGTH('a))
 2. \<And>a wl. \<lbrakk>n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)); n < length (a # wl) * LENGTH('a)\<rbrakk> \<Longrightarrow> rev (concat (map to_bl (a # wl))) ! n = rev (to_bl (rev (a # wl) ! (n div LENGTH('a)))) ! (n mod LENGTH('a))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a wl. \<lbrakk>n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)); n < length (a # wl) * LENGTH('a)\<rbrakk> \<Longrightarrow> rev (concat (map to_bl (a # wl))) ! n = rev (to_bl (rev (a # wl) ! (n div LENGTH('a)))) ! (n mod LENGTH('a))
[PROOF STEP]
apply (clarsimp simp add : nth_append size_rcat_lem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a wl. \<lbrakk>n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)); n < LENGTH('a) + length wl * LENGTH('a)\<rbrakk> \<Longrightarrow> (n div LENGTH('a) < length wl \<longrightarrow> \<not> n < length wl * LENGTH('a) \<longrightarrow> rev (to_bl a) ! (n - length wl * LENGTH('a)) = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))) \<and> (\<not> n div LENGTH('a) < length wl \<longrightarrow> (n < length wl * LENGTH('a) \<longrightarrow> rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a)) = rev (to_bl ([a] ! (n div LENGTH('a) - length wl))) ! (n mod LENGTH('a))) \<and> (\<not> n < length wl * LENGTH('a) \<longrightarrow> rev (to_bl a) ! (n - length wl * LENGTH('a)) = rev (to_bl ([a] ! (n div LENGTH('a) - length wl))) ! (n mod LENGTH('a))))
[PROOF STEP]
apply (simp flip: mult_Suc minus_div_mult_eq_mod add: less_Suc_eq_le not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a wl. \<lbrakk>n < length wl * LENGTH('a) \<Longrightarrow> rev (concat (map to_bl wl)) ! n = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n - n div LENGTH('a) * LENGTH('a)); n < Suc (length wl) * LENGTH('a)\<rbrakk> \<Longrightarrow> (n div LENGTH('a) < length wl \<longrightarrow> length wl * LENGTH('a) \<le> n \<longrightarrow> rev (to_bl a) ! (n - length wl * LENGTH('a)) = rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n - n div LENGTH('a) * LENGTH('a))) \<and> (length wl \<le> n div LENGTH('a) \<longrightarrow> (n < length wl * LENGTH('a) \<longrightarrow> rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n - n div LENGTH('a) * LENGTH('a)) = rev (to_bl ([a] ! (n div LENGTH('a) - length wl))) ! (n - n div LENGTH('a) * LENGTH('a))) \<and> (length wl * LENGTH('a) \<le> n \<longrightarrow> rev (to_bl a) ! (n - length wl * LENGTH('a)) = rev (to_bl ([a] ! (n div LENGTH('a) - length wl))) ! (n - n div LENGTH('a) * LENGTH('a))))
[PROOF STEP]
apply (metis (no_types, lifting) diff_is_0_eq div_le_mono len_not_eq_0 less_Suc_eq less_mult_imp_div_less nonzero_mult_div_cancel_right not_le nth_Cons_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0"
  for x :: "'a::comm_monoid_add"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (+) x xs = foldr (+) (x # xs) (0::'a)
[PROOF STEP]
by (induct xs arbitrary: x) (auto simp: add.assoc)


[STATEMENT]
lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (word_rotl n w) = rotate n (to_bl w)
[PROOF STEP]
by (simp add: word_rotl_eq to_bl_use_of_bl)


[STATEMENT]
lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (word_rotr n w) = rotater n (to_bl w)
[PROOF STEP]
by (simp add: word_rotr_eq to_bl_use_of_bl)


[STATEMENT]
lemma bl_word_roti_dt':
  "n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow>
    to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = nat (- i mod int (size w)) \<Longrightarrow> to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)
[PROOF STEP]
apply (unfold word_roti_eq_word_rotr_word_rotl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = nat (- i mod int (size w)) \<Longrightarrow> to_bl (if 0 \<le> i then word_rotr (nat i) w else word_rotl (nat (- i)) w) = drop n (to_bl w) @ take n (to_bl w)
[PROOF STEP]
apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = nat (- i mod int LENGTH('a)) \<Longrightarrow> (0 \<le> i \<longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w)) \<and> (\<not> 0 \<le> i \<longrightarrow> drop (nat (- i) mod LENGTH('a)) (to_bl w) @ take (nat (- i) mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = nat (- i mod int LENGTH('a)); 0 \<le> i\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w)
 2. \<lbrakk>n = nat (- i mod int LENGTH('a)); \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> drop (nat (- i) mod LENGTH('a)) (to_bl w) @ take (nat (- i) mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w)
[PROOF STEP]
apply (simp add: zmod_zminus1_eq_if)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = nat (if i mod int LENGTH('a) = 0 then 0 else int LENGTH('a) - i mod int LENGTH('a)); 0 \<le> i\<rbrakk> \<Longrightarrow> (i mod int LENGTH('a) = 0 \<longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = to_bl w) \<and> (i mod int LENGTH('a) \<noteq> 0 \<longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) @ take (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w))
 2. \<lbrakk>n = nat (- i mod int LENGTH('a)); \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> drop (nat (- i) mod LENGTH('a)) (to_bl w) @ take (nat (- i) mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>n = nat (if int LENGTH('a) * q mod int LENGTH('a) = 0 then 0 else int LENGTH('a) - int LENGTH('a) * q mod int LENGTH('a)); 0 \<le> int LENGTH('a) * q; i = int LENGTH('a) * q\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat (int LENGTH('a) * q) mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat (int LENGTH('a) * q) mod LENGTH('a)) (to_bl w) = to_bl w
 2. \<lbrakk>n = nat (if i mod int LENGTH('a) = 0 then 0 else int LENGTH('a) - i mod int LENGTH('a)); 0 \<le> i; i mod int LENGTH('a) \<noteq> 0\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) @ take (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w)
 3. \<lbrakk>n = nat (- i mod int LENGTH('a)); \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> drop (nat (- i) mod LENGTH('a)) (to_bl w) @ take (nat (- i) mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w)
[PROOF STEP]
apply (auto simp add: nat_mult_distrib nat_mod_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = nat (int LENGTH('a) - i mod int LENGTH('a)); 0 \<le> i; i mod int LENGTH('a) \<noteq> 0\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) @ take (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w)
[PROOF STEP]
using nat_0_le nat_minus_as_int zmod_int
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?z \<Longrightarrow> int (nat ?z) = ?z
(-) = (\<lambda>a b. nat (int a - int b))
int (?a mod ?b) = int ?a mod int ?b

goal (1 subgoal):
 1. \<lbrakk>n = nat (int LENGTH('a) - i mod int LENGTH('a)); 0 \<le> i; i mod int LENGTH('a) \<noteq> 0\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) @ take (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w)
[PROOF STEP]
apply presburger
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma max_word_bl: "to_bl (- 1::'a::len word) = replicate LENGTH('a) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (- 1) = replicate LENGTH('a) True
[PROOF STEP]
by (fact to_bl_n1)


[STATEMENT]
lemma to_bl_mask:
  "to_bl (mask n :: 'a::len word) =
  replicate (LENGTH('a) - n) False @
    replicate (min (LENGTH('a)) n) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (mask n) = replicate (LENGTH('a) - n) False @ replicate (min LENGTH('a) n) True
[PROOF STEP]
by (simp add: mask_bl word_rep_drop min_def)


[STATEMENT]
lemma map_replicate_True:
  "n = length xs \<Longrightarrow>
    map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> map2 (\<and>) xs (replicate n True) = xs
[PROOF STEP]
by (induct xs arbitrary: n) auto


[STATEMENT]
lemma map_replicate_False:
  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
    (zip xs (replicate n False)) = replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> map2 (\<and>) xs (replicate n False) = replicate n False
[PROOF STEP]
by (induct xs arbitrary: n) auto


[STATEMENT]
lemma bl_and_mask:
  fixes w :: "'a::len word"
    and n :: nat
  defines "n' \<equiv> LENGTH('a) - n"
  shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
note [simp] = map_replicate_True map_replicate_False
[PROOF STATE]
proof (state)
this:
?n = length ?xs \<Longrightarrow> map2 (\<and>) ?xs (replicate ?n True) = ?xs
?n = length ?xs \<Longrightarrow> map2 (\<and>) ?xs (replicate ?n False) = replicate ?n False

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n))
[PROOF STEP]
by (simp add: bl_word_and)
[PROOF STATE]
proof (state)
this:
to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n))

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n))

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = take n' (to_bl w) @ drop n' (to_bl w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
to_bl w = take n' (to_bl w) @ drop n' (to_bl w)

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
to_bl w = take n' (to_bl w) @ drop n' (to_bl w)

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) =
      replicate n' False @ drop n' (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<and>) (take n' (to_bl w) @ drop n' (to_bl w)) (to_bl (mask n)) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
unfolding to_bl_mask n'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<and>) (take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl w)) (replicate (LENGTH('a) - n) False @ replicate (min LENGTH('a) n) True) = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl w)
[PROOF STEP]
by (subst zip_append) auto
[PROOF STATE]
proof (state)
this:
map2 (\<and>) (take n' (to_bl w) @ drop n' (to_bl w)) (to_bl (mask n)) = replicate n' False @ drop n' (to_bl w)

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)

goal (1 subgoal):
 1. to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drop_rev_takefill:
  "length xs \<le> n \<Longrightarrow>
    drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<le> n \<Longrightarrow> drop (n - length xs) (rev (takefill False n (rev xs))) = xs
[PROOF STEP]
by (simp add: takefill_alt rev_take)


[STATEMENT]
lemma uint_of_bl_is_bl_to_bin_drop:
  "length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> uint (of_bl l :: 'a::len word) = bl_to_bin l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> uint (of_bl l) = bl_to_bin l
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> take_bit LENGTH('a) (bl_to_bin l) = bl_to_bin l
[PROOF STEP]
apply (simp add: take_bit_eq_mod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> bl_to_bin l mod 2 ^ LENGTH('a) = bl_to_bin l
[PROOF STEP]
apply (rule Divides.mod_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> 0 \<le> bl_to_bin l
 2. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> bl_to_bin l < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule bl_to_bin_ge0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> bl_to_bin l < 2 ^ LENGTH('a)
[PROOF STEP]
using bl_to_bin_lt2p_drop
[PROOF STATE]
proof (prove)
using this:
bl_to_bin ?bs < 2 ^ length (dropWhile Not ?bs)

goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> bl_to_bin l < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule order.strict_trans2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> 2 ^ length (dropWhile Not l) \<le> 2 ^ LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_to_bl_or:
  "bin_to_bl n (a OR b) = map2 (\<or>) (bin_to_bl n a) (bin_to_bl n b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (a OR b) = map2 (\<or>) (bin_to_bl n a) (bin_to_bl n b)
[PROOF STEP]
using bl_or_aux_bin[where n=n and v=a and w=b and bs="[]" and cs="[]"]
[PROOF STATE]
proof (prove)
using this:
map2 (\<or>) (bin_to_bl_aux n a []) (bin_to_bl_aux n b []) = bin_to_bl_aux n (a OR b) (map2 (\<or>) [] [])

goal (1 subgoal):
 1. bin_to_bl n (a OR b) = map2 (\<or>) (bin_to_bl n a) (bin_to_bl n b)
[PROOF STEP]
by simp


[STATEMENT]
lemma word_and_1_bl:
  fixes x::"'a::len word"
  shows "(x AND 1) = of_bl [bit x 0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND 1 = of_bl [bit x 0]
[PROOF STEP]
by (simp add: word_and_1)


[STATEMENT]
lemma word_1_and_bl:
  fixes x::"'a::len word"
  shows "(1 AND x) = of_bl [bit x 0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 AND x = of_bl [bit x 0]
[PROOF STEP]
using word_and_1_bl [of x]
[PROOF STATE]
proof (prove)
using this:
x AND 1 = of_bl [bit x 0]

goal (1 subgoal):
 1. 1 AND x = of_bl [bit x 0]
[PROOF STEP]
by (simp add: ac_simps)


[STATEMENT]
lemma of_bl_drop:
  "of_bl (drop n xs) = (of_bl xs AND mask (length xs - n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (drop n xs) = of_bl xs AND mask (length xs - n)
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (of_bl (drop n xs)) na = bit (of_bl xs AND mask (length xs - n)) na
[PROOF STEP]
apply (auto simp: rev_nth bit_simps cong: rev_conj_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma to_bl_1:
  "to_bl (1::'a::len word) = replicate (LENGTH('a) - 1) False @ [True]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl 1 = replicate (LENGTH('a) - 1) False @ [True]
[PROOF STEP]
by (rule nth_equalityI) (auto simp add: to_bl_unfold nth_append rev_nth bit_1_iff not_less not_le)


[STATEMENT]
lemma eq_zero_set_bl:
  "(w = 0) = (True \<notin> set (to_bl w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w = 0) = (True \<notin> set (to_bl w))
[PROOF STEP]
apply (auto simp add: to_bl_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..<LENGTH('a)}. \<not> bit w x \<Longrightarrow> w = 0
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>{0..<LENGTH('a)}. \<not> bit w x; n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit w n = bit 0 n
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma of_drop_to_bl:
  "of_bl (drop n (to_bl x)) = (x AND mask (size x - n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (drop n (to_bl x)) = x AND mask (size x - n)
[PROOF STEP]
by (simp add: of_bl_drop word_size_bl)


[STATEMENT]
lemma unat_of_bl_length:
  "unat (of_bl xs :: 'a::len word) < 2 ^ (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
proof (cases "length xs < LENGTH('a)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
 2. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs < LENGTH('a)

goal (2 subgoals):
 1. length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
 2. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs < LENGTH('a)
[PROOF STEP]
have "(of_bl xs::'a::len word) < 2 ^ length xs"
[PROOF STATE]
proof (prove)
using this:
length xs < LENGTH('a)

goal (1 subgoal):
 1. of_bl xs < 2 ^ length xs
[PROOF STEP]
by (simp add: of_bl_length_less)
[PROOF STATE]
proof (state)
this:
of_bl xs < 2 ^ length xs

goal (2 subgoals):
 1. length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
 2. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
length xs < LENGTH('a)
of_bl xs < 2 ^ length xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs < LENGTH('a)
of_bl xs < 2 ^ length xs

goal (1 subgoal):
 1. unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
by (simp add: word_less_nat_alt unat_of_nat)
[PROOF STATE]
proof (state)
this:
unat (of_bl xs) < 2 ^ length xs

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xs < LENGTH('a)

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
have "unat (of_bl xs::'a::len word) < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (of_bl xs) < 2 ^ LENGTH('a)
[PROOF STEP]
by (simp split: unat_split)
[PROOF STATE]
proof (state)
this:
unat (of_bl xs) < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unat (of_bl xs) < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> length xs < LENGTH('a)
[PROOF STEP]
have "LENGTH('a) \<le> length xs"
[PROOF STATE]
proof (prove)
using this:
\<not> length xs < LENGTH('a)

goal (1 subgoal):
 1. LENGTH('a) \<le> length xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LENGTH('a) \<le> length xs

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
LENGTH('a) \<le> length xs
[PROOF STEP]
have "2 ^ LENGTH('a) \<le> (2::nat) ^ length xs"
[PROOF STATE]
proof (prove)
using this:
LENGTH('a) \<le> length xs

goal (1 subgoal):
 1. 2 ^ LENGTH('a) \<le> 2 ^ length xs
[PROOF STEP]
by (rule power_increasing) simp
[PROOF STATE]
proof (state)
this:
2 ^ LENGTH('a) \<le> 2 ^ length xs

goal (1 subgoal):
 1. \<not> length xs < LENGTH('a) \<Longrightarrow> unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unat (of_bl xs) < 2 ^ length xs

goal (1 subgoal):
 1. unat (of_bl xs) < 2 ^ length xs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
unat (of_bl xs) < 2 ^ length xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma word_lsb_last:
  \<open>lsb w \<longleftrightarrow> last (to_bl w)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsb w = last (to_bl w)
[PROOF STEP]
using nth_to_bl [of \<open>LENGTH('a) - Suc 0\<close> w]
[PROOF STATE]
proof (prove)
using this:
LENGTH('a) - Suc 0 < LENGTH('a) \<Longrightarrow> to_bl w ! (LENGTH('a) - Suc 0) = bit w (LENGTH('a) - Suc (LENGTH('a) - Suc 0))

goal (1 subgoal):
 1. lsb w = last (to_bl w)
[PROOF STEP]
by (simp add: last_conv_nth bit_0 lsb_odd)


[STATEMENT]
lemma is_aligned_to_bl:
  "is_aligned (w :: 'a :: len word) n = (True \<notin> set (drop (size w - n) (to_bl w)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w n = (True \<notin> set (drop (size w - n) (to_bl w)))
[PROOF STEP]
by (simp add: is_aligned_mask eq_zero_set_bl bl_and_mask word_size)


[STATEMENT]
lemma is_aligned_replicate:
  fixes w::"'a::len word"
  assumes aligned: "is_aligned w n"
  and          nv: "n \<le> LENGTH('a)"
  shows   "to_bl w = (take (LENGTH('a) - n) (to_bl w)) @ replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (to_bl w) = length (take (LENGTH('a) - n) (to_bl w) @ replicate n False)
 2. \<And>i. i < length (to_bl w) \<Longrightarrow> to_bl w ! i = (take (LENGTH('a) - n) (to_bl w) @ replicate n False) ! i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_aligned w n
n \<le> LENGTH('a)

goal (2 subgoals):
 1. length (to_bl w) = length (take (LENGTH('a) - n) (to_bl w) @ replicate n False)
 2. \<And>i. i < length (to_bl w) \<Longrightarrow> to_bl w ! i = (take (LENGTH('a) - n) (to_bl w) @ replicate n False) ! i
[PROOF STEP]
apply (simp_all add: nth_append not_less word_size to_bl_nth is_aligned_imp_not_bit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_drop:
  fixes w::"'a::len word"
  assumes "is_aligned w n" "n \<le> LENGTH('a)"
  shows "drop (LENGTH('a) - n) (to_bl w) = replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
have "to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False
[PROOF STEP]
by (rule is_aligned_replicate) fact+
[PROOF STATE]
proof (state)
this:
to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False
[PROOF STEP]
have "drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) \<dots>"
[PROOF STATE]
proof (prove)
using this:
to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False)

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False)

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
have "\<dots> = replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False) = replicate n False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop (LENGTH('a) - n) (take (LENGTH('a) - n) (to_bl w) @ replicate n False) = replicate n False

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
drop (LENGTH('a) - n) (to_bl w) = replicate n False

goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
drop (LENGTH('a) - n) (to_bl w) = replicate n False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_is_drop_replicate:
  fixes x::"'a::len word"
  assumes lt: "x < 2 ^ n"
  shows   "to_bl x = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl x = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl x)
[PROOF STEP]
by (metis assms bl_and_mask' less_mask_eq)