diff --git a/thys/Word_Lib/Bitwise.thy b/thys/Word_Lib/Bitwise.thy
--- a/thys/Word_Lib/Bitwise.thy
+++ b/thys/Word_Lib/Bitwise.thy
@@ -1,507 +1,507 @@
 (*
  * Copyright Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 theory Bitwise
   imports
     "HOL-Library.Word"
     More_Arithmetic
     Reversed_Bit_Lists
     Bit_Shifts_Infix_Syntax
 begin
 
 text \<open>Helper constants used in defining addition\<close>
 
 definition xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
   where "xor3 a b c = (a = (b = c))"
 
 definition carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
   where "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
 
 lemma carry_simps:
   "carry True a b = (a \<or> b)"
   "carry a True b = (a \<or> b)"
   "carry a b True = (a \<or> b)"
   "carry False a b = (a \<and> b)"
   "carry a False b = (a \<and> b)"
   "carry a b False = (a \<and> b)"
   by (auto simp add: carry_def)
 
 lemma xor3_simps:
   "xor3 True a b = (a = b)"
   "xor3 a True b = (a = b)"
   "xor3 a b True = (a = b)"
   "xor3 False a b = (a \<noteq> b)"
   "xor3 a False b = (a \<noteq> b)"
   "xor3 a b False = (a \<noteq> b)"
   by (simp_all add: xor3_def)
 
 text \<open>Breaking up word equalities into equalities on their
   bit lists. Equalities are generated and manipulated in the
   reverse order to \<^const>\<open>to_bl\<close>.\<close>
 
 lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))"
   by simp
 
 lemma rbl_word_1: "rev (to_bl (1 :: 'a::len word)) = takefill False (LENGTH('a)) [True]"
   apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
    apply simp
   apply (simp only: rtb_rbl_ariths(1)[OF refl])
   apply simp
   apply (case_tac "LENGTH('a)")
    apply simp
   apply (simp add: takefill_alt)
   done
 
 lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: split_def)
 
 lemma rbl_add_carry_Cons:
   "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) =
     xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)"
   by (simp add: carry_def xor3_def)
 
 lemma rbl_add_suc_carry_fold:
   "length xs = length ys \<Longrightarrow>
     \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) =
       (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. [])) car"
   apply (erule list_induct2)
    apply simp
   apply (simp only: rbl_add_carry_Cons)
   apply simp
   done
 
 lemma to_bl_plus_carry:
   "to_bl (x + y) =
     rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
       (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
   using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
   apply (simp add: word_add_rbl[OF refl refl])
   apply (drule_tac x=False in spec)
   apply (simp add: zip_rev)
   done
 
 definition "rbl_plus cin xs ys =
   foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) cin"
 
 lemma rbl_plus_simps:
   "rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
   "rbl_plus cin [] ys = []"
   "rbl_plus cin xs [] = []"
   by (simp_all add: rbl_plus_def)
 
 lemma rbl_word_plus: "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
 
 definition "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
 
 lemma rbl_succ2_simps:
   "rbl_succ2 b [] = []"
   "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
   by (simp_all add: rbl_succ2_def)
 
 lemma twos_complement: "- x = word_succ (not x)"
   using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
   by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not)
 
 lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
   for x :: \<open>'a::len word\<close>
   by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def)
 
 lemma rbl_word_cat:
   "rev (to_bl (word_cat x y :: 'a::len word)) =
     takefill False (LENGTH('a)) (rev (to_bl y) @ rev (to_bl x))"
   by (simp add: word_cat_bl word_rev_tf)
 
 lemma rbl_word_slice:
   "rev (to_bl (slice n w :: 'a::len word)) =
     takefill False (LENGTH('a)) (drop n (rev (to_bl w)))"
   apply (simp add: slice_take word_rev_tf rev_take)
   apply (cases "n < LENGTH('b)", simp_all)
   done
 
 lemma rbl_word_ucast:
   "rev (to_bl (ucast x :: 'a::len word)) = takefill False (LENGTH('a)) (rev (to_bl x))"
   apply (simp add: to_bl_ucast takefill_alt)
   apply (simp add: rev_drop)
   apply (cases "LENGTH('a) < LENGTH('b)")
    apply simp_all
   done
 
 lemma rbl_shiftl:
   "rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))"
   by (simp add: bl_shiftl takefill_alt word_size rev_drop)
 
 lemma rbl_shiftr:
   "rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))"
   by (simp add: shiftr_slice rbl_word_slice word_size)
 
 definition "drop_nonempty v n xs = (if n < length xs then drop n xs else [last (v # xs)])"
 
 lemma drop_nonempty_simps:
   "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
   "drop_nonempty v 0 (x # xs) = (x # xs)"
   "drop_nonempty v n [] = [v]"
   by (simp_all add: drop_nonempty_def)
 
 definition "takefill_last x n xs = takefill (last (x # xs)) n xs"
 
 lemma takefill_last_simps:
   "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
   "takefill_last z 0 xs = []"
   "takefill_last z n [] = replicate n z"
   by (simp_all add: takefill_last_def) (simp_all add: takefill_alt)
 
 lemma rbl_sshiftr:
   "rev (to_bl (w >>> n)) = takefill_last False (size w) (drop_nonempty False n (rev (to_bl w)))"
   apply (cases "n < size w")
    apply (simp add: bl_sshiftr takefill_last_def word_size
       takefill_alt rev_take last_rev
       drop_nonempty_def)
   apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
    apply (simp add: word_size takefill_last_def takefill_alt
       last_rev word_msb_alt word_rev_tf
       drop_nonempty_def take_Cons')
    apply (case_tac "LENGTH('a)", simp_all)
   apply (rule word_eqI)
   apply (simp add: bit_simps word_size test_bit_of_bl
       msb_nth)
   done
 
 lemma nth_word_of_int:
   "bit (word_of_int x :: 'a::len word) n = (n < LENGTH('a) \<and> bit x n)"
   apply (simp add: test_bit_bl word_size to_bl_of_bin)
   apply (subst conj_cong[OF refl], erule bin_nth_bl)
   apply auto
   done
 
 lemma nth_scast:
   "bit (scast (x :: 'a::len word) :: 'b::len word) n =
     (n < LENGTH('b) \<and>
     (if n < LENGTH('a) - 1 then bit x n
      else bit x (LENGTH('a) - 1)))"
   apply transfer
   apply (auto simp add: bit_signed_take_bit_iff min_def)
   done
 
 lemma rbl_word_scast:
   "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (LENGTH('a)) (rev (to_bl x))"
   apply (rule nth_equalityI)
    apply (simp add: word_size takefill_last_def)
   apply (clarsimp simp: nth_scast takefill_last_def
       nth_takefill word_size rev_nth to_bl_nth)
   apply (cases "LENGTH('b)")
    apply simp
   apply (clarsimp simp: less_Suc_eq_le linorder_not_less
       last_rev word_msb_alt[symmetric]
       msb_nth)
   done
 
 definition rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   where "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map ((\<and>) x) ys) (False # sm)) xs []"
 
 lemma rbl_mul_simps:
   "rbl_mul (x # xs) ys = rbl_plus False (map ((\<and>) x) ys) (False # rbl_mul xs ys)"
   "rbl_mul [] ys = []"
   by (simp_all add: rbl_mul_def)
 
 lemma takefill_le2: "length xs \<le> n \<Longrightarrow> takefill x m (takefill x n xs) = takefill x m xs"
   by (simp add: takefill_alt replicate_add[symmetric])
 
 lemma take_rbl_plus: "\<forall>n b. take n (rbl_plus b xs ys) = rbl_plus b (take n xs) (take n ys)"
   apply (simp add: rbl_plus_def take_zip[symmetric])
   apply (rule_tac list="zip xs ys" in list.induct)
    apply simp
   apply (clarsimp simp: split_def)
   apply (case_tac n, simp_all)
   done
 
 lemma word_rbl_mul_induct:
   "length xs \<le> size y \<Longrightarrow>
     rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
   for y :: "'a::len word"
 proof (induct xs)
   case Nil
   show ?case by (simp add: rbl_mul_simps)
 next
   case (Cons z zs)
 
   have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
     for x y :: "'a word"
     by (simp add: rbl_word_plus[symmetric])
 
   have mult_bit: "to_bl (of_bl [z] * y) = map ((\<and>) z) (to_bl y)"
     by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong)
 
   have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs
     by (simp add: push_bit_eq_mult)
 
   have zip_take_triv: "\<And>xs ys n. n = length ys \<Longrightarrow> zip (take n xs) ys = zip xs ys"
     by (rule nth_equalityI) simp_all
 
   from Cons show ?case
     apply (simp add: trans [OF of_bl_append add.commute]
         rbl_mul_simps rbl_word_plus' distrib_right mult_bit shiftl rbl_shiftl)
     apply (simp add: takefill_alt word_size rev_map take_rbl_plus min_def)
     apply (simp add: rbl_plus_def)
     apply (simp add: zip_take_triv)
-    apply (simp only: mult.commute [of _ 2] mult.assoc bl_shiftl1)
+    apply (simp only: mult.commute [of _ 2] mult.assoc to_bl_double_eq)
     apply (simp flip: butlast_rev add: take_butlast)
     done
 qed
 
 lemma rbl_word_mul: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
   for x :: "'a::len word"
   using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size)
 
 text \<open>Breaking up inequalities into bitlist properties.\<close>
 
 definition
   "rev_bl_order F xs ys =
      (length xs = length ys \<and>
        ((xs = ys \<and> F)
           \<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys
                    \<and> \<not> xs ! n \<and> ys ! n)))"
 
 lemma rev_bl_order_simps:
   "rev_bl_order F [] [] = F"
   "rev_bl_order F (x # xs) (y # ys) = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
    apply (simp_all add: rev_bl_order_def)
   apply (rule conj_cong[OF refl])
   apply (cases "xs = ys")
    apply (simp add: nth_Cons')
    apply blast
   apply (simp add: nth_Cons')
   apply safe
    apply (rule_tac x="n - 1" in exI)
    apply simp
   apply (rule_tac x="Suc n" in exI)
   apply simp
   done
 
 lemma rev_bl_order_rev_simp:
   "length xs = length ys \<Longrightarrow>
    rev_bl_order F (xs @ [x]) (ys @ [y]) = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
   by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps)
 
 lemma rev_bl_order_bl_to_bin:
   "length xs = length ys \<Longrightarrow>
     rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and>
     rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
   apply (induct xs ys rule: list_induct2)
    apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat concat_bit_Suc)
   apply (auto simp add: bl_to_bin_def add1_zle_eq)
   done
 
 lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
   for x y :: "'a::len word"
   by (simp add: rev_bl_order_bl_to_bin word_le_def)
 
 lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
   for x y :: "'a::len word"
   by (simp add: word_less_alt rev_bl_order_bl_to_bin)
 
 definition "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
 
 lemma map_last_simps:
   "map_last f [] = []"
   "map_last f [x] = [f x]"
   "map_last f (x # y # zs) = x # map_last f (y # zs)"
   by (simp_all add: map_last_def)
 
 lemma word_sle_rbl:
   "x <=s y \<longleftrightarrow> rev_bl_order True (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
   using word_msb_alt[where w=x] word_msb_alt[where w=y]
   apply (simp add: word_sle_msb_le word_le_rbl)
   apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
    apply (cases "to_bl x", simp)
    apply (cases "to_bl y", simp)
    apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
    apply auto
   done
 
 lemma word_sless_rbl:
   "x <s y \<longleftrightarrow> rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
   using word_msb_alt[where w=x] word_msb_alt[where w=y]
   apply (simp add: word_sless_msb_less word_less_rbl)
   apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
    apply (cases "to_bl x", simp)
    apply (cases "to_bl y", simp)
    apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
    apply auto
   done
 
 text \<open>Lemmas for unpacking \<^term>\<open>rev (to_bl n)\<close> for numerals n and also
   for irreducible values and expressions.\<close>
 
 lemma rev_bin_to_bl_simps:
   "rev (bin_to_bl 0 x) = []"
   "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))"
   "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm))"
   "rev (bin_to_bl (Suc n) (numeral (num.One))) = True # replicate n False"
   "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))"
   "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) =
     True # rev (bin_to_bl n (- numeral (nm + num.One)))"
   "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True"
   "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) =
     True # rev (bin_to_bl n (- numeral (nm + num.One)))"
   "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) =
     False # rev (bin_to_bl n (- numeral (nm + num.One)))"
   "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) =
     False # rev (bin_to_bl n (- numeral num.One))"
   by (simp_all add: bin_to_bl_aux_append bin_to_bl_zero_aux bin_to_bl_minus1_aux replicate_append_same)
 
 lemma to_bl_upt: "to_bl x = rev (map (bit x) [0 ..< size x])"
   by (simp add: to_bl_eq_rev word_size rev_map)
 
 lemma rev_to_bl_upt: "rev (to_bl x) = map (bit x) [0 ..< size x]"
   by (simp add: to_bl_upt)
 
 lemma upt_eq_list_intros:
   "j \<le> i \<Longrightarrow> [i ..< j] = []"
   "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)"
   by (simp_all add: upt_eq_Cons_conv)
 
 
 subsection \<open>Tactic definition\<close>
 
 lemma if_bool_simps:
   "If p True y = (p \<or> y) \<and> If p False y = (\<not> p \<and> y) \<and>
     If p y True = (p \<longrightarrow> y) \<and> If p y False = (p \<and> y)"
   by auto
 
 ML \<open>
 structure Word_Bitwise_Tac =
 struct
 
 val word_ss = simpset_of \<^theory_context>\<open>Word\<close>;
 
 fun mk_nat_clist ns =
   fold_rev (Thm.mk_binop \<^cterm>\<open>Cons :: nat \<Rightarrow> _\<close>)
     ns \<^cterm>\<open>[] :: nat list\<close>;
 
 fun upt_conv ctxt ct =
   case Thm.term_of ct of
     \<^Const_>\<open>upt for n m\<close> =>
       let
         val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
         val ns = map (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close>) (i upto (j - 1))
           |> mk_nat_clist;
         val prop =
           Thm.mk_binop \<^cterm>\<open>(=) :: nat list \<Rightarrow> _\<close> ct ns
           |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
       in
         try (fn () =>
           Goal.prove_internal ctxt [] prop
             (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
                 ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
       end
   | _ => NONE;
 
 val expand_upt_simproc =
   Simplifier.make_simproc \<^context> "expand_upt"
    {lhss = [\<^term>\<open>upt x y\<close>], proc = K upt_conv};
 
 fun word_len_simproc_fn ctxt ct =
   (case Thm.term_of ct of
     \<^Const_>\<open>len_of _ for t\<close> =>
      (let
         val T = fastype_of t |> dest_Type |> snd |> the_single
         val n = Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> (Word_Lib.dest_binT T);
         val prop =
           Thm.mk_binop \<^cterm>\<open>(=) :: nat \<Rightarrow> _\<close> ct n
           |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
       in
         Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
         |> mk_meta_eq |> SOME
       end handle TERM _ => NONE | TYPE _ => NONE)
   | _ => NONE);
 
 val word_len_simproc =
   Simplifier.make_simproc \<^context> "word_len"
    {lhss = [\<^term>\<open>len_of x\<close>], proc = K word_len_simproc_fn};
 
 (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
    or just 5 (discarding nat) when n_sucs = 0 *)
 
 fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
   let
     val (f, arg) = dest_comb (Thm.term_of ct);
     val n =
       (case arg of \<^term>\<open>nat\<close> $ n => n | n => n)
       |> HOLogic.dest_number |> snd;
     val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) else (n, 0);
     val arg' = funpow i HOLogic.mk_Suc (HOLogic.mk_number \<^typ>\<open>nat\<close> j);
     val _ = if arg = arg' then raise TERM ("", []) else ();
     fun propfn g =
       HOLogic.mk_eq (g arg, g arg')
       |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
     val eq1 =
       Goal.prove_internal ctxt [] (propfn I)
         (K (simp_tac (put_simpset word_ss ctxt) 1));
   in
     Goal.prove_internal ctxt [] (propfn (curry (op $) f))
       (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
     |> mk_meta_eq |> SOME
   end handle TERM _ => NONE;
 
 fun nat_get_Suc_simproc n_sucs ts =
   Simplifier.make_simproc \<^context> "nat_get_Suc"
    {lhss = map (fn t => t $ \<^term>\<open>n :: nat\<close>) ts,
     proc = K (nat_get_Suc_simproc_fn n_sucs)};
 
 val no_split_ss =
   simpset_of (put_simpset HOL_ss \<^context>
     |> Splitter.del_split @{thm if_split});
 
 val expand_word_eq_sss =
   (simpset_of (put_simpset HOL_basic_ss \<^context> addsimps
        @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
   map simpset_of [
    put_simpset no_split_ss \<^context> addsimps
     @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not
                                 rbl_word_neg bl_word_sub rbl_word_xor
                                 rbl_word_cat rbl_word_slice rbl_word_scast
                                 rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr
                                 rbl_word_if},
    put_simpset no_split_ss \<^context> addsimps
     @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1},
    put_simpset no_split_ss \<^context> addsimps
     @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
           addsimprocs [word_len_simproc],
    put_simpset no_split_ss \<^context> addsimps
     @{thms list.simps split_conv replicate.simps list.map
                                 zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
                                 foldr.simps list.map zip.simps(1) zip_Nil zip_Cons_Cons takefill_Suc_Cons
                                 takefill_Suc_Nil takefill.Z rbl_succ2_simps
                                 rbl_plus_simps rev_bin_to_bl_simps append.simps
                                 takefill_last_simps drop_nonempty_simps
                                 rev_bl_order_simps}
           addsimprocs [expand_upt_simproc,
                        nat_get_Suc_simproc 4
                          [\<^term>\<open>replicate\<close>, \<^term>\<open>takefill x\<close>,
                           \<^term>\<open>drop\<close>, \<^term>\<open>bin_to_bl\<close>,
                           \<^term>\<open>takefill_last x\<close>,
                           \<^term>\<open>drop_nonempty x\<close>]],
     put_simpset no_split_ss \<^context> addsimps @{thms xor3_simps carry_simps if_bool_simps}
   ])
 
 fun tac ctxt =
   let
     val (ss, sss) = expand_word_eq_sss;
   in
     foldr1 (op THEN_ALL_NEW)
       ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
         map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
   end;
 
 end
 \<close>
 
 method_setup word_bitwise =
   \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close>
   "decomposer for word equalities and inequalities into bit propositions"
 
 end
diff --git a/thys/Word_Lib/Guide.thy b/thys/Word_Lib/Guide.thy
--- a/thys/Word_Lib/Guide.thy
+++ b/thys/Word_Lib/Guide.thy
@@ -1,429 +1,432 @@
 (*
  * Copyright Florian Haftmann
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 (*<*)
 theory Guide
   imports Word_Lib_Sumo Word_64 Ancient_Numeral
 begin
 
 context semiring_bit_operations
 begin
 
 lemma bit_eq_iff:
   \<open>a = b \<longleftrightarrow> (\<forall>n. 2 ^ n \<noteq> 0 \<longrightarrow> bit a n \<longleftrightarrow> bit b n)\<close>
   using bit_eq_iff [of a b] by (simp add: possible_bit_def)
 
 end
 
 notation (output)  push_bit (\<open>push'_bit\<close>)
 
 notation (output)  drop_bit (\<open>drop'_bit\<close>)
 
 notation (output)  signed_drop_bit (\<open>signed'_drop'_bit\<close>)
 
 notation (output)  Generic_set_bit.set_bit (\<open>Generic'_set'_bit.set'_bit\<close>)
 
 hide_const (open) Generic_set_bit.set_bit push_bit drop_bit signed_drop_bit
 
 no_notation bit  (infixl \<open>!!\<close> 100)
 
 abbreviation \<open>push_bit n a \<equiv> a << n\<close>
 
 abbreviation \<open>drop_bit n a \<equiv> a >> n\<close>
 
 abbreviation \<open>signed_drop_bit n a \<equiv> a >>> n\<close>
 
 (*>*)
 section \<open>A short overview over bit operations and word types\<close>
 
 subsection \<open>Key principles\<close>
 
 text \<open>
   When formalizing bit operations, it is tempting to represent
   bit values as explicit lists over a binary type. This however
   is a bad idea, mainly due to the inherent ambiguities in
   representation concerning repeating leading bits.
 
   Hence this approach avoids such explicit lists altogether
   following an algebraic path:
 
     \<^item> Bit values are represented by numeric types: idealized
       unbounded bit values can be represented by type \<^typ>\<open>int\<close>,
       bounded bit values by quotient types over \<^typ>\<open>int\<close>, aka \<^typ>\<open>'a word\<close>.
 
     \<^item> (A special case are idealized unbounded bit values ending
       in @{term [source] 0} which can be represented by type \<^typ>\<open>nat\<close> but
       only support a restricted set of operations).
 
   The fundamental principles are developed in theory \<^theory>\<open>HOL.Bit_Operations\<close>
   (which is part of \<^theory>\<open>Main\<close>):
 
     \<^item> Multiplication by \<^term>\<open>2 :: int\<close> is a bit shift to the left and
 
     \<^item> Division by \<^term>\<open>2 :: int\<close> is a bit shift to the right.
 
     \<^item> Concerning bounded bit values, iterated shifts to the left
     may result in eliminating all bits by shifting them all
     beyond the boundary.  The property \<^prop>\<open>(2 :: int) ^ n \<noteq> 0\<close>
     represents that \<^term>\<open>n\<close> is \<^emph>\<open>not\<close> beyond that boundary.
 
     \<^item> The projection on a single bit is then @{thm [mode=iff] bit_iff_odd [where ?'a = int, no_vars]}.
 
     \<^item> This leads to the most fundamental properties of bit values:
 
       \<^item> Equality rule: @{thm [display, mode=iff] bit_eq_iff [where ?'a = int, no_vars]}
 
       \<^item> Induction rule: @{thm [display, mode=iff] bits_induct [where ?'a = int, no_vars]}
 
     \<^item> Characteristic properties @{prop [source] \<open>bit (f x) n \<longleftrightarrow> P x n\<close>}
       are available in fact collection \<^text>\<open>bit_simps\<close>.
 
   On top of this, the following generic operations are provided::
 
     \<^item> Singleton \<^term>\<open>n\<close>th bit: \<^term>\<open>(2 :: int) ^ n\<close>
 
     \<^item> Bit mask upto bit \<^term>\<open>n\<close>: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]}
 
     \<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]}
 
     \<^item> Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]}
 
     \<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]}
 
     \<^item> Bitwise negation: @{thm [mode=iff] bit_not_iff_eq [where ?'a = int, no_vars]}
 
     \<^item> Bitwise conjunction: @{thm [mode=iff] bit_and_iff [where ?'a = int, no_vars]}
 
     \<^item> Bitwise disjunction: @{thm [mode=iff] bit_or_iff [where ?'a = int, no_vars]}
 
     \<^item> Bitwise exclusive disjunction: @{thm [mode=iff] bit_xor_iff [where ?'a = int, no_vars]}
 
     \<^item> Setting a single bit: @{thm set_bit_def [where ?'a = int, no_vars]}
 
     \<^item> Unsetting a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]}
 
     \<^item> Flipping a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}
 
     \<^item> Signed truncation, or modulus centered around \<^term>\<open>0::int\<close>:
         @{thm [display] signed_take_bit_def [where ?'a = int, no_vars]}
 
     \<^item> (Bounded) conversion from and to a list of bits:
         @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 
   Bit concatenation on \<^typ>\<open>int\<close> as given by 
     @{thm [display] concat_bit_def [no_vars]}
   appears quite
   technical but is the logical foundation for the quite natural bit concatenation
   on \<^typ>\<open>'a word\<close> (see below).
 \<close>
 
 subsection \<open>Core word theory\<close>
 
 text \<open>
   Proper word types are introduced in theory \<^theory>\<open>HOL-Library.Word\<close>, with
   the following specific operations:
 
     \<^item> Standard arithmetic:
         @{term \<open>(+) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>},
         @{term \<open>uminus :: 'a::len word \<Rightarrow> 'a word\<close>},
         @{term \<open>(-) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>},
         @{term \<open>(*) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>},
         @{term \<open>0 :: 'a::len word\<close>}, @{term \<open>1 :: 'a::len word\<close>}, numerals etc.
 
     \<^item> Standard bit operations: see above.
 
     \<^item> Conversion with unsigned interpretation of words:
 
         \<^item> @{term [source] \<open>unsigned :: 'a::len word \<Rightarrow> 'b::semiring_1\<close>}
 
         \<^item> Important special cases as abbreviations:
 
             \<^item> @{term [source] \<open>unat :: 'a::len word \<Rightarrow> nat\<close>}
 
             \<^item> @{term [source] \<open>uint :: 'a::len word \<Rightarrow> int\<close>}
 
             \<^item> @{term [source] \<open>ucast :: 'a::len word \<Rightarrow> 'b::len word\<close>}
 
     \<^item> Conversion with signed interpretation of words:
 
         \<^item> @{term [source] \<open>signed :: 'a::len word \<Rightarrow> 'b::ring_1\<close>}
 
         \<^item> Important special cases as abbreviations:
 
             \<^item> @{term [source] \<open>sint :: 'a::len word \<Rightarrow> int\<close>}
 
             \<^item> @{term [source] \<open>scast :: 'a::len word \<Rightarrow> 'b::len word\<close>}
 
     \<^item> Operations with unsigned interpretation of words:
 
         \<^item> @{thm [mode=iff] word_le_nat_alt [no_vars]}
 
         \<^item> @{thm [mode=iff] word_less_nat_alt [no_vars]}
 
         \<^item> @{thm unat_div_distrib [no_vars]}
 
         \<^item> @{thm unat_drop_bit_eq [no_vars]}
 
         \<^item> @{thm unat_mod_distrib [no_vars]}
 
         \<^item> @{thm [mode=iff] udvd_iff_dvd [no_vars]}
 
     \<^item> Operations with signed interpretation of words:
 
         \<^item> @{thm [mode=iff] word_sle_eq [no_vars]}
 
         \<^item> @{thm [mode=iff] word_sless_alt [no_vars]}
 
         \<^item> @{thm sint_signed_drop_bit_eq [no_vars]}
 
     \<^item> Rotation and reversal:
 
         \<^item> @{term [source] \<open>word_rotl :: nat \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>}
 
         \<^item> @{term [source] \<open>word_rotr :: nat \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>}
 
         \<^item> @{term [source] \<open>word_roti :: int \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>}
 
         \<^item> @{term [source] \<open>word_reverse :: 'a::len word \<Rightarrow> 'a word\<close>}
 
     \<^item> Concatenation: @{term [source, display] \<open>word_cat :: 'a::len word \<Rightarrow> 'b::len word \<Rightarrow> 'c::len word\<close>}
 
   For proofs about words the following default strategies are applicable:
 
     \<^item> Using bit extensionality (facts \<^text>\<open>bit_eq_iff\<close>, \<^text>\<open>bit_eqI\<close>; fact
       collection \<^text>\<open>bit_simps\<close>).
 
     \<^item> Using the @{method transfer} method.
 \<close>
 
 subsection \<open>More library theories\<close>
 
 text \<open>
   Note: currently, the theories listed here are hardly separate
   entities since they import each other in various ways.
   Always inspect them to understand what you pull in if you
   want to import one.
 
     \<^descr>[Syntax]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Syntax_Bundles\<close>]
         Bundles to provide alternative syntax for various bit operations.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Hex_Words\<close>]
         Printing word numerals as hexadecimal numerals.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Type_Syntax\<close>]
         Pretty type-sensitive syntax for cast operations.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Syntax\<close>]
         Specific ASCII syntax for prominent bit operations on word.
 
     \<^descr>[Proof tools]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Norm_Words\<close>]
         Rewriting word numerals to normal forms.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Bitwise\<close>]
         Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Bitwise_Signed\<close>]
         Method @{method word_bitwise_signed} decomposes word equalities and inequalities into bit propositions.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_EqI\<close>]
         Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions.
 
     \<^descr>[Operations]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Signed_Division_Word\<close>]
 
         Signed division on word:
 
           \<^item> @{term [source] \<open>(sdiv) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>}
 
           \<^item> @{term [source] \<open>(smod) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>}
 
       \<^descr>[\<^theory>\<open>Word_Lib.Aligned\<close>] \
 
           \<^item> @{thm [mode=iff] is_aligned_iff_udvd [no_vars]}
 
       \<^descr>[\<^theory>\<open>Word_Lib.Least_significant_bit\<close>]
 
         The least significant bit as an alias:
         @{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]}
 
       \<^descr>[\<^theory>\<open>Word_Lib.Most_significant_bit\<close>]
 
         The most significant bit:
 
           \<^item> @{thm [mode=iff] msb_int_def [of k]}
 
           \<^item> @{thm [mode=iff] word_msb_sint [no_vars]}
 
           \<^item> @{thm [mode=iff] msb_word_iff_sless_0 [no_vars]}
 
           \<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]}
 
       \<^descr>[\<^theory>\<open>Word_Lib.Bit_Shifts_Infix_Syntax\<close>]
 
         Abbreviations for bit shifts decorated with
         traditional infix syntax:
 
           \<^item> @{abbrev shiftl}
 
           \<^item> @{abbrev shiftr}
 
           \<^item> @{abbrev sshiftr}
 
       \<^descr>[\<^theory>\<open>Word_Lib.Next_and_Prev\<close>] \
 
           \<^item> @{thm word_next_unfold [no_vars]}
 
           \<^item> @{thm word_prev_unfold [no_vars]}
 
       \<^descr>[\<^theory>\<open>Word_Lib.Enumeration_Word\<close>]
 
         More on explicit enumeration of word types.
 
       \<^descr>[\<^theory>\<open>Word_Lib.More_Word_Operations\<close>]
 
         Even more operations on word.
 
     \<^descr>[Types]
 
       \<^descr>[\<^theory>\<open>Word_Lib.Signed_Words\<close>]
 
           Formal tagging of word types with a \<^text>\<open>signed\<close> marker.
 
     \<^descr>[Lemmas]
 
       \<^descr>[\<^theory>\<open>Word_Lib.More_Word\<close>]
 
           More lemmas on words.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_Lemmas\<close>]
 
           More lemmas on words, covering many other theories mentioned here.
 
     \<^descr>[Words of popular lengths].
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_8\<close>]
 
           for 8-bit words.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_16\<close>]
 
           for 16-bit words.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_32\<close>]
 
           for 32-bit words.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Word_64\<close>]
 
           for 64-bit words. This theory is not part of \<^text>\<open>Word_Lib_Sumo\<close>, because it shadows
           names from \<^theory>\<open>Word_Lib.Word_32\<close>. They can be used together, but then require
           to use qualified names in applications.
 \<close>
 
 
 subsection \<open>More library sessions\<close>
 
 text \<open>
   \<^descr>[\<^text>\<open>Native_Word\<close>] Makes machine words and machine arithmetic available for code generation.
   It provides a common abstraction that hides the differences between the different target languages.
   The code generator maps these operations to the APIs of the target languages.
 \<close>
 
 subsection \<open>Legacy theories\<close>
 
 text \<open>
   The following theories contain material which has been
   factored out since it is not recommended to use it in
   new applications, mostly because matters can be expressed
   succinctly using already existing operations.
 
   This section gives some indication how to migrate away
   from those theories.  However theorem coverage may still
   be terse in some cases.
 
   \<^descr>[\<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>]
 
     An entry point importing any relevant theory in that session.  Intended
     for backward compatibility: start importing this theory when
     migrating applications to Isabelle2021, and later sort out
     what you really need. You may need to include
    \<^theory>\<open>Word_Lib.Word_64\<close> separately.
 
   \<^descr>[\<^theory>\<open>Word_Lib.Generic_set_bit\<close>]
 
     Kind of an alias: @{thm set_bit_eq [no_vars]}
 
   \<^descr>[\<^theory>\<open>Word_Lib.Typedef_Morphisms\<close>]
 
     A low-level extension to HOL typedef providing
     conversions along type morphisms.  The @{method transfer} method
     seems to be sufficient for most applications though.
 
   \<^descr>[\<^theory>\<open>Word_Lib.Bit_Comprehension\<close>]
 
     Comprehension syntax for bit values over predicates
     \<^typ>\<open>nat \<Rightarrow> bool\<close>.  For \<^typ>\<open>'a::len word\<close>, straightforward
     alternatives exist; difficult to handle for \<^typ>\<open>int\<close>.
 
   \<^descr>[\<^theory>\<open>Word_Lib.Reversed_Bit_Lists\<close>]
 
     Representation of bit values as explicit list in
     \<^emph>\<open>reversed\<close> order.
 
     This should rarely be necessary: the \<^const>\<open>bit\<close> projection
     should be sufficient in most cases.  In case explicit lists
     are needed, existing operations can be used:
 
     @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 
   \<^descr>[\<^theory>\<open>Word_Lib.Many_More\<close>]
 
     Collection of operations and theorems which are kept for backward
     compatibility and not used in other theories in session \<^text>\<open>Word_Lib\<close>.
     They are used in applications of \<^text>\<open>Word_Lib\<close>, but should be migrated to there.
 \<close>
 
 section \<open>Changelog\<close>
 
 text \<open>
   \<^descr>[Changes since AFP 2021] ~
 
     \<^item> Theory \<^theory>\<open>Word_Lib.Ancient_Numeral\<close> is no part of \<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>
       any longer.
 
     \<^item> Infix syntax for \<^term>\<open>(AND)\<close>, \<^term>\<open>(OR)\<close>, \<^term>\<open>(XOR)\<close> organized in
       syntax bundle \<^bundle>\<open>bit_operations_syntax\<close>.
 
     \<^item> Abbreviation \<^abbrev>\<open>max_word\<close> moved from distribution into theory
       \<^theory>\<open>Word_Lib.Legacy_Aliases\<close>.
 
     \<^item> Operation \<^const>\<open>test_bit\<close> replaced by input abbreviation \<^abbrev>\<open>test_bit\<close>.
 
     \<^item> Operation \<^const>\<open>shiftl\<close> replaced by abbreviation \<^abbrev>\<open>shiftl\<close>.
 
     \<^item> Operation \<^const>\<open>shiftr\<close> replaced by abbreviation \<^abbrev>\<open>shiftr\<close>.
 
     \<^item> Operation \<^const>\<open>sshiftr\<close> replaced by abbreviation \<^abbrev>\<open>sshiftr\<close>.
 
     \<^item> Abbreviations \<^abbrev>\<open>bin_nth\<close>, \<^abbrev>\<open>bin_last\<close>, \<^abbrev>\<open>bin_rest\<close>,
       \<^abbrev>\<open>bintrunc\<close>, \<^abbrev>\<open>sbintrunc\<close>, \<^abbrev>\<open>norm_sint\<close>,
       \<^abbrev>\<open>bin_cat\<close> moved into theory \<^theory>\<open>Word_Lib.Legacy_Aliases\<close>.
 
-    \<^item> Operations \<^abbrev>\<open>shiftl1\<close>, \<^abbrev>\<open>shiftr1\<close>, \<^abbrev>\<open>sshiftr1\<close>, \<^abbrev>\<open>bshiftr1\<close>,
+    \<^item> Operations \<^abbrev>\<open>bshiftr1\<close>,
       \<^abbrev>\<open>setBit\<close>, \<^abbrev>\<open>clearBit\<close> moved from distribution into theory
       \<^theory>\<open>Word_Lib.Legacy_Aliases\<close> and replaced by input abbreviations.
 
+    \<^item> Operations \<^const>\<open>shiftl1\<close>, \<^const>\<open>shiftr1\<close>, \<^const>\<open>sshiftr1\<close>
+      moved here from distribution.
+
     \<^item> Operation \<^const>\<open>complement\<close> replaced by input abbreviation \<^abbrev>\<open>complement\<close>.
 \<close>
 
 (*<*)
 end
 (*>*)
diff --git a/thys/Word_Lib/Legacy_Aliases.thy b/thys/Word_Lib/Legacy_Aliases.thy
--- a/thys/Word_Lib/Legacy_Aliases.thy
+++ b/thys/Word_Lib/Legacy_Aliases.thy
@@ -1,271 +1,139 @@
 (*
  * Copyright Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section \<open>Legacy aliases\<close>
 
 theory Legacy_Aliases
   imports "HOL-Library.Word"
 begin
 
 context abstract_boolean_algebra
 begin
 
 lemma conj_assoc: "(x \<^bold>\<sqinter> y) \<^bold>\<sqinter> z = x \<^bold>\<sqinter> (y \<^bold>\<sqinter> z)"
   by (fact conj.assoc)
 
 lemma conj_commute: "x \<^bold>\<sqinter> y = y \<^bold>\<sqinter> x"
   by (fact conj.commute)
 
 lemmas conj_left_commute = conj.left_commute
 lemmas conj_ac = conj.assoc conj.commute conj.left_commute
 
 lemma conj_one_left: "\<^bold>1 \<^bold>\<sqinter> x = x"
   by (fact conj.left_neutral)
 
 lemma conj_left_absorb: "x \<^bold>\<sqinter> (x \<^bold>\<sqinter> y) = x \<^bold>\<sqinter> y"
   by (fact conj.left_idem)
 
 lemma conj_absorb: "x \<^bold>\<sqinter> x = x"
   by (fact conj.idem)
 
 lemma disj_assoc: "(x \<^bold>\<squnion> y) \<^bold>\<squnion> z = x \<^bold>\<squnion> (y \<^bold>\<squnion> z)"
   by (fact disj.assoc)
 
 lemma disj_commute: "x \<^bold>\<squnion> y = y \<^bold>\<squnion> x"
   by (fact disj.commute)
 
 lemmas disj_left_commute = disj.left_commute
 
 lemmas disj_ac = disj.assoc disj.commute disj.left_commute
 
 lemma disj_zero_left: "\<^bold>0 \<^bold>\<squnion> x = x"
   by (fact disj.left_neutral)
 
 lemma disj_left_absorb: "x \<^bold>\<squnion> (x \<^bold>\<squnion> y) = x \<^bold>\<squnion> y"
   by (fact disj.left_idem)
 
 lemma disj_absorb: "x \<^bold>\<squnion> x = x"
   by (fact disj.idem)
 
 end
 
 context abstract_boolean_algebra_sym_diff
 begin
 
 lemmas xor_assoc = xor.assoc
 lemmas xor_commute = xor.commute
 lemmas xor_left_commute = xor.left_commute
 
 lemmas xor_ac = xor.assoc xor.commute xor.left_commute
 
 lemma xor_zero_right: "x \<^bold>\<ominus> \<^bold>0 = x"
   by (fact xor.comm_neutral)
 
 lemma xor_zero_left: "\<^bold>0 \<^bold>\<ominus> x = x"
   by (fact xor.left_neutral)
 
 end
 
 abbreviation (input) test_bit :: \<open>'a::semiring_bits \<Rightarrow> nat \<Rightarrow> bool\<close>
   where \<open>test_bit \<equiv> bit\<close>
 
 abbreviation (input) bin_nth :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
   where \<open>bin_nth \<equiv> bit\<close>
 
 abbreviation (input) bin_last :: \<open>int \<Rightarrow> bool\<close>
   where \<open>bin_last \<equiv> odd\<close>
 
 abbreviation (input) bin_rest :: \<open>int \<Rightarrow> int\<close>
   where \<open>bin_rest w \<equiv> w div 2\<close>
 
 abbreviation (input) bintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>bintrunc \<equiv> take_bit\<close>
 
 abbreviation (input) sbintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>sbintrunc \<equiv> signed_take_bit\<close>
 
 abbreviation (input) bin_cat :: \<open>int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>bin_cat k n l \<equiv> concat_bit n l k\<close>
 
 abbreviation (input) norm_sint :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>norm_sint n \<equiv> signed_take_bit (n - 1)\<close>
 
 abbreviation (input) max_word :: \<open>'a::len word\<close>
   where \<open>max_word \<equiv> - 1\<close>
 
 abbreviation (input) complement :: \<open>'a::len word \<Rightarrow> 'a word\<close>
   where \<open>complement \<equiv> not\<close>
 
 lemma complement_mask:
   "complement (2 ^ n - 1) = not (mask n)"
   unfolding mask_eq_decr_exp by simp
 
-abbreviation (input) shiftl1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
-  where \<open>shiftl1 \<equiv> (*) 2\<close>
-
-abbreviation (input)  shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
-  where \<open>shiftr1 w \<equiv> w div 2\<close>
-
-abbreviation (input) sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
-  where \<open>sshiftr1 \<equiv> signed_drop_bit (Suc 0)\<close>
-
 context
   includes bit_operations_syntax
 begin
 
 abbreviation (input) bshiftr1 :: \<open>bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>
   where \<open>bshiftr1 b w \<equiv> w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b) \<close>
 
 end
 
-lemma shiftr1_1: "shiftr1 (1::'a::len word) = 0"
-  by (fact bits_1_div_2)
-
-lemma sshiftr1_eq:
-  \<open>sshiftr1 w = word_of_int (sint w div 2)\<close>
-  by (rule bit_word_eqI) (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE)
-
-lemma shiftl1_eq:
-  \<open>shiftl1 w = word_of_int (2 * uint w)\<close>
-  by (rule bit_word_eqI) (simp add: bit_simps)
-
-lemma bit_shiftl1_iff:
-  \<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close>
-  for w :: \<open>'a::len word\<close>
-  by (auto simp add: bit_simps)
-
-lemma bit_shiftr1_iff:
-  \<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close>
-  by (simp add: bit_Suc)
-
-lemma shiftr1_eq:
-  \<open>shiftr1 w = word_of_int (uint w div 2)\<close>
-  by (rule bit_word_eqI) (simp add: bit_simps flip: bit_Suc)
-
-lemma shiftl1_rev:
-  "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
-  by (rule bit_word_eqI) (auto simp add: bit_simps Suc_diff_Suc simp flip: bit_Suc)
-
-lemma shiftl1_p:
-  "shiftl1 w = w + w"
-  for w :: "'a::len word"
-  by (fact mult_2)
-
-lemma shiftr1_bintr:
-  "(shiftr1 (numeral w) :: 'a::len word) =
-    word_of_int (take_bit LENGTH('a) (numeral w) div 2)"
-  by (rule bit_word_eqI) (simp add: bit_simps bit_numeral_iff [where ?'a = int] flip: bit_Suc)
-
-lemma sshiftr1_sbintr:
-  "(sshiftr1 (numeral w) :: 'a::len word) =
-    word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2)"
-  apply (cases \<open>LENGTH('a)\<close>)
-  apply simp_all
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE)
-  done
-
-lemma shiftl1_wi:
-  "shiftl1 (word_of_int w) = word_of_int (2 * w)"
-  by transfer simp
-
-lemma shiftl1_numeral:
-  "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
-  unfolding word_numeral_alt shiftl1_wi by simp
-
-lemma shiftl1_neg_numeral:
-  "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
-  unfolding word_neg_numeral_alt shiftl1_wi by simp
-
-lemma shiftl1_0:
-  "shiftl1 0 = 0"
-  by (fact mult_zero_right)
-
-lemma shiftl1_def_u:
-  "shiftl1 w = word_of_int (2 * uint w)"
-  by (fact shiftl1_eq)
-
-lemma shiftl1_def_s:
-  "shiftl1 w = word_of_int (2 * sint w)"
-  by simp
-
-lemma shiftr1_0:
-  "shiftr1 0 = 0"
-  by (fact bits_div_0)
-
-lemma sshiftr1_0:
-  "sshiftr1 0 = 0"
-  by (fact signed_drop_bit_of_0)
-
-lemma sshiftr1_n1:
-  "sshiftr1 (- 1) = - 1"
-  by (fact signed_drop_bit_of_minus_1)
-
-lemma uint_shiftr1:
-  "uint (shiftr1 w) = uint w div 2"
-  by (rule bit_eqI) (simp add: bit_simps flip: bit_Suc)
-
-lemma shiftr1_div_2:
-  "uint (shiftr1 w) = uint w div 2"
-  by (fact uint_shiftr1)
-
-lemma sshiftr1_div_2:
-  "sint (sshiftr1 w) = sint w div 2"
-  by (rule bit_eqI) (auto simp add: bit_simps ac_simps min_def simp flip: bit_Suc elim: le_SucE)
-
-lemma bit_sshiftr1_iff:
-  \<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
-    for w :: \<open>'a::len word\<close>
-  by (auto simp add: bit_simps)
-
 lemma bit_bshiftr1_iff:
   \<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
     for w :: \<open>'a::len word\<close>
   by (auto simp add: bit_simps simp flip: bit_Suc)
 
-lemma nth_shiftl1:
-  "bit (shiftl1 w) n \<longleftrightarrow> n < size w \<and> n > 0 \<and> bit w (n - 1)"
-  by (auto simp add: word_size bit_simps)
-
-lemma nth_shiftr1:
-  "bit (shiftr1 w) n = bit w (Suc n)"
-  by (simp add: bit_Suc)
-
-lemma nth_sshiftr1: "bit (sshiftr1 w) n = (if n = size w - 1 then bit w n else bit w (Suc n))"
-  by (auto simp add: word_size bit_simps)
-
-lemma shiftl_power:
-  "(shiftl1 ^^ x) (y::'a::len word) = 2 ^ x * y"
-  by (induction x) simp_all
-
-lemma le_shiftr1:
-  \<open>shiftr1 u \<le> shiftr1 v\<close> if \<open>u \<le> v\<close>
-  using that by (simp add: word_le_nat_alt unat_div div_le_mono)
-
-lemma le_shiftr1':
-  "\<lbrakk> shiftr1 u \<le> shiftr1 v ; shiftr1 u \<noteq> shiftr1 v \<rbrakk> \<Longrightarrow> u \<le> v"
-  by (meson dual_order.antisym le_cases le_shiftr1)
-
 abbreviation (input) setBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>
   where \<open>setBit w n \<equiv> set_bit n w\<close>
 
 abbreviation (input) clearBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>
   where \<open>clearBit w n \<equiv> unset_bit n w\<close>
 
 lemma bit_setBit_iff:
   \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
   for w :: \<open>'a::len word\<close>
   by (auto simp add: bit_simps)
 
 lemma bit_clearBit_iff:
   \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
   for w :: \<open>'a::len word\<close>
   by (auto simp add: bit_simps)
 
 lemmas less_def = less_eq [symmetric]
 lemmas le_def = not_less [symmetric, where ?'a = nat]
 
 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,2240 +1,2250 @@
 (*
  * Copyright Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 (* Author: Jeremy Dawson, NICTA *)
 
 section \<open>Bit values as reversed lists of bools\<close>
 
 theory Reversed_Bit_Lists
   imports
     "HOL-Library.Word"
     Typedef_Morphisms
     Least_significant_bit
     Most_significant_bit
     Even_More_List
     "HOL-Library.Sublist"
     Aligned
+    Singleton_Bit_Shifts
     Legacy_Aliases
 begin
 
 context
   includes bit_operations_syntax
 begin
 
 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 (w div 2) (odd 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 (take_bit 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) = take_bit 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 (take_bit 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 (take_bit 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 (take_bit 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 (signed_take_bit 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 (signed_take_bit n w) = -1)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
 
 lemma bin_nth_of_bl_aux:
   "bit (bl_to_bin_aux bl w) n =
     (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bit 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: "bit (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> bit 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 = bit 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) (w div 2)"
   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) (bl_to_bin bl div 2)"
   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 = bl_to_bin_aux bl w div 2"
   by (induct bl arbitrary: w) auto
 
 lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bl_to_bin bl div 2"
   by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
 
 lemma trunc_bl2bin_aux:
   "take_bit m (bl_to_bin_aux bl w) =
     bl_to_bin_aux (drop (length bl - m) bl) (take_bit (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: "take_bit 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]: "take_bit (length bl) (bl_to_bin bl) = bl_to_bin bl"
   by (simp add: trunc_bl2bin)
 
 lemma bl2bin_drop: "bl_to_bin (drop k bl) = take_bit (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 (((\<lambda>w. w div 2) ^^ (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> odd (bl_to_bin_aux xs w)"
   by (induct xs arbitrary: w) auto
 
 lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> odd (bl_to_bin xs)"
   unfolding bl_to_bin_def by (erule last_bin_last')
 
 lemma bin_last_last: "odd 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 (concat_bit nv v w) =
     concat_bit (nv + length bs) (bl_to_bin_aux bs v) w"
   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) (concat_bit nw w v) 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 = concat_bit (length bs) (bl_to_bin bs) w"
   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) (concat_bit nw w v) =
     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) = concat_bit (length bs) (bl_to_bin bs) (bl_to_bin bsa)"
   by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
 
 lemma bin_to_bl_cat_app:
   "bin_to_bl (n + nw) (concat_bit nw wa w) = 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: "concat_bit n w (bl_to_bin cs) = 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 (auto 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_all 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_all add: bin_to_bl_aux_alt)
   apply (simp_all 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 (simp add: length_concat comp_def sum_list_triv)
 
 lemma bin_cat_foldl_lem:
   "foldl (\<lambda>u k. concat_bit n k u) x xs =
     concat_bit (size xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x"
   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 = "concat_bit n a y" in meta_spec)
   apply (simp add: bin_cat_assoc_sym)
   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: "odd (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: "bl_to_bin bs div 2 = 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 [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 (rule bit_word_eqI)
   apply (auto simp add: bit_simps to_bl_eq_rev nth_append rev_nth nth_butlast not_less simp flip: bit_Suc)
   apply (metis Suc_pred len_gt_0 less_eq_decr_length_iff not_bit_length verit_la_disequality)
   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
 
 global_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:
   "bit (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': "bit (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: "bit 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 = bit 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 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>Word.the_int (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 (fact to_bl_eq_rev)
 
 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 (rule bit_word_eqI) (auto simp add: bit_simps rev_nth nth_append nth_butlast nth_bin_to_bl simp flip: bit_Suc)
 
 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)
+  apply (rule bit_word_eqI)
+  apply (simp add: bit_simps)
+  subgoal for n
+    apply (cases n)
+     apply simp_all
+    done
+  done
 
 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
+  apply (rule bit_word_eqI)
+  apply (simp add: bit_simps)
+  subgoal for n
+    apply (cases n)
+     apply (simp_all add: nth_rev_to_bl)
+    done
+  done
 
 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)
 
+lemma to_bl_double_eq:
+  \<open>to_bl (2 * w) = tl (to_bl w) @ [False]\<close>
+  using bl_shiftl1 [of w] by (simp add: shiftl1_def ac_simps)
+
 \<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 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 bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl)
     done
 qed simp
 
 lemma drop_shiftr: "drop n (to_bl (drop_bit n w)) = take (size w - n) (to_bl w)"
   for w :: "'a::len word"
   apply (rule nth_equalityI)
    apply (simp_all add: word_size to_bl_nth bit_simps)
   done
 
 lemma drop_sshiftr: "drop n (to_bl (signed_drop_bit n w)) = take (size w - n) (to_bl w)"
   for w :: "'a::len word"
    apply (simp_all add: word_size)
   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 (drop_bit n w)) = replicate n False"
   apply (rule nth_equalityI)
    apply (simp_all add: word_size to_bl_nth bit_simps)
   using bit_imp_le_length by fastforce
 
 lemma take_sshiftr':
   "n \<le> size w \<Longrightarrow> hd (to_bl (signed_drop_bit n w)) = hd (to_bl w) \<and>
     take n (to_bl (signed_drop_bit n w)) = replicate n (hd (to_bl w))"
   for w :: "'a::len word"
   apply (auto simp add: 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: "push_bit n (of_bl bl) = of_bl (bl @ replicate n False)"
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_simps nth_append)
   done
 
 lemma shiftl_bl: "push_bit n w = of_bl (to_bl w @ replicate n False)"
   for w :: "'a::len word"
 proof -
   have "push_bit n w = push_bit n (of_bl (to_bl w))"
     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 (push_bit n w) = 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)"
+  apply (rule bit_word_eqI)
+  apply (simp add: bit_simps)
   apply (cases bl rule: rev_cases)
-  apply simp_all
-  apply (rule bit_word_eqI)
-  apply (auto simp add: bit_simps simp flip: bit_Suc)
+  apply auto
   done
 
 lemma shiftr_bl_of:
   "length bl \<le> LENGTH('a) \<Longrightarrow>
     drop_bit n (of_bl bl::'a::len word) = of_bl (take (length bl - n) bl)"
   by (rule bit_word_eqI) (auto simp add: bit_simps rev_nth)
 
 lemma shiftr_bl: "drop_bit n x \<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: bit_simps 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 bit_simps)
   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"]
 
 end
 
 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 (- 1::'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
 
 context
   includes bit_operations_syntax
 begin
 
 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]
 
 lemmas of_bl_reasoning = to_bl_use_of_bl of_bl_append
 
 lemma uint_of_bl_is_bl_to_bin_drop:
   "length (dropWhile Not l) \<le> LENGTH('a) \<Longrightarrow> uint (of_bl l :: 'a::len word) = bl_to_bin l"
   apply transfer
   apply (simp add: take_bit_eq_mod)
   apply (rule Divides.mod_less)
    apply (rule bl_to_bin_ge0)
   using bl_to_bin_lt2p_drop apply (rule order.strict_trans2)
   apply simp
   done
 
 corollary uint_of_bl_is_bl_to_bin:
   "length l\<le>LENGTH('a) \<Longrightarrow> uint ((of_bl::bool list\<Rightarrow> ('a :: len) word) l) = bl_to_bin l"
   apply(rule uint_of_bl_is_bl_to_bin_drop)
   using le_trans length_dropWhile_le by blast
 
 lemma bin_to_bl_or:
   "bin_to_bl n (a OR b) = map2 (\<or>) (bin_to_bl n a) (bin_to_bl n b)"
   using bl_or_aux_bin[where n=n and v=a and w=b and bs="[]" and cs="[]"]
   by simp
 
 lemma word_and_1_bl:
   fixes x::"'a::len word"
   shows "(x AND 1) = of_bl [bit x 0]"
   by (simp add: mod_2_eq_odd and_one_eq)
 
 lemma word_1_and_bl:
   fixes x::"'a::len word"
   shows "(1 AND x) = of_bl [bit x 0]"
   by (simp add: mod_2_eq_odd one_and_eq)
 
 lemma of_bl_drop:
   "of_bl (drop n xs) = (of_bl xs AND mask (length xs - n))"
   apply (rule bit_word_eqI)
   apply (auto simp: rev_nth bit_simps cong: rev_conj_cong)
   done
 
 lemma to_bl_1:
   "to_bl (1::'a::len word) = replicate (LENGTH('a) - 1) False @ [True]"
   by (rule nth_equalityI) (auto simp add: to_bl_unfold nth_append rev_nth bit_1_iff not_less not_le)
 
 lemma eq_zero_set_bl:
   "(w = 0) = (True \<notin> set (to_bl w))"
   apply (auto simp add: to_bl_unfold)
   apply (rule bit_word_eqI)
   apply auto
   done
 
 lemma of_drop_to_bl:
   "of_bl (drop n (to_bl x)) = (x AND mask (size x - n))"
   by (simp add: of_bl_drop word_size_bl)
 
 lemma unat_of_bl_length:
   "unat (of_bl xs :: 'a::len word) < 2 ^ (length xs)"
 proof (cases "length xs < LENGTH('a)")
   case True
   then have "(of_bl xs::'a::len word) < 2 ^ length xs"
     by (simp add: of_bl_length_less)
   with True
   show ?thesis
     by (simp add: word_less_nat_alt unat_of_nat)
 next
   case False
   have "unat (of_bl xs::'a::len word) < 2 ^ LENGTH('a)"
     by (simp split: unat_split)
   also
   from False
   have "LENGTH('a) \<le> length xs" by simp
   then have "2 ^ LENGTH('a) \<le> (2::nat) ^ length xs"
     by (rule power_increasing) simp
   finally
   show ?thesis .
 qed
 
 lemma word_msb_alt: "msb w \<longleftrightarrow> hd (to_bl w)"
   for w :: "'a::len word"
   apply (simp add: msb_word_eq)
   apply (subst hd_conv_nth)
    apply simp
   apply (subst nth_to_bl)
    apply simp
   apply simp
   done
 
 lemma word_lsb_last:
   \<open>lsb w \<longleftrightarrow> last (to_bl w)\<close>
   for w :: \<open>'a::len word\<close>
   using nth_to_bl [of \<open>LENGTH('a) - Suc 0\<close> w]
   by (simp add: lsb_odd last_conv_nth)
 
 lemma is_aligned_to_bl:
   "is_aligned (w :: 'a :: len word) n = (True \<notin> set (drop (size w - n) (to_bl w)))"
   by (simp add: is_aligned_mask eq_zero_set_bl bl_and_mask word_size)
 
 lemma is_aligned_replicate:
   fixes w::"'a::len word"
   assumes aligned: "is_aligned w n"
   and          nv: "n \<le> LENGTH('a)"
   shows   "to_bl w = (take (LENGTH('a) - n) (to_bl w)) @ replicate n False"
   apply (rule nth_equalityI)
   using assms apply (simp_all add: nth_append not_less word_size to_bl_nth is_aligned_imp_not_bit)
   done
 
 lemma is_aligned_drop:
   fixes w::"'a::len word"
   assumes "is_aligned w n" "n \<le> LENGTH('a)"
   shows "drop (LENGTH('a) - n) (to_bl w) = replicate n False"
 proof -
   have "to_bl w = take (LENGTH('a) - n) (to_bl w) @ replicate n False"
     by (rule is_aligned_replicate) fact+
   then have "drop (LENGTH('a) - n) (to_bl w) = drop (LENGTH('a) - n) \<dots>" by simp
   also have "\<dots> = replicate n False" by simp
   finally show ?thesis .
 qed
 
 lemma less_is_drop_replicate:
   fixes x::"'a::len word"
   assumes lt: "x < 2 ^ n"
   shows   "to_bl x = replicate (LENGTH('a) - n) False @ drop (LENGTH('a) - n) (to_bl x)"
   by (metis assms bl_and_mask' less_mask_eq)
 
 lemma is_aligned_add_conv:
   fixes off::"'a::len word"
   assumes aligned: "is_aligned w n"
   and        offv: "off < 2 ^ n"
   shows    "to_bl (w + off) =
    (take (LENGTH('a) - n) (to_bl w)) @ (drop (LENGTH('a) - n) (to_bl off))"
 proof cases
   assume nv: "n \<le> LENGTH('a)"
   show ?thesis
   proof (subst aligned_bl_add_size, simp_all only: word_size)
     show "drop (LENGTH('a) - n) (to_bl w) = replicate n False"
       by (subst is_aligned_replicate [OF aligned nv]) (simp add: word_size)
 
     from offv show "take (LENGTH('a) - n) (to_bl off) =
                     replicate (LENGTH('a) - n) False"
       by (subst less_is_drop_replicate, assumption) simp
   qed fact
 next
   assume "\<not> n \<le> LENGTH('a)"
   with offv show ?thesis by (simp add: power_overflow)
 qed
 
 lemma is_aligned_replicateI:
   "to_bl p = addr @ replicate n False \<Longrightarrow> is_aligned (p::'a::len word) n"
   apply (simp add: is_aligned_to_bl word_size)
   apply (subgoal_tac "length addr = LENGTH('a) - n")
    apply (simp add: replicate_not_True)
   apply (drule arg_cong [where f=length])
   apply simp
   done
 
 lemma to_bl_2p:
   "n < LENGTH('a) \<Longrightarrow>
    to_bl ((2::'a::len word) ^ n) =
    replicate (LENGTH('a) - Suc n) False @ True # replicate n False"
   apply (rule nth_equalityI)
    apply (auto simp add: nth_append to_bl_nth word_size bit_simps not_less nth_Cons le_diff_conv)
   subgoal for i
   apply (cases \<open>Suc (i + n) - LENGTH('a)\<close>)
   apply simp_all
     done
   done
 
 lemma xor_2p_to_bl:
   fixes x::"'a::len word"
   shows "to_bl (x XOR 2^n) =
   (if n < LENGTH('a)
    then take (LENGTH('a)-Suc n) (to_bl x) @ (\<not>rev (to_bl x)!n) # drop (LENGTH('a)-n) (to_bl x)
    else to_bl x)"
   apply (auto simp add: to_bl_eq_rev take_map drop_map take_rev drop_rev bit_simps)
   apply (rule nth_equalityI)
    apply (auto simp add: bit_simps rev_nth nth_append Suc_diff_Suc)
   done
 
 lemma is_aligned_replicateD:
   "\<lbrakk> is_aligned (w::'a::len word) n; n \<le> LENGTH('a) \<rbrakk>
      \<Longrightarrow> \<exists>xs. to_bl w = xs @ replicate n False
                \<and> length xs = size w - n"
   apply (subst is_aligned_replicate, assumption+)
   apply (rule exI, rule conjI, rule refl)
   apply (simp add: word_size)
   done
 
 text \<open>right-padding a word to a certain length\<close>
 
 definition
   "bl_pad_to bl sz \<equiv> bl @ (replicate (sz - length bl) False)"
 
 lemma bl_pad_to_length:
   assumes lbl: "length bl \<le> sz"
   shows   "length (bl_pad_to bl sz) = sz"
   using lbl by (simp add: bl_pad_to_def)
 
 lemma bl_pad_to_prefix:
   "prefix bl (bl_pad_to bl sz)"
   by (simp add: bl_pad_to_def)
 
 
 lemma of_bl_length:
   "length xs < LENGTH('a) \<Longrightarrow> of_bl xs < (2 :: 'a::len word) ^ length xs"
   by (simp add: of_bl_length_less)
 
 lemma of_bl_mult_and_not_mask_eq:
   "\<lbrakk>is_aligned (a :: 'a::len word) n; length b + m \<le> n\<rbrakk>
    \<Longrightarrow> a + of_bl b * (2^m) AND NOT(mask n) = a"
   apply (simp flip: push_bit_eq_mult subtract_mask(1) take_bit_eq_mask)
   apply (subst disjunctive_add)
    apply (auto simp add: bit_simps not_le not_less)
    apply (meson is_aligned_imp_not_bit is_aligned_weaken less_diff_conv2)
   apply (erule is_alignedE')
   apply (simp add: take_bit_push_bit)
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_simps)
   done
 
 lemma bin_to_bl_of_bl_eq:
   "\<lbrakk>is_aligned (a::'a::len word) n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk>
   \<Longrightarrow> bin_to_bl (length b) (uint (drop_bit c (a + of_bl b * 2^c))) = b"
   apply (simp flip: push_bit_eq_mult take_bit_eq_mask)
   apply (subst disjunctive_add)
    apply (auto simp add: bit_simps not_le not_less unsigned_or_eq unsigned_drop_bit_eq
      unsigned_push_bit_eq bin_to_bl_or simp flip: bin_to_bl_def)
    apply (meson is_aligned_imp_not_bit is_aligned_weaken less_diff_conv2)
   apply (erule is_alignedE')
   apply (rule nth_equalityI)
    apply (auto simp add: nth_bin_to_bl bit_simps rev_nth simp flip: bin_to_bl_def)
   done
 
 (* FIXME: move to Word distribution *)
 lemma bin_nth_minus_Bit0[simp]:
   "0 < n \<Longrightarrow> bit (numeral (num.Bit0 w) :: int) n = bit (numeral w :: int) (n - 1)"
   by (cases n; simp)
 
 lemma bin_nth_minus_Bit1[simp]:
   "0 < n \<Longrightarrow> bit (numeral (num.Bit1 w) :: int) n = bit (numeral w :: int) (n - 1)"
   by (cases n; simp)
 
 (* casting a long word to a shorter word and casting back to the long word
    is equal to the original long word -- if the word is small enough.
   'l is the longer word.
   's is the shorter word.
 *)
 lemma bl_cast_long_short_long_ingoreLeadingZero_generic:
   "\<lbrakk> length (dropWhile Not (to_bl w)) \<le> LENGTH('s); LENGTH('s) \<le> LENGTH('l) \<rbrakk> \<Longrightarrow>
    (of_bl :: _ \<Rightarrow> 'l::len word) (to_bl ((of_bl::_ \<Rightarrow> 's::len word) (to_bl w))) = w"
   by (rule word_uint_eqI) (simp add: uint_of_bl_is_bl_to_bin uint_of_bl_is_bl_to_bin_drop)
 
 (*
  Casting between longer and shorter word.
   'l is the longer word.
   's is the shorter word.
  For example: 'l::len word is 128 word (full ipv6 address)
               's::len word is 16 word (address piece of ipv6 address in colon-text-representation)
 *)
 corollary ucast_short_ucast_long_ingoreLeadingZero:
   "\<lbrakk> length (dropWhile Not (to_bl w)) \<le> LENGTH('s); LENGTH('s) \<le> LENGTH('l) \<rbrakk> \<Longrightarrow>
    (ucast:: 's::len word \<Rightarrow> 'l::len word) ((ucast:: 'l::len word \<Rightarrow> 's::len word) w) = w"
   apply (subst ucast_bl)+
   apply (rule bl_cast_long_short_long_ingoreLeadingZero_generic; simp)
   done
 
 lemma length_drop_mask:
   fixes w::"'a::len word"
   shows "length (dropWhile Not (to_bl (w AND mask n))) \<le> n"
 proof -
   have "length (takeWhile Not (replicate n False @ ls)) = n + length (takeWhile Not ls)"
     for ls n by(subst takeWhile_append2) simp+
   then show ?thesis
     unfolding bl_and_mask by (simp add: dropWhile_eq_drop)
 qed
 
 lemma map_bits_rev_to_bl:
   "map (bit x) [0..<size x] = rev (to_bl x)"
   by (auto simp: list_eq_iff_nth_eq test_bit_bl word_size)
 
 lemma of_bl_length2:
   "length xs + c < LENGTH('a) \<Longrightarrow> of_bl xs * 2^c < (2::'a::len word) ^ (length xs + c)"
   by (simp add: of_bl_length word_less_power_trans2)
 
 lemma of_bl_max:
   "(of_bl xs :: 'a::len word) \<le> mask (length xs)"
 proof -
   define ys where \<open>ys = rev xs\<close>
   have \<open>take_bit (length ys) (horner_sum of_bool 2 ys :: 'a word) = horner_sum of_bool 2 ys\<close>
     by transfer (simp add: take_bit_horner_sum_bit_eq min_def)
   then have \<open>(of_bl (rev ys) :: 'a word) \<le> mask (length ys)\<close>
     by (simp only: of_bl_rev_eq less_eq_mask_iff_take_bit_eq_self)
   with ys_def show ?thesis
     by simp
 qed
 
 text\<open>Some auxiliaries for sign-shifting by the entire word length or more\<close>
 
 lemma sshiftr_clamp_pos:
   assumes
     "LENGTH('a) \<le> n"
     "0 \<le> sint x"
   shows "signed_drop_bit n (x::'a::len word) = 0"
   apply (rule word_sint.Rep_eqD)
   apply (simp add: sint_signed_drop_bit_eq)
   using assms
   by (metis Word.sint_0 bit_last_iff not_less signed_drop_bit_beyond sint_signed_drop_bit_eq) 
 
 lemma sshiftr_clamp_neg:
   assumes
     "LENGTH('a) \<le> n"
     "sint x < 0"
   shows "signed_drop_bit n (x::'a::len word) = -1"
   apply (rule word_sint.Rep_eqD)
   apply (simp add: sint_signed_drop_bit_eq)
   using assms
   by (metis bit_last_iff signed_drop_bit_beyond sint_n1 sint_signed_drop_bit_eq) 
 
 lemma sshiftr_clamp:
   assumes "LENGTH('a) \<le> n"
   shows "signed_drop_bit n (x::'a::len word) = signed_drop_bit LENGTH('a) x"
   apply (cases "0 \<le> sint x")
   subgoal
     apply (subst sshiftr_clamp_pos[OF assms])
     defer apply (subst sshiftr_clamp_pos)
     by auto
   apply (subst sshiftr_clamp_neg[OF assms])
   defer apply (subst sshiftr_clamp_neg)
   by auto
 
 text\<open>
 Like @{thm shiftr1_bl_of}, but the precondition is stronger because we need to pick the msb out of
 the list.
 \<close>
 lemma sshiftr1_bl_of:
   "length bl = LENGTH('a) \<Longrightarrow>
     sshiftr1 (of_bl bl::'a::len word) = of_bl (hd bl # butlast bl)"
   apply (rule word_bl.Rep_eqD)
   apply (subst bl_sshiftr1[of "of_bl bl :: 'a word"])
   by (simp add: word_bl.Abs_inverse)
 
 text\<open>
 Like @{thm sshiftr1_bl_of}, with a weaker precondition.
 We still get a direct equation for @{term \<open>sshiftr1 (of_bl bl)\<close>}, it's just uglier.
 \<close>
 lemma sshiftr1_bl_of':
   "LENGTH('a) \<le> length bl \<Longrightarrow>
     sshiftr1 (of_bl bl::'a::len word) =
     of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))"
   apply (subst of_bl_drop'[symmetric, of "length bl - LENGTH('a)"])
   using sshiftr1_bl_of[of "drop (length bl - LENGTH('a)) bl"]
   by auto
 
 text\<open>
 Like @{thm shiftr_bl_of}.
 \<close>
 lemma sshiftr_bl_of:
   assumes "length bl = LENGTH('a)"
   shows "signed_drop_bit n (of_bl bl::'a::len word) = of_bl (replicate n (hd bl) @ take (length bl - n) bl)"
 proof -
   from assms obtain b bs where \<open>bl = b # bs\<close>
     by (cases bl) simp_all
   then have *: \<open>bl ! 0 \<longleftrightarrow> b\<close> \<open>hd bl \<longleftrightarrow> b\<close>
     by simp_all
   show ?thesis
   apply (rule bit_word_eqI)
     using assms * by (auto simp add: bit_simps nth_append rev_nth not_less)
 qed
 
 text\<open>Like @{thm shiftr_bl}\<close>
 lemma sshiftr_bl: "signed_drop_bit n x \<equiv> of_bl (replicate n (msb x) @ take (LENGTH('a) - n) (to_bl x))"
   for x :: "'a::len word"
   unfolding word_msb_alt
   by (smt (z3) length_to_bl_eq sshiftr_bl_of word_bl.Rep_inverse)
 
 end
 
 end
diff --git a/thys/Word_Lib/Singleton_Bit_Shifts.thy b/thys/Word_Lib/Singleton_Bit_Shifts.thy
new file mode 100644
--- /dev/null
+++ b/thys/Word_Lib/Singleton_Bit_Shifts.thy
@@ -0,0 +1,138 @@
+theory Singleton_Bit_Shifts
+  imports "HOL-Library.Word"
+begin
+
+definition shiftl1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
+  where \<open>shiftl1 = push_bit 1\<close>
+
+lemma bit_shiftl1_iff [bit_simps]:
+  \<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close>
+  for w :: \<open>'a::len word\<close>
+  by (simp only: shiftl1_def bit_push_bit_iff) auto
+
+definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
+  where \<open>shiftr1 = drop_bit 1\<close>
+
+lemma bit_shiftr1_iff [bit_simps]:
+  \<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close>
+  for w :: \<open>'a::len word\<close>
+  by (simp add: shiftr1_def bit_drop_bit_eq)
+
+definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
+  where \<open>sshiftr1 \<equiv> signed_drop_bit 1\<close>
+
+lemma bit_sshiftr1_iff [bit_simps]:
+  \<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
+  for w :: \<open>'a::len word\<close>
+  by (auto simp add: sshiftr1_def bit_signed_drop_bit_iff)
+
+lemma shiftr1_1: "shiftr1 (1::'a::len word) = 0"
+  by (simp add: shiftr1_def)
+
+lemma sshiftr1_eq:
+  \<open>sshiftr1 w = word_of_int (sint w div 2)\<close>
+  by (rule bit_word_eqI) (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE)
+
+lemma shiftl1_eq:
+  \<open>shiftl1 w = word_of_int (2 * uint w)\<close>
+  by (rule bit_word_eqI) (auto simp add: bit_simps)
+
+lemma shiftr1_eq:
+  \<open>shiftr1 w = word_of_int (uint w div 2)\<close>
+  by (rule bit_word_eqI) (simp add: bit_simps flip: bit_Suc)
+
+lemma shiftl1_rev:
+  "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
+  by (rule bit_word_eqI) (auto simp add: bit_simps Suc_diff_Suc simp flip: bit_Suc)
+
+lemma shiftl1_p:
+  "shiftl1 w = w + w"
+  for w :: "'a::len word"
+  by (simp add: shiftl1_def)
+
+lemma shiftr1_bintr:
+  "(shiftr1 (numeral w) :: 'a::len word) =
+    word_of_int (take_bit LENGTH('a) (numeral w) div 2)"
+  by (rule bit_word_eqI) (simp add: bit_simps bit_numeral_iff [where ?'a = int] flip: bit_Suc)
+
+lemma sshiftr1_sbintr:
+  "(sshiftr1 (numeral w) :: 'a::len word) =
+    word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2)"
+  apply (cases \<open>LENGTH('a)\<close>)
+  apply simp_all
+  apply (rule bit_word_eqI)
+  apply (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE)
+  done
+
+lemma shiftl1_wi:
+  "shiftl1 (word_of_int w) = word_of_int (2 * w)"
+  by (rule bit_word_eqI) (auto simp add: bit_simps)
+
+lemma shiftl1_numeral:
+  "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
+  unfolding word_numeral_alt shiftl1_wi by simp
+
+lemma shiftl1_neg_numeral:
+  "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
+  unfolding word_neg_numeral_alt shiftl1_wi by simp
+
+lemma shiftl1_0:
+  "shiftl1 0 = 0"
+  by (simp add: shiftl1_def)
+
+lemma shiftl1_def_u:
+  "shiftl1 w = word_of_int (2 * uint w)"
+  by (fact shiftl1_eq)
+
+lemma shiftl1_def_s:
+  "shiftl1 w = word_of_int (2 * sint w)"
+  by (simp add: shiftl1_def)
+
+lemma shiftr1_0:
+  "shiftr1 0 = 0"
+  by (simp add: shiftr1_def)
+
+lemma sshiftr1_0:
+  "sshiftr1 0 = 0"
+  by (simp add: sshiftr1_def)
+
+lemma sshiftr1_n1:
+  "sshiftr1 (- 1) = - 1"
+  by (simp add: sshiftr1_def)
+
+lemma uint_shiftr1:
+  "uint (shiftr1 w) = uint w div 2"
+  by (rule bit_eqI) (simp add: bit_simps flip: bit_Suc)
+
+lemma shiftr1_div_2:
+  "uint (shiftr1 w) = uint w div 2"
+  by (fact uint_shiftr1)
+
+lemma sshiftr1_div_2:
+  "sint (sshiftr1 w) = sint w div 2"
+  by (rule bit_eqI) (auto simp add: bit_simps ac_simps min_def simp flip: bit_Suc elim: le_SucE)
+
+lemma nth_shiftl1:
+  "bit (shiftl1 w) n \<longleftrightarrow> n < size w \<and> n > 0 \<and> bit w (n - 1)"
+  by (auto simp add: word_size bit_simps)
+
+lemma nth_shiftr1:
+  "bit (shiftr1 w) n = bit w (Suc n)"
+  by (fact bit_shiftr1_iff)
+
+lemma nth_sshiftr1: "bit (sshiftr1 w) n = (if n = size w - 1 then bit w n else bit w (Suc n))"
+  by (auto simp add: word_size bit_simps)
+
+lemma shiftl_power:
+  "(shiftl1 ^^ x) (y::'a::len word) = 2 ^ x * y"
+  by (induction x) (simp_all add: shiftl1_def)
+
+lemma le_shiftr1:
+  \<open>shiftr1 u \<le> shiftr1 v\<close> if \<open>u \<le> v\<close>
+  using that by (simp add: word_le_nat_alt unat_div div_le_mono shiftr1_def drop_bit_Suc)
+
+lemma le_shiftr1':
+  "\<lbrakk> shiftr1 u \<le> shiftr1 v ; shiftr1 u \<noteq> shiftr1 v \<rbrakk> \<Longrightarrow> u \<le> v"
+  by (meson dual_order.antisym le_cases le_shiftr1)
+
+end
\ No newline at end of file
diff --git a/thys/Word_Lib/Word_Lib_Sumo.thy b/thys/Word_Lib/Word_Lib_Sumo.thy
--- a/thys/Word_Lib/Word_Lib_Sumo.thy
+++ b/thys/Word_Lib/Word_Lib_Sumo.thy
@@ -1,135 +1,136 @@
 (*
  * Copyright Florian Haftmann
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section \<open>Ancient comprehensive Word Library\<close>
 
 theory Word_Lib_Sumo
 imports
   "HOL-Library.Word"
   Aligned
   Bit_Comprehension
   Bit_Shifts_Infix_Syntax
   Bits_Int
   Bitwise_Signed
   Bitwise
   Enumeration_Word
   Generic_set_bit
   Hex_Words
   Least_significant_bit
   More_Arithmetic
   More_Divides
   More_Sublist
   Even_More_List
   More_Misc
   Strict_part_mono
   Legacy_Aliases
   Most_significant_bit
   Next_and_Prev
   Norm_Words
   Reversed_Bit_Lists
   Rsplit
   Signed_Words
   Syntax_Bundles
   Typedef_Morphisms
   Type_Syntax
   Word_EqI
   Word_Lemmas
   Word_8
   Word_16
   Word_32
   Word_Syntax
   Signed_Division_Word
+  Singleton_Bit_Shifts
   More_Word_Operations
   Many_More
 begin
 
 unbundle bit_operations_syntax
 unbundle bit_projection_infix_syntax
 
 declare word_induct2[induct type]
 declare word_nat_cases[cases type]
 
 declare signed_take_bit_Suc [simp]
 
 (* these generate take_bit terms, which we often don't want for concrete lengths *)
 lemmas of_int_and_nat = unsigned_of_nat unsigned_of_int signed_of_int signed_of_nat
 
 bundle no_take_bit
 begin
 declare of_int_and_nat[simp del]
 end
 
 lemmas bshiftr1_def = bshiftr1_eq
 lemmas is_down_def = is_down_eq
 lemmas is_up_def = is_up_eq
 lemmas mask_def = mask_eq
 lemmas scast_def = scast_eq
 lemmas shiftl1_def = shiftl1_eq
 lemmas shiftr1_def = shiftr1_eq
 lemmas sshiftr1_def = sshiftr1_eq
 lemmas sshiftr_def = sshiftr_eq_funpow_sshiftr1
 lemmas to_bl_def = to_bl_eq
 lemmas ucast_def = ucast_eq
 lemmas unat_def = unat_eq_nat_uint
 lemmas word_cat_def = word_cat_eq
 lemmas word_reverse_def = word_reverse_eq_of_bl_rev_to_bl
 lemmas word_roti_def = word_roti_eq_word_rotr_word_rotl
 lemmas word_rotl_def = word_rotl_eq
 lemmas word_rotr_def = word_rotr_eq
 lemmas word_sle_def = word_sle_eq
 lemmas word_sless_def = word_sless_eq
 
 lemmas uint_0 = uint_nonnegative
 lemmas uint_lt = uint_bounded
 lemmas uint_mod_same = uint_idem
 lemmas of_nth_def = word_set_bits_def
 
 lemmas of_nat_word_eq_iff = word_of_nat_eq_iff
 lemmas of_nat_word_eq_0_iff = word_of_nat_eq_0_iff
 lemmas of_int_word_eq_iff = word_of_int_eq_iff
 lemmas of_int_word_eq_0_iff = word_of_int_eq_0_iff
 
 lemmas word_next_def = word_next_unfold
 
 lemmas word_prev_def = word_prev_unfold
 
 lemmas is_aligned_def = is_aligned_iff_dvd_nat
 
 lemmas word_and_max_simps =
   word8_and_max_simp
   word16_and_max_simp
   word32_and_max_simp
 
 lemma distinct_lemma: "f x \<noteq> f y \<Longrightarrow> x \<noteq> y" by auto
 
 lemmas and_bang = word_and_nth
 
 lemmas sdiv_int_def = signed_divide_int_def
 lemmas smod_int_def = signed_modulo_int_def
 
 (* shortcut for some specific lengths *)
 lemma word_fixed_sint_1[simp]:
   "sint (1::8 word) = 1"
   "sint (1::16 word) = 1"
   "sint (1::32 word) = 1"
   "sint (1::64 word) = 1"
   by (auto simp: sint_word_ariths)
 
 declare of_nat_diff [simp]
 
 (* Haskellish names/syntax *)
 notation (input)
   bit ("testBit")
 
 lemmas cast_simps = cast_simps ucast_down_bl
 
 (* shadows the slightly weaker Word.nth_ucast *)
 lemma nth_ucast:
   "(ucast (w::'a::len word)::'b::len word) !! n =
    (w !! n \<and> n < min LENGTH('a) LENGTH('b))"
   by (auto simp add: bit_simps not_le dest: bit_imp_le_length)
 
 end