diff --git a/thys/Word_Lib/Generic_set_bit.thy b/thys/Word_Lib/Generic_set_bit.thy
--- a/thys/Word_Lib/Generic_set_bit.thy
+++ b/thys/Word_Lib/Generic_set_bit.thy
@@ -1,175 +1,175 @@
 (*  Author:     Jeremy Dawson, NICTA
 *)
 
 section \<open>Operation variant for setting and unsetting bits\<close>
 
 theory Generic_set_bit
   imports "HOL-Library.Word" Most_significant_bit
 begin
 
 class set_bit = ring_bit_operations +
   fixes set_bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a\<close>
   assumes set_bit_eq: \<open>set_bit a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\<close>
 
 instantiation int :: set_bit
 begin
 
 definition set_bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> int\<close>
   where \<open>set_bit i n b = bin_sc n b i\<close>
 
 instance
   by standard (simp add: set_bit_int_def bin_sc_eq)
 
 end
 
 lemma int_set_bit_0 [simp]: fixes x :: int shows
   "set_bit x 0 b = of_bool b + 2 * (x div 2)"
   by (auto simp add: set_bit_int_def intro: bin_rl_eqI)
 
 lemma int_set_bit_Suc: fixes x :: int shows
   "set_bit x (Suc n) b = of_bool (odd x) + 2 * set_bit (x div 2) n b"
   by (auto simp add: set_bit_int_def intro: bin_rl_eqI)
 
 lemma bin_last_set_bit:
   "bin_last (set_bit x n b) = (if n > 0 then bin_last x else b)"
   by (cases n) (simp_all add: int_set_bit_Suc)
 
 lemma bin_rest_set_bit: 
   "bin_rest (set_bit x n b) = (if n > 0 then set_bit (x div 2) (n - 1) b else x div 2)"
   by (cases n) (simp_all add: int_set_bit_Suc)
 
 lemma int_set_bit_numeral: fixes x :: int shows
   "set_bit x (numeral w) b = of_bool (odd x) + 2 * set_bit (x div 2) (pred_numeral w) b"
   by (simp add: set_bit_int_def)
 
 lemmas int_set_bit_numerals [simp] =
   int_set_bit_numeral[where x="numeral w'"] 
   int_set_bit_numeral[where x="- numeral w'"]
   int_set_bit_numeral[where x="Numeral1"]
   int_set_bit_numeral[where x="1"]
   int_set_bit_numeral[where x="0"]
   int_set_bit_Suc[where x="numeral w'"]
   int_set_bit_Suc[where x="- numeral w'"]
   int_set_bit_Suc[where x="Numeral1"]
   int_set_bit_Suc[where x="1"]
   int_set_bit_Suc[where x="0"]
   for w'
 
 lemma msb_set_bit [simp]: "msb (set_bit (x :: int) n b) \<longleftrightarrow> msb x"
 by(simp add: msb_conv_bin_sign set_bit_int_def)
 
 instantiation word :: (len) set_bit
 begin
 
 definition set_bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a word\<close>
   where word_set_bit_def: \<open>set_bit a n x = word_of_int (bin_sc n x (uint a))\<close>
 
 instance
   apply standard
   apply (simp add: word_set_bit_def bin_sc_eq Bit_Operations.set_bit_def unset_bit_def)
   apply transfer
   apply simp
   done
 
 end
 
 lemma set_bit_unfold:
   \<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close>
   for w :: \<open>'a::len word\<close>
   by (simp add: set_bit_eq)
 
-lemma bit_set_bit_word_iff:
+lemma bit_set_bit_word_iff [bit_simps]:
   \<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close>
   for w :: \<open>'a::len word\<close>
   by (auto simp add: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff exp_eq_zero_iff not_le bit_imp_le_length)
 
 lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
   for w :: "'a::len word"
   by (auto simp: word_test_bit_def word_set_bit_def)
 
 lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
   for w :: "'a::len word"
   by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)
 
 lemma test_bit_set_gen:
   "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
   for w :: "'a::len word"
   apply (unfold word_size word_test_bit_def word_set_bit_def)
   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
   apply (auto elim!: test_bit_size [unfolded word_size]
       simp add: word_test_bit_def [symmetric])
   done
 
 lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
   for w :: "'a::len word"
   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
 
 lemma word_set_set_diff:
   fixes w :: "'a::len word"
   assumes "m \<noteq> n"
   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
   by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
 
 lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
   unfolding word_set_bit_def
   by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
 
 lemma word_set_numeral [simp]:
   "set_bit (numeral bin::'a::len word) n b =
     word_of_int (bin_sc n b (numeral bin))"
   unfolding word_numeral_alt by (rule set_bit_word_of_int)
 
 lemma word_set_neg_numeral [simp]:
   "set_bit (- numeral bin::'a::len word) n b =
     word_of_int (bin_sc n b (- numeral bin))"
   unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
 
 lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
   unfolding word_0_wi by (rule set_bit_word_of_int)
 
 lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
   unfolding word_1_wi by (rule set_bit_word_of_int)
 
 lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
   for w :: "'a::len word"
   apply (rule iffI)
    apply (rule disjCI)
    apply (drule word_eqD)
    apply (erule sym [THEN trans])
    apply (simp add: test_bit_set)
   apply (erule disjE)
    apply clarsimp
   apply (rule word_eqI)
   apply (clarsimp simp add : test_bit_set_gen)
   apply (drule test_bit_size)
   apply force
   done
 
 lemma word_clr_le: "w \<ge> set_bit w n False"
   for w :: "'a::len word"
   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
   apply (rule order_trans)
    apply (rule bintr_bin_clr_le)
   apply simp
   done
 
 lemma word_set_ge: "w \<le> set_bit w n True"
   for w :: "'a::len word"
   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
   apply (rule order_trans [OF _ bintr_bin_set_ge])
   apply simp
   done
 
 lemma set_bit_beyond:
   "size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len word"
   by (auto intro: word_eqI simp add: test_bit_set_gen word_size)
 
 lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n"
   apply (rule word_eqI)
   apply (auto simp add: test_bit_set_gen nth_shiftl word_size
               simp del: word_set_bit_0 shiftl_1)
   done
 
 lemmas one_bit_pow = trans [OF one_bit_shiftl shiftl_1]
 
 end
diff --git a/thys/Word_Lib/Reversed_Bit_Lists.thy b/thys/Word_Lib/Reversed_Bit_Lists.thy
--- a/thys/Word_Lib/Reversed_Bit_Lists.thy
+++ b/thys/Word_Lib/Reversed_Bit_Lists.thy
@@ -1,1869 +1,1869 @@
 (*  Author:     Jeremy Dawson, NICTA
 *)
 
 section \<open>Bit values as reversed lists of bools\<close>
 
 theory Reversed_Bit_Lists
   imports "HOL-Library.Word" Typedef_Morphisms
 begin
 
 context comm_semiring_1
 begin
 
 lemma horner_sum_append:
   \<open>horner_sum f a (xs @ ys) = horner_sum f a xs + a ^ length xs * horner_sum f a ys\<close>
   using sum.atLeastLessThan_shift_bounds [of _ 0 \<open>length xs\<close> \<open>length ys\<close>]
     atLeastLessThan_add_Un [of 0 \<open>length xs\<close> \<open>length ys\<close>]
   by (simp add: horner_sum_eq_sum sum_distrib_left sum.union_disjoint ac_simps nth_append power_add)
 
 end
 
 lemma horner_sum_of_bool_2_concat:
   \<open>horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws\<close>
   for ws :: \<open>'a::len word list\<close>
 proof (induction ws)
   case Nil
   then show ?case
     by simp
 next
   case (Cons w ws)
   moreover have \<open>horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w\<close>
   proof transfer
     fix k :: int
     have \<open>map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]
       = map (bit k) [0..<LENGTH('a)]\<close>
       by simp
     then show \<open>horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)])
       = take_bit LENGTH('a) k\<close>
       by (simp only: horner_sum_bit_eq_take_bit)
   qed
   ultimately show ?case
     by (simp add: horner_sum_append)
 qed
 
 
 subsection \<open>Implicit augmentation of list prefixes\<close>
 
 primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
     Z: "takefill fill 0 xs = []"
   | Suc: "takefill fill (Suc n) xs =
       (case xs of
         [] \<Rightarrow> fill # takefill fill n xs
       | y # ys \<Rightarrow> y # takefill fill n ys)"
 
 lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
   apply (induct n arbitrary: m l)
    apply clarsimp
   apply clarsimp
   apply (case_tac m)
    apply (simp split: list.split)
   apply (simp split: list.split)
   done
 
 lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
   by (induct n arbitrary: l) (auto split: list.split)
 
 lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
   by (simp add: takefill_alt replicate_add [symmetric])
 
 lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
   by (induct m arbitrary: l n) (auto split: list.split)
 
 lemma length_takefill [simp]: "length (takefill fill n l) = n"
   by (simp add: takefill_alt)
 
 lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
   by (induct k arbitrary: w n) (auto split: list.split)
 
 lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
   by (induct k arbitrary: w) (auto split: list.split)
 
 lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
   by (auto simp: le_iff_add takefill_le')
 
 lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
   by (auto simp: le_iff_add take_takefill')
 
 lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
   by (induct xs) auto
 
 lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
   by (induct xs arbitrary: l) auto
 
 lemmas takefill_same [simp] = takefill_same' [OF refl]
 
 lemma tf_rev:
   "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
     rev (takefill y m (rev (takefill x k (rev bl))))"
   apply (rule nth_equalityI)
    apply (auto simp add: nth_takefill rev_nth)
   apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
   apply arith
   done
 
 lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
   by auto
 
 lemmas takefill_Suc_cases =
   list.cases [THEN takefill.Suc [THEN trans]]
 
 lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
 lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
 
 lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
   takefill_minus [symmetric, THEN trans]]
 
 lemma takefill_numeral_Nil [simp]:
   "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
   by (simp add: numeral_eq_Suc)
 
 lemma takefill_numeral_Cons [simp]:
   "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
   by (simp add: numeral_eq_Suc)
 
 
 subsection \<open>Range projection\<close>
 
 definition bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list"
   where "bl_of_nth n f = map f (rev [0..<n])"
 
 lemma bl_of_nth_simps [simp, code]:
   "bl_of_nth 0 f = []"
   "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
   by (simp_all add: bl_of_nth_def)
 
 lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
   by (simp add: bl_of_nth_def)
 
 lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
   by (simp add: bl_of_nth_def rev_map)
 
 lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
   by (simp add: bl_of_nth_def)
 
 lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
   apply (induct n arbitrary: xs)
    apply clarsimp
   apply clarsimp
   apply (rule trans [OF _ hd_Cons_tl])
    apply (frule Suc_le_lessD)
    apply (simp add: rev_nth trans [OF drop_Suc drop_tl, symmetric])
    apply (subst hd_drop_conv_nth)
     apply force
    apply simp_all
   apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
   apply simp
   done
 
 lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
   by (simp add: bl_of_nth_nth_le)
 
 
 subsection \<open>More\<close>
 
 definition rotater1 :: "'a list \<Rightarrow> 'a list"
   where "rotater1 ys =
     (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)"
 
 definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   where "rotater n = rotater1 ^^ n"
 
 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
 
 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
   by (cases l) (auto simp: rotater1_def)
 
 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
   apply (unfold rotater1_def)
   apply (cases "l")
    apply (case_tac [2] "list")
     apply auto
   done
 
 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
   by (cases l) (auto simp: rotater1_def)
 
 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
   by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
 
 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
   by (induct n) (auto simp: rotater_def intro: rotater1_rev')
 
 lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
   using rotater_rev' [where xs = "rev ys"] by simp
 
 lemma rotater_drop_take:
   "rotater n xs =
     drop (length xs - n mod length xs) xs @
     take (length xs - n mod length xs) xs"
   by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
 
 lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
   unfolding rotater_def by auto
 
 lemma nth_rotater:
   \<open>rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)\<close> if \<open>n < length xs\<close>
   using that by (simp add: rotater_drop_take nth_append not_less less_diff_conv ac_simps le_mod_geq)
 
 lemma nth_rotater1:
   \<open>rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)\<close> if \<open>n < length xs\<close>
   using that nth_rotater [of n xs 1] by simp
 
 lemma rotate_inv_plus [rule_format]:
   "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
     rotate k (rotater n xs) = rotate m xs \<and>
     rotater n (rotate k xs) = rotate m xs \<and>
     rotate n (rotater k xs) = rotater m xs"
   by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
 
 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
 
 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
 
 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
 lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
 
 lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
   by auto
 
 lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
   by auto
 
 lemma length_rotater [simp]: "length (rotater n xs) = length xs"
   by (simp add : rotater_rev)
 
 lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
   apply (rule box_equals)
     defer
     apply (rule rotate_conv_mod [symmetric])+
   apply simp
   done
 
 lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
   by simp
 
 lemmas rotate_eqs =
   trans [OF rotate0 [THEN fun_cong] id_apply]
   rotate_rotate [symmetric]
   rotate_id
   rotate_conv_mod
   rotate_eq_mod
 
 lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
   simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
 lemmas rotater_eqs = rrs1 [simplified length_rotater]
 lemmas rotater_0 = rotater_eqs (1)
 lemmas rotater_add = rotater_eqs (2)
 
 lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   by (induct xs) auto
 
 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
   by (cases xs) (auto simp: rotater1_def last_map butlast_map)
 
 lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
   by (induct n) (auto simp: rotater_def rotater1_map)
 
 lemma but_last_zip [rule_format] :
   "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
     last (zip xs ys) = (last xs, last ys) \<and>
     butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
   apply (induct xs)
    apply auto
      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
   done
 
 lemma but_last_map2 [rule_format] :
   "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
     last (map2 f xs ys) = f (last xs) (last ys) \<and>
     butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
   apply (induct xs)
    apply auto
      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
   done
 
 lemma rotater1_zip:
   "length xs = length ys \<Longrightarrow>
     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
   apply (unfold rotater1_def)
   apply (cases xs)
    apply auto
    apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
   done
 
 lemma rotater1_map2:
   "length xs = length ys \<Longrightarrow>
     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
   by (simp add: rotater1_map rotater1_zip)
 
 lemmas lrth =
   box_equals [OF asm_rl length_rotater [symmetric]
                  length_rotater [symmetric],
               THEN rotater1_map2]
 
 lemma rotater_map2:
   "length xs = length ys \<Longrightarrow>
     rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
   by (induct n) (auto intro!: lrth)
 
 lemma rotate1_map2:
   "length xs = length ys \<Longrightarrow>
     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
   by (cases xs; cases ys) auto
 
 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
   length_rotate [symmetric], THEN rotate1_map2]
 
 lemma rotate_map2:
   "length xs = length ys \<Longrightarrow>
     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
   by (induct n) (auto intro!: lth)
 
 
 subsection \<open>Explicit bit representation of \<^typ>\<open>int\<close>\<close>
 
 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
   where
     Nil: "bl_to_bin_aux [] w = w"
   | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (of_bool b + 2 * w)"
 
 definition bl_to_bin :: "bool list \<Rightarrow> int"
   where "bl_to_bin bs = bl_to_bin_aux bs 0"
 
 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
   where
     Z: "bin_to_bl_aux 0 w bl = bl"
   | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
 
 definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
   where "bin_to_bl n w = bin_to_bl_aux n w []"
 
 lemma bin_to_bl_aux_zero_minus_simp [simp]:
   "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_minus1_minus_simp [simp]:
   "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_one_minus_simp [simp]:
   "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
   "0 < n \<Longrightarrow>
     bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
   by (cases n) simp_all
 
 lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
   "0 < n \<Longrightarrow>
     bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
   by (cases n) simp_all
 
 lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
   by (induct bs arbitrary: w) auto
 
 lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
   by (induct n arbitrary: w bs) auto
 
 lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
   unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
 
 lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
   by (simp add: bin_to_bl_def bin_to_bl_aux_append)
 
 lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
   by (auto simp: bin_to_bl_def)
 
 lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
   by (induct n arbitrary: w bs) auto
 
 lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
   by (simp add: bin_to_bl_def size_bin_to_bl_aux)
 
 lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
   apply (induct bs arbitrary: w n)
    apply auto
     apply (simp_all only: add_Suc [symmetric])
     apply (auto simp add: bin_to_bl_def)
   done
 
 lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
   unfolding bl_to_bin_def
   apply (rule box_equals)
     apply (rule bl_bin_bl')
    prefer 2
    apply (rule bin_to_bl_aux.Z)
   apply simp
   done
 
 lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
   apply (rule_tac box_equals)
     defer
     apply (rule bl_bin_bl)
    apply (rule bl_bin_bl)
   apply simp
   done
 
 lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
   by (auto simp: bl_to_bin_def)
 
 lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
   by (auto simp: bl_to_bin_def)
 
 lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
 lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
   by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
 
 lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
 lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
   by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
 
 
 subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
 
 lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
   by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)
 
 lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
   by (auto simp: bin_to_bl_def bin_bl_bin')
 
 lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
   by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
 
 lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
   by (auto intro: bl_to_bin_inj)
 
 lemma bin_to_bl_aux_bintr:
   "bin_to_bl_aux n (bintrunc m bin) bl =
     replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
   apply (induct n arbitrary: m bin bl)
    apply clarsimp
   apply clarsimp
   apply (case_tac "m")
    apply (clarsimp simp: bin_to_bl_zero_aux)
    apply (erule thin_rl)
    apply (induct_tac n)
     apply (auto simp add: take_bit_Suc)
   done
 
 lemma bin_to_bl_bintr:
   "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
   unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
 
 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
   by (induct n) auto
 
 lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
   by (fact size_bin_to_bl_aux)
 
 lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
   by (fact size_bin_to_bl) (* FIXME: duplicate *)
 
 lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
   by (induction bs arbitrary: w) (simp_all add: bin_sign_def)
 
 lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
   by (simp add: bl_to_bin_def sign_bl_bin')
 
 lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
   by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
 
 lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
 
 lemma bin_nth_of_bl_aux:
   "bin_nth (bl_to_bin_aux bl w) n =
     (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
   apply (induction bl arbitrary: w)
    apply simp_all
   apply safe
                       apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
   done
 
 lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
   by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
 
 lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
   apply (induct n arbitrary: m w)
    apply clarsimp
    apply (case_tac m, clarsimp)
    apply (clarsimp simp: bin_to_bl_def)
    apply (simp add: bin_to_bl_aux_alt)
   apply (case_tac m, clarsimp)
   apply (clarsimp simp: bin_to_bl_def)
   apply (simp add: bin_to_bl_aux_alt bit_Suc)
   done
 
 lemma nth_bin_to_bl_aux:
   "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
     (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
   apply (induction bl arbitrary: w)
    apply simp_all
    apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def)
    apply (metis One_nat_def Suc_pred add_diff_cancel_left'
      add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
      diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
      less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
   done
 
 lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
   by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
 
 lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
   apply (rule nth_equalityI)
    apply simp
   apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl)
   done
 
 lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
   by (simp add: takefill_bintrunc)
 
 lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
 proof (induction bs arbitrary: w)
   case Nil
   then show ?case
     by simp
 next
   case (Cons b bs)
   from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
   show ?case
     apply (auto simp add: algebra_simps)
     apply (subst mult_2 [of \<open>2 ^ length bs\<close>])
     apply (simp only: add.assoc)
     apply (rule pos_add_strict)
      apply simp_all
     done
 qed
 
 lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
 proof (induct bs)
   case Nil
   then show ?case by simp
 next
   case (Cons b bs)
   with bl_to_bin_lt2p_aux[where w=1] show ?case
     by (simp add: bl_to_bin_def)
 qed
 
 lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
   by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
 
 lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
 proof (induction bs arbitrary: w)
   case Nil
   then show ?case
     by simp
 next
   case (Cons b bs)
   from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
   show ?case
     apply (auto simp add: algebra_simps)
     apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>])
     apply (rule add_increasing)
     apply simp_all
     done
 qed
 
 lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
   apply (unfold bl_to_bin_def)
   apply (rule xtrans(4))
    apply (rule bl_to_bin_ge2p_aux)
   apply simp
   done
 
 lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
   apply (unfold bin_to_bl_def)
   apply (cases n, clarsimp)
   apply clarsimp
   apply (auto simp add: bin_to_bl_aux_alt)
   done
 
 lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
   using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
 
 lemma butlast_rest_bl2bin_aux:
   "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
   by (induct bl arbitrary: w) auto
 
 lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
   by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
 
 lemma trunc_bl2bin_aux:
   "bintrunc m (bl_to_bin_aux bl w) =
     bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
 proof (induct bl arbitrary: w)
   case Nil
   show ?case by simp
 next
   case (Cons b bl)
   show ?case
   proof (cases "m - length bl")
     case 0
     then have "Suc (length bl) - m = Suc (length bl - m)" by simp
     with Cons show ?thesis by simp
   next
     case (Suc n)
     then have "m - Suc (length bl) = n" by simp
     with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps)
   qed
 qed
 
 lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
   by (simp add: bl_to_bin_def trunc_bl2bin_aux)
 
 lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
   by (simp add: trunc_bl2bin)
 
 lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
   apply (rule trans)
    prefer 2
    apply (rule trunc_bl2bin [symmetric])
   apply (cases "k \<le> length bl")
    apply auto
   done
 
 lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
   apply (rule nth_equalityI)
    apply simp
   apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
   done
 
 lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
   by (induct xs arbitrary: w) auto
 
 lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
   unfolding bl_to_bin_def by (erule last_bin_last')
 
 lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
   by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
 
 lemma drop_bin2bl_aux:
   "drop m (bin_to_bl_aux n bin bs) =
     bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
   apply (induction n arbitrary: m bin bs)
    apply auto
   apply (case_tac "m \<le> n")
    apply (auto simp add: not_le Suc_diff_le)
   apply (case_tac "m - n")
    apply auto
   apply (use Suc_diff_Suc in fastforce)
   done
 
 lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
   by (simp add: bin_to_bl_def drop_bin2bl_aux)
 
 lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
   apply (induct m arbitrary: w bs)
    apply clarsimp
   apply clarsimp
   apply (simp add: bin_to_bl_aux_alt)
   apply (simp add: bin_to_bl_def)
   apply (simp add: bin_to_bl_aux_alt)
   done
 
 lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
   by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
 
 lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
   apply (induct n arbitrary: b c)
    apply clarsimp
   apply (clarsimp simp: Let_def split: prod.split_asm)
   apply (simp add: bin_to_bl_def)
   apply (simp add: take_bin2bl_lem drop_bit_Suc)
   done
 
 lemma bin_to_bl_drop_bit:
   "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)"
   using bin_split_take by simp
 
 lemma bin_split_take1:
   "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
   using bin_split_take by simp
 
 lemma bl_bin_bl_rep_drop:
   "bin_to_bl n (bl_to_bin bl) =
     replicate (n - length bl) False @ drop (length bl - n) bl"
   by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)
 
 lemma bl_to_bin_aux_cat:
   "bl_to_bin_aux bs (bin_cat w nv v) =
     bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
   by (rule bit_eqI)
     (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
 
 lemma bin_to_bl_aux_cat:
   "bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
     bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
   by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
 
 lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
   using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
   by (simp add: bl_to_bin_def [symmetric])
 
 lemma bin_to_bl_cat:
   "bin_to_bl (nv + nw) (bin_cat v nw w) =
     bin_to_bl_aux nv v (bin_to_bl nw w)"
   by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
 
 lemmas bl_to_bin_aux_app_cat =
   trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
 
 lemmas bin_to_bl_aux_cat_app =
   trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
 
 lemma bl_to_bin_app_cat:
   "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
   by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
 
 lemma bin_to_bl_cat_app:
   "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
   by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
 
 text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
 lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
   by (simp add: bl_to_bin_app_cat)
 
 lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
   apply (unfold bl_to_bin_def)
   apply (induct n)
    apply simp
   apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
   apply simp
   done
 
 lemma bin_exhaust:
   "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int
   apply (cases \<open>even bin\<close>)
    apply (auto elim!: evenE oddE)
    apply fastforce
   apply fastforce
   done
 
 primrec rbl_succ :: "bool list \<Rightarrow> bool list"
   where
     Nil: "rbl_succ Nil = Nil"
   | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
 
 primrec rbl_pred :: "bool list \<Rightarrow> bool list"
   where
     Nil: "rbl_pred Nil = Nil"
   | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
 
 primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
     Nil: "rbl_add Nil x = Nil"
   | Cons: "rbl_add (y # ys) x =
       (let ws = rbl_add ys (tl x)
        in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
 
 primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   where \<comment> \<open>result is length of first arg, second arg may be longer\<close>
     Nil: "rbl_mult Nil x = Nil"
   | Cons: "rbl_mult (y # ys) x =
       (let ws = False # rbl_mult ys x
        in if y then rbl_add ws x else ws)"
 
 lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
   by (induct bl) auto
 
 lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
   by (induct bl) auto
 
 lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
   by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
 
 lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
   by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
 
 lemmas rbl_sizes [simp] =
   size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
 
 lemmas rbl_Nils =
   rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
 
 lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
   apply (induct bla arbitrary: blb)
    apply simp
   apply clarsimp
   apply (case_tac blb, clarsimp)
   apply (clarsimp simp: Let_def)
   done
 
 lemma rbl_add_take2:
   "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
   apply (induct bla arbitrary: blb)
    apply simp
   apply clarsimp
   apply (case_tac blb, clarsimp)
   apply (clarsimp simp: Let_def)
   done
 
 lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
   apply (induct bla arbitrary: blb)
    apply simp
   apply clarsimp
   apply (case_tac blb, clarsimp)
   apply (clarsimp simp: Let_def rbl_add_app2)
   done
 
 lemma rbl_mult_take2:
   "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
   apply (rule trans)
    apply (rule rbl_mult_app2 [symmetric])
    apply simp
   apply (rule_tac f = "rbl_mult bla" in arg_cong)
   apply (rule append_take_drop_id)
   done
 
 lemma rbl_add_split:
   "P (rbl_add (y # ys) (x # xs)) =
     (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
       (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
       (\<not> y \<longrightarrow> P (x # ws)))"
   by (cases y) (auto simp: Let_def)
 
 lemma rbl_mult_split:
   "P (rbl_mult (y # ys) xs) =
     (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
       (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
   by (auto simp: Let_def)
 
 lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
 proof (unfold bin_to_bl_def, induction n arbitrary: bin)
   case 0
   then show ?case
     by simp
 next
   case (Suc n)
   obtain b k where \<open>bin = of_bool b + 2 * k\<close>
     using bin_exhaust by blast
   moreover have \<open>(2 * k - 1) div 2 = k - 1\<close>
     using even_succ_div_2 [of \<open>2 * (k - 1)\<close>] 
     by simp
   ultimately show ?case
     using Suc [of \<open>bin div 2\<close>]
     by simp (simp add: bin_to_bl_aux_alt)
 qed
 
 lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
   apply (unfold bin_to_bl_def)
   apply (induction n arbitrary: bin)
    apply simp_all
   apply (case_tac bin rule: bin_exhaust)
   apply simp
   apply (simp add: bin_to_bl_aux_alt ac_simps)
   done
 
 lemma rbl_add:
   "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
     rev (bin_to_bl n (bina + binb))"
   apply (unfold bin_to_bl_def)
   apply (induct n)
    apply simp
   apply clarsimp
   apply (case_tac bina rule: bin_exhaust)
   apply (case_tac binb rule: bin_exhaust)
   apply (case_tac b)
    apply (case_tac [!] "ba")
      apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
   done
 
 lemma rbl_add_long:
   "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
     rev (bin_to_bl n (bina + binb))"
   apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
    apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
    apply (rule rev_swap [THEN iffD1])
    apply (simp add: rev_take drop_bin2bl)
   apply simp
   done
 
 lemma rbl_mult_gt1:
   "m \<ge> length bl \<Longrightarrow>
     rbl_mult bl (rev (bin_to_bl m binb)) =
     rbl_mult bl (rev (bin_to_bl (length bl) binb))"
   apply (rule trans)
    apply (rule rbl_mult_take2 [symmetric])
    apply simp_all
   apply (rule_tac f = "rbl_mult bl" in arg_cong)
   apply (rule rev_swap [THEN iffD1])
   apply (simp add: rev_take drop_bin2bl)
   done
 
 lemma rbl_mult_gt:
   "m > n \<Longrightarrow>
     rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
     rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
   by (auto intro: trans [OF rbl_mult_gt1])
 
 lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
 
 lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))"
   by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
 
 lemma rbl_mult:
   "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
     rev (bin_to_bl n (bina * binb))"
   apply (induct n arbitrary: bina binb)
    apply simp_all
   apply (unfold bin_to_bl_def)
   apply clarsimp
   apply (case_tac bina rule: bin_exhaust)
   apply (case_tac binb rule: bin_exhaust)
   apply simp
   apply (simp add: bin_to_bl_aux_alt)
   apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
   done
 
 lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
   by (induct xs) auto
 
 lemma bin_cat_foldl_lem:
   "foldl (\<lambda>u. bin_cat u n) x xs =
     bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
   apply (induct xs arbitrary: x)
    apply simp
   apply (simp (no_asm))
   apply (frule asm_rl)
   apply (drule meta_spec)
   apply (erule trans)
   apply (drule_tac x = "bin_cat y n a" in meta_spec)
   apply (simp add: bin_cat_assoc_sym min.absorb2)
   done
 
 lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
   apply (unfold bin_rcat_eq_foldl)
   apply (rule sym)
   apply (induct wl)
    apply (auto simp add: bl_to_bin_append)
   apply (simp add: bl_to_bin_aux_alt sclem)
   apply (simp add: bin_cat_foldl_lem [symmetric])
   done
 
 lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
 by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])
 
 lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)"
 by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)
 
 lemma bl_xor_aux_bin:
   "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
     bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
   apply (induction n arbitrary: v w bs cs)
    apply auto
   apply (case_tac v rule: bin_exhaust)
   apply (case_tac w rule: bin_exhaust)
   apply clarsimp
   done
 
 lemma bl_or_aux_bin:
   "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
     bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
   by (induct n arbitrary: v w bs cs) simp_all
 
 lemma bl_and_aux_bin:
   "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
     bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
   by (induction n arbitrary: v w bs cs) simp_all
 
 lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
   by (induct n arbitrary: w cs) auto
 
 lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
   by (simp add: bin_to_bl_def bl_not_aux_bin)
 
 lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
   by (simp add: bin_to_bl_def bl_and_aux_bin)
 
 lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
   by (simp add: bin_to_bl_def bl_or_aux_bin)
 
 lemma bl_xor_bin: "map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
   using bl_xor_aux_bin by (simp add: bin_to_bl_def)
 
 
 subsection \<open>Type \<^typ>\<open>'a word\<close>\<close>
 
 lift_definition of_bl :: \<open>bool list \<Rightarrow> 'a::len word\<close>
   is bl_to_bin .
 
 lift_definition to_bl :: \<open>'a::len word \<Rightarrow> bool list\<close>
   is \<open>bin_to_bl LENGTH('a)\<close>
   by (simp add: bl_to_bin_inj)
 
 lemma to_bl_eq:
   \<open>to_bl w = bin_to_bl (LENGTH('a)) (uint w)\<close>
   for w :: \<open>'a::len word\<close>
   by transfer simp
 
-lemma bit_of_bl_iff:
+lemma bit_of_bl_iff [bit_simps]:
   \<open>bit (of_bl bs :: 'a word) n \<longleftrightarrow> rev bs ! n \<and> n < LENGTH('a::len) \<and> n < length bs\<close>
   by transfer (simp add: bin_nth_of_bl ac_simps)
 
 lemma rev_to_bl_eq:
   \<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close>
   for w :: \<open>'a::len word\<close>
   apply (rule nth_equalityI)
    apply (simp add: to_bl.rep_eq)
   apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq)
   done
 
 lemma to_bl_eq_rev:
   \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a)])\<close>
   for w :: \<open>'a::len word\<close>
   using rev_to_bl_eq [of w]
   apply (subst rev_is_rev_conv [symmetric])
   apply (simp add: rev_map)
   done
 
 lemma of_bl_rev_eq:
   \<open>of_bl (rev bs) = horner_sum of_bool 2 bs\<close>
   apply (rule bit_word_eqI)
   apply (simp add: bit_of_bl_iff)
   apply transfer
   apply (simp add: bit_horner_sum_bit_iff ac_simps)
   done
 
 lemma of_bl_eq:
   \<open>of_bl bs = horner_sum of_bool 2 (rev bs)\<close>
   using of_bl_rev_eq [of \<open>rev bs\<close>] by simp
 
 lemma bshiftr1_eq:
   \<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close>
   apply transfer
   apply auto
    apply (subst bl_to_bin_app_cat [of \<open>[True]\<close>, simplified])
    apply simp
    apply (metis One_nat_def add.commute bin_bl_bin bin_last_bl_to_bin bin_rest_bl_to_bin butlast_bin_rest concat_bit_eq last.simps list.distinct(1) list.size(3) list.size(4) odd_iff_mod_2_eq_one plus_1_eq_Suc power_Suc0_right push_bit_of_1 size_bin_to_bl take_bit_eq_mod trunc_bl2bin_len)
   apply (simp add: butlast_rest_bl2bin)
   done
 
 lemma length_to_bl_eq:
   \<open>length (to_bl w) = LENGTH('a)\<close>
   for w :: \<open>'a::len word\<close>
   by transfer simp
 
 lemma word_rotr_eq:
   \<open>word_rotr n w = of_bl (rotater n (to_bl w))\<close>
   apply (rule bit_word_eqI)
   subgoal for n
     apply (cases \<open>n < LENGTH('a)\<close>)
      apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff rotater_rev length_to_bl_eq nth_rotate rev_to_bl_eq ac_simps)
     done
   done
 
 lemma word_rotl_eq:
   \<open>word_rotl n w = of_bl (rotate n (to_bl w))\<close>
 proof -
   have \<open>rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))\<close>
     by (simp add: rotater_rev')
   then show ?thesis
     apply (simp add: word_rotl_eq_word_rotr bit_of_bl_iff length_to_bl_eq rev_to_bl_eq)
     apply (rule bit_word_eqI)
     subgoal for n
       apply (cases \<open>n < LENGTH('a)\<close>)
        apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff nth_rotater)
       done
     done
 qed
 
 lemma to_bl_def': "(to_bl :: 'a::len word \<Rightarrow> bool list) = bin_to_bl (LENGTH('a)) \<circ> uint"
   by transfer (simp add: fun_eq_iff)
 
 \<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close>
 lemma td_bl:
   "type_definition
     (to_bl :: 'a::len word \<Rightarrow> bool list)
     of_bl
     {bl. length bl = LENGTH('a)}"
   apply (standard; transfer)
   apply (auto dest: sym)
   done
 
 interpretation word_bl:
   type_definition
     "to_bl :: 'a::len word \<Rightarrow> bool list"
     of_bl
     "{bl. length bl = LENGTH('a::len)}"
   by (fact td_bl)
 
 lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
 
 lemma word_size_bl: "size w = size (to_bl w)"
   by (auto simp: word_size)
 
 lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)"
   by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
 
 lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)"
   for x :: "'a::len word"
   unfolding word_bl_Rep' by (rule len_gt_0)
 
 lemma bl_not_Nil [iff]: "to_bl x \<noteq> []"
   for x :: "'a::len word"
   by (fact length_bl_gt_0 [unfolded length_greater_0_conv])
 
 lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0"
   for x :: "'a::len word"
   by (fact length_bl_gt_0 [THEN gr_implies_not0])
 
 lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
   apply transfer
   apply (auto simp add: bin_sign_def)
   using bin_sign_lem bl_sbin_sign apply fastforce
   using bin_sign_lem bl_sbin_sign apply force
   done
 
 lemma of_bl_drop':
   "lend = length bl - LENGTH('a::len) \<Longrightarrow>
     of_bl (drop lend bl) = (of_bl bl :: 'a word)"
   by transfer (simp flip: trunc_bl2bin)
 
 lemma test_bit_of_bl:
   "(of_bl bl::'a::len word) !! n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)"
   by transfer (simp add: bin_nth_of_bl ac_simps)
 
 lemma no_of_bl: "(numeral bin ::'a::len word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))"
   by transfer simp
 
 lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
   by transfer simp
 
 lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
   by (simp add: uint_bl word_size)
 
 lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len word) = bin_to_bl (LENGTH('a)) bin"
   by (auto simp: uint_bl word_ubin.eq_norm word_size)
 
 lemma to_bl_numeral [simp]:
   "to_bl (numeral bin::'a::len word) =
     bin_to_bl (LENGTH('a)) (numeral bin)"
   unfolding word_numeral_alt by (rule to_bl_of_bin)
 
 lemma to_bl_neg_numeral [simp]:
   "to_bl (- numeral bin::'a::len word) =
     bin_to_bl (LENGTH('a)) (- numeral bin)"
   unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
 
 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   by (simp add: uint_bl word_size)
 
 lemma uint_bl_bin: "bl_to_bin (bin_to_bl (LENGTH('a)) (uint x)) = uint x"
   for x :: "'a::len word"
   by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
 
 lemma ucast_bl: "ucast w = of_bl (to_bl w)"
   by transfer simp
 
 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>
   using that by transfer simp
 
 lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
   by transfer (simp add: bl_to_bin_app_cat) 
 
 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>
   using that
   apply transfer
   apply (rule bit_eqI)
   apply (auto simp add: bit_take_bit_iff)
   apply (subst (asm) trunc_bl2bin_len [symmetric])
   apply (auto simp only: bit_take_bit_iff)
   done
 
 lemma word_rev_tf:
   "to_bl (of_bl bl::'a::len word) =
     rev (takefill False (LENGTH('a)) (rev bl))"
   by transfer (simp add: bl_bin_bl_rtf)
 
 lemma word_rep_drop:
   "to_bl (of_bl bl::'a::len word) =
     replicate (LENGTH('a) - length bl) False @
     drop (length bl - LENGTH('a)) bl"
   by (simp add: word_rev_tf takefill_alt rev_take)
 
 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)"
   apply (unfold ucast_bl)
   apply (rule trans)
    apply (rule word_rep_drop)
   apply simp
   done
 
 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>
   using that
   by (auto simp add : source_size target_size to_bl_ucast)
 
 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)"
   by (auto simp add : source_size target_size to_bl_ucast)
 
 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)"
   apply (subgoal_tac "sc = ucast")
    apply safe
    apply simp
    apply (erule ucast_down_drop)
   apply (rule down_cast_same [symmetric])
   apply (simp add : source_size target_size is_down)
   done
 
 lemma word_0_bl [simp]: "of_bl [] = 0"
   by transfer simp
 
 lemma word_1_bl: "of_bl [True] = 1"
   by transfer (simp add: bl_to_bin_def)
 
 lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
   by transfer (simp add: bl_to_bin_rep_False)
 
 lemma to_bl_0 [simp]: "to_bl (0::'a::len word) = replicate (LENGTH('a)) False"
   by (simp add: uint_bl word_size bin_to_bl_zero)
 
 \<comment> \<open>links with \<open>rbl\<close> operations\<close>
 lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
   by transfer (simp add: rbl_succ)
 
 lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))"
   by transfer (simp add: rbl_pred)
 
 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))"
   apply transfer
   apply (drule sym)
   apply (drule sym)
   apply (simp add: rbl_add)
   done
 
 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))"
   apply transfer
   apply (drule sym)
   apply (drule sym)
   apply (simp add: rbl_mult)
   done
 
 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"
   by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl)
 
 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 -
   from that have \<open>length x < LENGTH('a)\<close>
     by simp
   then have \<open>(of_bl x :: 'a::len word) < 2 ^ length x\<close>
     apply (simp add: of_bl_eq)
     apply transfer
     apply (simp add: take_bit_horner_sum_bit_eq)
     apply (subst length_rev [symmetric])
     apply (simp only: horner_sum_of_bool_2_less)
     done
   with that show ?thesis
     by simp
 qed
 
 lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
   by simp
 
 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
   by transfer (simp add: bl_not_bin)
 
 lemma bl_word_xor: "to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)"
   by transfer (simp flip: bl_xor_bin)
 
 lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)"
   by transfer (simp flip: bl_or_bin)
 
 lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)"
   by transfer (simp flip: bl_and_bin)
 
 lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
   apply (unfold word_size)
   apply (safe elim!: bin_nth_uint_imp)
    apply (frule bin_nth_uint_imp)
    apply (fast dest!: bin_nth_bl)+
   done
 
 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
 
 lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
   by transfer (auto simp add: bin_nth_bl)
 
 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
   by (simp add: word_size rev_nth test_bit_bl)
 
 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 (rule nth_equalityI)
   show \<open>length (map (bit w) [0..<n]) =
     length (takefill False n (rev (to_bl w)))\<close>
     by simp
   fix m
   assume \<open>m < length (map (bit w) [0..<n])\<close>
   then have \<open>m < n\<close>
     by simp
   then have \<open>bit w m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
     by (auto simp add: nth_takefill not_less rev_nth to_bl_nth word_size test_bit_word_eq dest: bit_imp_le_length)
   with \<open>m < n \<close>show \<open>map (bit w) [0..<n] ! m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
     by simp
 qed
 
 lemma to_bl_unfold:
   \<open>to_bl w = rev (map (bit w) [0..<LENGTH('a)])\<close> for w :: \<open>'a::len word\<close>
   by (simp add: map_bit_interval_eq takefill_bintrunc to_bl_def flip: bin_to_bl_def)
 
 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>
   using that by (simp add: to_bl_unfold)
 
 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>
   using that by (simp add: to_bl_unfold rev_nth)
 
 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
   by (auto simp: of_bl_def bl_to_bin_rep_F)
 
 lemma [code abstract]:
   \<open>uint (of_bl bs :: 'a word) = horner_sum of_bool 2 (take LENGTH('a::len) (rev bs))\<close>
   apply (simp add: of_bl_eq flip: take_bit_horner_sum_bit_eq)
   apply transfer
   apply simp
   done
 
 lemma [code]:
   \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a::len)])\<close>
   for w :: \<open>'a::len word\<close>
   by (simp add: to_bl_unfold rev_map)
 
 lemma word_reverse_eq_of_bl_rev_to_bl:
   \<open>word_reverse w = of_bl (rev (to_bl w))\<close>
   by (rule bit_word_eqI)
     (auto simp add: bit_word_reverse_iff bit_of_bl_iff nth_to_bl)
 
 lemmas word_reverse_no_def [simp] =
   word_reverse_eq_of_bl_rev_to_bl [of "numeral w"] for w
 
 lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
   by (rule nth_equalityI) (simp_all add: nth_rev_to_bl word_reverse_def word_rep_drop flip: of_bl_eq)
 
 lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True"
   apply (rule word_bl.Abs_inverse')
    apply simp
   apply (rule word_eqI)
   apply (clarsimp simp add: word_size)
   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
   done
 
 lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: zip_rev bl_word_or rev_map)
 
 lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: zip_rev bl_word_and rev_map)
 
 lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: zip_rev bl_word_xor rev_map)
 
 lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
   by (simp add: bl_word_not rev_map)
 
 lemma bshiftr1_numeral [simp]:
   \<open>bshiftr1 b (numeral w :: 'a word) = of_bl (b # butlast (bin_to_bl LENGTH('a::len) (numeral w)))\<close>
   by (simp add: bshiftr1_eq)
 
 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
   unfolding bshiftr1_eq by (rule word_bl.Abs_inverse) simp
 
 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
   by transfer (simp add: bl_to_bin_append)
 
 lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
   for w :: "'a::len word"
 proof -
   have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
     by simp
   also have "\<dots> = of_bl (to_bl w @ [False])"
     by (rule shiftl1_of_bl)
   finally show ?thesis .
 qed
 
 lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
   for w :: "'a::len word"
   by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
 
 \<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>
 lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
   by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
 
 lemma shiftr1_bl:
   \<open>shiftr1 w = of_bl (butlast (to_bl w))\<close>
 proof (rule bit_word_eqI)
   fix n
   assume \<open>n < LENGTH('a)\<close>
   show \<open>bit (shiftr1 w) n \<longleftrightarrow> bit (of_bl (butlast (to_bl w)) :: 'a word) n\<close>
   proof (cases \<open>n = LENGTH('a) - 1\<close>)
     case True
     then show ?thesis
       by (simp add: bit_shiftr1_iff bit_of_bl_iff)
   next
     case False
     with \<open>n < LENGTH('a)\<close>
     have \<open>n < LENGTH('a) - 1\<close>
       by simp
     with \<open>n < LENGTH('a)\<close> show ?thesis 
       by (simp add: bit_shiftr1_iff bit_of_bl_iff rev_nth nth_butlast
         word_size test_bit_word_eq to_bl_nth)
   qed
 qed
 
 lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)"
   for w :: "'a::len word"
   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>
 lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
   apply (rule word_bl.Abs_inverse')
    apply (simp del: butlast.simps)
   apply (simp add: shiftr1_bl of_bl_def)
   done
 
 lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)"
   for w :: "'a::len word"
 proof (rule nth_equalityI)
   fix n
   assume \<open>n < length (to_bl (sshiftr1 w))\<close>
   then have \<open>n < LENGTH('a)\<close>
     by simp
   then show \<open>to_bl (sshiftr1 w) ! n \<longleftrightarrow> (hd (to_bl w) # butlast (to_bl w)) ! n\<close>
     apply (cases n)
      apply (simp_all add: to_bl_nth word_size hd_conv_nth test_bit_eq_bit bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl)
     done
 qed simp
 
 lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
   for w :: "'a::len word"
   apply (unfold shiftr_def)
   apply (induct n)
    prefer 2
    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
    apply (rule butlast_take [THEN trans])
     apply (auto simp: word_size)
   done
 
 lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
   for w :: "'a::len word"
    apply (simp_all add: word_size sshiftr_eq)
   apply (rule nth_equalityI)
    apply (simp_all add: word_size nth_to_bl bit_signed_drop_bit_iff)
   done
 
 lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
   apply (unfold shiftr_def)
   apply (induct n)
    prefer 2
    apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
    apply (rule take_butlast [THEN trans])
     apply (auto simp: word_size)
   done
 
 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"
   apply (auto simp add: sshiftr_eq hd_bl_sign_sint bin_sign_def not_le word_size sint_signed_drop_bit_eq)
   apply (rule nth_equalityI)
     apply (auto simp add: nth_to_bl bit_signed_drop_bit_iff bit_last_iff)
   apply (rule nth_equalityI)
    apply (auto simp add: nth_to_bl bit_signed_drop_bit_iff bit_last_iff)
   done
 
 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
 
 lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
   by (auto intro: append_take_drop_id [symmetric])
 
 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
 
 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
   by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same)
 
 lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
   for w :: "'a::len word"
 proof -
   have "w << n = of_bl (to_bl w) << n"
     by simp
   also have "\<dots> = of_bl (to_bl w @ replicate n False)"
     by (rule shiftl_of_bl)
   finally show ?thesis .
 qed
 
 lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
   by (simp add: shiftl_bl word_rep_drop word_size)
 
 lemma shiftr1_bl_of:
   "length bl \<le> LENGTH('a) \<Longrightarrow>
     shiftr1 (of_bl bl::'a::len word) = of_bl (butlast bl)"
   by transfer (simp add: butlast_rest_bl2bin trunc_bl2bin)
 
 lemma shiftr_bl_of:
   "length bl \<le> LENGTH('a) \<Longrightarrow>
     (of_bl bl::'a::len word) >> n = of_bl (take (length bl - n) bl)"
   apply (unfold shiftr_def)
   apply (induct n)
    apply clarsimp
   apply clarsimp
   apply (subst shiftr1_bl_of)
    apply simp
   apply (simp add: butlast_take)
   done
 
 lemma shiftr_bl: "x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))"
   for x :: "'a::len word"
   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
 
 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>
   apply (subgoal_tac "x AND y = 0")
    prefer 2
    apply (rule word_bl.Rep_eqD)
    apply (simp add: bl_word_and)
    apply (rule align_lem_and [THEN trans])
        apply (simp_all add: word_size)[5]
    apply simp
   apply (subst word_plus_and_or [symmetric])
   apply (simp add : bl_word_or)
   apply (rule align_lem_or)
      apply (simp_all add: word_size)
   done
 
 lemma mask_bl: "mask n = of_bl (replicate n True)"
   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
 
 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)"
   apply (rule nth_equalityI)
    apply simp
   apply (clarsimp simp add: to_bl_nth word_size)
   apply (simp add: word_size word_ops_nth_size)
   apply (auto simp add: word_size test_bit_bl nth_append rev_nth)
   done
 
 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 (rule bit_word_eqI)
   fix m
   assume \<open>m < LENGTH('b)\<close>
   show \<open>bit (slice1 n w :: 'b::len word) m \<longleftrightarrow> bit (of_bl (takefill False n (to_bl w)) :: 'b word) m\<close>
     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)
 qed
 
 lemma slice1_no_bin [simp]:
   "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len)) (numeral w)))"
   by (simp add: slice1_eq_of_bl) (* TODO: neg_numeral *)
 
 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)))"
   by (simp add: slice_def) (* TODO: neg_numeral *)
 
 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
   by (simp add: slice_def word_size slice1_eq_of_bl takefill_alt)
 
 lemmas slice_take = slice_take' [unfolded word_size]
 
 \<comment> \<open>shiftr to a word of the same size is just slice,
     slice is just shiftr then ucast\<close>
 lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
 
 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))"
   apply (simp add: slice1_eq_of_bl)
   apply transfer
   apply (simp add: bl_bin_bl_rep_drop)
   using drop_takefill
   apply force
   done
 
 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))"
   apply (simp add: slice1_eq_of_bl)
   apply transfer
   apply (simp add: bl_bin_bl_rep_drop flip: takefill_append)
   apply (metis diff_add_inverse)
   done
 
 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
 lemmas slice1_up_alts =
   le_add_diff_inverse [symmetric, THEN su1]
   le_add_diff_inverse2 [symmetric, THEN su1]
 
 lemma slice1_tf_tf':
   "to_bl (slice1 n w :: 'a::len word) =
     rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))"
   unfolding slice1_eq_of_bl by (rule word_rev_tf)
 
 lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
 
 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>
   by (simp add: revcast_def slice1_eq_of_bl)
 
 lemmas revcast_no_def [simp] = revcast_eq_of_bl [where w="numeral w", unfolded word_size] for w
 
 lemma to_bl_revcast:
   "to_bl (revcast w :: 'a::len word) = takefill False (LENGTH('a)) (to_bl w)"
   apply (rule nth_equalityI)
   apply simp
   apply (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>)
    apply (auto simp add: nth_to_bl nth_takefill bit_revcast_iff)
   done
 
 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
   apply (rule bit_word_eqI)
   apply (simp add: bit_word_cat_iff bit_of_bl_iff nth_append not_less nth_rev_to_bl)
   apply (meson bit_word.rep_eq less_diff_conv2 nth_rev_to_bl)
   done
 
 lemma of_bl_append:
   "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
   apply transfer
   apply (simp add: bl_to_bin_app_cat bin_cat_num)
   done
 
 lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
   by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)
 
 lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
   by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)
 
 lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   by (cases x) simp_all
 
 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)))"
   apply (simp add: word_split_def)
   apply transfer
   apply (cases \<open>LENGTH('b) \<le> LENGTH('a)\<close>)
    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)
   done
 
 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)"
   apply (rule iffI)
    defer
    apply (erule (1) word_split_bl')
   apply (case_tac "word_split c")
   apply (auto simp add: word_size)
   apply (frule word_split_bl' [rotated])
    apply (auto simp add: word_size)
   done
 
 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"
   apply (rule word_split_bl [THEN iffD1])
    apply (unfold word_size)
    apply (rule refl conjI)+
   done
 
 lemma word_rcat_bl:
   \<open>word_rcat wl = of_bl (concat (map to_bl wl))\<close>
 proof -
   define ws where \<open>ws = rev wl\<close>
   moreover have \<open>word_rcat (rev ws) = of_bl (concat (map to_bl (rev ws)))\<close>
     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)
     apply transfer
     apply simp
     done
   ultimately show ?thesis
     by simp
 qed
 
 lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
   by (induct wl) (auto simp: word_size)
 
 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
 
 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))"
   apply (induct wl)
    apply clarsimp
   apply (clarsimp simp add : nth_append size_rcat_lem)
   apply (simp flip: mult_Suc minus_div_mult_eq_mod add: less_Suc_eq_le not_less)
   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)
   done
 
 lemma foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0"
   for x :: "'a::comm_monoid_add"
   by (induct xs arbitrary: x) (auto simp: add.assoc)
 
 lemmas word_cat_bl_no_bin [simp] =
   word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral]
   for a b (* FIXME: negative numerals, 0 and 1 *)
 
 lemmas word_split_bl_no_bin [simp] =
   word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
 
 lemmas word_rot_defs = word_roti_eq_word_rotr_word_rotl word_rotr_eq word_rotl_eq
 
 lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
   by (simp add: word_rotl_eq to_bl_use_of_bl)
 
 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
 
 lemmas word_rotl_eqs =
   blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
 
 lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
   by (simp add: word_rotr_eq to_bl_use_of_bl)
 
 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
 
 lemmas word_rotr_eqs =
   brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
 
 declare word_rotr_eqs (1) [simp]
 declare word_rotl_eqs (1) [simp]
 
 lemmas abl_cong = arg_cong [where f = "of_bl"]
 
 locale word_rotate
 begin
 
 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
 
 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
 
 lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
 
 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
 
 lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
 
 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
 
 end
 
 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
   simplified word_bl_Rep']
 
 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
   simplified word_bl_Rep']
 
 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)"
   apply (unfold word_roti_eq_word_rotr_word_rotl)
   apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
   apply safe
    apply (simp add: zmod_zminus1_eq_if)
    apply safe
     apply (simp add: nat_mult_distrib)
    apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
                                       [THEN conjunct2, THEN order_less_imp_le]]
                     nat_mod_distrib)
   apply (simp add: nat_mod_distrib)
   done
 
 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
 
 lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]]
 lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
 lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
 
 lemmas word_rotr_dt_no_bin' [simp] =
   word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
   (* FIXME: negative numerals, 0 and 1 *)
 
 lemmas word_rotl_dt_no_bin' [simp] =
   word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
   (* FIXME: negative numerals, 0 and 1 *)
 
 lemma max_word_bl: "to_bl (max_word::'a::len word) = replicate LENGTH('a) True"
   by (fact to_bl_n1)
 
 lemma to_bl_mask:
   "to_bl (mask n :: 'a::len word) =
   replicate (LENGTH('a) - n) False @
     replicate (min (LENGTH('a)) n) True"
   by (simp add: mask_bl word_rep_drop min_def)
 
 lemma map_replicate_True:
   "n = length xs \<Longrightarrow>
     map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
   by (induct xs arbitrary: n) auto
 
 lemma map_replicate_False:
   "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
     (zip xs (replicate n False)) = replicate n False"
   by (induct xs arbitrary: n) auto
 
 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 -
   note [simp] = map_replicate_True map_replicate_False
   have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))"
     by (simp add: bl_word_and)
   also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
     by simp
   also have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) =
       replicate n' False @ drop n' (to_bl w)"
     unfolding to_bl_mask n'_def by (subst zip_append) auto
   finally show ?thesis .
 qed
 
 lemma drop_rev_takefill:
   "length xs \<le> n \<Longrightarrow>
     drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
   by (simp add: takefill_alt rev_take)
 
 declare bin_to_bl_def [simp]
 
 end
diff --git a/thys/Word_Lib/Traditional_Infix_Syntax.thy b/thys/Word_Lib/Traditional_Infix_Syntax.thy
--- a/thys/Word_Lib/Traditional_Infix_Syntax.thy
+++ b/thys/Word_Lib/Traditional_Infix_Syntax.thy
@@ -1,534 +1,534 @@
 (*  Author:     Jeremy Dawson, NICTA
 *)
 
 section \<open>Operation variants with traditional syntax\<close>
 
 theory Traditional_Infix_Syntax
   imports "HOL-Library.Word"
 begin
 
 class semiring_bit_syntax = semiring_bit_shifts
 begin
 
 definition test_bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>  (infixl "!!" 100)
   where test_bit_eq_bit: \<open>test_bit = bit\<close>
 
 definition shiftl :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close>  (infixl "<<" 55)
   where shiftl_eq_push_bit: \<open>a << n = push_bit n a\<close>
 
 definition shiftr :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close>  (infixl ">>" 55)
   where shiftr_eq_drop_bit: \<open>a >> n = drop_bit n a\<close>
 
 end
 
 instance word :: (len) semiring_bit_syntax ..
 
 context
   includes lifting_syntax
 begin
 
 lemma test_bit_word_transfer [transfer_rule]:
   \<open>(pcr_word ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) (test_bit :: 'a::len word \<Rightarrow> _)\<close>
   by (unfold test_bit_eq_bit) transfer_prover
 
 lemma shiftl_word_transfer [transfer_rule]:
   \<open>(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. push_bit n k) shiftl\<close>
   by (unfold shiftl_eq_push_bit) transfer_prover
 
 lemma shiftr_word_transfer [transfer_rule]:
   \<open>(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. (drop_bit n \<circ> take_bit LENGTH('a)) k) (shiftr :: 'a::len word \<Rightarrow> _)\<close>
   by (unfold shiftr_eq_drop_bit) transfer_prover
 
 end
 
 lemma test_bit_word_eq:
   \<open>test_bit = (bit :: 'a::len word \<Rightarrow> _)\<close>
   by (fact test_bit_eq_bit)
 
 lemma shiftl_word_eq:
   \<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close>
   by (fact shiftl_eq_push_bit)
 
 lemma shiftr_word_eq:
   \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close>
   by (fact shiftr_eq_drop_bit)
 
 lemma test_bit_eq_iff: "test_bit u = test_bit v \<longleftrightarrow> u = v"
   for u v :: "'a::len word"
   by (simp add: bit_eq_iff test_bit_eq_bit fun_eq_iff)
 
 lemma test_bit_size: "w !! n \<Longrightarrow> n < size w"
   for w :: "'a::len word"
   by transfer simp
 
 lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). x !! n = y !! n)" (is \<open>?P \<longleftrightarrow> ?Q\<close>)
   for x y :: "'a::len word"
   by transfer (auto simp add: bit_eq_iff bit_take_bit_iff)
 
 lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> u !! n = v !! n) \<Longrightarrow> u = v"
   for u :: "'a::len word"
   by (simp add: word_size word_eq_iff)
 
 lemma word_eqD: "u = v \<Longrightarrow> u !! x = v !! x"
   for u v :: "'a::len word"
   by simp
 
 lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bit (uint w) n"
   by transfer (simp add: bit_take_bit_iff)
 
 lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
 
 lemma word_test_bit_def: 
   \<open>test_bit a = bit (uint a)\<close>
   by transfer (simp add: fun_eq_iff bit_take_bit_iff)
 
 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
 
 lemma word_test_bit_transfer [transfer_rule]:
   "(rel_fun pcr_word (rel_fun (=) (=)))
     (\<lambda>x n. n < LENGTH('a) \<and> bit x n) (test_bit :: 'a::len word \<Rightarrow> _)"
   by (simp only: test_bit_eq_bit) transfer_prover
 
 lemma test_bit_wi [simp]:
   "(word_of_int x :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bit x n"
   by transfer simp
 
 lemma word_ops_nth_size:
   "n < size x \<Longrightarrow>
     (x OR y) !! n = (x !! n | y !! n) \<and>
     (x AND y) !! n = (x !! n \<and> y !! n) \<and>
     (x XOR y) !! n = (x !! n \<noteq> y !! n) \<and>
     (NOT x) !! n = (\<not> x !! n)"
   for x :: "'a::len word"
   by transfer (simp add: bit_or_iff bit_and_iff bit_xor_iff bit_not_iff)
 
 lemma word_ao_nth:
   "(x OR y) !! n = (x !! n | y !! n) \<and>
     (x AND y) !! n = (x !! n \<and> y !! n)"
   for x :: "'a::len word"
   by transfer (auto simp add: bit_or_iff bit_and_iff)
 
 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
 lemmas msb1 = msb0 [where i = 0]
 
 lemma test_bit_numeral [simp]:
   "(numeral w :: 'a::len word) !! n \<longleftrightarrow>
     n < LENGTH('a) \<and> bit (numeral w :: int) n"
   by transfer (rule refl)
 
 lemma test_bit_neg_numeral [simp]:
   "(- numeral w :: 'a::len word) !! n \<longleftrightarrow>
     n < LENGTH('a) \<and> bit (- numeral w :: int) n"
   by transfer (rule refl)
 
 lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \<longleftrightarrow> n = 0"
   by transfer (auto simp add: bit_1_iff) 
 
 lemma nth_0 [simp]: "\<not> (0 :: 'a::len word) !! n"
   by transfer simp
 
 lemma nth_minus1 [simp]: "(-1 :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a)"
   by transfer simp
 
 lemma shiftl1_code [code]:
   \<open>shiftl1 w = push_bit 1 w\<close>
   by transfer (simp add: ac_simps)
 
 lemma uint_shiftr_eq:
   \<open>uint (w >> n) = uint w div 2 ^ n\<close>
   by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit min_def le_less less_diff_conv)
 
 lemma shiftr1_code [code]:
   \<open>shiftr1 w = drop_bit 1 w\<close>
   by transfer (simp add: drop_bit_Suc)
 
 lemma shiftl_def:
   \<open>w << n = (shiftl1 ^^ n) w\<close>
 proof -
   have \<open>push_bit n = (((*) 2 ^^ n) :: int \<Rightarrow> int)\<close> for n
     by (induction n) (simp_all add: fun_eq_iff funpow_swap1, simp add: ac_simps)
   then show ?thesis
     by transfer simp
 qed
 
 lemma shiftr_def:
   \<open>w >> n = (shiftr1 ^^ n) w\<close>
 proof -
   have \<open>shiftr1 ^^ n = (drop_bit n :: 'a word \<Rightarrow> 'a word)\<close>
     apply (induction n)
     apply simp
     apply (simp only: shiftr1_eq_div_2 [abs_def] drop_bit_eq_div [abs_def] funpow_Suc_right)
     apply (use div_exp_eq [of _ 1, where ?'a = \<open>'a word\<close>] in simp)
     done
   then show ?thesis
     by (simp add: shiftr_eq_drop_bit)
 qed
 
-lemma bit_shiftl_word_iff:
+lemma bit_shiftl_word_iff [bit_simps]:
   \<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close>
   for w :: \<open>'a::len word\<close>
   by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le)
 
-lemma bit_shiftr_word_iff:
+lemma bit_shiftr_word_iff [bit_simps]:
   \<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close>
   for w :: \<open>'a::len word\<close>
   by (simp add: shiftr_word_eq bit_drop_bit_eq)
 
 lift_definition sshiftr :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>  (infixl \<open>>>>\<close> 55)
   is \<open>\<lambda>k n. take_bit LENGTH('a) (drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k))\<close>
   by (simp flip: signed_take_bit_decr_length_iff)
 
 lemma sshiftr_eq [code]:
   \<open>w >>> n = signed_drop_bit n w\<close>
   by transfer simp
 
 lemma sshiftr_eq_funpow_sshiftr1:
   \<open>w >>> n = (sshiftr1 ^^ n) w\<close>
   apply (rule sym)
   apply (simp add: sshiftr1_eq_signed_drop_bit_Suc_0 sshiftr_eq)
   apply (induction n)
    apply simp_all
   done
 
 lemma uint_sshiftr_eq:
   \<open>uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^  n)\<close>
   for w :: \<open>'a::len word\<close>
   by transfer (simp flip: drop_bit_eq_div)
 
 lemma sshift1_code [code]:
   \<open>sshiftr1 w = signed_drop_bit 1 w\<close>
   by transfer (simp add: drop_bit_Suc)
 
 lemma sshiftr_0 [simp]: "0 >>> n = 0"
   by transfer simp
 
 lemma sshiftr_n1 [simp]: "-1 >>> n = -1"
   by transfer simp
 
-lemma bit_sshiftr_word_iff:
+lemma bit_sshiftr_word_iff [bit_simps]:
   \<open>bit (w >>> m) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else (m + n))\<close>
   for w :: \<open>'a::len word\<close>
   apply transfer
   apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le simp flip: bit_Suc)
   using le_less_Suc_eq apply fastforce
   using le_less_Suc_eq apply fastforce
   done
 
 lemma nth_sshiftr :
   "(w >>> m) !! n =
     (n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))"
   apply transfer
   apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_signed_take_bit_iff min_def not_le ac_simps)
   using le_less_Suc_eq apply fastforce
   using le_less_Suc_eq apply fastforce
   done
 
 lemma sshiftr_numeral [simp]:
   \<open>(numeral k >>> numeral n :: 'a::len word) =
     word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH('a) - 1) (numeral k)))\<close>
   apply (rule word_eqI)
   apply (cases \<open>LENGTH('a)\<close>)
    apply (simp_all add: word_size bit_drop_bit_eq nth_sshiftr bit_signed_take_bit_iff min_def not_le not_less less_Suc_eq_le ac_simps)
   done
 
 lemma revcast_down_us [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_revcast_iff bit_ucast_iff bit_sshiftr_word_iff ac_simps)
   done
 
 lemma revcast_down_ss [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_revcast_iff bit_word_scast_iff bit_sshiftr_word_iff ac_simps)
   done
 
 lemma sshiftr_div_2n: "sint (w >>> n) = sint w div 2 ^ n"
   using sint_signed_drop_bit_eq [of n w]
   by (simp add: drop_bit_eq_div sshiftr_eq) 
 
 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
 
 lemma nth_sint:
   fixes w :: "'a::len word"
   defines "l \<equiv> LENGTH('a)"
   shows "bit (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
   unfolding sint_uint l_def
   by (auto simp: bit_signed_take_bit_iff word_test_bit_def not_less min_def)
 
 lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)"
   by transfer (auto simp add: bit_exp_iff)
 
 lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a::len)"
   by transfer (auto simp add: bit_exp_iff)
 
 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x"
   for x :: "'a::len word"
   apply (rule xtrans(3))
    apply (rule_tac [2] y = "x" in le_word_or2)
   apply (rule word_eqI)
   apply (auto simp add: word_ao_nth nth_w2p word_size)
   done
 
 lemma mask_eq:
   \<open>mask n = (1 << n) - (1 :: 'a::len word)\<close>
   by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1) 
 
 lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))"
   by transfer (simp add: bit_take_bit_iff ac_simps)
 
 lemma shiftl_0 [simp]: "(0::'a::len word) << n = 0"
   by transfer simp
 
 lemma shiftr_0 [simp]: "(0::'a::len word) >> n = 0"
   by transfer simp
 
 lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)"
   by transfer (auto simp add: bit_double_iff)
 
 lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)"
   for w :: "'a::len word"
   by transfer (auto simp add: bit_push_bit_iff)
 
 lemmas nth_shiftl = nth_shiftl' [unfolded word_size]
 
 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
   by transfer (auto simp add: bit_take_bit_iff simp flip: bit_Suc)
 
 lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)"
   for w :: "'a::len word"
   apply (unfold shiftr_def)
   apply (induct "m" arbitrary: n)
    apply (auto simp add: nth_shiftr1)
   done
 
 lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
   apply transfer
   apply (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def simp flip: bit_Suc)
   using le_less_Suc_eq apply fastforce
   using le_less_Suc_eq apply fastforce
   done
 
 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
   by (fact uint_shiftr_eq)
 
 lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
   by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev)
 
 lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
   by (simp add: shiftl_rev)
 
 lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
   by (simp add: rev_shiftl)
 
 lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
   by (simp add: shiftr_rev)
 
 lemma shiftl_numeral [simp]:
   \<open>numeral k << numeral l = (push_bit (numeral l) (numeral k) :: 'a::len word)\<close>
   by (fact shiftl_word_eq)
 
 lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
   for x :: "'a::len word"
   apply transfer
   apply (simp add: take_bit_push_bit)
   done
 
 lemma shiftl_t2n: "shiftl w n = 2 ^ n * w"
   for w :: "'a::len word"
   by (induct n) (auto simp: shiftl_def shiftl1_2t)
 
 lemma shiftr_numeral [simp]:
   \<open>(numeral k >> numeral n :: 'a::len word) = drop_bit (numeral n) (numeral k)\<close>
   by (fact shiftr_word_eq)
 
 lemma nth_mask [simp]:
   \<open>(mask n :: 'a::len word) !! i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close>
   by (auto simp add: test_bit_word_eq word_size Word.bit_mask_iff)
 
 lemma slice_shiftr: "slice n w = ucast (w >> n)"
   apply (rule bit_word_eqI)
   apply (cases \<open>n \<le> LENGTH('b)\<close>)
    apply (auto simp add: bit_slice_iff bit_ucast_iff bit_shiftr_word_iff ac_simps
     dest: bit_imp_le_length)
   done
 
 lemma nth_slice: "(slice n w :: 'a::len word) !! m = (w !! (m + n) \<and> m < LENGTH('a))"
   by (simp add: slice_shiftr nth_ucast nth_shiftr)
 
 lemma revcast_down_uu [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_revcast_iff bit_ucast_iff bit_shiftr_word_iff ac_simps)
   done
 
 lemma revcast_down_su [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_revcast_iff bit_word_scast_iff bit_shiftr_word_iff ac_simps)
   done
 
 lemma cast_down_rev [OF refl]:
   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (w << n)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff)
   done
 
 lemma revcast_up [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
     rc w = (ucast w :: 'a::len word) << n"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_revcast_iff bit_word_ucast_iff bit_shiftl_word_iff)
   apply auto
   apply (metis add.commute add_diff_cancel_right)
   apply (metis diff_add_inverse2 diff_diff_add)
   done
 
 lemmas rc1 = revcast_up [THEN
   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
 lemmas rc2 = revcast_down_uu [THEN
   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
 
 lemmas ucast_up =
   rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
 lemmas ucast_down =
   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
 
 \<comment> \<open>problem posed by TPHOLs referee:
       criterion for overflow of addition of signed integers\<close>
 
 lemma sofl_test:
   \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
     (x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0\<close>
   for x y :: \<open>'a::len word\<close>
 proof -
   obtain n where n: \<open>LENGTH('a) = Suc n\<close>
     by (cases \<open>LENGTH('a)\<close>) simp_all
   have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close>
     \<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close>
     using signed_take_bit_int_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_int_less_eq [of n \<open>sint x + sint y\<close>]
     by (auto intro: ccontr)
   have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
     (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
     (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close>
     using sint_less [of x] sint_greater_eq [of x] sint_less [of y] sint_greater_eq [of y]
     signed_take_bit_int_eq_self [of \<open>LENGTH('a) - 1\<close> \<open>sint x + sint y\<close>]
     apply (auto simp add: not_less)
        apply (unfold sint_word_ariths)
        apply (subst signed_take_bit_int_eq_self)
          prefer 4
        apply (subst signed_take_bit_int_eq_self)
          prefer 7
        apply (subst signed_take_bit_int_eq_self)
          prefer 10
              apply (subst signed_take_bit_int_eq_self)
        apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
     done
   then show ?thesis
     apply (simp only: One_nat_def word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
     apply (simp add: bit_last_iff)
     done
 qed
 
 lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0"
   for x :: "'a :: len word"
   by (rule word_eqI) (auto simp add: nth_shiftr dest: test_bit_size)
 
 lemma test_bit_cat [OF refl]:
   "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
     (if n < size b then b !! n else a !! (n - size b)))"
   apply (simp add: word_size not_less; transfer)
        apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff)
   done
 
 \<comment> \<open>keep quantifiers for use in simplification\<close>
 lemma test_bit_split':
   "word_split c = (a, b) \<longrightarrow>
     (\<forall>n m.
       b !! n = (n < size b \<and> c !! n) \<and>
       a !! m = (m < size a \<and> c !! (m + size b)))"
   by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size
     bit_drop_bit_eq ac_simps exp_eq_zero_iff
     dest: bit_imp_le_length)
 
 lemma test_bit_split:
   "word_split c = (a, b) \<Longrightarrow>
     (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and>
     (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
   by (simp add: test_bit_split')
 
 lemma test_bit_split_eq:
   "word_split c = (a, b) \<longleftrightarrow>
     ((\<forall>n::nat. b !! n = (n < size b \<and> c !! n)) \<and>
      (\<forall>m::nat. a !! m = (m < size a \<and> c !! (m + size b))))"
   apply (rule_tac iffI)
    apply (rule_tac conjI)
     apply (erule test_bit_split [THEN conjunct1])
    apply (erule test_bit_split [THEN conjunct2])
   apply (case_tac "word_split c")
   apply (frule test_bit_split)
   apply (erule trans)
   apply (fastforce intro!: word_eqI simp add: word_size)
   done
 
 lemma test_bit_rcat:
   "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
     (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
   for wl :: "'a::len word list"
   by (simp add: word_size word_rcat_def foldl_map rev_map bit_horner_sum_uint_exp_iff)
     (simp add: test_bit_eq_bit)
 
 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
 
 lemma max_test_bit: "(max_word::'a::len word) !! n \<longleftrightarrow> n < LENGTH('a)"
   by (fact nth_minus1)
 
 lemma shiftr_x_0 [iff]: "x >> 0 = x"
   for x :: "'a::len word"
   by transfer simp
 
 lemma shiftl_x_0 [simp]: "x << 0 = x"
   for x :: "'a::len word"
   by (simp add: shiftl_t2n)
 
 lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n"
   by (simp add: shiftl_t2n)
 
 lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
   by (induct n) (auto simp: shiftr_def)
 
 lemma map_nth_0 [simp]: "map ((!!) (0::'a::len word)) xs = replicate (length xs) False"
   by (induct xs) auto
 
 lemma word_and_1:
   "n AND 1 = (if n !! 0 then 1 else 0)" for n :: "_ word"
   by (rule bit_word_eqI) (auto simp add: bit_and_iff test_bit_eq_bit bit_1_iff intro: gr0I)
 
 lemma test_bit_1' [simp]:
   "(1 :: 'a :: len word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
   by simp
 
 lemma shiftl0:
   "x << 0 = (x :: 'a :: len word)"
   by (fact shiftl_x_0)
 
 setup \<open>
   Context.theory_map (fold SMT_Word.add_word_shift' [
     (\<^term>\<open>shiftl :: 'a::len word \<Rightarrow> _\<close>, "bvshl"),
     (\<^term>\<open>shiftr :: 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
     (\<^term>\<open>sshiftr :: 'a::len word \<Rightarrow> _\<close>, "bvashr")
   ])
 \<close>
 
 end