diff --git a/thys/Native_Word/Word_Type_Copies.thy b/thys/Native_Word/Word_Type_Copies.thy
--- a/thys/Native_Word/Word_Type_Copies.thy
+++ b/thys/Native_Word/Word_Type_Copies.thy
@@ -1,332 +1,332 @@
 (*  Title:      Word_Type_Copies.thy
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 chapter \<open>Systematic approach towards type copies of word type\<close>
 
 theory Word_Type_Copies
   imports
     "HOL-Library.Word"
     "Word_Lib.Most_significant_bit"
     "Word_Lib.Least_significant_bit"
     "Word_Lib.Generic_set_bit"
     "Word_Lib.Bit_Comprehension"
     "Code_Target_Word_Base"
 begin
 
 text \<open>The lifting machinery is not localized, hence the abstract proofs are carried out using morphisms.\<close>
 
 locale word_type_copy =
   fixes of_word :: \<open>'b::len word \<Rightarrow> 'a\<close>
     and word_of :: \<open>'a \<Rightarrow> 'b word\<close>
   assumes type_definition: \<open>type_definition word_of of_word UNIV\<close>
 begin
 
 lemma word_of_word:
   \<open>word_of (of_word w) = w\<close>
   using type_definition by (simp add: type_definition_def)
 
 lemma of_word_of [code abstype]:
   \<open>of_word (word_of p) = p\<close>
     \<comment> \<open>Use an abstract type for code generation to disable pattern matching on \<^term>\<open>of_word\<close>.\<close>
   using type_definition by (simp add: type_definition_def)
 
 lemma word_of_eqI:
   \<open>p = q\<close> if \<open>word_of p = word_of q\<close>
 proof -
   from that have \<open>of_word (word_of p) = of_word (word_of q)\<close>
     by simp
   then show ?thesis
     by (simp add: of_word_of)
 qed
 
 lemma eq_iff_word_of:
   \<open>p = q \<longleftrightarrow> word_of p = word_of q\<close>
   by (auto intro: word_of_eqI)
 
 end
 
 bundle constraintless
 begin
 
 declaration \<open>
   let
     val cs = map (rpair NONE o fst o dest_Const)
       [\<^term>\<open>0\<close>, \<^term>\<open>(+)\<close>, \<^term>\<open>uminus\<close>, \<^term>\<open>(-)\<close>,
        \<^term>\<open>1\<close>, \<^term>\<open>(*)\<close>, \<^term>\<open>(div)\<close>, \<^term>\<open>(mod)\<close>,
        \<^term>\<open>HOL.equal\<close>, \<^term>\<open>(\<le>)\<close>, \<^term>\<open>(<)\<close>,
        \<^term>\<open>(dvd)\<close>, \<^term>\<open>of_bool\<close>, \<^term>\<open>numeral\<close>, \<^term>\<open>of_nat\<close>,
        \<^term>\<open>bit\<close>,
        \<^term>\<open>Bit_Operations.not\<close>, \<^term>\<open>Bit_Operations.and\<close>, \<^term>\<open>Bit_Operations.or\<close>, \<^term>\<open>Bit_Operations.xor\<close>, \<^term>\<open>mask\<close>,
        \<^term>\<open>push_bit\<close>, \<^term>\<open>drop_bit\<close>, \<^term>\<open>take_bit\<close>,
        \<^term>\<open>Bit_Operations.set_bit\<close>, \<^term>\<open>unset_bit\<close>, \<^term>\<open>flip_bit\<close>,
        \<^term>\<open>msb\<close>, \<^term>\<open>lsb\<close>, \<^term>\<open>size\<close>, \<^term>\<open>Generic_set_bit.set_bit\<close>, \<^term>\<open>set_bits\<close>]
   in
     K (Context.mapping I (fold Proof_Context.add_const_constraint cs))
   end
 \<close>
 
 end
 
 locale word_type_copy_ring = word_type_copy
   opening constraintless +
   constrains word_of :: \<open>'a \<Rightarrow> 'b::len word\<close>
   assumes word_of_0 [code]: \<open>word_of 0 = 0\<close>
     and word_of_1 [code]: \<open>word_of 1 = 1\<close>
     and word_of_add [code]: \<open>word_of (p + q) = word_of p + word_of q\<close>
     and word_of_minus [code]: \<open>word_of (- p) = - (word_of p)\<close>
     and word_of_diff [code]: \<open>word_of (p - q) = word_of p - word_of q\<close>
     and word_of_mult [code]: \<open>word_of (p * q) = word_of p * word_of q\<close>
     and word_of_div [code]: \<open>word_of (p div q) = word_of p div word_of q\<close>
     and word_of_mod [code]: \<open>word_of (p mod q) = word_of p mod word_of q\<close>
     and equal_iff_word_of [code]: \<open>HOL.equal p q \<longleftrightarrow> HOL.equal (word_of p) (word_of q)\<close>
     and less_eq_iff_word_of [code]: \<open>p \<le> q \<longleftrightarrow> word_of p \<le> word_of q\<close>
     and less_iff_word_of [code]: \<open>p < q \<longleftrightarrow> word_of p < word_of q\<close>
 begin
 
 lemma of_class_comm_ring_1:
   \<open>OFCLASS('a, comm_ring_1_class)\<close>
   by standard (simp_all add: eq_iff_word_of word_of_0 word_of_1
     word_of_add word_of_minus word_of_diff word_of_mult algebra_simps)
 
 lemma of_class_semiring_modulo:
   \<open>OFCLASS('a, semiring_modulo_class)\<close>
   by standard (simp_all add: eq_iff_word_of word_of_0 word_of_1
     word_of_add word_of_minus word_of_diff word_of_mult word_of_mod word_of_div algebra_simps
     mod_mult_div_eq)
 
 lemma of_class_equal:
   \<open>OFCLASS('a, equal_class)\<close>
   by standard (simp add: eq_iff_word_of equal_iff_word_of equal)
 
 lemma of_class_linorder:
   \<open>OFCLASS('a, linorder_class)\<close>
   by standard (auto simp add: eq_iff_word_of less_eq_iff_word_of less_iff_word_of)
 
 end
 
 locale word_type_copy_bits = word_type_copy_ring
   opening constraintless bit_operations_syntax +
   constrains word_of :: \<open>'a::{comm_ring_1, semiring_modulo, equal, linorder} \<Rightarrow> 'b::len word\<close>
   fixes signed_drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   assumes bit_eq_word_of [code]: \<open>bit p = bit (word_of p)\<close>
     and word_of_not [code]: \<open>word_of (NOT p) = NOT (word_of p)\<close>
     and word_of_and [code]: \<open>word_of (p AND q) = word_of p AND word_of q\<close>
     and word_of_or [code]: \<open>word_of (p OR q) = word_of p OR word_of q\<close>
     and word_of_xor [code]: \<open>word_of (p XOR q) = word_of p XOR word_of q\<close>
     and word_of_mask [code]: \<open>word_of (mask n) = mask n\<close>
     and word_of_push_bit [code]: \<open>word_of (push_bit n p) = push_bit n (word_of p)\<close>
     and word_of_drop_bit [code]: \<open>word_of (drop_bit n p) = drop_bit n (word_of p)\<close>
     and word_of_signed_drop_bit [code]: \<open>word_of (signed_drop_bit n p) = Word.signed_drop_bit n (word_of p)\<close>
     and word_of_take_bit [code]: \<open>word_of (take_bit n p) = take_bit n (word_of p)\<close>
     and word_of_set_bit [code]: \<open>word_of (Bit_Operations.set_bit n p) = Bit_Operations.set_bit n (word_of p)\<close>
     and word_of_unset_bit [code]: \<open>word_of (unset_bit n p) = unset_bit n (word_of p)\<close>
     and word_of_flip_bit [code]: \<open>word_of (flip_bit n p) = flip_bit n (word_of p)\<close>
 begin
 
 lemma word_of_bool:
   \<open>word_of (of_bool n) = of_bool n\<close>
   by (simp add: word_of_0 word_of_1)
 
 lemma word_of_nat:
   \<open>word_of (of_nat n) = of_nat n\<close>
   by (induction n) (simp_all add: word_of_0 word_of_1 word_of_add)
 
 lemma word_of_numeral [simp]:
   \<open>word_of (numeral n) = numeral n\<close>
 proof -
   have \<open>word_of (of_nat (numeral n)) = of_nat (numeral n)\<close>
     by (simp only: word_of_nat)
   then show ?thesis by simp
 qed
 
 lemma word_of_power:
   \<open>word_of (p ^ n) = word_of p ^ n\<close>
   by (induction n) (simp_all add: word_of_1 word_of_mult)
 
 lemma even_iff_word_of:
   \<open>2 dvd p \<longleftrightarrow> 2 dvd word_of p\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
 proof
   assume ?P
   then obtain q where \<open>p = 2 * q\<close> ..
   then show ?Q by (simp add: word_of_mult)
 next
   assume ?Q
   then obtain w where \<open>word_of p = 2 * w\<close> ..
   then have \<open>of_word (word_of p) = of_word (2 * w)\<close>
     by simp
   then have \<open>p = 2 * of_word w\<close>
     by (simp add: eq_iff_word_of word_of_word word_of_mult)
   then show ?P
     by simp
 qed
 
 lemma of_class_ring_bit_operations:
   \<open>OFCLASS('a, ring_bit_operations_class)\<close>
 proof -
   have induct: \<open>P p\<close> if stable: \<open>(\<And>p. p div 2 = p \<Longrightarrow> P p)\<close>
       and rec: \<open>(\<And>p b. P p \<Longrightarrow> (of_bool b + 2 * p) div 2 = p \<Longrightarrow> P (of_bool b + 2 * p))\<close>
     for p :: 'a and P
   proof -
     from stable have stable': \<open>(\<And>p. word_of p div 2 = word_of p \<Longrightarrow> P p)\<close>
       by (simp add: eq_iff_word_of word_of_div)
     from rec have rec': \<open>(\<And>p b. P p \<Longrightarrow> (of_bool b + 2 * word_of p) div 2 = word_of p \<Longrightarrow> P (of_bool b + 2 * p))\<close>
       by (simp add: eq_iff_word_of word_of_add word_of_bool word_of_mult word_of_div)
     define w where \<open>w = word_of p\<close>
     then have \<open>p = of_word w\<close>
       by (simp add: of_word_of)
     also have \<open>P (of_word w)\<close>
-    proof (induction w rule: bits_induct)
+    proof (induction w rule: bit_induct)
       case (stable w)
       show ?case
         by (rule stable') (simp add: word_of_word stable)
     next
       case (rec w b)
       have \<open>P (of_bool b + 2 * of_word w)\<close>
         by (rule rec') (simp_all add: word_of_word rec)
       also have \<open>of_bool b + 2 * of_word w = of_word (of_bool b + 2 * w)\<close>
         by (simp add: eq_iff_word_of word_of_word word_of_add word_of_1 word_of_mult word_of_0)
       finally show ?case .
     qed
     finally show \<open>P p\<close> .
   qed
   have \<open>class.semiring_parity_axioms (+) (0::'a) (*) 1 (mod)\<close>
     by standard (simp_all add: eq_iff_word_of word_of_0 word_of_1 even_iff_word_of word_of_mod even_iff_mod_2_eq_zero)
   with of_class_semiring_modulo have \<open>OFCLASS('a, semiring_parity_class)\<close>
     by (rule semiring_parity_class.intro) 
   moreover have \<open>class.semiring_bits_axioms (+) (-) (0::'a) (*) 1 (div) (mod) bit\<close>
     apply (standard, fact induct)
     apply (simp_all only: eq_iff_word_of word_of_0 word_of_1 word_of_bool word_of_numeral
       word_of_add word_of_diff word_of_mult word_of_div word_of_mod word_of_power even_iff_word_of
       bit_eq_word_of push_bit_take_bit drop_bit_take_bit
       even_drop_bit_iff_not_bit
       flip: push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod mask_eq_exp_minus_1)
                apply (auto simp add: ac_simps bit_simps drop_bit_exp_eq)
     done
   ultimately have \<open>OFCLASS('a, semiring_bits_class)\<close>
     by (rule semiring_bits_class.intro)
   moreover have \<open>class.semiring_bit_operations_axioms (+) (-) (0::'a) (*) (1::'a) (div) (mod) (AND) (OR) (XOR) mask Bit_Operations.set_bit unset_bit flip_bit push_bit drop_bit take_bit\<close>
     apply standard
     apply (simp_all add: eq_iff_word_of word_of_add word_of_push_bit word_of_power
       bit_eq_word_of word_of_and word_of_or word_of_xor word_of_mask word_of_diff
       word_of_0 word_of_1 bit_simps
       word_of_set_bit set_bit_eq_or word_of_unset_bit unset_bit_Suc word_of_flip_bit flip_bit_eq_xor
       word_of_mult
       word_of_drop_bit word_of_div word_of_take_bit word_of_mod
       and_rec [of \<open>word_of a\<close> \<open>word_of b\<close> for a b]
       or_rec [of \<open>word_of a\<close> \<open>word_of b\<close> for a b]
       xor_rec [of \<open>word_of a\<close> \<open>word_of b\<close> for a b] even_iff_word_of
       flip: mask_eq_exp_minus_1 push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)
     done
   ultimately have \<open>OFCLASS('a, semiring_bit_operations_class)\<close>
     by (rule semiring_bit_operations_class.intro)
   moreover have \<open>OFCLASS('a, ring_parity_class)\<close>
     using \<open>OFCLASS('a, semiring_parity_class)\<close> by (rule ring_parity_class.intro) standard
   moreover have \<open>class.ring_bit_operations_axioms (-) (1::'a) uminus NOT\<close>
     by standard
       (simp add: eq_iff_word_of word_of_not word_of_diff word_of_minus word_of_1 not_eq_complement)
   ultimately show \<open>OFCLASS('a, ring_bit_operations_class)\<close>
     by (rule ring_bit_operations_class.intro)
 qed
 
 lemma [code]:
   \<open>take_bit n a = a AND mask n\<close> for a :: 'a
   by (simp add: eq_iff_word_of word_of_take_bit word_of_and word_of_mask take_bit_eq_mask)
 
 lemma [code]:
   \<open>mask (Suc n) = push_bit n (1 :: 'a) OR mask n\<close>
   \<open>mask 0 = (0 :: 'a)\<close>
   by (simp_all add: eq_iff_word_of word_of_mask word_of_or word_of_push_bit word_of_0 word_of_1 mask_Suc_exp)
 
 lemma [code]:
   \<open>Bit_Operations.set_bit n w = w OR push_bit n 1\<close> for w :: 'a
   by (simp add: eq_iff_word_of word_of_set_bit word_of_or word_of_push_bit word_of_1 set_bit_eq_or)
 
 lemma [code]:
   \<open>unset_bit n w = w AND NOT (push_bit n 1)\<close> for w :: 'a
   by (simp add: eq_iff_word_of word_of_unset_bit word_of_and word_of_not word_of_push_bit word_of_1 unset_bit_eq_and_not)
 
 lemma [code]:
   \<open>flip_bit n w = w XOR push_bit n 1\<close> for w :: 'a
   by (simp add: eq_iff_word_of word_of_flip_bit word_of_xor word_of_push_bit word_of_1 flip_bit_eq_xor)
 
 end
 
 locale word_type_copy_more = word_type_copy_bits +
   constrains word_of :: \<open>'a::{ring_bit_operations, equal, linorder} \<Rightarrow> 'b::len word\<close>
   fixes of_nat :: \<open>nat \<Rightarrow> 'a\<close> and nat_of :: \<open>'a \<Rightarrow> nat\<close>
     and of_int :: \<open>int \<Rightarrow> 'a\<close> and int_of :: \<open>'a \<Rightarrow> int\<close>
     and of_integer :: \<open>integer \<Rightarrow> 'a\<close> and integer_of :: \<open>'a \<Rightarrow> integer\<close>
   assumes word_of_nat_eq: \<open>word_of (of_nat n) = word_of_nat n\<close>
     and nat_of_eq_word_of: \<open>nat_of p = unat (word_of p)\<close>
     and word_of_int_eq: \<open>word_of (of_int k) = word_of_int k\<close>
     and int_of_eq_word_of: \<open>int_of p = uint (word_of p)\<close>
     and word_of_integer_eq: \<open>word_of (of_integer l) = word_of_integer l\<close>
     and integer_of_eq_word_of: \<open>integer_of p = unsigned (word_of p)\<close>
 begin
 
 lemma of_word_numeral [code_post]:
   \<open>of_word (numeral n) = numeral n\<close>
   by (simp add: eq_iff_word_of word_of_word)
 
 lemma of_word_0 [code_post]:
   \<open>of_word 0 = 0\<close>
   by (simp add: eq_iff_word_of word_of_0 word_of_word)
 
 lemma of_word_1 [code_post]:
   \<open>of_word 1 = 1\<close>
   by (simp add: eq_iff_word_of word_of_1 word_of_word)
 
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 lemma numeral_eq_integer [code_unfold]:
   \<open>numeral n = of_integer (numeral n)\<close>
   by (simp add: eq_iff_word_of word_of_integer_eq)
 
 lemma neg_numeral_eq_integer [code_unfold]:
   \<open>- numeral n = of_integer (- numeral n)\<close>
   by (simp add: eq_iff_word_of word_of_integer_eq word_of_minus)
 
 end
 
 locale word_type_copy_misc = word_type_copy_more
   opening constraintless bit_operations_syntax +
   constrains word_of :: \<open>'a::{ring_bit_operations, equal, linorder} \<Rightarrow> 'b::len word\<close>
   fixes size :: nat and set_bits_aux :: \<open>(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
     assumes size_eq_length: \<open>size = LENGTH('b::len)\<close>
     and msb_iff_word_of [code]: \<open>msb p \<longleftrightarrow> msb (word_of p)\<close>
     and lsb_iff_word_of [code]: \<open>lsb p \<longleftrightarrow> lsb (word_of p)\<close>
     and size_eq_word_of: \<open>Nat.size (p :: 'a) = Nat.size (word_of p)\<close>
     and word_of_generic_set_bit [code]: \<open>word_of (Generic_set_bit.set_bit p n b) = Generic_set_bit.set_bit (word_of p) n b\<close>
     and word_of_set_bits: \<open>word_of (set_bits P) = set_bits P\<close>
     and word_of_set_bits_aux: \<open>word_of (set_bits_aux P n p) = Bit_Comprehension.set_bits_aux P n (word_of p)\<close>
 begin
 
 lemma size_eq [code]:
   \<open>Nat.size p = size\<close> for p :: 'a
   by (simp add: size_eq_length size_eq_word_of word_size)
 
 lemma set_bits_aux_code [code]:
   \<open>set_bits_aux f n w =
   (if n = 0 then w 
    else let n' = n - 1 in set_bits_aux f n' (push_bit 1 w OR (if f n' then 1 else 0)))\<close>
   by (simp add: eq_iff_word_of word_of_set_bits_aux Let_def word_of_mult word_of_or word_of_0 word_of_1 set_bits_aux_rec [of f n])
 
 lemma set_bits_code [code]: \<open>set_bits P = set_bits_aux P size 0\<close>
   by (simp add: fun_eq_iff eq_iff_word_of word_of_set_bits word_of_set_bits_aux word_of_0 size_eq_length set_bits_conv_set_bits_aux)
 
 lemma of_class_lsb:
   \<open>OFCLASS('a, lsb_class)\<close>
   by standard (simp add: fun_eq_iff lsb_iff_word_of even_iff_word_of lsb_odd)
 
 lemma of_class_set_bit:
   \<open>OFCLASS('a, set_bit_class)\<close>
   by standard (simp add: eq_iff_word_of word_of_generic_set_bit bit_eq_word_of word_of_power word_of_0 bit_simps linorder_not_le)
 
 lemma of_class_bit_comprehension:
   \<open>OFCLASS('a, bit_comprehension_class)\<close>
   by standard (simp add: eq_iff_word_of word_of_set_bits bit_eq_word_of set_bits_bit_eq)
 
 end
 
 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,432 +1,432 @@
 (*
  * Copyright Florian Haftmann
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 (*<*)
 theory Guide
   imports Word_Lib_Sumo Machine_Word_32 Machine_Word_64
 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)  Generic_set_bit.set_bit (\<open>Generic'_set'_bit.set'_bit\<close>)
 
 hide_const (open) Generic_set_bit.set_bit
 
 no_notation bit  (infixl \<open>!!\<close> 100)
 
 (*>*)
 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> Induction rule: @{thm [display, mode=iff] bit_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_word_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, most 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>]
 
         Bit shifts decorated with infix syntax:
 
           \<^item> @{thm Bit_Shifts_Infix_Syntax.shiftl_def [no_vars]}
 
           \<^item> @{thm Bit_Shifts_Infix_Syntax.shiftr_def [no_vars]}
 
           \<^item> @{thm Bit_Shifts_Infix_Syntax.sshiftr_def [no_vars]}
 
       \<^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 will have
           to use qualified names in applications.
 
       \<^descr>[\<^theory>\<open>Word_Lib.Machine_Word_32\<close> and \<^theory>\<open>Word_Lib.Machine_Word_64\<close>]
 
           provide lemmas for 32-bit words and 64-bit words under the same name,
           which can help to organize applications relying on some form
           of genericity.
 \<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.
 
   \<^descr>[\<^theory>\<open>Word_Lib.Bit_Comprehension_Int\<close>]
 
     Comprehension syntax for bit values over predicates
     \<^typ>\<open>nat \<Rightarrow> bool\<close>, for \<^typ>\<open>int\<close>; inherently non-computational.
 
   \<^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 2022] ~
 
     \<^item> Theory \<^text>\<open>Word_Lib.Ancient_Numeral\<close> has been removed from session.
 
     \<^item> Bit comprehension syntax for \<^typ>\<open>int\<close> moved to separate theory
       \<^theory>\<open>Word_Lib.Bit_Comprehension_Int\<close>.
 
   \<^descr>[Changes since AFP 2021] ~
 
     \<^item> Theory \<^text>\<open>Word_Lib.Ancient_Numeral\<close> is not 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> 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>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
 (*>*)