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,414 +1,418 @@
 (*
  * Copyright Florian Haftmann
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 (*<*)
 theory Guide
-  imports Word_Lib_Sumo Word_64 Ancient_Numeral
+  imports Word_Lib_Sumo Machine_Word_32 Machine_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)  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> 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 require
-          to use qualified names in applications.
+          for 64-bit words.
+
+      \<^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; 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> 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
 (*>*)
diff --git a/thys/Word_Lib/Machine_Word_32.thy b/thys/Word_Lib/Machine_Word_32.thy
new file mode 100644
--- /dev/null
+++ b/thys/Word_Lib/Machine_Word_32.thy
@@ -0,0 +1,136 @@
+(*
+ * Copyright 2014, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+section "32-Bit Machine Word Setup"
+
+theory Machine_Word_32
+  imports Machine_Word_32_Basics More_Word Bit_Shifts_Infix_Syntax Rsplit
+begin
+
+context
+  includes bit_operations_syntax
+begin
+
+type_synonym machine_word = \<open>machine_word_len word\<close>
+
+lemma word_bits_len_of:
+  \<open>LENGTH(machine_word_len) = word_bits\<close>
+  by (simp add: word_bits_conv)  
+
+lemma word_bits_size:
+  "size (w :: machine_word) = word_bits"
+  by (simp add: word_bits_def word_size)
+
+lemma word_bits_word_size_conv:
+  \<open>word_bits = word_size * 8\<close>
+  by (simp add: word_bits_def word_size_def)
+
+lemma word_size_word_size_bits:
+  \<open>word_size = (2 :: 'a :: semiring_1) ^ word_size_bits\<close>
+  by (simp add: word_size_def word_size_bits_def)
+
+lemma lt_word_bits_lt_pow:
+  "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
+  by (simp add: word_bits_conv)
+
+lemma if_then_1_else_0:
+  "((if P then 1 else 0) = (0 :: machine_word)) = (\<not> P)"
+  by simp
+
+lemma if_then_0_else_1:
+  "((if P then 0 else 1) = (0 :: machine_word)) = (P)"
+  by simp
+
+lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
+
+lemma bool_mask [simp]:
+  \<open>0 < x AND 1 \<longleftrightarrow> x AND 1 = 1\<close> for x :: machine_word
+  by (rule bool_mask') auto
+
+lemma in_16_range:
+  "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: machine_word)) ` S"
+  "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: machine_word. r + x * 16) ` S"
+  by (clarsimp simp: image_def elim!: bexI[rotated])+
+
+lemma le_step_down_word_3:
+  fixes x :: machine_word
+  shows "\<lbrakk>x \<le> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1"
+  by (fact le_step_down_word_2)
+
+lemma shiftr_1:
+  "(x::machine_word) >> 1 = 0 \<Longrightarrow> x < 2"
+  apply transfer
+  apply (simp add: take_bit_drop_bit)
+  apply (simp add: drop_bit_Suc)
+  done
+
+lemma Suc_unat_mask_div:
+  "Suc (unat (mask sz div word_size :: machine_word)) = 2 ^ (min sz word_bits - word_size_bits)"
+  by (simp add: word_size_word_size_bits unat_drop_bit_eq unat_mask_eq drop_bit_mask_eq Suc_mask_eq_exp
+    flip: drop_bit_eq_div word_bits_conv)
+
+lemma ucast_not_helper:
+  fixes a::"8 word"
+  assumes a: "a \<noteq> 0xFF"
+  shows "ucast a \<noteq> (0xFF::machine_word)"
+proof
+  assume "ucast a = (0xFF::machine_word)"
+  also
+  have "(0xFF::machine_word) = ucast (0xFF::8 word)" by simp
+  finally
+  show False using a
+    apply -
+    apply (drule up_ucast_inj, simp)
+    apply simp
+    done
+qed
+
+lemma unat_less_2p_word_bits:
+  "unat (x :: machine_word) < 2 ^ word_bits"
+  apply (simp only: word_bits_def)
+  apply (rule unat_lt2p)
+  done
+
+lemma unat_less_word_bits:
+  fixes y :: machine_word
+  shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
+  unfolding word_bits_def
+  by (rule order_less_trans [OF _ unat_lt2p])
+
+lemma unat_mask_2_less_4:
+  "unat (p AND mask 2 :: machine_word) < 4"
+  by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)
+
+lemma unat_mult_simple:
+  \<open>unat (x * y) = unat x * unat y\<close>
+    if \<open>unat x * unat y < 2 ^ LENGTH(machine_word_len)\<close>
+    for x y :: machine_word
+  using that by (simp flip: unat_mult_lem)
+
+lemma upto_2_helper:
+  "{0..<2 :: machine_word} = {0, 1}"
+  by (safe; simp) unat_arith
+
+lemma word_ge_min:
+  \<open>- (2 ^ (word_bits - 1)) \<le> sint x\<close> for x :: machine_word
+  using sint_ge [of x] by (simp add: word_bits_def)
+
+lemma word_rsplit_0:
+  "word_rsplit (0 :: machine_word) = replicate (word_bits div 8) (0 :: 8 word)"
+  by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)
+
+lemma x_less_2_0_1:
+  fixes x :: machine_word
+  shows "x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
+  by (rule x_less_2_0_1') auto
+
+end
+
+end
diff --git a/thys/Word_Lib/Machine_Word_32_Basics.thy b/thys/Word_Lib/Machine_Word_32_Basics.thy
new file mode 100644
--- /dev/null
+++ b/thys/Word_Lib/Machine_Word_32_Basics.thy
@@ -0,0 +1,66 @@
+(*
+ * Copyright 2014, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+section \<open>32 bit standard platform-specific word size and alignment.\<close>
+
+theory Machine_Word_32_Basics
+imports "HOL-Library.Word" Word_32
+begin
+
+type_synonym machine_word_len = 32
+
+definition word_bits :: nat
+where
+  \<open>word_bits = LENGTH(machine_word_len)\<close>
+
+lemma word_bits_conv [code]:
+  \<open>word_bits = 32\<close>
+  by (simp add: word_bits_def)
+
+text \<open>The following two are numerals so they can be used as nats and words.\<close>
+
+definition word_size_bits :: \<open>'a :: numeral\<close>
+where
+  \<open>word_size_bits = 2\<close>
+
+definition word_size :: \<open>'a :: numeral\<close>
+where
+  \<open>word_size = 4\<close>
+
+lemma n_less_word_bits:
+  "(n < word_bits) = (n < 32)"
+  by (simp add: word_bits_def word_size_def)
+
+lemmas upper_bits_unset_is_l2p_32 = upper_bits_unset_is_l2p [where 'a=32, folded word_bits_def]
+
+lemmas le_2p_upper_bits_32 = le_2p_upper_bits [where 'a=32, folded word_bits_def]
+lemmas le2p_bits_unset_32 = le2p_bits_unset[where 'a=32, folded word_bits_def]
+
+lemmas unat_power_lower32 [simp] = unat_power_lower32'[folded word_bits_def]
+
+lemmas word32_less_sub_le[simp] = word32_less_sub_le' [folded word_bits_def]
+
+lemmas word32_power_less_1[simp] = word32_power_less_1'[folded word_bits_def]
+
+lemma of_nat32_0:
+  "\<lbrakk>of_nat n = (0::word32); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
+  by (erule of_nat_0, simp add: word_bits_def)
+
+lemmas unat_of_nat32 = unat_of_nat32'[folded word_bits_def]
+
+lemmas word_power_nonzero_32 = word_power_nonzero [where 'a=32, folded word_bits_def]
+
+lemmas div_power_helper_32 = div_power_helper [where 'a=32, folded word_bits_def]
+
+lemmas of_nat_less_pow_32 = of_nat_power [where 'a=32, folded word_bits_def]
+
+lemmas unat_mask_word32 = unat_mask_word32'[folded word_bits_def]
+
+end
diff --git a/thys/Word_Lib/Machine_Word_64.thy b/thys/Word_Lib/Machine_Word_64.thy
new file mode 100644
--- /dev/null
+++ b/thys/Word_Lib/Machine_Word_64.thy
@@ -0,0 +1,136 @@
+(*
+ * Copyright 2014, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+section "64-Bit Machine Word Setup"
+
+theory Machine_Word_64
+imports Machine_Word_64_Basics More_Word Bit_Shifts_Infix_Syntax Rsplit
+begin
+
+context
+  includes bit_operations_syntax
+begin
+
+type_synonym machine_word = \<open>machine_word_len word\<close>
+
+lemma word_bits_len_of:
+  \<open>LENGTH(machine_word_len) = word_bits\<close>
+  by (simp add: word_bits_conv)
+
+lemma word_bits_size:
+  "size (w :: machine_word) = word_bits"
+  by (simp add: word_bits_def word_size)
+
+lemma word_bits_word_size_conv:
+  \<open>word_bits = word_size * 8\<close>
+  by (simp add: word_bits_def word_size_def)
+
+lemma word_size_word_size_bits:
+  \<open>word_size = (2 :: 'a :: semiring_1) ^ word_size_bits\<close>
+  by (simp add: word_size_def word_size_bits_def)
+
+lemma lt_word_bits_lt_pow:
+  "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
+  by (simp add: word_bits_conv)
+
+lemma if_then_1_else_0:
+  "((if P then 1 else 0) = (0 :: machine_word)) = (\<not> P)"
+  by simp
+
+lemma if_then_0_else_1:
+  "((if P then 0 else 1) = (0 :: machine_word)) = (P)"
+  by simp
+
+lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
+
+lemma bool_mask [simp]:
+  \<open>0 < x AND 1 \<longleftrightarrow> x AND 1 = 1\<close> for x :: machine_word
+  by (rule bool_mask') auto
+
+lemma in_16_range:
+  "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: machine_word)) ` S"
+  "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: machine_word. r + x * 16) ` S"
+  by (clarsimp simp: image_def elim!: bexI[rotated])+
+
+lemma le_step_down_word_3:
+  fixes x :: machine_word
+  shows "\<lbrakk>x \<le> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1"
+  by (fact le_step_down_word_2)
+
+lemma shiftr_1:
+  "(x::machine_word) >> 1 = 0 \<Longrightarrow> x < 2"
+  apply transfer
+  apply (simp add: take_bit_drop_bit)
+  apply (simp add: drop_bit_Suc)
+  done
+
+lemma Suc_unat_mask_div:
+  "Suc (unat (mask sz div word_size :: machine_word)) = 2 ^ (min sz word_bits - word_size_bits)"
+  by (simp add: word_size_word_size_bits unat_drop_bit_eq unat_mask_eq drop_bit_mask_eq Suc_mask_eq_exp
+    flip: drop_bit_eq_div word_bits_conv)
+
+lemma ucast_not_helper:
+  fixes a::"8 word"
+  assumes a: "a \<noteq> 0xFF"
+  shows "ucast a \<noteq> (0xFF::machine_word)"
+proof
+  assume "ucast a = (0xFF::machine_word)"
+  also
+  have "(0xFF::machine_word) = ucast (0xFF::8 word)" by simp
+  finally
+  show False using a
+    apply -
+    apply (drule up_ucast_inj, simp)
+    apply simp
+    done
+qed
+
+lemma unat_less_2p_word_bits:
+  "unat (x :: machine_word) < 2 ^ word_bits"
+  apply (simp only: word_bits_def)
+  apply (rule unat_lt2p)
+  done
+
+lemma unat_less_word_bits:
+  fixes y :: machine_word
+  shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
+  unfolding word_bits_def
+  by (rule order_less_trans [OF _ unat_lt2p])
+
+lemma unat_mask_2_less_4:
+  "unat (p AND mask 2 :: machine_word) < 4"
+  by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)
+
+lemma unat_mult_simple:
+  \<open>unat (x * y) = unat x * unat y\<close>
+    if \<open>unat x * unat y < 2 ^ LENGTH(machine_word_len)\<close>
+    for x y :: machine_word
+  using that by (simp flip: unat_mult_lem)
+
+lemma upto_2_helper:
+  "{0..<2 :: machine_word} = {0, 1}"
+  by (safe; simp) unat_arith
+
+lemma word_ge_min:
+  \<open>- (2 ^ (word_bits - 1)) \<le> sint x\<close> for x :: machine_word
+  using sint_ge [of x] by (simp add: word_bits_def)
+
+lemma word_rsplit_0:
+  "word_rsplit (0 :: machine_word) = replicate (word_bits div 8) (0 :: 8 word)"
+  by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)
+
+lemma x_less_2_0_1:
+  fixes x :: machine_word
+  shows "x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
+  by (rule x_less_2_0_1') auto
+
+end
+
+end
diff --git a/thys/Word_Lib/Machine_Word_64_Basics.thy b/thys/Word_Lib/Machine_Word_64_Basics.thy
new file mode 100644
--- /dev/null
+++ b/thys/Word_Lib/Machine_Word_64_Basics.thy
@@ -0,0 +1,66 @@
+(*
+ * Copyright 2014, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+section \<open>64 bit standard platform-specific word size and alignment.\<close>
+
+theory Machine_Word_64_Basics
+imports "HOL-Library.Word" Word_64
+begin
+
+type_synonym machine_word_len = 64
+
+definition word_bits :: nat
+where
+  \<open>word_bits = LENGTH(machine_word_len)\<close>
+
+lemma word_bits_conv [code]:
+  \<open>word_bits = 64\<close>
+  by (simp add: word_bits_def)
+
+text \<open>The following two are numerals so they can be used as nats and words.\<close>
+
+definition word_size_bits :: \<open>'a :: numeral\<close>
+where
+  \<open>word_size_bits = 3\<close>
+
+definition word_size :: \<open>'a :: numeral\<close>
+where
+  \<open>word_size = 8\<close>
+
+lemma n_less_word_bits:
+  "(n < word_bits) = (n < 64)"
+  by (simp add: word_bits_def word_size_def)
+
+lemmas upper_bits_unset_is_l2p_64 = upper_bits_unset_is_l2p [where 'a=64, folded word_bits_def]
+
+lemmas le_2p_upper_bits_64 = le_2p_upper_bits [where 'a=64, folded word_bits_def]
+lemmas le2p_bits_unset_64 = le2p_bits_unset[where 'a=64, folded word_bits_def]
+
+lemmas unat_power_lower64 [simp] = unat_power_lower64'[folded word_bits_def]
+
+lemmas word64_less_sub_le[simp] = word64_less_sub_le' [folded word_bits_def]
+
+lemmas word64_power_less_1[simp] = word64_power_less_1'[folded word_bits_def]
+
+lemma of_nat64_0:
+  "\<lbrakk>of_nat n = (0::word64); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
+  by (erule of_nat_0, simp add: word_bits_def)
+
+lemmas unat_of_nat64 = unat_of_nat64'[folded word_bits_def]
+
+lemmas word_power_nonzero_64 = word_power_nonzero [where 'a=64, folded word_bits_def]
+
+lemmas div_power_helper_64 = div_power_helper [where 'a=64, folded word_bits_def]
+
+lemmas of_nat_less_pow_64 = of_nat_power [where 'a=64, folded word_bits_def]
+
+lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def]
+
+end
diff --git a/thys/Word_Lib/More_Word.thy b/thys/Word_Lib/More_Word.thy
--- a/thys/Word_Lib/More_Word.thy
+++ b/thys/Word_Lib/More_Word.thy
@@ -1,2550 +1,2563 @@
 (*
  * Copyright Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section \<open>Lemmas on words\<close>
 
 theory More_Word
   imports
     "HOL-Library.Word"
     More_Arithmetic
     More_Divides
 begin
 
+context unique_euclidean_semiring_with_bit_operations \<comment>\<open>TODO: move\<close>
+begin
+
+lemma possible_bit [simp]:
+  \<open>possible_bit TYPE('a) n\<close>
+  by (simp add: possible_bit_def)
+
+lemma drop_bit_mask_eq:
+  \<open>drop_bit m (mask n) = mask (n - m)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps possible_bit_def)
+
+end
+
 context
   includes bit_operations_syntax
 begin
 
 \<comment> \<open>problem posed by TPHOLs referee:
       criterion for overflow of addition of signed integers\<close>
 
 lemma sofl_test:
   \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
     drop_bit (size x - 1) ((x + y XOR x) AND (x + y XOR y)) = 0\<close>
   for x y :: \<open>'a::len word\<close>
 proof -
   obtain n where n: \<open>LENGTH('a) = Suc n\<close>
     by (cases \<open>LENGTH('a)\<close>) simp_all
   have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close>
     \<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close>
     using signed_take_bit_int_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_int_less_eq [of n \<open>sint x + sint y\<close>]
     by (auto intro: ccontr)
   have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
     (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
     (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close>
     using sint_less [of x] sint_greater_eq [of x] sint_less [of y] sint_greater_eq [of y]
     signed_take_bit_int_eq_self [of \<open>LENGTH('a) - 1\<close> \<open>sint x + sint y\<close>]
     apply (auto simp add: not_less)
        apply (unfold sint_word_ariths)
        apply (subst signed_take_bit_int_eq_self)
          prefer 4
          apply (subst signed_take_bit_int_eq_self)
            prefer 7
            apply (subst signed_take_bit_int_eq_self)
              prefer 10
              apply (subst signed_take_bit_int_eq_self)
                apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
        apply (smt (z3) take_bit_nonnegative)
       apply (smt (z3) take_bit_int_less_exp)
      apply (smt (z3) take_bit_nonnegative)
     apply (smt (z3) take_bit_int_less_exp)
     done
   then show ?thesis
     apply (simp only: One_nat_def word_size drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
     apply (simp add: bit_last_iff)
     done
 qed
 
 lemma unat_power_lower [simp]:
   "unat ((2::'a::len word) ^ n) = 2 ^ n" if "n < LENGTH('a::len)"
   using that by transfer simp
 
 lemma unat_p2: "n < LENGTH('a :: len) \<Longrightarrow> unat (2 ^ n :: 'a word) = 2 ^ n"
   by (fact unat_power_lower)
 
 lemma word_div_lt_eq_0:
   "x < y \<Longrightarrow> x div y = 0" for x :: "'a :: len word"
   by transfer simp
 
 lemma word_div_eq_1_iff: "n div m = 1 \<longleftrightarrow> n \<ge> m \<and> unat n < 2 * unat (m :: 'a :: len word)"
   apply (simp only: word_arith_nat_defs word_le_nat_alt word_of_nat_eq_iff flip: nat_div_eq_Suc_0_iff)
   apply (simp flip: unat_div unsigned_take_bit_eq)
   done
 
 lemma AND_twice [simp]:
   "(w AND m) AND m = w AND m"
   by (fact and.right_idem)
 
 lemma word_combine_masks:
   "w AND m = z \<Longrightarrow> w AND m' = z' \<Longrightarrow> w AND (m OR m') = (z OR z')"
   for w m m' z z' :: \<open>'a::len word\<close>
   by (simp add: bit.conj_disj_distrib)
 
 lemma p2_gt_0:
   "(0 < (2 ^ n :: 'a :: len word)) = (n < LENGTH('a))"
   by (simp add : word_gt_0 not_le)
 
 lemma uint_2p_alt:
   \<open>n < LENGTH('a::len) \<Longrightarrow> uint ((2::'a::len word) ^ n) = 2 ^ n\<close>
   using p2_gt_0 [of n, where ?'a = 'a] by (simp add: uint_2p)
 
 lemma p2_eq_0:
   \<open>(2::'a::len word) ^ n = 0 \<longleftrightarrow> LENGTH('a::len) \<le> n\<close>
   by (fact exp_eq_zero_iff)
 
 lemma p2len:
   \<open>(2 :: 'a word) ^ LENGTH('a::len) = 0\<close>
   by simp
 
 lemma neg_mask_is_div:
   "w AND NOT (mask n) = (w div 2^n) * 2^n"
   for w :: \<open>'a::len word\<close>
   by (rule bit_word_eqI)
     (auto simp add: bit_simps simp flip: push_bit_eq_mult drop_bit_eq_div)
 
 lemma neg_mask_is_div':
   "n < size w \<Longrightarrow> w AND NOT (mask n) = ((w div (2 ^ n)) * (2 ^ n))"
   for w :: \<open>'a::len word\<close>
   by (rule neg_mask_is_div)
 
 lemma and_mask_arith:
   "w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
   for w :: \<open>'a::len word\<close>
   by (rule bit_word_eqI)
     (auto simp add: bit_simps word_size simp flip: push_bit_eq_mult drop_bit_eq_div)
 
 lemma and_mask_arith':
   "0 < n \<Longrightarrow> w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
   for w :: \<open>'a::len word\<close>
   by (rule and_mask_arith)
 
 lemma mask_2pm1: "mask n = 2 ^ n - (1 :: 'a::len word)"
   by (fact mask_eq_decr_exp)
 
 lemma add_mask_fold:
   "x + 2 ^ n - 1 = x + mask n"
   for x :: \<open>'a::len word\<close>
   by (simp add: mask_eq_decr_exp)
 
 lemma word_and_mask_le_2pm1: "w AND mask n \<le> 2 ^ n - 1"
   for w :: \<open>'a::len word\<close>
   by (simp add: mask_2pm1[symmetric] word_and_le1)
 
 lemma is_aligned_AND_less_0:
   "u AND mask n = 0 \<Longrightarrow> v < 2^n \<Longrightarrow> u AND v = 0"
   for u v :: \<open>'a::len word\<close>
   apply (drule less_mask_eq)
   apply (simp flip: take_bit_eq_mask)
   apply (simp add: bit_eq_iff)
   apply (auto simp add: bit_simps)
   done
 
 lemma and_mask_eq_iff_le_mask:
   \<open>w AND mask n = w \<longleftrightarrow> w \<le> mask n\<close>
   for w :: \<open>'a::len word\<close>
   apply (simp flip: take_bit_eq_mask)
   apply (cases \<open>n \<ge> LENGTH('a)\<close>; transfer)
    apply (simp_all add: not_le min_def)
    apply (simp_all add: mask_eq_exp_minus_1)
   apply auto
    apply (metis take_bit_int_less_exp)
   apply (metis min_def nat_less_le take_bit_int_eq_self_iff take_bit_take_bit)
   done
 
 lemma less_eq_mask_iff_take_bit_eq_self:
   \<open>w \<le> mask n \<longleftrightarrow> take_bit n w = w\<close>
   for w :: \<open>'a::len word\<close>
   by (simp add: and_mask_eq_iff_le_mask take_bit_eq_mask)
 
 lemma NOT_eq:
   "NOT (x :: 'a :: len word) = - x - 1"
   apply (cut_tac x = "x" in word_add_not)
   apply (drule add.commute [THEN trans])
   apply (drule eq_diff_eq [THEN iffD2])
   by simp
 
 lemma NOT_mask: "NOT (mask n :: 'a::len word) = - (2 ^ n)"
   by (simp add : NOT_eq mask_2pm1)
 
 lemma le_m1_iff_lt: "(x > (0 :: 'a :: len word)) = ((y \<le> x - 1) = (y < x))"
   by uint_arith
 
 lemma gt0_iff_gem1:
   \<open>0 < x \<longleftrightarrow> x - 1 < x\<close>
   for x :: \<open>'a::len word\<close>
   by (metis add.right_neutral diff_add_cancel less_irrefl measure_unat unat_arith_simps(2) word_neq_0_conv word_sub_less_iff)
 
 lemma power_2_ge_iff:
   \<open>2 ^ n - (1 :: 'a::len word) < 2 ^ n \<longleftrightarrow> n < LENGTH('a)\<close>
   using gt0_iff_gem1 p2_gt_0 by blast
 
 lemma le_mask_iff_lt_2n:
   "n < len_of TYPE ('a) = (((w :: 'a :: len word) \<le> mask n) = (w < 2 ^ n))"
   unfolding mask_2pm1 by (rule trans [OF p2_gt_0 [THEN sym] le_m1_iff_lt])
 
 lemma mask_lt_2pn:
   \<open>n < LENGTH('a) \<Longrightarrow> mask n < (2 :: 'a::len word) ^ n\<close>
   by (simp add: mask_eq_exp_minus_1 power_2_ge_iff)
 
 lemma word_unat_power:
   "(2 :: 'a :: len word) ^ n = of_nat (2 ^ n)"
   by simp
 
 lemma of_nat_mono_maybe:
   assumes xlt: "x < 2 ^ len_of TYPE ('a)"
   shows   "y < x \<Longrightarrow> of_nat y < (of_nat x :: 'a :: len word)"
   apply (subst word_less_nat_alt)
   apply (subst unat_of_nat)+
   apply (subst mod_less)
    apply (erule order_less_trans [OF _ xlt])
   apply (subst mod_less [OF xlt])
   apply assumption
   done
 
 lemma word_and_max_word:
   fixes a::"'a::len word"
   shows "x = - 1 \<Longrightarrow> a AND x = a"
   by simp
 
 lemma word_and_full_mask_simp:
   \<open>x AND mask LENGTH('a) = x\<close> for x :: \<open>'a::len word\<close>
   by (simp add: bit_eq_iff bit_simps)
 
 lemma of_int_uint:
   "of_int (uint x) = x"
   by (fact word_of_int_uint)
 
 corollary word_plus_and_or_coroll:
   "x AND y = 0 \<Longrightarrow> x + y = x OR y"
   for x y :: \<open>'a::len word\<close>
   using word_plus_and_or[where x=x and y=y]
   by simp
 
 corollary word_plus_and_or_coroll2:
   "(x AND w) + (x AND NOT w) = x"
   for x w :: \<open>'a::len word\<close>
   apply (subst disjunctive_add)
    apply (simp add: bit_simps)
   apply (simp flip: bit.conj_disj_distrib)
   done
 
 lemma unat_mask_eq:
   \<open>unat (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close>
   by transfer (simp add: nat_mask_eq)
 
 lemma word_plus_mono_left:
   fixes x :: "'a :: len word"
   shows "\<lbrakk>y \<le> z; x \<le> x + z\<rbrakk> \<Longrightarrow> y + x \<le> z + x"
   by unat_arith
 
 lemma less_Suc_unat_less_bound:
   "n < Suc (unat (x :: 'a :: len word)) \<Longrightarrow> n < 2 ^ LENGTH('a)"
   by (auto elim!: order_less_le_trans intro: Suc_leI)
 
 lemma up_ucast_inj:
   "\<lbrakk> ucast x = (ucast y::'b::len word); LENGTH('a) \<le> len_of TYPE ('b) \<rbrakk> \<Longrightarrow> x = (y::'a::len word)"
   by transfer (simp add: min_def split: if_splits)
 
 lemmas ucast_up_inj = up_ucast_inj
 
 lemma up_ucast_inj_eq:
   "LENGTH('a) \<le> len_of TYPE ('b) \<Longrightarrow> (ucast x = (ucast y::'b::len word)) = (x = (y::'a::len word))"
   by (fastforce dest: up_ucast_inj)
 
 lemma no_plus_overflow_neg:
   "(x :: 'a :: len word) < -y \<Longrightarrow> x \<le> x + y"
   by (metis diff_minus_eq_add less_imp_le sub_wrap_lt)
 
 lemma ucast_ucast_eq:
   "\<lbrakk> ucast x = (ucast (ucast y::'a word)::'c::len word); LENGTH('a) \<le> LENGTH('b);
      LENGTH('b) \<le> LENGTH('c) \<rbrakk> \<Longrightarrow>
    x = ucast y" for x :: "'a::len word" and y :: "'b::len word"
   apply transfer
   apply (cases \<open>LENGTH('c) = LENGTH('a)\<close>)
    apply (auto simp add: min_def)
   done
 
 lemma ucast_0_I:
   "x = 0 \<Longrightarrow> ucast x = 0"
   by simp
 
 lemma word_add_offset_less:
   fixes x :: "'a :: len word"
   assumes yv: "y < 2 ^ n"
   and     xv: "x < 2 ^ m"
   and     mnv: "sz < LENGTH('a :: len)"
   and    xv': "x < 2 ^ (LENGTH('a :: len) - n)"
   and     mn: "sz = m + n"
   shows   "x * 2 ^ n + y < 2 ^ sz"
 proof (subst mn)
   from mnv mn have nv: "n < LENGTH('a)" and mv: "m < LENGTH('a)"  by auto
 
   have uy: "unat y < 2 ^ n"
     by (rule order_less_le_trans [OF unat_mono [OF yv] order_eq_refl],
         rule unat_power_lower[OF nv])
 
   have ux: "unat x < 2 ^ m"
     by (rule order_less_le_trans [OF unat_mono [OF xv] order_eq_refl],
         rule unat_power_lower[OF mv])
 
   then show "x * 2 ^ n + y < 2 ^ (m + n)" using ux uy nv mnv xv'
     apply (subst word_less_nat_alt)
     apply (subst unat_word_ariths)+
     apply (subst mod_less)
      apply simp
      apply (subst mult.commute)
      apply (rule nat_less_power_trans [OF _ order_less_imp_le [OF nv]])
      apply (rule order_less_le_trans [OF unat_mono [OF xv']])
      apply (cases "n = 0"; simp)
     apply (subst unat_power_lower[OF nv])
     apply (subst mod_less)
      apply (erule order_less_le_trans [OF nat_add_offset_less], assumption)
       apply (rule mn)
      apply simp
     apply (simp add: mn mnv)
     apply (erule nat_add_offset_less; simp)
     done
 qed
 
 lemma word_less_power_trans:
   fixes n :: "'a :: len word"
   assumes nv: "n < 2 ^ (m - k)"
   and     kv: "k \<le> m"
   and     mv: "m < len_of TYPE ('a)"
   shows "2 ^ k * n < 2 ^ m"
   using nv kv mv
   apply -
   apply (subst word_less_nat_alt)
   apply (subst unat_word_ariths)
   apply (subst mod_less)
    apply simp
    apply (rule nat_less_power_trans)
     apply (erule order_less_trans [OF unat_mono])
     apply simp
    apply simp
   apply simp
   apply (rule nat_less_power_trans)
    apply (subst unat_power_lower[where 'a = 'a, symmetric])
     apply simp
    apply (erule unat_mono)
   apply simp
   done
 
 lemma  word_less_power_trans2:
   fixes n :: "'a::len word"
   shows "\<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk> \<Longrightarrow> n * 2 ^ k < 2 ^ m"
   by (subst field_simps, rule word_less_power_trans)
 
 lemma Suc_unat_diff_1:
   fixes x :: "'a :: len word"
   assumes lt: "1 \<le> x"
   shows "Suc (unat (x - 1)) = unat x"
 proof -
   have "0 < unat x"
     by (rule order_less_le_trans [where y = 1], simp, subst unat_1 [symmetric],
         rule iffD1 [OF word_le_nat_alt lt])
 
   then show ?thesis
     by ((subst unat_sub [OF lt])+, simp only:  unat_1)
 qed
 
 lemma word_eq_unatI:
   \<open>v = w\<close> if \<open>unat v = unat w\<close>
   using that by transfer (simp add: nat_eq_iff)
 
 lemma word_div_sub:
   fixes x :: "'a :: len word"
   assumes yx: "y \<le> x"
   and     y0: "0 < y"
   shows "(x - y) div y = x div y - 1"
   apply (rule word_eq_unatI)
   apply (subst unat_div)
   apply (subst unat_sub [OF yx])
   apply (subst unat_sub)
    apply (subst word_le_nat_alt)
    apply (subst unat_div)
    apply (subst le_div_geq)
      apply (rule order_le_less_trans [OF _ unat_mono [OF y0]])
      apply simp
     apply (subst word_le_nat_alt [symmetric], rule yx)
    apply simp
   apply (subst unat_div)
   apply (subst le_div_geq [OF _ iffD1 [OF word_le_nat_alt yx]])
    apply (rule order_le_less_trans [OF _ unat_mono [OF y0]])
    apply simp
   apply simp
   done
 
 lemma word_mult_less_mono1:
   fixes i :: "'a :: len word"
   assumes ij: "i < j"
   and    knz: "0 < k"
   and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
   shows  "i * k < j * k"
 proof -
   from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)"
     by (auto intro: order_less_subst2 simp: word_less_nat_alt elim: mult_less_mono1)
 
   then show ?thesis using ujk knz ij
     by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem])
 qed
 
 lemma word_mult_less_dest:
   fixes i :: "'a :: len word"
   assumes ij: "i * k < j * k"
   and    uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
   and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
   shows  "i < j"
   using uik ujk ij
   by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem] elim: mult_less_mono1)
 
 lemma word_mult_less_cancel:
   fixes k :: "'a :: len word"
   assumes knz: "0 < k"
   and    uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
   and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
   shows "(i * k < j * k) = (i < j)"
   by (rule iffI [OF word_mult_less_dest [OF _ uik ujk] word_mult_less_mono1 [OF _ knz ujk]])
 
 lemma Suc_div_unat_helper:
   assumes szv: "sz < LENGTH('a :: len)"
   and   usszv: "us \<le> sz"
   shows "2 ^ (sz - us) = Suc (unat (((2::'a :: len word) ^ sz - 1) div 2 ^ us))"
 proof -
   note usv = order_le_less_trans [OF usszv szv]
 
   from usszv obtain q where qv: "sz = us + q" by (auto simp: le_iff_add)
 
   have "Suc (unat (((2:: 'a word) ^ sz - 1) div 2 ^ us)) =
     (2 ^ us + unat ((2:: 'a word) ^ sz - 1)) div 2 ^ us"
     apply (subst unat_div unat_power_lower[OF usv])+
     apply (subst div_add_self1, simp+)
     done
 
   also have "\<dots> = ((2 ^ us - 1) + 2 ^ sz) div 2 ^ us" using szv
     by (simp add: unat_minus_one)
 
   also have "\<dots> = 2 ^ q + ((2 ^ us - 1) div 2 ^ us)"
     apply (subst qv)
     apply (subst power_add)
     apply (subst div_mult_self2; simp)
     done
 
   also have "\<dots> = 2 ^ (sz - us)" using qv by simp
 
   finally show ?thesis ..
 qed
 
 lemma enum_word_nth_eq:
   \<open>(Enum.enum :: 'a::len word list) ! n = word_of_nat n\<close>
     if \<open>n < 2 ^ LENGTH('a)\<close>
     for n
   using that by (simp add: enum_word_def)
 
 lemma length_enum_word_eq:
   \<open>length (Enum.enum :: 'a::len word list) = 2 ^ LENGTH('a)\<close>
   by (simp add: enum_word_def)
 
 lemma unat_lt2p [iff]:
   \<open>unat x < 2 ^ LENGTH('a)\<close> for x :: \<open>'a::len word\<close>
   by transfer simp
 
 lemma of_nat_unat [simp]:
   "of_nat \<circ> unat = id"
   by (rule ext, simp)
 
 lemma Suc_unat_minus_one [simp]:
   "x \<noteq> 0 \<Longrightarrow> Suc (unat (x - 1)) = unat x"
   by (metis Suc_diff_1 unat_gt_0 unat_minus_one)
 
 lemma word_add_le_dest:
   fixes i :: "'a :: len word"
   assumes le: "i + k \<le> j + k"
   and    uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
   and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
   shows  "i \<le> j"
   using uik ujk le
   by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem] elim: add_le_mono1)
 
 lemma word_add_le_mono1:
   fixes i :: "'a :: len word"
   assumes ij: "i \<le> j"
   and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
   shows  "i + k \<le> j + k"
 proof -
   from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)"
     by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: add_le_mono1)
 
   then show ?thesis using ujk ij
     by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem])
 qed
 
 lemma word_add_le_mono2:
   fixes i :: "'a :: len word"
   shows "\<lbrakk>i \<le> j; unat j + unat k < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> k + i \<le> k + j"
   by (subst field_simps, subst field_simps, erule (1) word_add_le_mono1)
 
 lemma word_add_le_iff:
   fixes i :: "'a :: len word"
   assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
   and     ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
   shows  "(i + k \<le> j + k) = (i \<le> j)"
 proof
   assume "i \<le> j"
   show "i + k \<le> j + k" by (rule word_add_le_mono1) fact+
 next
   assume "i + k \<le> j + k"
   show "i \<le> j" by (rule word_add_le_dest) fact+
 qed
 
 lemma word_add_less_mono1:
   fixes i :: "'a :: len word"
   assumes ij: "i < j"
   and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
   shows  "i + k < j + k"
 proof -
   from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)"
     by (auto elim: order_le_less_subst2 simp: word_less_nat_alt elim: add_less_mono1)
 
   then show ?thesis using ujk ij
     by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem])
 qed
 
 lemma word_add_less_dest:
   fixes i :: "'a :: len word"
   assumes le: "i + k < j + k"
   and    uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
   and    ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
   shows  "i < j"
   using uik ujk le
   by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem] elim: add_less_mono1)
 
 lemma word_add_less_iff:
   fixes i :: "'a :: len word"
   assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
   and     ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
   shows  "(i + k < j + k) = (i < j)"
 proof
   assume "i < j"
   show "i + k < j + k" by (rule word_add_less_mono1) fact+
 next
   assume "i + k < j + k"
   show "i < j" by (rule word_add_less_dest) fact+
 qed
 
 lemma word_mult_less_iff:
   fixes i :: "'a :: len word"
   assumes knz: "0 < k"
   and     uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
   and     ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
   shows  "(i * k < j * k) = (i < j)"
   using assms by (rule word_mult_less_cancel)
 
 lemma word_le_imp_diff_le:
   fixes n :: "'a::len word"
   shows "\<lbrakk>k \<le> n; n \<le> m\<rbrakk> \<Longrightarrow> n - k \<le> m"
   by (auto simp: unat_sub word_le_nat_alt)
 
 lemma word_less_imp_diff_less:
   fixes n :: "'a::len word"
   shows "\<lbrakk>k \<le> n; n < m\<rbrakk> \<Longrightarrow> n - k < m"
   by (clarsimp simp: unat_sub word_less_nat_alt
              intro!: less_imp_diff_less)
 
 lemma word_mult_le_mono1:
   fixes i :: "'a :: len word"
   assumes ij: "i \<le> j"
   and    knz: "0 < k"
   and    ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
   shows  "i * k \<le> j * k"
 proof -
   from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)"
     by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: mult_le_mono1)
 
   then show ?thesis using ujk knz ij
     by (auto simp: word_le_nat_alt iffD1 [OF unat_mult_lem])
 qed
 
 lemma word_mult_le_iff:
   fixes i :: "'a :: len word"
   assumes knz: "0 < k"
   and     uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
   and     ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
   shows  "(i * k \<le> j * k) = (i \<le> j)"
 proof
   assume "i \<le> j"
   show "i * k \<le> j * k" by (rule word_mult_le_mono1) fact+
 next
   assume p: "i * k \<le> j * k"
 
   have "0 < unat k" using knz by (simp add: word_less_nat_alt)
   then show "i \<le> j" using p
     by (clarsimp simp: word_le_nat_alt iffD1 [OF unat_mult_lem uik]
       iffD1 [OF unat_mult_lem ujk])
 qed
 
 lemma word_diff_less:
   fixes n :: "'a :: len word"
   shows "\<lbrakk>0 < n; 0 < m; n \<le> m\<rbrakk> \<Longrightarrow> m - n < m"
   apply (subst word_less_nat_alt)
   apply (subst unat_sub)
    apply assumption
   apply (rule diff_less)
    apply (simp_all add: word_less_nat_alt)
   done
 
 lemma word_add_increasing:
   fixes x :: "'a :: len word"
   shows "\<lbrakk> p + w \<le> x; p \<le> p + w \<rbrakk> \<Longrightarrow> p \<le> x"
   by unat_arith
 
 lemma word_random:
   fixes x :: "'a :: len word"
   shows "\<lbrakk> p \<le> p + x'; x \<le> x' \<rbrakk> \<Longrightarrow> p \<le> p + x"
   by unat_arith
 
 lemma word_sub_mono:
   "\<lbrakk> a \<le> c; d \<le> b; a - b \<le> a; c - d \<le> c \<rbrakk>
     \<Longrightarrow> (a - b) \<le> (c - d :: 'a :: len word)"
   by unat_arith
 
 lemma power_not_zero:
   "n < LENGTH('a::len) \<Longrightarrow> (2 :: 'a word) ^ n \<noteq> 0"
   by (metis p2_gt_0 word_neq_0_conv)
 
 lemma word_gt_a_gt_0:
   "a < n \<Longrightarrow> (0 :: 'a::len word) < n"
   apply (case_tac "n = 0")
    apply clarsimp
   apply (clarsimp simp: word_neq_0_conv)
   done
 
 lemma word_power_less_1 [simp]:
   "sz < LENGTH('a::len) \<Longrightarrow> (2::'a word) ^ sz - 1 < 2 ^ sz"
   apply (simp add: word_less_nat_alt)
   apply (subst unat_minus_one)
   apply simp_all
   done
 
 lemma word_sub_1_le:
   "x \<noteq> 0 \<Longrightarrow> x - 1 \<le> (x :: ('a :: len) word)"
   apply (subst no_ulen_sub)
   apply simp
   apply (cases "uint x = 0")
    apply (simp add: uint_0_iff)
   apply (insert uint_ge_0[where x=x])
   apply arith
   done
 
 lemma push_bit_word_eq_nonzero:
   \<open>push_bit n w \<noteq> 0\<close> if \<open>w < 2 ^ m\<close> \<open>m + n < LENGTH('a)\<close> \<open>w \<noteq> 0\<close>
     for w :: \<open>'a::len word\<close>
   using that
   apply (simp only: word_neq_0_conv word_less_nat_alt
                     mod_0 unat_word_ariths
                     unat_power_lower word_le_nat_alt)
   apply (metis add_diff_cancel_right' gr0I gr_implies_not0 less_or_eq_imp_le min_def push_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_push_bit take_bit_take_bit unsigned_push_bit_eq)
   done
 
 lemma unat_less_power:
   fixes k :: "'a::len word"
   assumes szv: "sz < LENGTH('a)"
   and     kv:  "k < 2 ^ sz"
   shows   "unat k < 2 ^ sz"
   using szv unat_mono [OF kv] by simp
 
 lemma unat_mult_power_lem:
   assumes kv: "k < 2 ^ (LENGTH('a::len) - sz)"
   shows "unat (2 ^ sz * of_nat k :: (('a::len) word)) = 2 ^ sz * k"
 proof (cases \<open>sz < LENGTH('a)\<close>)
   case True
   with assms show ?thesis
     by (simp add: unat_word_ariths take_bit_eq_mod mod_simps unsigned_of_nat)
       (simp add: take_bit_nat_eq_self_iff nat_less_power_trans flip: take_bit_eq_mod)
 next
   case False
   with assms show ?thesis
     by simp
 qed
 
 lemma word_plus_mcs_4:
   "\<lbrakk>v + x \<le> w + x; x \<le> v + x\<rbrakk> \<Longrightarrow> v \<le> (w::'a::len word)"
   by uint_arith
 
 lemma word_plus_mcs_3:
   "\<lbrakk>v \<le> w; x \<le> w + x\<rbrakk> \<Longrightarrow> v + x \<le> w + (x::'a::len word)"
   by unat_arith
 
 lemma word_le_minus_one_leq:
   "x < y \<Longrightarrow> x \<le> y - 1" for x :: "'a :: len word"
   by transfer (metis le_less_trans less_irrefl take_bit_decr_eq take_bit_nonnegative zle_diff1_eq)
 
 lemma word_less_sub_le[simp]:
   fixes x :: "'a :: len word"
   assumes nv: "n < LENGTH('a)"
   shows "(x \<le> 2 ^ n - 1) = (x < 2 ^ n)"
   using le_less_trans word_le_minus_one_leq nv power_2_ge_iff by blast
 
 lemma unat_of_nat_len:
   "x < 2 ^ LENGTH('a) \<Longrightarrow> unat (of_nat x :: 'a::len word) = x"
   by (simp add: unsigned_of_nat take_bit_nat_eq_self_iff)
 
 lemma unat_of_nat_eq:
   "x < 2 ^ LENGTH('a) \<Longrightarrow> unat (of_nat x ::'a::len word) = x"
   by (rule unat_of_nat_len)
 
 lemma unat_eq_of_nat:
   "n < 2 ^ LENGTH('a) \<Longrightarrow> (unat (x :: 'a::len word) = n) = (x = of_nat n)"
   by transfer
     (auto simp add: take_bit_of_nat nat_eq_iff take_bit_nat_eq_self_iff intro: sym)
 
 lemma alignUp_div_helper:
   fixes a :: "'a::len word"
   assumes kv: "k < 2 ^ (LENGTH('a) - n)"
   and     xk: "x = 2 ^ n * of_nat k"
   and    le: "a \<le> x"
   and    sz: "n < LENGTH('a)"
   and   anz: "a mod 2 ^ n \<noteq> 0"
   shows "a div 2 ^ n < of_nat k"
 proof -
   have kn: "unat (of_nat k :: 'a word) * unat ((2::'a word) ^ n) < 2 ^ LENGTH('a)"
     using xk kv sz
     apply (subst unat_of_nat_eq)
      apply (erule order_less_le_trans)
      apply simp
     apply (subst unat_power_lower, simp)
     apply (subst mult.commute)
     apply (rule nat_less_power_trans)
      apply simp
     apply simp
     done
 
   have "unat a div 2 ^ n * 2 ^ n \<noteq> unat a"
   proof -
     have "unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n"
       by (simp add: div_mult_mod_eq)
     also have "\<dots> \<noteq> unat a div 2 ^ n * 2 ^ n" using sz anz
       by (simp add: unat_arith_simps)
     finally show ?thesis ..
   qed
 
   then have "a div 2 ^ n * 2 ^ n < a" using sz anz
     apply (subst word_less_nat_alt)
     apply (subst unat_word_ariths)
     apply (subst unat_div)
     apply simp
     apply (rule order_le_less_trans [OF mod_less_eq_dividend])
     apply (erule order_le_neq_trans [OF div_mult_le])
     done
 
   also from xk le have "\<dots> \<le> of_nat k * 2 ^ n" by (simp add: field_simps)
   finally show ?thesis using sz kv
     apply -
     apply (erule word_mult_less_dest [OF _ _ kn])
     apply (simp add: unat_div)
     apply (rule order_le_less_trans [OF div_mult_le])
     apply (rule unat_lt2p)
     done
 qed
 
 lemma mask_out_sub_mask:
   "(x AND NOT (mask n)) = x - (x AND (mask n))"
   for x :: \<open>'a::len word\<close>
   by (simp add: field_simps word_plus_and_or_coroll2)
 
 lemma subtract_mask:
   "p - (p AND mask n) = (p AND NOT (mask n))"
   "p - (p AND NOT (mask n)) = (p AND mask n)"
   for p :: \<open>'a::len word\<close>
   by (simp add: field_simps word_plus_and_or_coroll2)+
 
 lemma take_bit_word_eq_self_iff:
   \<open>take_bit n w = w \<longleftrightarrow> n \<ge> LENGTH('a) \<or> w < 2 ^ n\<close>
   for w :: \<open>'a::len word\<close>
   using take_bit_int_eq_self_iff [of n \<open>take_bit LENGTH('a) (uint w)\<close>]
   by (transfer fixing: n) auto
 
 lemma word_power_increasing:
   assumes x: "2 ^ x < (2 ^ y::'a::len word)" "x < LENGTH('a::len)" "y < LENGTH('a::len)"
   shows "x < y" using x
   using assms by transfer simp
 
 lemma mask_twice:
   "(x AND mask n) AND mask m = x AND mask (min m n)"
   for x :: \<open>'a::len word\<close>
   by (simp flip: take_bit_eq_mask)
 
 lemma plus_one_helper[elim!]:
   "x < n + (1 :: 'a :: len word) \<Longrightarrow> x \<le> n"
   apply (simp add: word_less_nat_alt word_le_nat_alt field_simps)
   apply (case_tac "1 + n = 0")
    apply simp_all
   apply (subst(asm) unatSuc, assumption)
   apply arith
   done
 
 lemma plus_one_helper2:
   "\<lbrakk> x \<le> n; n + 1 \<noteq> 0 \<rbrakk> \<Longrightarrow> x < n + (1 :: 'a :: len word)"
   by (simp add: word_less_nat_alt word_le_nat_alt field_simps
                 unatSuc)
 
 lemma less_x_plus_1:
   fixes x :: "'a :: len word" shows
   "x \<noteq> - 1 \<Longrightarrow> (y < (x + 1)) = (y < x \<or> y = x)"
   apply (rule iffI)
    apply (rule disjCI)
    apply (drule plus_one_helper)
    apply simp
   apply (subgoal_tac "x < x + 1")
    apply (erule disjE, simp_all)
   apply (rule plus_one_helper2 [OF order_refl])
   apply (rule notI, drule max_word_wrap)
   apply simp
   done
 
 lemma word_Suc_leq:
   fixes k::"'a::len word" shows "k \<noteq> - 1 \<Longrightarrow> x < k + 1 \<longleftrightarrow> x \<le> k"
   using less_x_plus_1 word_le_less_eq by auto
 
 lemma word_Suc_le:
    fixes k::"'a::len word" shows "x \<noteq> - 1 \<Longrightarrow> x + 1 \<le> k \<longleftrightarrow> x < k"
   by (meson not_less word_Suc_leq)
 
 lemma word_lessThan_Suc_atMost:
   \<open>{..< k + 1} = {..k}\<close> if \<open>k \<noteq> - 1\<close> for k :: \<open>'a::len word\<close>
   using that by (simp add: lessThan_def atMost_def word_Suc_leq)
 
 lemma word_atLeastLessThan_Suc_atLeastAtMost:
   \<open>{l ..< u + 1} = {l..u}\<close> if \<open>u \<noteq> - 1\<close> for l :: \<open>'a::len word\<close>
   using that by (simp add: atLeastAtMost_def atLeastLessThan_def word_lessThan_Suc_atMost)
 
 lemma word_atLeastAtMost_Suc_greaterThanAtMost:
   \<open>{m<..u} = {m + 1..u}\<close> if \<open>m \<noteq> - 1\<close> for m :: \<open>'a::len word\<close>
   using that by (simp add: greaterThanAtMost_def greaterThan_def atLeastAtMost_def atLeast_def word_Suc_le)
 
 lemma word_atLeastLessThan_Suc_atLeastAtMost_union:
   fixes l::"'a::len word"
   assumes "m \<noteq> - 1" and "l \<le> m" and "m \<le> u"
   shows "{l..m} \<union> {m+1..u} = {l..u}"
   proof -
   from ivl_disj_un_two(8)[OF assms(2) assms(3)] have "{l..u} = {l..m} \<union> {m<..u}" by blast
   with assms show ?thesis by(simp add: word_atLeastAtMost_Suc_greaterThanAtMost)
   qed
 
 lemma max_word_less_eq_iff [simp]:
   \<open>- 1 \<le> w \<longleftrightarrow> w = - 1\<close> for w :: \<open>'a::len word\<close>
   by (fact word_order.extremum_unique)
 
 lemma word_or_zero:
   "(a OR b = 0) = (a = 0 \<and> b = 0)"
   for a b :: \<open>'a::len word\<close>
   by (fact or_eq_0_iff)
 
 lemma word_2p_mult_inc:
   assumes x: "2 * 2 ^ n < (2::'a::len word) * 2 ^ m"
   assumes suc_n: "Suc n < LENGTH('a::len)"
   shows "2^n < (2::'a::len word)^m"
   by (smt suc_n le_less_trans lessI nat_less_le nat_mult_less_cancel_disj p2_gt_0
           power_Suc power_Suc unat_power_lower word_less_nat_alt x)
 
 lemma power_overflow:
   "n \<ge> LENGTH('a) \<Longrightarrow> 2 ^ n = (0 :: 'a::len word)"
   by simp
 
 lemmas extra_sle_sless_unfolds [simp] =
     word_sle_eq[where a=0 and b=1]
     word_sle_eq[where a=0 and b="numeral n"]
     word_sle_eq[where a=1 and b=0]
     word_sle_eq[where a=1 and b="numeral n"]
     word_sle_eq[where a="numeral n" and b=0]
     word_sle_eq[where a="numeral n" and b=1]
     word_sless_alt[where a=0 and b=1]
     word_sless_alt[where a=0 and b="numeral n"]
     word_sless_alt[where a=1 and b=0]
     word_sless_alt[where a=1 and b="numeral n"]
     word_sless_alt[where a="numeral n" and b=0]
     word_sless_alt[where a="numeral n" and b=1]
   for n
 
 lemma word_sint_1:
   "sint (1::'a::len word) = (if LENGTH('a) = 1 then -1 else 1)"
   by (fact signed_1)
 
 lemma ucast_of_nat:
   "is_down (ucast :: 'a :: len word \<Rightarrow> 'b :: len word)
     \<Longrightarrow> ucast (of_nat n :: 'a word) = (of_nat n :: 'b word)"
   by transfer simp
 
 lemma scast_1':
   "(scast (1::'a::len word) :: 'b::len word) =
    (word_of_int (signed_take_bit (LENGTH('a::len) - Suc 0) (1::int)))"
   by transfer simp
 
 lemma scast_1:
   "(scast (1::'a::len word) :: 'b::len word) = (if LENGTH('a) = 1 then -1 else 1)"
   by (fact signed_1)
 
 lemma unat_minus_one_word:
   "unat (-1 :: 'a :: len word) = 2 ^ LENGTH('a) - 1"
   by (simp add: mask_eq_exp_minus_1 unsigned_minus_1_eq_mask)
 
 lemmas word_diff_ls'' = word_diff_ls [where xa=x and x=x for x]
 lemmas word_diff_ls' = word_diff_ls'' [simplified]
 
 lemmas word_l_diffs' = word_l_diffs [where xa=x and x=x for x]
 lemmas word_l_diffs = word_l_diffs' [simplified]
 
 lemma two_power_increasing:
   "\<lbrakk> n \<le> m; m < LENGTH('a) \<rbrakk> \<Longrightarrow> (2 :: 'a :: len word) ^ n \<le> 2 ^ m"
   by (simp add: word_le_nat_alt)
 
 lemma word_leq_le_minus_one:
   "\<lbrakk> x \<le> y; x \<noteq> 0 \<rbrakk> \<Longrightarrow> x - 1 < (y :: 'a :: len word)"
   apply (simp add: word_less_nat_alt word_le_nat_alt)
   apply (subst unat_minus_one)
    apply assumption
   apply (cases "unat x")
    apply (simp add: unat_eq_zero)
   apply arith
   done
 
 lemma neg_mask_combine:
   "NOT(mask a) AND NOT(mask b) = NOT(mask (max a b) :: 'a::len word)"
   by (rule bit_word_eqI) (auto simp add: bit_simps)
 
 lemma neg_mask_twice:
   "x AND NOT(mask n) AND NOT(mask m) = x AND NOT(mask (max n m))"
   for x :: \<open>'a::len word\<close>
   by (rule bit_word_eqI) (auto simp add: bit_simps)
 
 lemma multiple_mask_trivia:
   "n \<ge> m \<Longrightarrow> (x AND NOT(mask n)) + (x AND mask n AND NOT(mask m)) = x AND NOT(mask m)"
   for x :: \<open>'a::len word\<close>
   apply (rule trans[rotated], rule_tac w="mask n" in word_plus_and_or_coroll2)
   apply (simp add: word_bw_assocs word_bw_comms word_bw_lcs neg_mask_twice
                    max_absorb2)
   done
 
 lemma word_of_nat_less:
   "\<lbrakk> n < unat x \<rbrakk> \<Longrightarrow> of_nat n < x"
   apply (simp add: word_less_nat_alt)
   apply (erule order_le_less_trans[rotated])
   apply (simp add: unsigned_of_nat take_bit_eq_mod)
   done
 
 lemma unat_mask:
   "unat (mask n :: 'a :: len word) = 2 ^ (min n (LENGTH('a))) - 1"
   apply (subst min.commute)
   apply (simp add: mask_eq_decr_exp not_less min_def  split: if_split_asm)
   apply (intro conjI impI)
    apply (simp add: unat_sub_if_size)
    apply (simp add: power_overflow word_size)
   apply (simp add: unat_sub_if_size)
   done
 
 lemma mask_over_length:
   "LENGTH('a) \<le> n \<Longrightarrow> mask n = (-1::'a::len word)"
   by (simp add: mask_eq_decr_exp)
 
 lemma Suc_2p_unat_mask:
   "n < LENGTH('a) \<Longrightarrow> Suc (2 ^ n * k + unat (mask n :: 'a::len word)) = 2 ^ n * (k+1)"
   by (simp add: unat_mask)
 
 lemma sint_of_nat_ge_zero:
   "x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (of_nat x :: 'a :: len word) \<ge> 0"
   by (simp add: bit_iff_odd signed_of_nat)
 
 lemma int_eq_sint:
   "x < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> sint (of_nat x :: 'a :: len word) = int x"
   apply transfer
   apply (rule signed_take_bit_int_eq_self)
    apply simp_all
   apply (metis negative_zle numeral_power_eq_of_nat_cancel_iff)
   done
 
 lemma sint_of_nat_le:
   "\<lbrakk> b < 2 ^ (LENGTH('a) - 1); a \<le> b \<rbrakk>
    \<Longrightarrow> sint (of_nat a :: 'a :: len word) \<le> sint (of_nat b :: 'a :: len word)"
   apply (cases \<open>LENGTH('a)\<close>)
   apply simp_all
   apply transfer
   apply (subst signed_take_bit_eq_if_positive)
    apply (simp add: bit_simps)
   apply (metis bit_take_bit_iff nat_less_le order_less_le_trans take_bit_nat_eq_self_iff)
   apply (subst signed_take_bit_eq_if_positive)
     apply (simp add: bit_simps)
   apply (metis bit_take_bit_iff nat_less_le take_bit_nat_eq_self_iff)
     apply (simp flip: of_nat_take_bit add: take_bit_nat_eq_self)
   done
 
 lemma word_le_not_less:
   "((b::'a::len word) \<le> a) = (\<not>(a < b))"
   by fastforce
 
 lemma less_is_non_zero_p1:
   fixes a :: "'a :: len word"
   shows "a < k \<Longrightarrow> a + 1 \<noteq> 0"
   apply (erule contrapos_pn)
   apply (drule max_word_wrap)
   apply (simp add: not_less)
   done
 
 lemma unat_add_lem':
   "(unat x + unat y < 2 ^ LENGTH('a)) \<Longrightarrow>
     (unat (x + y :: 'a :: len word) = unat x + unat y)"
   by (subst unat_add_lem[symmetric], assumption)
 
 lemma word_less_two_pow_divI:
   "\<lbrakk> (x :: 'a::len word) < 2 ^ (n - m); m \<le> n; n < LENGTH('a) \<rbrakk> \<Longrightarrow> x < 2 ^ n div 2 ^ m"
   apply (simp add: word_less_nat_alt)
   apply (subst unat_word_ariths)
   apply (subst mod_less)
    apply (rule order_le_less_trans [OF div_le_dividend])
    apply (rule unat_lt2p)
   apply (simp add: power_sub)
   done
 
 lemma word_less_two_pow_divD:
   "\<lbrakk> (x :: 'a::len word) < 2 ^ n div 2 ^ m \<rbrakk>
      \<Longrightarrow> n \<ge> m \<and> (x < 2 ^ (n - m))"
   apply (cases "n < LENGTH('a)")
    apply (cases "m < LENGTH('a)")
     apply (simp add: word_less_nat_alt)
     apply (subst(asm) unat_word_ariths)
     apply (subst(asm) mod_less)
      apply (rule order_le_less_trans [OF div_le_dividend])
      apply (rule unat_lt2p)
     apply (clarsimp dest!: less_two_pow_divD)
    apply (simp add: power_overflow)
    apply (simp add: word_div_def)
   apply (simp add: power_overflow word_div_def)
   done
 
 lemma of_nat_less_two_pow_div_set:
   "\<lbrakk> n < LENGTH('a) \<rbrakk> \<Longrightarrow>
    {x. x < (2 ^ n div 2 ^ m :: 'a::len word)}
       = of_nat ` {k. k < 2 ^ n div 2 ^ m}"
   apply (simp add: image_def)
   apply (safe dest!: word_less_two_pow_divD less_two_pow_divD
              intro!: word_less_two_pow_divI)
    apply (rule_tac x="unat x" in exI)
    apply (simp add: power_sub[symmetric])
    apply (subst unat_power_lower[symmetric, where 'a='a])
     apply simp
    apply (erule unat_mono)
   apply (subst word_unat_power)
   apply (rule of_nat_mono_maybe)
    apply (rule power_strict_increasing)
     apply simp
    apply simp
   apply assumption
   done
 
 lemma ucast_less:
   "LENGTH('b) < LENGTH('a) \<Longrightarrow>
    (ucast (x :: 'b :: len word) :: ('a :: len word)) < 2 ^ LENGTH('b)"
   by transfer simp
 
 lemma ucast_range_less:
   "LENGTH('a :: len) < LENGTH('b :: len) \<Longrightarrow>
    range (ucast :: 'a word \<Rightarrow> 'b word) = {x. x < 2 ^ len_of TYPE ('a)}"
   apply safe
    apply (erule ucast_less)
   apply (simp add: image_def)
   apply (rule_tac x="ucast x" in exI)
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_simps)
   apply (metis bit_take_bit_iff take_bit_word_eq_self_iff)
   done
 
 lemma word_power_less_diff:
   "\<lbrakk>2 ^ n * q < (2::'a::len word) ^ m; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> q < 2 ^ (m - n)"
   apply (case_tac "m \<ge> LENGTH('a)")
    apply (simp add: power_overflow)
   apply (case_tac "n \<ge> LENGTH('a)")
    apply (simp add: power_overflow)
   apply (cases "n = 0")
    apply simp
   apply (subst word_less_nat_alt)
   apply (subst unat_power_lower)
    apply simp
   apply (rule nat_power_less_diff)
   apply (simp add: word_less_nat_alt)
   apply (subst (asm) iffD1 [OF unat_mult_lem])
    apply (simp add:nat_less_power_trans)
   apply simp
   done
 
 lemma word_less_sub_1:
   "x < (y :: 'a :: len word) \<Longrightarrow> x \<le> y - 1"
   by (fact word_le_minus_one_leq)
 
 lemma word_sub_mono2:
   "\<lbrakk> a + b \<le> c + d; c \<le> a; b \<le> a + b; d \<le> c + d \<rbrakk>
     \<Longrightarrow> b \<le> (d :: 'a :: len word)"
   apply (drule(1) word_sub_mono)
     apply simp
    apply simp
   apply simp
   done
 
 lemma word_not_le:
   "(\<not> x \<le> (y :: 'a :: len word)) = (y < x)"
   by fastforce
 
 lemma word_subset_less:
   "\<lbrakk> {x .. x + r - 1} \<subseteq> {y .. y + s - 1};
      x \<le> x + r - 1; y \<le> y + (s :: 'a :: len word) - 1;
      s \<noteq> 0 \<rbrakk>
      \<Longrightarrow> r \<le> s"
   apply (frule subsetD[where c=x])
    apply simp
   apply (drule subsetD[where c="x + r - 1"])
    apply simp
   apply (clarsimp simp: add_diff_eq[symmetric])
   apply (drule(1) word_sub_mono2)
     apply (simp_all add: olen_add_eqv[symmetric])
   apply (erule word_le_minus_cancel)
   apply (rule ccontr)
   apply (simp add: word_not_le)
   done
 
 lemma uint_power_lower:
   "n < LENGTH('a) \<Longrightarrow> uint (2 ^ n :: 'a :: len word) = (2 ^ n :: int)"
   by (rule uint_2p_alt)
 
 lemma power_le_mono:
   "\<lbrakk>2 ^ n \<le> (2::'a::len word) ^ m; n < LENGTH('a); m < LENGTH('a)\<rbrakk>
    \<Longrightarrow> n \<le> m"
   apply (clarsimp simp add: le_less)
   apply safe
   apply (simp add: word_less_nat_alt)
   apply (simp only: uint_arith_simps(3))
   apply (drule uint_power_lower)+
   apply simp
   done
 
 lemma two_power_eq:
   "\<lbrakk>n < LENGTH('a); m < LENGTH('a)\<rbrakk>
    \<Longrightarrow> ((2::'a::len word) ^ n = 2 ^ m) = (n = m)"
   apply safe
   apply (rule order_antisym)
    apply (simp add: power_le_mono[where 'a='a])+
   done
 
 lemma unat_less_helper:
   "x < of_nat n \<Longrightarrow> unat x < n"
   apply (simp add: word_less_nat_alt)
   apply (erule order_less_le_trans)
   apply (simp add: take_bit_eq_mod unsigned_of_nat)
   done
 
 lemma nat_uint_less_helper:
   "nat (uint y) = z \<Longrightarrow> x < y \<Longrightarrow> nat (uint x) < z"
   apply (erule subst)
   apply (subst unat_eq_nat_uint [symmetric])
   apply (subst unat_eq_nat_uint [symmetric])
   by (simp add: unat_mono)
 
 lemma of_nat_0:
   "\<lbrakk>of_nat n = (0::'a::len word); n < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> n = 0"
   by (auto simp add: word_of_nat_eq_0_iff)
 
 lemma of_nat_inj:
   "\<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow>
    (of_nat x = (of_nat y :: 'a :: len word)) = (x = y)"
   by (metis unat_of_nat_len)
 
 lemma div_to_mult_word_lt:
   "\<lbrakk> (x :: 'a :: len word) \<le> y div z \<rbrakk> \<Longrightarrow> x * z \<le> y"
   apply (cases "z = 0")
    apply simp
   apply (simp add: word_neq_0_conv)
   apply (rule order_trans)
    apply (erule(1) word_mult_le_mono1)
    apply (simp add: unat_div)
    apply (rule order_le_less_trans [OF div_mult_le])
    apply simp
   apply (rule word_div_mult_le)
   done
 
 lemma ucast_ucast_mask:
   "(ucast :: 'a :: len word \<Rightarrow> 'b :: len word) (ucast x) = x AND mask (len_of TYPE ('a))"
   apply (simp flip: take_bit_eq_mask)
   apply transfer
   apply (simp add: ac_simps)
   done
 
 lemma ucast_ucast_len:
   "\<lbrakk> x < 2 ^ LENGTH('b) \<rbrakk> \<Longrightarrow> ucast (ucast x::'b::len word) = (x::'a::len word)"
   apply (subst ucast_ucast_mask)
   apply (erule less_mask_eq)
   done
 
 lemma ucast_ucast_id:
   "LENGTH('a) < LENGTH('b) \<Longrightarrow> ucast (ucast (x::'a::len word)::'b::len word) = x"
   by (auto intro: ucast_up_ucast_id simp: is_up_def source_size_def target_size_def word_size)
 
 lemma unat_ucast:
   "unat (ucast x :: ('a :: len) word) = unat x mod 2 ^ (LENGTH('a))"
 proof -
   have \<open>2 ^ LENGTH('a) = nat (2 ^ LENGTH('a))\<close>
     by simp
   moreover have \<open>unat (ucast x :: 'a word) = unat x mod nat (2 ^ LENGTH('a))\<close>
     by transfer (simp flip: nat_mod_distrib take_bit_eq_mod)
   ultimately show ?thesis
     by (simp only:)
 qed
 
 lemma ucast_less_ucast:
   "LENGTH('a) \<le> LENGTH('b) \<Longrightarrow>
    (ucast x < ((ucast (y :: 'a::len word)) :: 'b::len word)) = (x < y)"
   apply (simp add: word_less_nat_alt unat_ucast)
   apply (subst mod_less)
    apply(rule less_le_trans[OF unat_lt2p], simp)
   apply (subst mod_less)
    apply(rule less_le_trans[OF unat_lt2p], simp)
   apply simp
   done
 
 \<comment> \<open>This weaker version was previously called @{text ucast_less_ucast}. We retain it to
     support existing proofs.\<close>
 lemmas ucast_less_ucast_weak = ucast_less_ucast[OF order.strict_implies_order]
 
 lemma unat_Suc2:
   fixes n :: "'a :: len word"
   shows
   "n \<noteq> -1 \<Longrightarrow> unat (n + 1) = Suc (unat n)"
   apply (subst add.commute, rule unatSuc)
   apply (subst eq_diff_eq[symmetric], simp add: minus_equation_iff)
   done
 
 lemma word_div_1:
   "(n :: 'a :: len word) div 1 = n"
   by (fact bits_div_by_1)
 
 lemma word_minus_one_le:
   "-1 \<le> (x :: 'a :: len word) = (x = -1)"
   by (fact word_order.extremum_unique)
 
 lemma up_scast_inj:
       "\<lbrakk> scast x = (scast y :: 'b :: len word); size x \<le> LENGTH('b) \<rbrakk>
          \<Longrightarrow> x = y"
   apply transfer
   apply (cases \<open>LENGTH('a)\<close>)
   apply simp_all
   apply (metis order_refl take_bit_signed_take_bit take_bit_tightened)
   done
 
 lemma up_scast_inj_eq:
   "LENGTH('a) \<le> len_of TYPE ('b) \<Longrightarrow>
   (scast x = (scast y::'b::len word)) = (x = (y::'a::len word))"
   by (fastforce dest: up_scast_inj simp: word_size)
 
 lemma word_le_add:
   fixes x :: "'a :: len word"
   shows "x \<le> y \<Longrightarrow> \<exists>n. y = x + of_nat n"
   by (rule exI [where x = "unat (y - x)"]) simp
 
 lemma word_plus_mcs_4':
   fixes x :: "'a :: len word"
   shows "\<lbrakk>x + v \<le> x + w; x \<le> x + v\<rbrakk> \<Longrightarrow> v \<le> w"
   apply (rule word_plus_mcs_4)
    apply (simp add: add.commute)
   apply (simp add: add.commute)
   done
 
 lemma unat_eq_1:
   \<open>unat x = Suc 0 \<longleftrightarrow> x = 1\<close>
   by (auto intro!: unsigned_word_eqI [where ?'a = nat])
 
 lemma word_unat_Rep_inject1:
   \<open>unat x = unat 1 \<longleftrightarrow> x = 1\<close>
   by (simp add: unat_eq_1)
 
 lemma and_not_mask_twice:
   "(w AND NOT (mask n)) AND NOT (mask m) = w AND NOT (mask (max m n))"
   for w :: \<open>'a::len word\<close>
   by (rule bit_word_eqI) (auto simp add: bit_simps)
 
 lemma word_less_cases:
   "x < y \<Longrightarrow> x = y - 1 \<or> x < y - (1 ::'a::len word)"
   apply (drule word_less_sub_1)
   apply (drule order_le_imp_less_or_eq)
   apply auto
   done
 
 lemma mask_and_mask:
   "mask a AND mask b = (mask (min a b) :: 'a::len word)"
   by (simp flip: take_bit_eq_mask ac_simps)
 
 lemma mask_eq_0_eq_x:
   "(x AND w = 0) = (x AND NOT w = x)"
   for x w :: \<open>'a::len word\<close>
   using word_plus_and_or_coroll2[where x=x and w=w]
   by auto
 
 lemma mask_eq_x_eq_0:
   "(x AND w = x) = (x AND NOT w = 0)"
   for x w :: \<open>'a::len word\<close>
   using word_plus_and_or_coroll2[where x=x and w=w]
   by auto
 
 lemma compl_of_1: "NOT 1 = (-2 :: 'a :: len word)"
   by (fact not_one_eq)
 
 lemma split_word_eq_on_mask:
   "(x = y) = (x AND m = y AND m \<and> x AND NOT m = y AND NOT m)"
   for x y m :: \<open>'a::len word\<close>
   apply transfer
   apply (simp add: bit_eq_iff)
   apply (auto simp add: bit_simps ac_simps)
   done
 
 lemma word_FF_is_mask:
   "0xFF = (mask 8 :: 'a::len word)"
   by (simp add: mask_eq_decr_exp)
 
 lemma word_1FF_is_mask:
   "0x1FF = (mask 9 :: 'a::len word)"
   by (simp add: mask_eq_decr_exp)
 
 lemma ucast_of_nat_small:
   "x < 2 ^ LENGTH('a) \<Longrightarrow> ucast (of_nat x :: 'a :: len word) = (of_nat x :: 'b :: len word)"
   apply transfer
   apply (auto simp add: take_bit_of_nat min_def not_le)
   apply (metis linorder_not_less min_def take_bit_nat_eq_self take_bit_take_bit)
   done
 
 lemma word_le_make_less:
   fixes x :: "'a :: len word"
   shows "y \<noteq> -1 \<Longrightarrow> (x \<le> y) = (x < (y + 1))"
   apply safe
   apply (erule plus_one_helper2)
   apply (simp add: eq_diff_eq[symmetric])
   done
 
 lemmas finite_word = finite [where 'a="'a::len word"]
 
 lemma word_to_1_set:
   "{0 ..< (1 :: 'a :: len word)} = {0}"
   by fastforce
 
 lemma word_leq_minus_one_le:
   fixes x :: "'a::len word"
   shows "\<lbrakk>y \<noteq> 0; x \<le> y - 1 \<rbrakk> \<Longrightarrow> x < y"
   using le_m1_iff_lt word_neq_0_conv by blast
 
 lemma word_count_from_top:
   "n \<noteq> 0 \<Longrightarrow> {0 ..< n :: 'a :: len word} = {0 ..< n - 1} \<union> {n - 1}"
   apply (rule set_eqI, rule iffI)
    apply simp
    apply (drule word_le_minus_one_leq)
    apply (rule disjCI)
    apply simp
   apply simp
   apply (erule word_leq_minus_one_le)
   apply fastforce
   done
 
 lemma word_minus_one_le_leq:
   "\<lbrakk> x - 1 < y \<rbrakk> \<Longrightarrow> x \<le> (y :: 'a :: len word)"
   apply (cases "x = 0")
    apply simp
   apply (simp add: word_less_nat_alt word_le_nat_alt)
   apply (subst(asm) unat_minus_one)
    apply (simp add: word_less_nat_alt)
   apply (cases "unat x")
    apply (simp add: unat_eq_zero)
   apply arith
   done
 
 lemma word_must_wrap:
   "\<lbrakk> x \<le> n - 1; n \<le> x \<rbrakk> \<Longrightarrow> n = (0 :: 'a :: len word)"
   using dual_order.trans sub_wrap word_less_1 by blast
 
 lemma range_subset_card:
   "\<lbrakk> {a :: 'a :: len word .. b} \<subseteq> {c .. d}; b \<ge> a \<rbrakk> \<Longrightarrow> d \<ge> c \<and> d - c \<ge> b - a"
   using word_sub_le word_sub_mono by fastforce
 
 lemma less_1_simp:
   "n - 1 < m = (n \<le> (m :: 'a :: len word) \<and> n \<noteq> 0)"
   by unat_arith
 
 lemma word_power_mod_div:
   fixes x :: "'a::len word"
   shows "\<lbrakk> n < LENGTH('a); m < LENGTH('a)\<rbrakk>
   \<Longrightarrow> x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)"
   apply (simp add: word_arith_nat_div unat_mod power_mod_div)
   apply (subst unat_arith_simps(3))
   apply (subst unat_mod)
   apply (subst unat_of_nat)+
   apply (simp add: mod_mod_power min.commute)
   done
 
 lemma word_range_minus_1':
   fixes a :: "'a :: len word"
   shows "a \<noteq> 0 \<Longrightarrow> {a - 1<..b} = {a..b}"
   by (simp add: greaterThanAtMost_def atLeastAtMost_def greaterThan_def atLeast_def less_1_simp)
 
 lemma word_range_minus_1:
   fixes a :: "'a :: len word"
   shows "b \<noteq> 0 \<Longrightarrow> {a..b - 1} = {a..<b}"
   apply (simp add: atLeastLessThan_def atLeastAtMost_def atMost_def lessThan_def)
   apply (rule arg_cong [where f = "\<lambda>x. {a..} \<inter> x"])
   apply rule
    apply clarsimp
    apply (erule contrapos_pp)
    apply (simp add: linorder_not_less linorder_not_le word_must_wrap)
   apply (clarsimp)
   apply (drule word_le_minus_one_leq)
   apply (auto simp: word_less_sub_1)
   done
 
 lemma ucast_nat_def:
   "of_nat (unat x) = (ucast :: 'a :: len word \<Rightarrow> 'b :: len word) x"
   by transfer simp
 
 lemma overflow_plus_one_self:
   "(1 + p \<le> p) = (p = (-1 :: 'a :: len word))"
   apply rule
   apply (rule ccontr)
    apply (drule plus_one_helper2)
    apply (rule notI)
    apply (drule arg_cong[where f="\<lambda>x. x - 1"])
    apply simp
    apply (simp add: field_simps)
   apply simp
   done
 
 lemma plus_1_less:
   "(x + 1 \<le> (x :: 'a :: len word)) = (x = -1)"
   apply (rule iffI)
    apply (rule ccontr)
    apply (cut_tac plus_one_helper2[where x=x, OF order_refl])
     apply simp
    apply clarsimp
    apply (drule arg_cong[where f="\<lambda>x. x - 1"])
    apply simp
   apply simp
   done
 
 lemma pos_mult_pos_ge:
   "[|x > (0::int); n>=0 |] ==> n * x >= n*1"
   apply (simp only: mult_left_mono)
   done
 
 lemma word_plus_strict_mono_right:
   fixes x :: "'a :: len word"
   shows "\<lbrakk>y < z; x \<le> x + z\<rbrakk> \<Longrightarrow> x + y < x + z"
   by unat_arith
 
 lemma word_div_mult:
   "0 < c \<Longrightarrow> a < b * c \<Longrightarrow> a div c < b" for a b c :: "'a::len word"
   by (rule classical)
      (use div_to_mult_word_lt [of b a c] in
       \<open>auto simp add: word_less_nat_alt word_le_nat_alt unat_div\<close>)
 
 lemma word_less_power_trans_ofnat:
   "\<lbrakk>n < 2 ^ (m - k); k \<le> m; m < LENGTH('a)\<rbrakk>
    \<Longrightarrow> of_nat n * 2 ^ k < (2::'a::len word) ^ m"
   apply (subst mult.commute)
   apply (rule word_less_power_trans)
     apply (simp_all add: word_less_nat_alt unsigned_of_nat)
   using take_bit_nat_less_eq_self
   apply (rule le_less_trans)
   apply assumption
   done
 
 lemma word_1_le_power:
   "n < LENGTH('a) \<Longrightarrow> (1 :: 'a :: len word) \<le> 2 ^ n"
   by (rule inc_le[where i=0, simplified], erule iffD2[OF p2_gt_0])
 
 lemma unat_1_0:
   "1 \<le> (x::'a::len word) = (0 < unat x)"
   by (auto simp add: word_le_nat_alt)
 
 lemma x_less_2_0_1':
   fixes x :: "'a::len word"
   shows "\<lbrakk>LENGTH('a) \<noteq> 1; x < 2\<rbrakk> \<Longrightarrow> x = 0 \<or> x = 1"
   apply (cases \<open>2 \<le> LENGTH('a)\<close>)
   apply simp_all
   apply transfer
   apply auto
   apply (metis add.commute add.right_neutral even_two_times_div_two mod_div_trivial mod_pos_pos_trivial mult.commute mult_zero_left not_less not_take_bit_negative odd_two_times_div_two_succ)
   done
 
 lemmas word_add_le_iff2 = word_add_le_iff [folded no_olen_add_nat]
 
 lemma of_nat_power:
   shows "\<lbrakk> p < 2 ^ x; x < len_of TYPE ('a) \<rbrakk> \<Longrightarrow> of_nat p < (2 :: 'a :: len word) ^ x"
   apply (rule order_less_le_trans)
    apply (rule of_nat_mono_maybe)
     apply (erule power_strict_increasing)
     apply simp
    apply assumption
   apply (simp add: word_unat_power del: of_nat_power)
   done
 
 lemma of_nat_n_less_equal_power_2:
   "n < LENGTH('a::len) \<Longrightarrow> ((of_nat n)::'a word) < 2 ^ n"
   apply (induct n)
    apply clarsimp
   apply clarsimp
   apply (metis of_nat_power n_less_equal_power_2 of_nat_Suc power_Suc)
   done
 
 lemma eq_mask_less:
   fixes w :: "'a::len word"
   assumes eqm: "w = w AND mask n"
   and      sz: "n < len_of TYPE ('a)"
   shows "w < (2::'a word) ^ n"
   by (subst eqm, rule and_mask_less' [OF sz])
 
 lemma of_nat_mono_maybe':
   fixes Y :: "nat"
   assumes xlt: "x < 2 ^ len_of TYPE ('a)"
   assumes ylt: "y < 2 ^ len_of TYPE ('a)"
   shows   "(y < x) = (of_nat y < (of_nat x :: 'a :: len word))"
   apply (subst word_less_nat_alt)
   apply (subst unat_of_nat)+
   apply (subst mod_less)
    apply (rule ylt)
   apply (subst mod_less)
    apply (rule xlt)
   apply simp
   done
 
 lemma of_nat_mono_maybe_le:
   "\<lbrakk>x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow>
   (y \<le> x) = ((of_nat y :: 'a :: len word) \<le> of_nat x)"
   apply (clarsimp simp: le_less)
   apply (rule disj_cong)
    apply (rule of_nat_mono_maybe', assumption+)
   apply auto
   using of_nat_inj apply blast
   done
 
 lemma mask_AND_NOT_mask:
   "(w AND NOT (mask n)) AND mask n = 0"
   for w :: \<open>'a::len word\<close>
   by (rule bit_word_eqI) (simp add: bit_simps)
 
 lemma AND_NOT_mask_plus_AND_mask_eq:
   "(w AND NOT (mask n)) + (w AND mask n) = w"
   for w :: \<open>'a::len word\<close>
   apply (subst disjunctive_add)
   apply (auto simp add: bit_simps)
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_simps)
   done
 
 lemma mask_eqI:
   fixes x :: "'a :: len word"
   assumes m1: "x AND mask n = y AND mask n"
   and     m2: "x AND NOT (mask n) = y AND NOT (mask n)"
   shows "x = y"
 proof -
   have *: \<open>x = x AND mask n OR x AND NOT (mask n)\<close> for x :: \<open>'a word\<close>
     by (rule bit_word_eqI) (auto simp add: bit_simps)
   from assms * [of x] * [of y] show ?thesis
     by simp
 qed
 
 lemma neq_0_no_wrap:
   fixes x :: "'a :: len word"
   shows "\<lbrakk> x \<le> x + y; x \<noteq> 0 \<rbrakk> \<Longrightarrow> x + y \<noteq> 0"
   by clarsimp
 
 lemma unatSuc2:
   fixes n :: "'a :: len word"
   shows "n + 1 \<noteq> 0 \<Longrightarrow> unat (n + 1) = Suc (unat n)"
   by (simp add: add.commute unatSuc)
 
 lemma word_of_nat_le:
   "n \<le> unat x \<Longrightarrow> of_nat n \<le> x"
   apply (simp add: word_le_nat_alt unat_of_nat)
   apply (erule order_trans[rotated])
   apply (simp add: take_bit_eq_mod)
   done
 
 lemma word_unat_less_le:
   "a \<le> of_nat b \<Longrightarrow> unat a \<le> b"
   by (metis eq_iff le_cases le_unat_uoi word_of_nat_le)
 
 lemma mask_Suc_0 : "mask (Suc 0) = (1 :: 'a::len word)"
   by (simp add: mask_eq_decr_exp)
 
 lemma bool_mask':
   fixes x :: "'a :: len word"
   shows "2 < LENGTH('a) \<Longrightarrow> (0 < x AND 1) = (x AND 1 = 1)"
   by (simp add: and_one_eq mod_2_eq_odd)
 
 lemma ucast_ucast_add:
   fixes x :: "'a :: len word"
   fixes y :: "'b :: len word"
   shows
   "LENGTH('b) \<ge> LENGTH('a) \<Longrightarrow>
     ucast (ucast x + y) = x + ucast y"
   apply transfer
   apply simp
   apply (subst (2) take_bit_add [symmetric])
   apply (subst take_bit_add [symmetric])
   apply simp
   done
 
 lemma lt1_neq0:
   fixes x :: "'a :: len word"
   shows "(1 \<le> x) = (x \<noteq> 0)" by unat_arith
 
 lemma word_plus_one_nonzero:
   fixes x :: "'a :: len word"
   shows "\<lbrakk>x \<le> x + y; y \<noteq> 0\<rbrakk> \<Longrightarrow> x + 1 \<noteq> 0"
   apply (subst lt1_neq0 [symmetric])
   apply (subst olen_add_eqv [symmetric])
   apply (erule word_random)
   apply (simp add: lt1_neq0)
   done
 
 lemma word_sub_plus_one_nonzero:
   fixes n :: "'a :: len word"
   shows "\<lbrakk>n' \<le> n; n' \<noteq> 0\<rbrakk> \<Longrightarrow> (n - n') + 1 \<noteq> 0"
   apply (subst lt1_neq0 [symmetric])
   apply (subst olen_add_eqv [symmetric])
   apply (rule word_random [where x' = n'])
    apply simp
    apply (erule word_sub_le)
   apply (simp add: lt1_neq0)
   done
 
 lemma word_le_minus_mono_right:
   fixes x :: "'a :: len word"
   shows "\<lbrakk> z \<le> y; y \<le> x; z \<le> x \<rbrakk> \<Longrightarrow> x - y \<le> x - z"
   apply (rule word_sub_mono)
      apply simp
     apply assumption
    apply (erule word_sub_le)
   apply (erule word_sub_le)
   done
 
 lemma word_0_sle_from_less:
   \<open>0 \<le>s x\<close> if \<open>x < 2 ^ (LENGTH('a) - 1)\<close> for x :: \<open>'a::len word\<close>
   using that
   apply transfer
   apply (cases \<open>LENGTH('a)\<close>)
    apply simp_all
   apply (metis bit_take_bit_iff min_def nat_less_le not_less_eq take_bit_int_eq_self_iff take_bit_take_bit)
   done
 
 lemma ucast_sub_ucast:
   fixes x :: "'a::len word"
   assumes "y \<le> x"
   assumes T: "LENGTH('a) \<le> LENGTH('b)"
   shows "ucast (x - y) = (ucast x - ucast y :: 'b::len word)"
 proof -
   from T
   have P: "unat x < 2 ^ LENGTH('b)" "unat y < 2 ^ LENGTH('b)"
     by (fastforce intro!: less_le_trans[OF unat_lt2p])+
   then show ?thesis
     by (simp add: unat_arith_simps unat_ucast assms[simplified unat_arith_simps])
 qed
 
 lemma word_1_0:
   "\<lbrakk>a + (1::('a::len) word) \<le> b; a < of_nat x\<rbrakk> \<Longrightarrow> a < b"
   apply transfer
   apply (subst (asm) take_bit_incr_eq)
    apply (auto simp add: diff_less_eq)
   using take_bit_int_less_exp le_less_trans by blast
 
 lemma unat_of_nat_less:"\<lbrakk> a < b; unat b = c \<rbrakk> \<Longrightarrow> a < of_nat c"
   by fastforce
 
 lemma word_le_plus_1: "\<lbrakk> (y::('a::len) word) < y + n; a < n \<rbrakk> \<Longrightarrow> y + a \<le> y + a + 1"
   by unat_arith
 
 lemma word_le_plus:"\<lbrakk>(a::('a::len) word) < a + b; c < b\<rbrakk> \<Longrightarrow> a \<le> a + c"
   by (metis order_less_imp_le word_random)
 
 lemma sint_minus1 [simp]: "(sint x = -1) = (x = -1)"
   apply (cases \<open>LENGTH('a)\<close>)
    apply simp_all
   apply transfer
   apply (simp only: flip: signed_take_bit_eq_iff_take_bit_eq)
   apply simp
   done
 
 lemma sint_0 [simp]: "(sint x = 0) = (x = 0)"
   by (fact signed_eq_0_iff)
 
 (* It is not always that case that "sint 1 = 1", because of 1-bit word sizes.
  * This lemma produces the different cases. *)
 lemma sint_1_cases:
   P if \<open>\<lbrakk> len_of TYPE ('a::len) = 1; (a::'a word) = 0; sint a = 0 \<rbrakk> \<Longrightarrow> P\<close>
      \<open>\<lbrakk> len_of TYPE ('a) = 1; a = 1; sint (1 :: 'a word) = -1 \<rbrakk> \<Longrightarrow> P\<close>
      \<open>\<lbrakk> len_of TYPE ('a) > 1; sint (1 :: 'a word) = 1 \<rbrakk> \<Longrightarrow> P\<close>
 proof (cases \<open>LENGTH('a) = 1\<close>)
   case True
   then have \<open>a = 0 \<or> a = 1\<close>
     by transfer auto
   with True that show ?thesis
     by auto
 next
   case False
   with that show ?thesis
     by (simp add: less_le Suc_le_eq)
 qed
 
 lemma sint_int_min:
   "sint (- (2 ^ (LENGTH('a) - Suc 0)) :: ('a::len) word) = - (2 ^ (LENGTH('a) - Suc 0))"
   apply (cases \<open>LENGTH('a)\<close>)
    apply simp_all
   apply transfer
   apply (simp add: signed_take_bit_int_eq_self)
   done
 
 lemma sint_int_max_plus_1:
   "sint (2 ^ (LENGTH('a) - Suc 0) :: ('a::len) word) = - (2 ^ (LENGTH('a) - Suc 0))"
   apply (cases \<open>LENGTH('a)\<close>)
    apply simp_all
   apply (subst word_of_int_2p [symmetric])
   apply (subst int_word_sint)
   apply simp
   done
 
 lemma uint_range':
   \<open>0 \<le> uint x \<and> uint x < 2 ^ LENGTH('a)\<close>
   for x :: \<open>'a::len word\<close>
   by transfer simp
 
 lemma sint_of_int_eq:
   "\<lbrakk> - (2 ^ (LENGTH('a) - 1)) \<le> x; x < 2 ^ (LENGTH('a) - 1) \<rbrakk> \<Longrightarrow> sint (of_int x :: ('a::len) word) = x"
   by (simp add: signed_take_bit_int_eq_self signed_of_int)
 
 lemma of_int_sint:
   "of_int (sint a) = a"
   by simp
 
 lemma sint_ucast_eq_uint:
     "\<lbrakk> \<not> is_down (ucast :: ('a::len word \<Rightarrow> 'b::len word)) \<rbrakk>
             \<Longrightarrow> sint ((ucast :: ('a::len word \<Rightarrow> 'b::len word)) x) = uint x"
   apply transfer
   apply (simp add: signed_take_bit_take_bit)
   done
 
 lemma word_less_nowrapI':
   "(x :: 'a :: len word) \<le> z - k \<Longrightarrow> k \<le> z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
   by uint_arith
 
 lemma mask_plus_1:
   "mask n + 1 = (2 ^ n :: 'a::len word)"
   by (clarsimp simp: mask_eq_decr_exp)
 
 lemma unat_inj: "inj unat"
   by (metis eq_iff injI word_le_nat_alt)
 
 lemma unat_ucast_upcast:
   "is_up (ucast :: 'b word \<Rightarrow> 'a word)
       \<Longrightarrow> unat (ucast x :: ('a::len) word) = unat (x :: ('b::len) word)"
   unfolding ucast_eq unat_eq_nat_uint
   apply transfer
   apply simp
   done
 
 lemma ucast_mono:
   "\<lbrakk> (x :: 'b :: len word) < y; y < 2 ^ LENGTH('a) \<rbrakk>
    \<Longrightarrow> ucast x < ((ucast y) :: 'a :: len word)"
   apply (simp only: flip: ucast_nat_def)
   apply (rule of_nat_mono_maybe)
   apply (rule unat_less_helper)
   apply simp
   apply (simp add: word_less_nat_alt)
   done
 
 lemma ucast_mono_le:
   "\<lbrakk>x \<le> y; y < 2 ^ LENGTH('b)\<rbrakk> \<Longrightarrow> (ucast (x :: 'a :: len word) :: 'b :: len word) \<le> ucast y"
   apply (simp only: flip: ucast_nat_def)
   apply (subst of_nat_mono_maybe_le[symmetric])
     apply (rule unat_less_helper)
     apply simp
    apply (rule unat_less_helper)
    apply (erule le_less_trans)
   apply (simp_all add: word_le_nat_alt)
   done
 
 lemma ucast_mono_le':
   "\<lbrakk> unat y < 2 ^ LENGTH('b); LENGTH('b::len) < LENGTH('a::len); x \<le> y \<rbrakk>
    \<Longrightarrow> ucast x \<le> (ucast y :: 'b word)" for x y :: \<open>'a::len word\<close>
   by (auto simp: word_less_nat_alt intro: ucast_mono_le)
 
 lemma neg_mask_add_mask:
   "((x:: 'a :: len word) AND NOT (mask n)) + (2 ^ n - 1) = x OR mask n"
   unfolding mask_2pm1 [symmetric]
   apply (subst word_plus_and_or_coroll; rule bit_word_eqI)
    apply (auto simp add: bit_simps)
   done
 
 lemma le_step_down_word:"\<lbrakk>(i::('a::len) word) \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by unat_arith
 
 lemma le_step_down_word_2:
   fixes x :: "'a::len word"
   shows "\<lbrakk>x \<le>  y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1"
   by (subst (asm) word_le_less_eq,
       clarsimp,
       simp add: word_le_minus_one_leq)
 
 lemma NOT_mask_AND_mask[simp]: "(w AND mask n) AND NOT (mask n) = 0"
   by (rule bit_eqI) (simp add: bit_simps)
 
 lemma and_and_not[simp]:"(a AND b) AND NOT b = 0"
   for a b :: \<open>'a::len word\<close>
   apply (subst word_bw_assocs(1))
   apply clarsimp
   done
 
 lemma ex_mask_1[simp]: "(\<exists>x. mask x = (1 :: 'a::len word))"
   apply (rule_tac x=1 in exI)
   apply (simp add:mask_eq_decr_exp)
   done
 
 lemma not_switch:"NOT a = x \<Longrightarrow> a = NOT x"
   by auto
 
 lemma test_bit_eq_iff: "bit u = bit v \<longleftrightarrow> u = v"
   for u v :: "'a::len word"
   by (auto intro: bit_eqI simp add: fun_eq_iff)
 
 lemma test_bit_size: "bit w n \<Longrightarrow> n < size w"
   for w :: "'a::len word"
   by transfer simp
 
 lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). bit x n = bit y n)" (is \<open>?P \<longleftrightarrow> ?Q\<close>)
   for x y :: "'a::len word"
   by transfer (auto simp add: bit_eq_iff bit_take_bit_iff)
 
 lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> bit u n = bit v n) \<Longrightarrow> u = v"
   for u :: "'a::len word"
   by (simp add: word_size word_eq_iff)
 
 lemma word_eqD: "u = v \<Longrightarrow> bit u x = bit v x"
   for u v :: "'a::len word"
   by simp
 
 lemma test_bit_bin': "bit w n \<longleftrightarrow> n < size w \<and> bit (uint w) n"
   by transfer (simp add: bit_take_bit_iff)
 
 lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
 
 lemma word_test_bit_def:
   \<open>bit a = bit (uint a)\<close>
   by transfer (simp add: fun_eq_iff bit_take_bit_iff)
 
 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
 
 lemma word_test_bit_transfer [transfer_rule]:
   "(rel_fun pcr_word (rel_fun (=) (=)))
     (\<lambda>x n. n < LENGTH('a) \<and> bit x n) (bit :: 'a::len word \<Rightarrow> _)"
   by transfer_prover
 
 lemma test_bit_wi:
   "bit (word_of_int x :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit x n"
   by transfer simp
 
 lemma word_ops_nth_size:
   "n < size x \<Longrightarrow>
     bit (x OR y) n = (bit x n | bit y n) \<and>
     bit (x AND y) n = (bit x n \<and> bit y n) \<and>
     bit (x XOR y) n = (bit x n \<noteq> bit y n) \<and>
     bit (NOT x) n = (\<not> bit x n)"
   for x :: "'a::len word"
   by transfer (simp add: bit_or_iff bit_and_iff bit_xor_iff bit_not_iff)
 
 lemma word_ao_nth:
   "bit (x OR y) n = (bit x n | bit y n) \<and>
     bit (x AND y) n = (bit x n \<and> bit y n)"
   for x :: "'a::len word"
   by transfer (auto simp add: bit_or_iff bit_and_iff)
 
 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
 
 lemma nth_sint:
   fixes w :: "'a::len word"
   defines "l \<equiv> LENGTH('a)"
   shows "bit (sint w) n = (if n < l - 1 then bit w n else bit w (l - 1))"
   unfolding sint_uint l_def
   by (auto simp: bit_signed_take_bit_iff word_test_bit_def not_less min_def)
 
 lemma test_bit_2p: "bit (word_of_int (2 ^ n)::'a::len word) m \<longleftrightarrow> m = n \<and> m < LENGTH('a)"
   by transfer (auto simp add: bit_exp_iff)
 
 lemma nth_w2p: "bit ((2::'a::len word) ^ n) m \<longleftrightarrow> m = n \<and> m < LENGTH('a::len)"
   by transfer (auto simp add: bit_exp_iff)
 
 lemma bang_is_le: "bit x m \<Longrightarrow> 2 ^ m \<le> x"
   for x :: "'a::len word"
   apply (rule xtrans(3))
    apply (rule_tac [2] y = "x" in le_word_or2)
   apply (rule word_eqI)
   apply (auto simp add: word_ao_nth nth_w2p word_size)
   done
 
 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
 lemmas msb1 = msb0 [where i = 0]
 
 lemma test_bit_1 [iff]: "bit (1 :: 'a::len word) n \<longleftrightarrow> n = 0"
   by transfer (auto simp add: bit_1_iff)
 
 lemma nth_0: "\<not> bit (0 :: 'a::len word) n"
   by transfer simp
 
 lemma nth_minus1: "bit (-1 :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a)"
   by transfer simp
 
 lemma nth_ucast:
   "bit (ucast w::'a::len word) n = (bit w n \<and> n < LENGTH('a))"
   by transfer (simp add: bit_take_bit_iff ac_simps)
 
 lemma drop_bit_numeral_bit0_1 [simp]:
   \<open>drop_bit (Suc 0) (numeral k) =
     (word_of_int (drop_bit (Suc 0) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
   by (metis Word_eq_word_of_int drop_bit_word.abs_eq of_int_numeral)
 
 lemma nth_mask:
   \<open>bit (mask n :: 'a::len word) i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close>
   by (auto simp add: word_size Word.bit_mask_iff)
 
 lemma nth_slice: "bit (slice n w :: 'a::len word) m = (bit w (m + n) \<and> m < LENGTH('a))"
   apply (auto simp add: bit_simps less_diff_conv dest: bit_imp_le_length)
   using bit_imp_le_length
   apply fastforce
   done
 
 lemma test_bit_cat [OF refl]:
   "wc = word_cat a b \<Longrightarrow> bit wc n = (n < size wc \<and>
     (if n < size b then bit b n else bit a (n - size b)))"
   apply (simp add: word_size not_less; transfer)
        apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff)
   done
 
 \<comment> \<open>keep quantifiers for use in simplification\<close>
 lemma test_bit_split':
   "word_split c = (a, b) \<longrightarrow>
     (\<forall>n m.
       bit b n = (n < size b \<and> bit c n) \<and>
       bit a m = (m < size a \<and> bit c (m + size b)))"
   by (auto simp add: word_split_bin' bit_unsigned_iff word_size bit_drop_bit_eq ac_simps
            dest: bit_imp_le_length)
 
 lemma test_bit_split:
   "word_split c = (a, b) \<Longrightarrow>
     (\<forall>n::nat. bit b n \<longleftrightarrow> n < size b \<and> bit c n) \<and>
     (\<forall>m::nat. bit a m \<longleftrightarrow> m < size a \<and> bit c (m + size b))"
   by (simp add: test_bit_split')
 
 lemma test_bit_split_eq:
   "word_split c = (a, b) \<longleftrightarrow>
     ((\<forall>n::nat. bit b n = (n < size b \<and> bit c n)) \<and>
      (\<forall>m::nat. bit a m = (m < size a \<and> bit c (m + size b))))"
   apply (rule_tac iffI)
    apply (rule_tac conjI)
     apply (erule test_bit_split [THEN conjunct1])
    apply (erule test_bit_split [THEN conjunct2])
   apply (case_tac "word_split c")
   apply (frule test_bit_split)
   apply (erule trans)
   apply (fastforce intro!: word_eqI simp add: word_size)
   done
 
 lemma test_bit_rcat:
   "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> bit rc n =
     (n < size rc \<and> n div sw < size wl \<and> bit ((rev wl) ! (n div sw)) (n mod sw))"
   for wl :: "'a::len word list"
   by (simp add: word_size word_rcat_def rev_map bit_horner_sum_uint_exp_iff bit_simps not_le)
 
 lemmas test_bit_cong = arg_cong [where f = "bit", THEN fun_cong]
 
 lemma max_test_bit: "bit (- 1::'a::len word) n \<longleftrightarrow> n < LENGTH('a)"
   by (fact nth_minus1)
 
 lemma map_nth_0 [simp]: "map (bit (0::'a::len word)) xs = replicate (length xs) False"
   by (simp flip: map_replicate_const)
 
 lemma word_and_1:
   "n AND 1 = (if bit n 0 then 1 else 0)" for n :: "_ word"
   by (rule bit_word_eqI) (auto simp add: bit_and_iff bit_1_iff intro: gr0I)
 
 lemma test_bit_1':
   "bit (1 :: 'a :: len word) n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
   by simp
 
 lemma nth_w2p_same:
   "bit (2^n :: 'a :: len word) n = (n < LENGTH('a))"
   by (simp add: nth_w2p)
 
 lemma word_leI:
   "(\<And>n.  \<lbrakk>n < size (u::'a::len word); bit u n \<rbrakk> \<Longrightarrow> bit (v::'a::len word) n) \<Longrightarrow> u <= v"
   apply (rule order_trans [of u \<open>u AND v\<close> v])
    apply (rule eq_refl)
    apply (rule bit_word_eqI)
    apply (auto simp add: bit_simps word_and_le1 word_size)
   done
 
 lemma bang_eq:
   fixes x :: "'a::len word"
   shows "(x = y) = (\<forall>n. bit x n = bit y n)"
   by (auto intro!: bit_eqI)
 
 lemma neg_mask_test_bit:
   "bit (NOT(mask n) :: 'a :: len word) m = (n \<le> m \<and> m < LENGTH('a))"
   by (auto simp add: bit_simps)
 
 lemma upper_bits_unset_is_l2p:
   \<open>(\<forall>n' \<ge> n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n') \<longleftrightarrow> (p < 2 ^ n)\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
     if \<open>n < LENGTH('a)\<close>
     for p :: "'a :: len word"
 proof
   assume ?Q
   then show ?P
     by (meson bang_is_le le_less_trans not_le word_power_increasing)
 next
   assume ?P
   have \<open>take_bit n p = p\<close>
   proof (rule bit_word_eqI)
     fix q
     assume \<open>q < LENGTH('a)\<close>
     show \<open>bit (take_bit n p) q \<longleftrightarrow> bit p q\<close>
     proof (cases \<open>q < n\<close>)
       case True
       then show ?thesis
         by (auto simp add: bit_simps)
     next
       case False
       then have \<open>n \<le> q\<close>
         by simp
       with \<open>?P\<close> \<open>q < LENGTH('a)\<close> have \<open>\<not> bit p q\<close>
         by simp
       then show ?thesis
         by (simp add: bit_simps)
     qed
   qed
   with that show ?Q
     using take_bit_word_eq_self_iff [of n p] by auto
 qed
 
 lemma less_2p_is_upper_bits_unset:
   "p < 2 ^ n \<longleftrightarrow> n < LENGTH('a) \<and> (\<forall>n' \<ge> n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n')" for p :: "'a :: len word"
   by (meson le_less_trans le_mask_iff_lt_2n upper_bits_unset_is_l2p word_zero_le)
 
 lemma test_bit_over:
   "n \<ge> size (x::'a::len word) \<Longrightarrow> (bit x n) = False"
   by transfer auto
 
 lemma le_mask_high_bits:
   "w \<le> mask n \<longleftrightarrow> (\<forall>i \<in> {n ..< size w}. \<not> bit w i)"
   for w :: \<open>'a::len word\<close>
   apply (auto simp add: bit_simps word_size less_eq_mask_iff_take_bit_eq_self)
    apply (metis bit_take_bit_iff leD)
   apply (metis atLeastLessThan_iff leI take_bit_word_eq_self_iff upper_bits_unset_is_l2p)
   done
 
 lemma test_bit_conj_lt:
   "(bit x m \<and> m < LENGTH('a)) = bit x m" for x :: "'a :: len word"
   using test_bit_bin by blast
 
 lemma neg_test_bit:
   "bit (NOT x) n = (\<not> bit x n \<and> n < LENGTH('a))" for x :: "'a::len word"
   by (cases "n < LENGTH('a)") (auto simp add: test_bit_over word_ops_nth_size word_size)
 
 lemma nth_bounded:
   "\<lbrakk>bit (x :: 'a :: len word) n; x < 2 ^ m; m \<le> len_of TYPE ('a)\<rbrakk> \<Longrightarrow> n < m"
   apply (rule ccontr)
   apply (auto simp add: not_less)
   apply (meson bit_imp_le_length bit_uint_iff less_2p_is_upper_bits_unset test_bit_bin)
   done
 
 lemma and_neq_0_is_nth:
   \<open>x AND y \<noteq> 0 \<longleftrightarrow> bit x n\<close> if \<open>y = 2 ^ n\<close> for x y :: \<open>'a::len word\<close>
   apply (simp add: bit_eq_iff bit_simps)
   using that apply (simp add: bit_simps not_le)
   apply transfer
   apply auto
   done
 
 lemma nth_is_and_neq_0:
   "bit (x::'a::len word) n = (x AND 2 ^ n \<noteq> 0)"
   by (subst and_neq_0_is_nth; rule refl)
 
 lemma max_word_not_less [simp]:
    "\<not> - 1 < x" for x :: \<open>'a::len word\<close>
   by (fact word_order.extremum_strict)
 
 lemma bit_twiddle_min:
   "(y::'a::len word) XOR (((x::'a::len word) XOR y) AND (if x < y then -1 else 0)) = min x y"
   by (rule bit_eqI) (auto simp add: bit_simps)
 
 lemma bit_twiddle_max:
   "(x::'a::len word) XOR (((x::'a::len word) XOR y) AND (if x < y then -1 else 0)) = max x y"
   by (rule bit_eqI) (auto simp add: bit_simps max_def)
 
 lemma swap_with_xor:
   "\<lbrakk>(x::'a::len word) = a XOR b; y = b XOR x; z = x XOR y\<rbrakk> \<Longrightarrow> z = b \<and> y = a"
   by (auto intro: bit_word_eqI simp add: bit_simps)
 
 lemma le_mask_imp_and_mask:
   "(x::'a::len word) \<le> mask n \<Longrightarrow> x AND mask n = x"
   by (metis and_mask_eq_iff_le_mask)
 
 lemma or_not_mask_nop:
   "((x::'a::len word) OR NOT (mask n)) AND mask n = x AND mask n"
   by (metis word_and_not word_ao_dist2 word_bw_comms(1) word_log_esimps(3))
 
 lemma mask_subsume:
   "\<lbrakk>n \<le> m\<rbrakk> \<Longrightarrow> ((x::'a::len word) OR y AND mask n) AND NOT (mask m) = x AND NOT (mask m)"
   by (rule bit_word_eqI) (auto simp add: bit_simps word_size)
 
 lemma and_mask_0_iff_le_mask:
   fixes w :: "'a::len word"
   shows "(w AND NOT(mask n) = 0) = (w \<le> mask n)"
   by (simp add: mask_eq_0_eq_x le_mask_imp_and_mask and_mask_eq_iff_le_mask)
 
 lemma mask_twice2:
   "n \<le> m \<Longrightarrow> ((x::'a::len word) AND mask m) AND mask n = x AND mask n"
   by (metis mask_twice min_def)
 
 lemma uint_2_id:
   "LENGTH('a) \<ge> 2 \<Longrightarrow> uint (2::('a::len) word) = 2"
   by simp
 
 lemma div_of_0_id[simp]:"(0::('a::len) word) div n = 0"
   by (simp add: word_div_def)
 
 lemma degenerate_word:"LENGTH('a) = 1 \<Longrightarrow> (x::('a::len) word) = 0 \<or> x = 1"
   by (metis One_nat_def less_irrefl_nat sint_1_cases)
 
 lemma div_by_0_word:"(x::('a::len) word) div 0 = 0"
   by (metis div_0 div_by_0 unat_0 word_arith_nat_defs(6) word_div_1)
 
 lemma div_less_dividend_word:"\<lbrakk>x \<noteq> 0; n \<noteq> 1\<rbrakk> \<Longrightarrow> (x::('a::len) word) div n < x"
   apply (cases \<open>n = 0\<close>)
    apply clarsimp
    apply (simp add:word_neq_0_conv)
   apply (subst word_arith_nat_div)
   apply (rule word_of_nat_less)
   apply (rule div_less_dividend)
   using unat_eq_zero word_unat_Rep_inject1 apply force
   apply (simp add:unat_gt_0)
   done
 
 lemma word_less_div:
   fixes x :: "('a::len) word"
     and y :: "('a::len) word"
   shows "x div y = 0 \<Longrightarrow> y = 0 \<or> x < y"
   apply (case_tac "y = 0", clarsimp+)
   by (metis One_nat_def Suc_le_mono le0 le_div_geq not_less unat_0 unat_div unat_gt_0 word_less_nat_alt zero_less_one)
 
 lemma not_degenerate_imp_2_neq_0:"LENGTH('a) > 1 \<Longrightarrow> (2::('a::len) word) \<noteq> 0"
   by (metis numerals(1) power_not_zero power_zero_numeral)
 
 lemma word_overflow:"(x::('a::len) word) + 1 > x \<or> x + 1 = 0"
   apply clarsimp
   by (metis diff_0 eq_diff_eq less_x_plus_1)
 
 lemma word_overflow_unat:"unat ((x::('a::len) word) + 1) = unat x + 1 \<or> x + 1 = 0"
   by (metis Suc_eq_plus1 add.commute unatSuc)
 
 lemma even_word_imp_odd_next:"even (unat (x::('a::len) word)) \<Longrightarrow> x + 1 = 0 \<or> odd (unat (x + 1))"
   apply (cut_tac x=x in word_overflow_unat)
   apply clarsimp
   done
 
 lemma odd_word_imp_even_next:"odd (unat (x::('a::len) word)) \<Longrightarrow> x + 1 = 0 \<or> even (unat (x + 1))"
   apply (cut_tac x=x in word_overflow_unat)
   apply clarsimp
   done
 
 lemma overflow_imp_lsb:"(x::('a::len) word) + 1 = 0 \<Longrightarrow> bit x 0"
   using even_plus_one_iff [of x] by simp
 
 lemma odd_iff_lsb:"odd (unat (x::('a::len) word)) = bit x 0"
   by transfer (simp add: even_nat_iff)
 
 lemma of_nat_neq_iff_word:
       "x mod 2 ^ LENGTH('a) \<noteq> y mod 2 ^ LENGTH('a) \<Longrightarrow>
          (((of_nat x)::('a::len) word) \<noteq> of_nat y) = (x \<noteq> y)"
   apply (rule iffI)
    apply (case_tac "x = y")
    apply (subst (asm) of_nat_eq_iff[symmetric])
    apply auto
   apply (case_tac "((of_nat x)::('a::len) word) = of_nat y")
   apply auto
    apply (metis unat_of_nat)
   done
 
 lemma lsb_this_or_next: "\<not> (bit ((x::('a::len) word) + 1) 0) \<Longrightarrow> bit x 0"
   by simp
 
 lemma mask_or_not_mask:
   "x AND mask n OR x AND NOT (mask n) = x"
   for x :: \<open>'a::len word\<close>
   apply (subst word_oa_dist, simp)
   apply (subst word_oa_dist2, simp)
   done
 
 lemma word_gr0_conv_Suc: "(m::'a::len word) > 0 \<Longrightarrow> \<exists>n. m = n + 1"
   by (metis add.commute add_minus_cancel)
 
 lemma revcast_down_us [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (signed_drop_bit n w)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_simps ac_simps)
   done
 
 lemma revcast_down_ss [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (signed_drop_bit n w)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_simps ac_simps)
   done
 
 lemma revcast_down_uu [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (drop_bit n w)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_simps ac_simps)
   done
 
 lemma revcast_down_su [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (drop_bit n w)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_simps ac_simps)
   done
 
 lemma cast_down_rev [OF refl]:
   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (push_bit n w)"
   for w :: "'a::len word"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_simps)
   done
 
 lemma revcast_up [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
     rc w = push_bit n (ucast w :: 'a::len word)"
   apply (simp add: source_size_def target_size_def)
   apply (rule bit_word_eqI)
   apply (simp add: bit_simps)
   apply auto
   apply (metis add.commute add_diff_cancel_right)
   apply (metis diff_add_inverse2 diff_diff_add)
   done
 
 lemmas rc1 = revcast_up [THEN
   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
 lemmas rc2 = revcast_down_uu [THEN
   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
 
 lemma word_ops_nth:
   fixes x y :: \<open>'a::len word\<close>
   shows
   word_or_nth:  "bit (x OR y) n = (bit x n \<or> bit y n)" and
   word_and_nth: "bit (x AND y) n = (bit x n \<and> bit y n)" and
   word_xor_nth: "bit (x XOR y) n = (bit x n \<noteq> bit y n)"
   by (simp_all add: bit_simps)
 
 lemma word_power_nonzero:
   "\<lbrakk> (x :: 'a::len word) < 2 ^ (LENGTH('a) - n); n < LENGTH('a); x \<noteq> 0 \<rbrakk>
   \<Longrightarrow> x * 2 ^ n \<noteq> 0"
   by (metis gr_implies_not0 mult_eq_0_iff nat_mult_power_less_eq numeral_2_eq_2
     p2_gt_0 unat_eq_zero unat_less_power unat_mult_lem unat_power_lower word_gt_a_gt_0 zero_less_Suc)
 
 lemma less_1_helper:
   "n \<le> m \<Longrightarrow> (n - 1 :: int) < m"
   by arith
 
 lemma div_power_helper:
   "\<lbrakk> x \<le> y; y < LENGTH('a) \<rbrakk> \<Longrightarrow> (2 ^ y - 1) div (2 ^ x :: 'a::len word) = 2 ^ (y - x) - 1"
   apply (simp flip: mask_eq_exp_minus_1 drop_bit_eq_div)
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_simps not_le)
   done
 
 lemma max_word_mask:
   "(- 1 :: 'a::len word) = mask LENGTH('a)"
   by (fact minus_1_eq_mask)
 
 lemmas mask_len_max = max_word_mask[symmetric]
 
 lemma mask_out_first_mask_some:
   "\<lbrakk> x AND NOT (mask n) = y; n \<le> m \<rbrakk> \<Longrightarrow> x AND NOT (mask m) = y AND NOT (mask m)"
   for x y :: \<open>'a::len word\<close>
   by (rule bit_word_eqI) (auto simp add: bit_simps word_size)
 
 lemma mask_lower_twice:
   "n \<le> m \<Longrightarrow> (x AND NOT (mask n)) AND NOT (mask m) = x AND NOT (mask m)"
   for x :: \<open>'a::len word\<close>
   by (rule bit_word_eqI) (auto simp add: bit_simps word_size)
 
 lemma mask_lower_twice2:
   "(a AND NOT (mask n)) AND NOT (mask m) = a AND NOT (mask (max n m))"
   for a :: \<open>'a::len word\<close>
   by (rule bit_word_eqI) (auto simp add: bit_simps)
 
 lemma ucast_and_neg_mask:
   "ucast (x AND NOT (mask n)) = ucast x AND NOT (mask n)"
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_simps dest: bit_imp_le_length)
   done
 
 lemma ucast_and_mask:
   "ucast (x AND mask n) = ucast x AND mask n"
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_simps dest: bit_imp_le_length)
   done
 
 lemma ucast_mask_drop:
   "LENGTH('a :: len) \<le> n \<Longrightarrow> (ucast (x AND mask n) :: 'a word) = ucast x"
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_simps dest: bit_imp_le_length)
   done
 
 lemma mask_exceed:
   "n \<ge> LENGTH('a) \<Longrightarrow> (x::'a::len word) AND NOT (mask n) = 0"
   by (rule bit_word_eqI) (simp add: bit_simps)
 
 lemma word_add_no_overflow:"(x::'a::len word) < - 1 \<Longrightarrow> x < x + 1"
   using less_x_plus_1 order_less_le by blast
 
 lemma lt_plus_1_le_word:
   fixes x :: "'a::len word"
   assumes bound:"n < unat (maxBound::'a word)"
   shows "x < 1 + of_nat n = (x \<le> of_nat n)"
   by (metis add.commute bound max_word_max word_Suc_leq word_not_le word_of_nat_less)
 
 lemma unat_ucast_up_simp:
   fixes x :: "'a::len word"
   assumes "LENGTH('a) \<le> LENGTH('b)"
   shows "unat (ucast x :: 'b::len word) = unat x"
   apply (rule bit_eqI)
   using assms apply (auto simp add: bit_simps dest: bit_imp_le_length)
   done
 
 lemma unat_ucast_less_no_overflow:
   "\<lbrakk>n < 2 ^ LENGTH('a); unat f < n\<rbrakk> \<Longrightarrow> (f::('a::len) word) < of_nat n"
   by (erule (1)  order_le_less_trans[OF _ of_nat_mono_maybe,rotated]) simp
 
 lemma unat_ucast_less_no_overflow_simp:
   "n < 2 ^ LENGTH('a) \<Longrightarrow> (unat f < n) = ((f::('a::len) word) < of_nat n)"
   using unat_less_helper unat_ucast_less_no_overflow by blast
 
 lemma unat_ucast_no_overflow_le:
   assumes no_overflow: "unat b < (2 :: nat) ^ LENGTH('a)"
   and upward_cast: "LENGTH('a) < LENGTH('b)"
   shows "(ucast (f::'a::len word) < (b :: 'b :: len word)) = (unat f < unat b)"
 proof -
   have LR: "ucast f < b \<Longrightarrow> unat f < unat b"
     apply (rule unat_less_helper)
     apply (simp add:ucast_nat_def)
     apply (rule_tac 'b1 = 'b in  ucast_less_ucast[OF order.strict_implies_order, THEN iffD1])
      apply (rule upward_cast)
     apply (simp add: ucast_ucast_mask less_mask_eq word_less_nat_alt
                      unat_power_lower[OF upward_cast] no_overflow)
     done
   have RL: "unat f < unat b \<Longrightarrow> ucast f < b"
   proof-
     assume ineq: "unat f < unat b"
     have "ucast (f::'a::len word) < ((ucast (ucast b ::'a::len word)) :: 'b :: len word)"
       apply (simp add: ucast_less_ucast[OF order.strict_implies_order] upward_cast)
       apply (simp only: flip: ucast_nat_def)
       apply (rule unat_ucast_less_no_overflow[OF no_overflow ineq])
       done
     then show ?thesis
       apply (rule order_less_le_trans)
       apply (simp add:ucast_ucast_mask word_and_le2)
       done
   qed
   then show ?thesis by (simp add:RL LR iffI)
 qed
 
 lemmas ucast_up_mono = ucast_less_ucast[THEN iffD2]
 
 lemma minus_one_word:
   "(-1 :: 'a :: len word) = 2 ^ LENGTH('a) - 1"
   by simp
 
 lemma le_2p_upper_bits:
   "\<lbrakk> (p::'a::len word) \<le> 2^n - 1; n < LENGTH('a) \<rbrakk> \<Longrightarrow>
   \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'"
   by (subst upper_bits_unset_is_l2p; simp)
 
 lemma le2p_bits_unset:
   "p \<le> 2 ^ n - 1 \<Longrightarrow> \<forall>n'\<ge>n. n' < LENGTH('a) \<longrightarrow> \<not> bit (p::'a::len word) n'"
   using upper_bits_unset_is_l2p [where p=p]
   by (cases "n < LENGTH('a)") auto
 
 lemma complement_nth_w2p:
   shows "n' < LENGTH('a) \<Longrightarrow> bit (NOT (2 ^ n :: 'a::len word)) n' = (n' \<noteq> n)"
   by (fastforce simp: word_ops_nth_size word_size nth_w2p)
 
 lemma word_unat_and_lt:
   "unat x < n \<or> unat y < n \<Longrightarrow> unat (x AND y) < n"
   by (meson le_less_trans word_and_le1 word_and_le2 word_le_nat_alt)
 
 lemma word_unat_mask_lt:
   "m \<le> size w \<Longrightarrow> unat ((w::'a::len word) AND mask m) < 2 ^ m"
   by (rule word_unat_and_lt) (simp add: unat_mask word_size)
 
 lemma word_sless_sint_le:"x <s y \<Longrightarrow> sint x \<le> sint y - 1"
   by (metis word_sless_alt zle_diff1_eq)
 
 lemma upper_trivial:
   fixes x :: "'a::len word"
   shows "x \<noteq> 2 ^ LENGTH('a) - 1 \<Longrightarrow> x < 2 ^ LENGTH('a) - 1"
   by (simp add: less_le)
 
 lemma constraint_expand:
   fixes x :: "'a::len word"
   shows "x \<in> {y. lower \<le> y \<and> y \<le> upper} = (lower \<le> x \<and> x \<le> upper)"
   by (rule mem_Collect_eq)
 
 lemma card_map_elide:
   "card ((of_nat :: nat \<Rightarrow> 'a::len word) ` {0..<n}) = card {0..<n}"
   if "n \<le> CARD('a::len word)"
 proof -
   let ?of_nat = "of_nat :: nat \<Rightarrow> 'a word"
   have "inj_on ?of_nat {i. i < CARD('a word)}"
     by (rule inj_onI) (simp add: card_word of_nat_inj)
   moreover have "{0..<n} \<subseteq> {i. i < CARD('a word)}"
     using that by auto
   ultimately have "inj_on ?of_nat {0..<n}"
     by (rule inj_on_subset)
   then show ?thesis
     by (simp add: card_image)
 qed
 
 lemma card_map_elide2:
   "n \<le> CARD('a::len word) \<Longrightarrow> card ((of_nat::nat \<Rightarrow> 'a::len word) ` {0..<n}) = n"
   by (subst card_map_elide) clarsimp+
 
 lemma eq_ucast_ucast_eq:
   "LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> x = ucast y \<Longrightarrow> ucast x = y"
   for x :: "'a::len word" and y :: "'b::len word"
   by transfer simp
 
 lemma le_ucast_ucast_le:
   "x \<le> ucast y \<Longrightarrow> ucast x \<le> y"
   for x :: "'a::len word" and y :: "'b::len word"
   by (smt le_unat_uoi linorder_not_less order_less_imp_le ucast_nat_def unat_arith_simps(1))
 
 lemma less_ucast_ucast_less:
   "LENGTH('b) \<le> LENGTH('a) \<Longrightarrow> x < ucast y \<Longrightarrow> ucast x < y"
   for x :: "'a::len word" and y :: "'b::len word"
   by (metis ucast_nat_def unat_mono unat_ucast_up_simp word_of_nat_less)
 
 lemma ucast_le_ucast:
   "LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> (ucast x \<le> (ucast y::'b::len word)) = (x \<le> y)"
   for x :: "'a::len word"
   by (simp add: unat_arith_simps(1) unat_ucast_up_simp)
 
 lemmas ucast_up_mono_le = ucast_le_ucast[THEN iffD2]
 
 lemma ucast_or_distrib:
   fixes x :: "'a::len word"
   fixes y :: "'a::len word"
   shows "(ucast (x OR y) :: ('b::len) word) = ucast x OR ucast y"
   by (fact unsigned_or_eq)
 
 lemma word_exists_nth:
   "(w::'a::len word) \<noteq> 0 \<Longrightarrow> \<exists>i. bit w i"
   by (auto simp add: bit_eq_iff)
 
 lemma max_word_not_0 [simp]:
   "- 1 \<noteq> (0 :: 'a::len word)"
   by simp
 
 lemma unat_max_word_pos[simp]: "0 < unat (- 1 :: 'a::len word)"
   using unat_gt_0 [of \<open>- 1 :: 'a::len word\<close>] by simp
 
 
 (* Miscellaneous conditional injectivity rules. *)
 
 lemma mult_pow2_inj:
   assumes ws: "m + n \<le> LENGTH('a)"
   assumes le: "x \<le> mask m" "y \<le> mask m"
   assumes eq: "x * 2 ^ n = y * (2 ^ n::'a::len word)"
   shows "x = y"
 proof (rule bit_word_eqI)
   fix q
   assume \<open>q < LENGTH('a)\<close>
   from eq have \<open>push_bit n x = push_bit n y\<close>
     by (simp add: push_bit_eq_mult)
   moreover from le have \<open>take_bit m x = x\<close> \<open>take_bit m y = y\<close>
     by (simp_all add: less_eq_mask_iff_take_bit_eq_self)
   ultimately have \<open>push_bit n (take_bit m x) = push_bit n (take_bit m y)\<close>
     by simp_all
   with \<open>q < LENGTH('a)\<close> ws show \<open>bit x q \<longleftrightarrow> bit y q\<close>
     apply (simp add: push_bit_take_bit)
     unfolding bit_eq_iff
     apply (simp add: bit_simps not_le)
     apply (metis (full_types) \<open>take_bit m x = x\<close> \<open>take_bit m y = y\<close> add.commute add_diff_cancel_right' add_less_cancel_right bit_take_bit_iff le_add2 less_le_trans)
     done
 qed
 
 lemma word_of_nat_inj:
   assumes bounded: "x < 2 ^ LENGTH('a)" "y < 2 ^ LENGTH('a)"
   assumes of_nats: "of_nat x = (of_nat y :: 'a::len word)"
   shows "x = y"
   by (rule contrapos_pp[OF of_nats]; cases "x < y"; cases "y < x")
      (auto dest: bounded[THEN of_nat_mono_maybe])
 
 lemma word_of_int_bin_cat_eq_iff:
   "(word_of_int (concat_bit LENGTH('b) (uint b) (uint a))::'c::len word) =
   word_of_int (concat_bit LENGTH('b) (uint d) (uint c)) \<longleftrightarrow> b = d \<and> a = c"
   if "LENGTH('a) + LENGTH('b) \<le> LENGTH('c)"
   for a::"'a::len word" and b::"'b::len word"
 proof -
   from that show ?thesis
   using that concat_bit_eq_iff [of \<open>LENGTH('b)\<close> \<open>uint b\<close> \<open>uint a\<close> \<open>uint d\<close> \<open>uint c\<close>]
   apply (simp add: word_of_int_eq_iff take_bit_int_eq_self flip: word_eq_iff_unsigned)
   apply (simp add: concat_bit_def take_bit_int_eq_self bintr_uint take_bit_push_bit)
   done
 qed
 
 lemma word_cat_inj: "(word_cat a b::'c::len word) = word_cat c d \<longleftrightarrow> a = c \<and> b = d"
   if "LENGTH('a) + LENGTH('b) \<le> LENGTH('c)"
   for a::"'a::len word" and b::"'b::len word"
   using word_of_int_bin_cat_eq_iff [OF that, of b a d c]
   by (simp add: word_cat_eq' ac_simps)
 
 lemma p2_eq_1: "2 ^ n = (1::'a::len word) \<longleftrightarrow> n = 0"
 proof -
   have "2 ^ n = (1::'a word) \<Longrightarrow> n = 0"
     by (metis One_nat_def not_less one_less_numeral_iff p2_eq_0 p2_gt_0 power_0 power_0
         power_inject_exp semiring_norm(76) unat_power_lower zero_neq_one)
   then show ?thesis by auto
 qed
 
 end
 
 lemmas word_div_less = div_word_less
 
 (* 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)
 
 lemma word_mod_by_0: "k mod (0::'a::len word) = k"
   by (simp add: word_arith_nat_mod)
 
 end
diff --git a/thys/Word_Lib/Word_32.thy b/thys/Word_Lib/Word_32.thy
--- a/thys/Word_Lib/Word_32.thy
+++ b/thys/Word_Lib/Word_32.thy
@@ -1,345 +1,177 @@
 (*
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section "Words of Length 32"
 
 theory Word_32
   imports
     Word_Lemmas
     Word_Syntax
     Word_Names
     Rsplit
     More_Word_Operations
     Bitwise
 begin
 
 context
   includes bit_operations_syntax
 begin
 
 type_synonym word32 = "32 word"
 lemma len32: "len_of (x :: 32 itself) = 32" by simp
 
 type_synonym sword32 = "32 sword"
 
-type_synonym machine_word_len = 32
-type_synonym machine_word = "machine_word_len word"
-
-definition word_bits :: nat
-where
-  "word_bits = LENGTH(machine_word_len)"
-
-text \<open>The following two are numerals so they can be used as nats and words.\<close>
-definition word_size_bits :: "'a :: numeral"
-where
-  "word_size_bits = 2"
-
-definition word_size :: "'a :: numeral"
-where
-  "word_size = 4"
-
-lemma word_bits_conv[code]:
-  "word_bits = 32"
-  unfolding word_bits_def by simp
-
-lemma word_size_word_size_bits:
-  "(word_size::nat) = 2 ^ word_size_bits"
-  unfolding word_size_def word_size_bits_def by simp
-
-lemma word_bits_word_size_conv:
-  "word_bits = word_size * 8"
-  unfolding word_bits_def word_size_def by simp
-
 lemma ucast_8_32_inj:
   "inj (ucast ::  8 word \<Rightarrow> 32 word)"
   by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size)
 
-lemma upto_2_helper:
-  "{0..<2 :: 32 word} = {0, 1}"
-  by (safe; simp) unat_arith
-
-lemmas upper_bits_unset_is_l2p_32 = upper_bits_unset_is_l2p [where 'a=32, folded word_bits_def]
-lemmas le_2p_upper_bits_32 = le_2p_upper_bits [where 'a=32, folded word_bits_def]
-lemmas le2p_bits_unset_32 = le2p_bits_unset[where 'a=32, folded word_bits_def]
-
-lemma word_bits_len_of:
-  "len_of TYPE (32) = word_bits"
-  by (simp add: word_bits_conv)
-
 lemmas unat_power_lower32' = unat_power_lower[where 'a=32]
-lemmas unat_power_lower32 [simp] = unat_power_lower32'[unfolded word_bits_len_of]
 
 lemmas word32_less_sub_le' = word_less_sub_le[where 'a = 32]
-lemmas word32_less_sub_le[simp] = word32_less_sub_le' [folded word_bits_def]
-
-lemma word_bits_size:
-  "size (w::word32) = word_bits"
-  by (simp add: word_bits_def word_size)
 
 lemmas word32_power_less_1' = word_power_less_1[where 'a = 32]
-lemmas word32_power_less_1[simp] = word32_power_less_1'[folded word_bits_def]
-
-lemma of_nat32_0:
-  "\<lbrakk>of_nat n = (0::word32); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
-  by (erule of_nat_0, simp add: word_bits_def)
-
-lemma unat_mask_2_less_4:
-  "unat (p && mask 2 :: word32) < 4"
-  by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)
 
 lemmas unat_of_nat32' = unat_of_nat_eq[where 'a=32]
-lemmas unat_of_nat32 = unat_of_nat32'[unfolded word_bits_len_of]
-
-lemmas word_power_nonzero_32 = word_power_nonzero [where 'a=32, folded word_bits_def]
-
-lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 32, unfolded word_bits_len_of]]
-
-lemmas div_power_helper_32 = div_power_helper [where 'a=32, folded word_bits_def]
-
-lemma n_less_word_bits:
-  "(n < word_bits) = (n < 32)"
-  by (simp add: word_bits_def)
-
-lemmas of_nat_less_pow_32 = of_nat_power [where 'a=32, folded word_bits_def]
-
-lemma lt_word_bits_lt_pow:
-  "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
-  by (simp add: word_bits_conv)
-
-lemma unat_less_word_bits:
-  fixes y :: word32
-  shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
-  unfolding word_bits_def
-  by (rule order_less_trans [OF _ unat_lt2p])
 
 lemmas unat_mask_word32' = unat_mask[where 'a=32]
-lemmas unat_mask_word32 = unat_mask_word32'[folded word_bits_def]
-
-lemma unat_less_2p_word_bits:
-  "unat (x :: 32 word) < 2 ^ word_bits"
-  apply (simp only: word_bits_def)
-  apply (rule unat_lt2p)
-  done
-
-lemma Suc_unat_mask_div:
-  "Suc (unat (mask sz div word_size::word32)) = 2 ^ (min sz word_bits - 2)"
-proof (cases \<open>sz \<ge> 2\<close>)
-  case False
-  then have \<open>sz \<in> {0, 1}\<close>
-    by auto
-  then show ?thesis by (auto simp add: unat_div word_size_def)
-next
-  case True
-  moreover define n where \<open>n = sz - 2\<close>
-  ultimately have \<open>sz = n + 2\<close>
-    by simp
-  moreover have \<open>4 * 2 ^ n = 2 ^ n * (4::nat)\<close>
-    by (simp add: ac_simps)
-  then have \<open>4 * 2 ^ n - Suc 0 = (2 ^ n - 1) * 4 + 3\<close>
-    by (simp add: mult_eq_if)
-  ultimately show ?thesis
-    by (simp add: unat_div unat_mask word_size_def word_bits_def min_def)
-qed
 
 lemmas word32_minus_one_le' = word_minus_one_le[where 'a=32]
 lemmas word32_minus_one_le = word32_minus_one_le'[simplified]
 
-lemma ucast_not_helper:
-  fixes a::"8 word"
-  assumes a: "a \<noteq> 0xFF"
-  shows "ucast a \<noteq> (0xFF::word32)"
-proof
-  assume "ucast a = (0xFF::word32)"
-  also
-  have "(0xFF::word32) = ucast (0xFF::8 word)" by simp
-  finally
-  show False using a
-    apply -
-    apply (drule up_ucast_inj, simp)
-    apply simp
-    done
-qed
-
-lemma less_4_cases:
-  "(x::word32) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3"
-  apply clarsimp
-  apply (drule word_less_cases, erule disjE, simp, simp)+
-  done
-
 lemma unat_ucast_8_32:
   fixes x :: "8 word"
   shows "unat (ucast x :: word32) = unat x"
   by transfer simp
 
-lemma if_then_1_else_0:
-  "((if P then 1 else 0) = (0 :: word32)) = (\<not> P)"
-  by simp
-
-lemma if_then_0_else_1:
-  "((if P then 0 else 1) = (0 :: word32)) = (P)"
-  by simp
-
-lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
-
 lemma ucast_le_ucast_8_32:
   "(ucast x \<le> (ucast y :: word32)) = (x \<le> (y :: 8 word))"
   by (simp add: ucast_le_ucast)
 
-lemma in_16_range:
-  "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: word32)) ` S"
-  "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: word32. r + x * 16) ` S"
-  by (clarsimp simp: image_def elim!: bexI[rotated])+
-
 lemma eq_2_32_0:
   "(2 ^ 32 :: word32) = 0"
   by simp
 
-lemma x_less_2_0_1:
-  fixes x :: word32 shows
-  "x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
-  by (rule x_less_2_0_1') auto
-
 lemmas mask_32_max_word  = max_word_mask [symmetric, where 'a=32, simplified]
 
 lemma of_nat32_n_less_equal_power_2:
  "n < 32 \<Longrightarrow> ((of_nat n)::32 word) < 2 ^ n"
   by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size)
 
-lemma word_rsplit_0:
-  "word_rsplit (0 :: word32) = [0, 0, 0, 0 :: 8 word]"
-  by (simp add: word_rsplit_def bin_rsplit_def)
-
 lemma unat_ucast_10_32 :
   fixes x :: "10 word"
   shows "unat (ucast x :: word32) = unat x"
   by transfer simp
 
-lemma bool_mask [simp]:
-  fixes x :: word32
-  shows "(0 < x && 1) = (x && 1 = 1)"
-  by (rule bool_mask') auto
-
 lemma word32_bounds:
   "- (2 ^ (size (x :: word32) - 1)) = (-2147483648 :: int)"
   "((2 ^ (size (x :: word32) - 1)) - 1) = (2147483647 :: int)"
   "- (2 ^ (size (y :: 32 signed word) - 1)) = (-2147483648 :: int)"
   "((2 ^ (size (y :: 32 signed word) - 1)) - 1) = (2147483647 :: int)"
   by (simp_all add: word_size)
 
-lemma word_ge_min:"sint (x::32 word) \<ge> -2147483648"
-  by (metis sint_ge word32_bounds(1) word_size)
-
 lemmas signed_arith_ineq_checks_to_eq_word32'
     = signed_arith_ineq_checks_to_eq[where 'a=32]
       signed_arith_ineq_checks_to_eq[where 'a="32 signed"]
 
 lemmas signed_arith_ineq_checks_to_eq_word32
     = signed_arith_ineq_checks_to_eq_word32' [unfolded word32_bounds]
 
 lemmas signed_mult_eq_checks32_to_64'
     = signed_mult_eq_checks_double_size[where 'a=32 and 'b=64]
       signed_mult_eq_checks_double_size[where 'a="32 signed" and 'b=64]
 
 lemmas signed_mult_eq_checks32_to_64 = signed_mult_eq_checks32_to_64'[simplified]
 
 lemmas sdiv_word32_max' = sdiv_word_max [where 'a=32] sdiv_word_max [where 'a="32 signed"]
 lemmas sdiv_word32_max = sdiv_word32_max'[simplified word_size, simplified]
 
 lemmas sdiv_word32_min' = sdiv_word_min [where 'a=32] sdiv_word_min [where 'a="32 signed"]
 lemmas sdiv_word32_min = sdiv_word32_min' [simplified word_size, simplified]
 
 lemmas sint32_of_int_eq' = sint_of_int_eq [where 'a=32]
 lemmas sint32_of_int_eq = sint32_of_int_eq' [simplified]
 
 lemma ucast_of_nats [simp]:
   "(ucast (of_nat x :: word32) :: sword32) = (of_nat x)"
   "(ucast (of_nat x :: word32) :: 16 sword) = (of_nat x)"
   "(ucast (of_nat x :: word32) :: 8 sword) = (of_nat x)"
   "(ucast (of_nat x :: 16 word) :: 16 sword) = (of_nat x)"
   "(ucast (of_nat x :: 16 word) :: 8 sword) = (of_nat x)"
   "(ucast (of_nat x :: 8 word) :: 8 sword) = (of_nat x)"
   by (simp_all add: of_nat_take_bit take_bit_word_eq_self unsigned_of_nat)
 
 lemmas signed_shift_guard_simpler_32'
     = power_strict_increasing_iff[where b="2 :: nat" and y=31]
 lemmas signed_shift_guard_simpler_32 = signed_shift_guard_simpler_32'[simplified]
 
 lemma word32_31_less:
   "31 < len_of TYPE (32 signed)" "31 > (0 :: nat)"
   "31 < len_of TYPE (32)" "31 > (0 :: nat)"
   by auto
 
 lemmas signed_shift_guard_to_word_32
     = signed_shift_guard_to_word[OF word32_31_less(1-2)]
     signed_shift_guard_to_word[OF word32_31_less(3-4)]
 
-lemma le_step_down_word_3:
-  fixes x :: "32 word"
-  shows "\<lbrakk>x \<le>  y; x \<noteq> y; y < 2 ^ 32 - 1\<rbrakk> \<Longrightarrow> x \<le> y - 1"
-  by (rule le_step_down_word_2, assumption+)
-
-lemma shiftr_1:
-  "(x::word32) >> 1 = 0 \<Longrightarrow> x < 2"
-  by transfer (simp add: take_bit_drop_bit drop_bit_Suc)
-
 lemma has_zero_byte:
   "~~ (((((v::word32) && 0x7f7f7f7f) + 0x7f7f7f7f) || v) || 0x7f7f7f7f) \<noteq> 0
     \<Longrightarrow> v && 0xff000000 = 0 \<or> v && 0xff0000 = 0 \<or> v && 0xff00 = 0 \<or> v && 0xff = 0"
   by word_bitwise auto
 
 lemma mask_step_down_32:
   \<open>\<exists>x. mask x = b\<close> if \<open>b && 1 = 1\<close>
     and \<open>\<exists>x. x < 32 \<and> mask x = b >> 1\<close> for b :: \<open>32word\<close>
 proof -
   from \<open>b && 1 = 1\<close> have \<open>odd b\<close>
     by (auto simp add: mod_2_eq_odd and_one_eq)
   then have \<open>b mod 2 = 1\<close>
     using odd_iff_mod_2_eq_one by blast
   from \<open>\<exists>x. x < 32 \<and> mask x = b >> 1\<close> obtain x where \<open>x < 32\<close> \<open>mask x = b >> 1\<close> by blast
   then have \<open>mask x = b div 2\<close>
     using shiftr1_is_div_2 [of b] by simp
   with \<open>b mod 2 = 1\<close> have \<open>2 * mask x + 1 = 2 * (b div 2) + b mod 2\<close>
     by (simp only:)
   also have \<open>\<dots> = b\<close>
     by (simp add: mult_div_mod_eq)
   finally have \<open>2 * mask x + 1 = b\<close> .
   moreover have \<open>mask (Suc x) = 2 * mask x + (1 :: 'a::len word)\<close>
     by (simp add: mask_Suc_rec)
   ultimately show ?thesis
     by auto
 qed
 
 lemma unat_of_int_32:
   "\<lbrakk>i \<ge> 0; i \<le>2 ^ 31\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword32)) = nat i"
   by (simp add: unsigned_of_int nat_take_bit_eq take_bit_nat_eq_self)
 
 lemmas word_ctz_not_minus_1_32 = word_ctz_not_minus_1[where 'a=32, simplified]
 
 (* Helper for packing then unpacking a 64-bit variable. *)
 lemma cast_chunk_assemble_id_64[simp]:
   "(((ucast ((ucast (x::64 word))::32 word))::64 word) || (((ucast ((ucast (x >> 32))::32 word))::64 word) << 32)) = x"
   by (simp add:cast_chunk_assemble_id)
 
 (* Another variant of packing and unpacking a 64-bit variable. *)
 lemma cast_chunk_assemble_id_64'[simp]:
   "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x"
   by (simp add:cast_chunk_scast_assemble_id)
 
 (* Specialisations of down_cast_same for adding to local simpsets. *)
 lemma cast_down_u64: "(scast::64 word \<Rightarrow> 32 word) = (ucast::64 word \<Rightarrow> 32 word)"
   by (subst down_cast_same[symmetric]; simp add:is_down)+
 
 lemma cast_down_s64: "(scast::64 sword \<Rightarrow> 32 word) = (ucast::64 sword \<Rightarrow> 32 word)"
   by (subst down_cast_same[symmetric]; simp add:is_down)
 
 lemma word32_and_max_simp:
   \<open>x AND 0xFFFFFFFF = x\<close> for x :: \<open>32 word\<close>
   using word_and_full_mask_simp [of x]
   by (simp add: numeral_eq_Suc mask_Suc_exp)
 
 end
 
 end
diff --git a/thys/Word_Lib/Word_64.thy b/thys/Word_Lib/Word_64.thy
--- a/thys/Word_Lib/Word_64.thy
+++ b/thys/Word_Lib/Word_64.thy
@@ -1,309 +1,149 @@
 (*
  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 section "Words of Length 64"
 
 theory Word_64
   imports
     Word_Lemmas
     Word_Names
     Word_Syntax
     Rsplit
     More_Word_Operations
 begin
 
 context
   includes bit_operations_syntax
 begin
 
 lemma len64: "len_of (x :: 64 itself) = 64" by simp
 
-type_synonym machine_word_len = 64
-type_synonym machine_word = "machine_word_len word"
-
-definition word_bits :: nat
-where
-  "word_bits = LENGTH(machine_word_len)"
-
-text \<open>The following two are numerals so they can be used as nats and words.\<close>
-definition word_size_bits :: "'a :: numeral"
-where
-  "word_size_bits = 3"
-
-definition word_size :: "'a :: numeral"
-where
-  "word_size = 8"
-
-lemma word_bits_conv[code]:
-  "word_bits = 64"
-  unfolding word_bits_def by simp
-
-lemma word_size_word_size_bits:
-  "(word_size::nat) = 2 ^ word_size_bits"
-  unfolding word_size_def word_size_bits_def by simp
-
-lemma word_bits_word_size_conv:
-  "word_bits = word_size * 8"
-  unfolding word_bits_def word_size_def by simp
-
 lemma ucast_8_64_inj:
   "inj (ucast ::  8 word \<Rightarrow> 64 word)"
   by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size)
 
-lemma upto_2_helper:
-  "{0..<2 :: 64 word} = {0, 1}"
-  by (safe; simp) unat_arith
-
-lemmas upper_bits_unset_is_l2p_64 = upper_bits_unset_is_l2p [where 'a=64, folded word_bits_def]
-lemmas le_2p_upper_bits_64 = le_2p_upper_bits [where 'a=64, folded word_bits_def]
-lemmas le2p_bits_unset_64 = le2p_bits_unset[where 'a=64, folded word_bits_def]
-
-lemma word_bits_len_of:
-  "len_of TYPE (64) = word_bits"
-  by (simp add: word_bits_conv)
-
 lemmas unat_power_lower64' = unat_power_lower[where 'a=64]
-lemmas unat_power_lower64 [simp] = unat_power_lower64'[unfolded word_bits_len_of]
 
 lemmas word64_less_sub_le' = word_less_sub_le[where 'a = 64]
-lemmas word64_less_sub_le[simp] = word64_less_sub_le' [folded word_bits_def]
-
-lemma word_bits_size:
-  "size (w::word64) = word_bits"
-  by (simp add: word_bits_def word_size)
 
 lemmas word64_power_less_1' = word_power_less_1[where 'a = 64]
-lemmas word64_power_less_1[simp] = word64_power_less_1'[folded word_bits_def]
-
-lemma of_nat64_0:
-  "\<lbrakk>of_nat n = (0::word64); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
-  by (erule of_nat_0, simp add: word_bits_def)
-
-lemma unat_mask_2_less_4:
-  "unat (p && mask 2 :: word64) < 4"
-  by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)
 
 lemmas unat_of_nat64' = unat_of_nat_eq[where 'a=64]
-lemmas unat_of_nat64 = unat_of_nat64'[unfolded word_bits_len_of]
-
-lemmas word_power_nonzero_64 = word_power_nonzero [where 'a=64, folded word_bits_def]
-
-lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 64, unfolded word_bits_len_of]]
-
-lemmas div_power_helper_64 = div_power_helper [where 'a=64, folded word_bits_def]
-
-lemma n_less_word_bits:
-  "(n < word_bits) = (n < 64)"
-  by (simp add: word_bits_def)
-
-lemmas of_nat_less_pow_64 = of_nat_power [where 'a=64, folded word_bits_def]
-
-lemma lt_word_bits_lt_pow:
-  "sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
-  by (simp add: word_bits_conv)
-
-lemma unat_less_word_bits:
-  fixes y :: word64
-  shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
-  unfolding word_bits_def
-  by (rule order_less_trans [OF _ unat_lt2p])
 
 lemmas unat_mask_word64' = unat_mask[where 'a=64]
-lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def]
-
-lemma unat_less_2p_word_bits:
-  "unat (x :: 64 word) < 2 ^ word_bits"
-  apply (simp only: word_bits_def)
-  apply (rule unat_lt2p)
-  done
-
-lemma Suc_unat_mask_div:
-  "Suc (unat (mask sz div word_size::word64)) = 2 ^ (min sz word_bits - 3)"
-proof (cases \<open>sz \<ge> 3\<close>)
-  case False
-  then have \<open>sz \<in> {0, 1, 2}\<close>
-    by auto
-  then show ?thesis by (auto simp add: unat_div word_size_def unat_mask)
-next
-  case True
-  moreover define n where \<open>n = sz - 3\<close>
-  ultimately have \<open>sz = n + 3\<close>
-    by simp
-  moreover have \<open>2 ^ n * 8 - Suc 0 = (2 ^ n - 1) * 8 + 7\<close>
-    by (simp add: mult_eq_if)
-  ultimately show ?thesis
-    by (simp add: unat_div unat_mask word_size_def word_bits_def min_def power_add)
-qed
 
 lemmas word64_minus_one_le' = word_minus_one_le[where 'a=64]
 lemmas word64_minus_one_le = word64_minus_one_le'[simplified]
 
-lemma ucast_not_helper:
-  fixes a::"8 word"
-  assumes a: "a \<noteq> 0xFF"
-  shows "ucast a \<noteq> (0xFF::word64)"
-proof
-  assume "ucast a = (0xFF::word64)"
-  also
-  have "(0xFF::word64) = ucast (0xFF::8 word)" by simp
-  finally
-  show False using a
-    apply -
-    apply (drule up_ucast_inj, simp)
-    apply simp
-    done
-qed
-
 lemma less_4_cases:
   "(x::word64) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3"
   apply clarsimp
   apply (drule word_less_cases, erule disjE, simp, simp)+
   done
 
-lemma if_then_1_else_0:
-  "((if P then 1 else 0) = (0 :: word64)) = (\<not> P)"
-  by simp
-
-lemma if_then_0_else_1:
-  "((if P then 0 else 1) = (0 :: word64)) = (P)"
-  by simp
-
-lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
-
 lemma ucast_le_ucast_8_64:
   "(ucast x \<le> (ucast y :: word64)) = (x \<le> (y :: 8 word))"
   by (simp add: ucast_le_ucast)
 
-lemma in_16_range:
-  "0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: word64)) ` S"
-  "n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: word64. r + x * 16) ` S"
-  by (clarsimp simp: image_def elim!: bexI[rotated])+
-
 lemma eq_2_64_0:
   "(2 ^ 64 :: word64) = 0"
   by simp
 
-lemma x_less_2_0_1:
-  fixes x :: word64 shows
-  "x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
-  by (rule x_less_2_0_1') auto
-
 lemmas mask_64_max_word  = max_word_mask [symmetric, where 'a=64, simplified]
 
 lemma of_nat64_n_less_equal_power_2:
  "n < 64 \<Longrightarrow> ((of_nat n)::64 word) < 2 ^ n"
   by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size)
 
-lemma word_rsplit_0:
-  "word_rsplit (0 :: word64) = [0, 0, 0, 0, 0, 0, 0, 0 :: 8 word]"
-  by (simp add: word_rsplit_def bin_rsplit_def)
-
 lemma unat_ucast_10_64 :
   fixes x :: "10 word"
   shows "unat (ucast x :: word64) = unat x"
   by transfer simp
 
-lemma bool_mask [simp]:
-  fixes x :: word64
-  shows "(0 < x && 1) = (x && 1 = 1)"
-  by (rule bool_mask') auto
-
 lemma word64_bounds:
   "- (2 ^ (size (x :: word64) - 1)) = (-9223372036854775808 :: int)"
   "((2 ^ (size (x :: word64) - 1)) - 1) = (9223372036854775807 :: int)"
   "- (2 ^ (size (y :: 64 signed word) - 1)) = (-9223372036854775808 :: int)"
   "((2 ^ (size (y :: 64 signed word) - 1)) - 1) = (9223372036854775807 :: int)"
   by (simp_all add: word_size)
 
-lemma word_ge_min:"sint (x::64 word) \<ge> -9223372036854775808"
-  by (metis sint_ge word64_bounds(1) word_size)
-
 lemmas signed_arith_ineq_checks_to_eq_word64'
     = signed_arith_ineq_checks_to_eq[where 'a=64]
       signed_arith_ineq_checks_to_eq[where 'a="64 signed"]
 
 lemmas signed_arith_ineq_checks_to_eq_word64
     = signed_arith_ineq_checks_to_eq_word64' [unfolded word64_bounds]
 
 lemmas signed_mult_eq_checks64_to_64'
     = signed_mult_eq_checks_double_size[where 'a=64 and 'b=64]
       signed_mult_eq_checks_double_size[where 'a="64 signed" and 'b=64]
 
 lemmas signed_mult_eq_checks64_to_64 = signed_mult_eq_checks64_to_64'[simplified]
 
 lemmas sdiv_word64_max' = sdiv_word_max [where 'a=64] sdiv_word_max [where 'a="64 signed"]
 lemmas sdiv_word64_max = sdiv_word64_max'[simplified word_size, simplified]
 
 lemmas sdiv_word64_min' = sdiv_word_min [where 'a=64] sdiv_word_min [where 'a="64 signed"]
 lemmas sdiv_word64_min = sdiv_word64_min' [simplified word_size, simplified]
 
 lemmas sint64_of_int_eq' = sint_of_int_eq [where 'a=64]
 lemmas sint64_of_int_eq = sint64_of_int_eq' [simplified]
 
 lemma ucast_of_nats [simp]:
   "(ucast (of_nat x :: word64) :: sword64) = (of_nat x)"
   "(ucast (of_nat x :: word64) :: 16 sword) = (of_nat x)"
   "(ucast (of_nat x :: word64) :: 8 sword) = (of_nat x)"
   by (simp_all add: of_nat_take_bit take_bit_word_eq_self unsigned_of_nat)
 
 lemmas signed_shift_guard_simpler_64'
     = power_strict_increasing_iff[where b="2 :: nat" and y=31]
 lemmas signed_shift_guard_simpler_64 = signed_shift_guard_simpler_64'[simplified]
 
 lemma word64_31_less:
   "31 < len_of TYPE (64 signed)" "31 > (0 :: nat)"
   "31 < len_of TYPE (64)" "31 > (0 :: nat)"
   by auto
 
 lemmas signed_shift_guard_to_word_64
     = signed_shift_guard_to_word[OF word64_31_less(1-2)]
     signed_shift_guard_to_word[OF word64_31_less(3-4)]
 
-lemma le_step_down_word_3:
-  fixes x :: "64 word"
-  shows "\<lbrakk>x \<le>  y; x \<noteq> y; y < 2 ^ 64 - 1\<rbrakk> \<Longrightarrow> x \<le> y - 1"
-  by (rule le_step_down_word_2, assumption+)
-
-lemma shiftr_1:
-  "(x::word64) >> 1 = 0 \<Longrightarrow> x < 2"
-  by transfer (simp add: take_bit_drop_bit drop_bit_Suc)
-
 lemma mask_step_down_64:
   \<open>\<exists>x. mask x = b\<close> if \<open>b && 1 = 1\<close>
     and \<open>\<exists>x. x < 64 \<and> mask x = b >> 1\<close> for b :: \<open>64word\<close>
 proof -
   from \<open>b && 1 = 1\<close> have \<open>odd b\<close>
     by (auto simp add: mod_2_eq_odd and_one_eq)
   then have \<open>b mod 2 = 1\<close>
     using odd_iff_mod_2_eq_one by blast
   from \<open>\<exists>x. x < 64 \<and> mask x = b >> 1\<close> obtain x where \<open>x < 64\<close> \<open>mask x = b >> 1\<close> by blast
   then have \<open>mask x = b div 2\<close>
     using shiftr1_is_div_2 [of b] by simp
   with \<open>b mod 2 = 1\<close> have \<open>2 * mask x + 1 = 2 * (b div 2) + b mod 2\<close>
     by (simp only:)
   also have \<open>\<dots> = b\<close>
     by (simp add: mult_div_mod_eq)
   finally have \<open>2 * mask x + 1 = b\<close> .
   moreover have \<open>mask (Suc x) = 2 * mask x + (1 :: 'a::len word)\<close>
     by (simp add: mask_Suc_rec)
   ultimately show ?thesis
     by auto
 qed
 
 lemma unat_of_int_64:
   "\<lbrakk>i \<ge> 0; i \<le> 2 ^ 63\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword64)) = nat i"
   by (simp add: unsigned_of_int nat_take_bit_eq take_bit_nat_eq_self)
 
 lemmas word_ctz_not_minus_1_64 = word_ctz_not_minus_1[where 'a=64, simplified]
 
 lemma word64_and_max_simp:
   \<open>x AND 0xFFFFFFFFFFFFFFFF = x\<close> for x :: \<open>64 word\<close>
   using word_and_full_mask_simp [of x]
   by (simp add: numeral_eq_Suc mask_Suc_exp)
 
 end
 
 end
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,136 +1,137 @@
 (*
  * 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_64
   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