diff --git a/thys/Native_Word/Uint.thy b/thys/Native_Word/Uint.thy
--- a/thys/Native_Word/Uint.thy
+++ b/thys/Native_Word/Uint.thy
@@ -1,855 +1,851 @@
 (*  Title:      Uint.thy
     Author:     Peter Lammich, TU Munich
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Unsigned words of default size\<close>
 
 theory Uint imports
   Code_Target_Word_Base
 begin
 
 text \<open>
   This theory provides access to words in the target languages of the code generator
   whose bit width is the default of the target language. To that end, the type \<open>uint\<close>
   models words of width \<open>dflt_size\<close>, but \<open>dflt_size\<close> is known only to be positive.
 
   Usage restrictions:
   Default-size words (type \<open>uint\<close>) cannot be used for evaluation, because 
   the results depend on the particular choice of word size in the target language
   and implementation. Symbolic evaluation has not yet been set up for \<open>uint\<close>.
 \<close>
 
 text \<open>The default size type\<close>
 typedecl dflt_size
 
 instantiation dflt_size :: typerep begin
 definition "typerep_class.typerep \<equiv>  \<lambda>_ :: dflt_size itself. Typerep.Typerep (STR ''Uint.dflt_size'') []"
 instance ..
 end
 
 consts dflt_size_aux :: "nat"
 specification (dflt_size_aux) dflt_size_aux_g0: "dflt_size_aux > 0"
   by auto
 hide_fact dflt_size_aux_def
 
 instantiation dflt_size :: len begin
 definition "len_of_dflt_size (_ :: dflt_size itself) \<equiv> dflt_size_aux"
 instance by(intro_classes)(simp add: len_of_dflt_size_def dflt_size_aux_g0)
 end
 
 abbreviation "dflt_size \<equiv> len_of (TYPE (dflt_size))"
 
 context includes integer.lifting begin
 lift_definition dflt_size_integer :: integer is "int dflt_size" .
 declare dflt_size_integer_def[code del]
   \<comment> \<open>The code generator will substitute a machine-dependent value for this constant\<close>
 
 lemma dflt_size_by_int[code]: "dflt_size = nat_of_integer dflt_size_integer"
 by transfer simp
 
 lemma dflt_size[simp]: 
   "dflt_size > 0"
   "dflt_size \<ge> Suc 0"
   "\<not> dflt_size < Suc 0"
   using len_gt_0[where 'a=dflt_size]
   by (simp_all del: len_gt_0)
 end
 
 declare prod.Quotient[transfer_rule]
 
 section \<open>Type definition and primitive operations\<close>
 
 typedef uint = "UNIV :: dflt_size word set" .. 
 
 setup_lifting type_definition_uint
 
 text \<open>Use an abstract type for code generation to disable pattern matching on @{term Abs_uint}.\<close>
 declare Rep_uint_inverse[code abstype]
 
 declare Quotient_uint[transfer_rule]
 
 instantiation uint :: comm_ring_1
 begin
 lift_definition zero_uint :: uint is "0 :: dflt_size word" .
 lift_definition one_uint :: uint is "1" .
 lift_definition plus_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(+) :: dflt_size word \<Rightarrow> _" .
 lift_definition minus_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(-)" .
 lift_definition uminus_uint :: "uint \<Rightarrow> uint" is uminus .
 lift_definition times_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(*)" .
 instance by (standard; transfer) (simp_all add: algebra_simps)
 end
 
 instantiation uint :: semiring_modulo
 begin
 lift_definition divide_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(div)" .
 lift_definition modulo_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is "(mod)" .
 instance by (standard; transfer) (fact word_mod_div_equality)
 end
 
 instantiation uint :: linorder begin
 lift_definition less_uint :: "uint \<Rightarrow> uint \<Rightarrow> bool" is "(<)" .
 lift_definition less_eq_uint :: "uint \<Rightarrow> uint \<Rightarrow> bool" is "(\<le>)" .
 instance by (standard; transfer) (simp_all add: less_le_not_le linear)
 end
 
 lemmas [code] = less_uint.rep_eq less_eq_uint.rep_eq
 
 context
   includes lifting_syntax
   notes
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> cr_uint) of_bool of_bool"
   by transfer_prover
 
 lemma transfer_rule_numeral_uint [transfer_rule]:
   "((=) ===> cr_uint) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   \<open>(cr_uint ===> (\<longleftrightarrow>)) even ((dvd) 2 :: uint \<Rightarrow> bool)\<close>
   by (unfold dvd_def) transfer_prover
 
 end
 
 instantiation uint :: semiring_bits
 begin
 
 lift_definition bit_uint :: \<open>uint \<Rightarrow> nat \<Rightarrow> bool\<close> is bit .
 
 instance
   by (standard; transfer)
     (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
        bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
        even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
        div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+
 
 end
 
 instantiation uint :: semiring_bit_shifts
 begin
 lift_definition push_bit_uint :: \<open>nat \<Rightarrow> uint \<Rightarrow> uint\<close> is push_bit .
 lift_definition drop_bit_uint :: \<open>nat \<Rightarrow> uint \<Rightarrow> uint\<close> is drop_bit .
 lift_definition take_bit_uint :: \<open>nat \<Rightarrow> uint \<Rightarrow> uint\<close> is take_bit .
 instance by (standard; transfer)
   (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 end
 
 instantiation uint :: ring_bit_operations
 begin
 lift_definition not_uint :: "uint \<Rightarrow> uint" is NOT .
 lift_definition and_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is \<open>(AND)\<close> .
 lift_definition or_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is \<open>(OR)\<close> .
 lift_definition xor_uint :: "uint \<Rightarrow> uint \<Rightarrow> uint" is \<open>(XOR)\<close> .
 instance by (standard; transfer)
   (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1)
 end
 
 instantiation uint :: bit_operations
 begin
 lift_definition test_bit_uint :: "uint \<Rightarrow> nat \<Rightarrow> bool" is test_bit .
 lift_definition set_bit_uint :: "uint \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint" is set_bit .
 lift_definition lsb_uint :: "uint \<Rightarrow> bool" is lsb .
 lift_definition shiftl_uint :: "uint \<Rightarrow> nat \<Rightarrow> uint" is shiftl .
 lift_definition shiftr_uint :: "uint \<Rightarrow> nat \<Rightarrow> uint" is shiftr .
 lift_definition msb_uint :: "uint \<Rightarrow> bool" is msb .
 instance ..
 end
 
 instantiation uint :: bit_comprehension begin
 lift_definition set_bits_uint :: "(nat \<Rightarrow> bool) \<Rightarrow> uint" is "set_bits" .
 instance ..
 end
 
 lemmas [code] = test_bit_uint.rep_eq lsb_uint.rep_eq msb_uint.rep_eq
 
 instantiation uint :: equal begin
 lift_definition equal_uint :: "uint \<Rightarrow> uint \<Rightarrow> bool" is "equal_class.equal" .
 instance by standard (transfer, simp add: equal_eq)
 end
 
 lemmas [code] = equal_uint.rep_eq
 
 instantiation uint :: size begin
 lift_definition size_uint :: "uint \<Rightarrow> nat" is "size" .
 instance ..
 end
 
 lemmas [code] = size_uint.rep_eq
 
 lift_definition sshiftr_uint :: "uint \<Rightarrow> nat \<Rightarrow> uint" (infixl ">>>" 55) is sshiftr .
 
 lift_definition uint_of_int :: "int \<Rightarrow> uint" is "word_of_int" .
 
-lemma of_bool_integer_transfer [transfer_rule]:
-  "(rel_fun (=) pcr_integer) of_bool of_bool"
-by(auto simp add: integer.pcr_cr_eq cr_integer_def split: bit.split)
-
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 context includes integer.lifting begin
 
 lift_definition Uint :: "integer \<Rightarrow> uint" is "word_of_int" .
 
 lemma Rep_uint_numeral [simp]: "Rep_uint (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint_def Abs_uint_inverse numeral.simps plus_uint_def)
 
 lemma numeral_uint_transfer [transfer_rule]:
   "(rel_fun (=) cr_uint) numeral numeral"
 by(auto simp add: cr_uint_def)
 
 lemma numeral_uint [code_unfold]: "numeral n = Uint (numeral n)"
 by transfer simp
 
 lemma Rep_uint_neg_numeral [simp]: "Rep_uint (- numeral n) = - numeral n"
 by(simp only: uminus_uint_def)(simp add: Abs_uint_inverse)
 
 lemma neg_numeral_uint [code_unfold]: "- numeral n = Uint (- numeral n)"
 by transfer(simp add: cr_uint_def)
 
 end
 
 lemma Abs_uint_numeral [code_post]: "Abs_uint (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint_def numeral.simps plus_uint_def Abs_uint_inverse)
 
 lemma Abs_uint_0 [code_post]: "Abs_uint 0 = 0"
 by(simp add: zero_uint_def)
 
 lemma Abs_uint_1 [code_post]: "Abs_uint 1 = 1"
 by(simp add: one_uint_def)
 
 section \<open>Code setup\<close>
 
 code_printing code_module Uint \<rightharpoonup> (SML)
 \<open>
 structure Uint : sig
   val set_bit : Word.word -> IntInf.int -> bool -> Word.word
   val shiftl : Word.word -> IntInf.int -> Word.word
   val shiftr : Word.word -> IntInf.int -> Word.word
   val shiftr_signed : Word.word -> IntInf.int -> Word.word
   val test_bit : Word.word -> IntInf.int -> bool
 end = struct
 
 fun set_bit x n b =
   let val mask = Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
   in if b then Word.orb (x, mask)
      else Word.andb (x, Word.notb mask)
   end
 
 fun shiftl x n =
   Word.<< (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr x n =
   Word.>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr_signed x n =
   Word.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun test_bit x n =
   Word.andb (x, Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word.fromInt 0
 
 end; (* struct Uint *)\<close>
 code_reserved SML Uint
 
 code_printing code_module Uint \<rightharpoonup> (Haskell)
  \<open>module Uint(Int, Word, dflt_size) where
 
   import qualified Prelude
   import Data.Int(Int)
   import Data.Word(Word)
   import qualified Data.Bits
 
   dflt_size :: Prelude.Integer
   dflt_size = Prelude.toInteger (bitSize_aux (0::Word)) where
     bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int
     bitSize_aux = Data.Bits.bitSize\<close>
   and (Haskell_Quickcheck)
  \<open>module Uint(Int, Word, dflt_size) where
 
   import qualified Prelude
   import Data.Int(Int)
   import Data.Word(Word)
   import qualified Data.Bits
 
   dflt_size :: Prelude.Int
   dflt_size = bitSize_aux (0::Word) where
     bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int
     bitSize_aux = Data.Bits.bitSize
 \<close>
 code_reserved Haskell Uint dflt_size
 
 text \<open>
   OCaml and Scala provide only signed bit numbers, so we use these and 
   implement sign-sensitive operations like comparisons manually.
 \<close>
 
 code_printing code_module "Uint" \<rightharpoonup> (OCaml)
 \<open>module Uint : sig
   type t = int
   val dflt_size : Z.t
   val less : t -> t -> bool
   val less_eq : t -> t -> bool
   val set_bit : t -> Z.t -> bool -> t
   val shiftl : t -> Z.t -> t
   val shiftr : t -> Z.t -> t
   val shiftr_signed : t -> Z.t -> t
   val test_bit : t -> Z.t -> bool
   val int_mask : int
   val int32_mask : int32
   val int64_mask : int64
 end = struct
 
 type t = int
 
 let dflt_size = Z.of_int Sys.int_size;;
 
 (* negative numbers have their highest bit set, 
    so they are greater than positive ones *)
 let less x y =
   if x<0 then
     y<0 && x<y
   else y < 0 || x < y;;
 
 let less_eq x y =
   if x < 0 then
     y < 0 &&  x <= y
   else y < 0 || x <= y;;
 
 let set_bit x n b =
   let mask = 1 lsl (Z.to_int n)
   in if b then x lor mask
      else x land (lnot mask);;
 
 let shiftl x n = x lsl (Z.to_int n);;
 
 let shiftr x n = x lsr (Z.to_int n);;
 
 let shiftr_signed x n = x asr (Z.to_int n);;
 
 let test_bit x n = x land (1 lsl (Z.to_int n)) <> 0;;
 
 let int_mask =
   if Sys.int_size < 32 then lnot 0 else 0xFFFFFFFF;;
 
 let int32_mask = 
   if Sys.int_size < 32 then Int32.pred (Int32.shift_left Int32.one Sys.int_size)
   else Int32.of_string "0xFFFFFFFF";;
 
 let int64_mask = 
   if Sys.int_size < 64 then Int64.pred (Int64.shift_left Int64.one Sys.int_size)
   else Int64.of_string "0xFFFFFFFFFFFFFFFF";;
 
 end;; (*struct Uint*)\<close>
 code_reserved OCaml Uint
 
 code_printing code_module Uint \<rightharpoonup> (Scala)
 \<open>object Uint {
 def dflt_size : BigInt = BigInt(32)
 
 def less(x: Int, y: Int) : Boolean =
   if (x < 0) y < 0 && x < y
   else y < 0 || x < y
 
 def less_eq(x: Int, y: Int) : Boolean =
   if (x < 0) y < 0 && x <= y
   else y < 0 || x <= y
 
 def set_bit(x: Int, n: BigInt, b: Boolean) : Int =
   if (b)
     x | (1 << n.intValue)
   else
     x & (1 << n.intValue).unary_~
 
 def shiftl(x: Int, n: BigInt) : Int = x << n.intValue
 
 def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue
 
 def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue
 
 def test_bit(x: Int, n: BigInt) : Boolean =
   (x & (1 << n.intValue)) != 0
 
 } /* object Uint */\<close>
 code_reserved Scala Uint
 
 
 text \<open>
   OCaml's conversion from Big\_int to int demands that the value fits into a signed integer.
   The following justifies the implementation.
 \<close>
 
 context includes integer.lifting begin
 definition wivs_mask :: int where "wivs_mask = 2^ dflt_size - 1"
 lift_definition wivs_mask_integer :: integer is wivs_mask .
 lemma [code]: "wivs_mask_integer = 2 ^ dflt_size - 1"
   by transfer (simp add: wivs_mask_def)
 
 definition wivs_shift :: int where "wivs_shift = 2 ^ dflt_size"
 lift_definition wivs_shift_integer :: integer is wivs_shift .
 lemma [code]: "wivs_shift_integer = 2 ^ dflt_size"
   by transfer (simp add: wivs_shift_def)
 
 definition wivs_index :: nat where "wivs_index == dflt_size - 1"
 lift_definition wivs_index_integer :: integer is "int wivs_index".
 lemma wivs_index_integer_code[code]: "wivs_index_integer = dflt_size_integer - 1"
   by transfer (simp add: wivs_index_def of_nat_diff)
 
 definition wivs_overflow :: int where "wivs_overflow == 2^ (dflt_size - 1)"
 lift_definition wivs_overflow_integer :: integer is wivs_overflow .
 lemma [code]: "wivs_overflow_integer = 2 ^ (dflt_size - 1)"
   by transfer (simp add: wivs_overflow_def)
 
 definition wivs_least :: int where "wivs_least == - wivs_overflow"
 lift_definition wivs_least_integer :: integer is wivs_least .
 lemma [code]: "wivs_least_integer = - (2 ^ (dflt_size - 1))"
   by transfer (simp add: wivs_overflow_def wivs_least_def)
 
 definition Uint_signed :: "integer \<Rightarrow> uint" where
   "Uint_signed i = (if i < wivs_least_integer \<or> wivs_overflow_integer \<le> i then undefined Uint i else Uint i)"
 
 lemma Uint_code [code]:
   "Uint i = 
   (let i' = i AND wivs_mask_integer in 
    if i' !! wivs_index then Uint_signed (i' - wivs_shift_integer) else Uint_signed i')"
   including undefined_transfer 
   unfolding Uint_signed_def
   apply transfer
   apply (rule word_of_int_via_signed)
   by (simp_all add: wivs_mask_def wivs_shift_def wivs_index_def wivs_overflow_def 
     wivs_least_def bin_mask_conv_pow2 shiftl_int_def)
 
 lemma Uint_signed_code [code abstract]:
   "Rep_uint (Uint_signed i) = 
   (if i < wivs_least_integer \<or> i \<ge> wivs_overflow_integer then Rep_uint (undefined Uint i) else word_of_int (int_of_integer_symbolic i))"
   unfolding Uint_signed_def Uint_def int_of_integer_symbolic_def word_of_integer_def
   by(simp add: Abs_uint_inverse)
 end
 
 text \<open>
   Avoid @{term Abs_uint} in generated code, use @{term Rep_uint'} instead. 
   The symbolic implementations for code\_simp use @{term Rep_uint}.
 
   The new destructor @{term Rep_uint'} is executable.
   As the simplifier is given the [code abstract] equations literally, 
   we cannot implement @{term Rep_uint} directly, because that makes code\_simp loop.
 
   If code generation raises Match, some equation probably contains @{term Rep_uint} 
   ([code abstract] equations for @{typ uint} may use @{term Rep_uint} because
   these instances will be folded away.)
 \<close>
 
 definition Rep_uint' where [simp]: "Rep_uint' = Rep_uint"
 
 lemma Rep_uint'_code [code]: "Rep_uint' x = (BITS n. x !! n)"
 unfolding Rep_uint'_def by transfer simp
 
 lift_definition Abs_uint' :: "dflt_size word \<Rightarrow> uint" is "\<lambda>x :: dflt_size word. x" .
 
 lemma Abs_uint'_code [code]:
   "Abs_uint' x = Uint (integer_of_int (uint x))"
 including integer.lifting by transfer simp
 
 declare [[code drop: "term_of_class.term_of :: uint \<Rightarrow> _"]]
 
 lemma term_of_uint_code [code]:
   defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" 
   shows
   "term_of_class.term_of x = 
    Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint.uint.Abs_uint'') (TR (STR ''fun'') [TR (STR ''Word.word'')  [TR (STR ''Uint.dflt_size'') []], TR (STR ''Uint.uint'') []]))
        (term_of_class.term_of (Rep_uint' x))"
   by(simp add: term_of_anything)
 
 text \<open>Important:
   We must prevent the reflection oracle (eval-tac) to 
   use our machine-dependent type.
 \<close>
 
 code_printing
   type_constructor uint \<rightharpoonup>
   (SML) "Word.word" and
   (Haskell) "Uint.Word" and
   (OCaml) "Uint.t" and
   (Scala) "Int" and
   (Eval) "*** \"Error: Machine dependent type\" ***" and
   (Quickcheck) "Word.word" 
 | constant dflt_size_integer \<rightharpoonup>
   (SML) "(IntInf.fromLarge (Int.toLarge Word.wordSize))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.wordSize" and
   (Haskell) "Uint.dflt'_size" and
   (OCaml) "Uint.dflt'_size" and
   (Scala) "Uint.dflt'_size"
 | constant Uint \<rightharpoonup>
   (SML) "Word.fromLargeInt (IntInf.toLarge _)" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.fromInt" and
   (Haskell) "(Prelude.fromInteger _ :: Uint.Word)" and
   (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint.Word)" and
   (Scala) "_.intValue"
 | constant Uint_signed \<rightharpoonup>
   (OCaml) "Z.to'_int"
 | constant "0 :: uint" \<rightharpoonup>
   (SML) "(Word.fromInt 0)" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "(Word.fromInt 0)" and
   (Haskell) "(0 :: Uint.Word)" and
   (OCaml) "0" and
   (Scala) "0"
 | constant "1 :: uint" \<rightharpoonup>
   (SML) "(Word.fromInt 1)" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "(Word.fromInt 1)" and
   (Haskell) "(1 :: Uint.Word)" and
   (OCaml) "1" and
   (Scala) "1"
 | constant "plus :: uint \<Rightarrow> _ " \<rightharpoonup>
   (SML) "Word.+ ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.+ ((_), (_))" and
   (Haskell) infixl 6 "+" and
   (OCaml) "Pervasives.(+)" and
   (Scala) infixl 7 "+"
 | constant "uminus :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.~" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.~" and
   (Haskell) "negate" and
   (OCaml) "Pervasives.(~-)" and
   (Scala) "!(- _)"
 | constant "minus :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.- ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.- ((_), (_))" and
   (Haskell) infixl 6 "-" and
   (OCaml) "Pervasives.(-)" and
   (Scala) infixl 7 "-"
 | constant "times :: uint \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.* ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.* ((_), (_))" and
   (Haskell) infixl 7 "*" and
   (OCaml) "Pervasives.( * )" and
   (Scala) infixl 8 "*"
 | constant "HOL.equal :: uint \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "!((_ : Word.word) = _)" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "!((_ : Word.word) = _)" and
   (Haskell) infix 4 "==" and
   (OCaml) "(Pervasives.(=):Uint.t -> Uint.t -> bool)" and
   (Scala) infixl 5 "=="
 | class_instance uint :: equal \<rightharpoonup>
   (Haskell) -
 | constant "less_eq :: uint \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word.<= ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.<= ((_), (_))" and
   (Haskell) infix 4 "<=" and
   (OCaml) "Uint.less'_eq" and
   (Scala) "Uint.less'_eq"
 | constant "less :: uint \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word.< ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.< ((_), (_))" and
   (Haskell) infix 4 "<" and
   (OCaml) "Uint.less" and
   (Scala) "Uint.less"
 | constant "NOT :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.notb" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.notb" and
   (Haskell) "Data'_Bits.complement" and
   (OCaml) "Pervasives.lnot" and
   (Scala) "_.unary'_~"
 | constant "(AND) :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.andb ((_),/ (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.andb ((_),/ (_))" and
   (Haskell) infixl 7 "Data_Bits..&." and
   (OCaml) "Pervasives.(land)" and
   (Scala) infixl 3 "&"
 | constant "(OR) :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.orb ((_),/ (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.orb ((_),/ (_))" and
   (Haskell) infixl 5 "Data_Bits..|." and
   (OCaml) "Pervasives.(lor)" and
   (Scala) infixl 1 "|"
 | constant "(XOR) :: uint \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word.xorb ((_),/ (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.xorb ((_),/ (_))" and
   (Haskell) "Data'_Bits.xor" and
   (OCaml) "Pervasives.(lxor)" and
   (Scala) infixl 2 "^"
 
 definition uint_divmod :: "uint \<Rightarrow> uint \<Rightarrow> uint \<times> uint" where
   "uint_divmod x y = 
   (if y = 0 then (undefined ((div) :: uint \<Rightarrow> _) x (0 :: uint), undefined ((mod) :: uint \<Rightarrow> _) x (0 :: uint)) 
   else (x div y, x mod y))"
 
 definition uint_div :: "uint \<Rightarrow> uint \<Rightarrow> uint" 
 where "uint_div x y = fst (uint_divmod x y)"
 
 definition uint_mod :: "uint \<Rightarrow> uint \<Rightarrow> uint" 
 where "uint_mod x y = snd (uint_divmod x y)"
 
 lemma div_uint_code [code]: "x div y = (if y = 0 then 0 else uint_div x y)"
 including undefined_transfer unfolding uint_divmod_def uint_div_def
 by transfer(simp add: word_div_def)
 
 lemma mod_uint_code [code]: "x mod y = (if y = 0 then x else uint_mod x y)"
 including undefined_transfer unfolding uint_mod_def uint_divmod_def
 by transfer(simp add: word_mod_def)
 
 definition uint_sdiv :: "uint \<Rightarrow> uint \<Rightarrow> uint"
 where [code del]:
   "uint_sdiv x y =
    (if y = 0 then undefined ((div) :: uint \<Rightarrow> _) x (0 :: uint)
     else Abs_uint (Rep_uint x sdiv Rep_uint y))"
 
 definition div0_uint :: "uint \<Rightarrow> uint"
 where [code del]: "div0_uint x = undefined ((div) :: uint \<Rightarrow> _) x (0 :: uint)"
 declare [[code abort: div0_uint]]
 
 definition mod0_uint :: "uint \<Rightarrow> uint"
 where [code del]: "mod0_uint x = undefined ((mod) :: uint \<Rightarrow> _) x (0 :: uint)"
 declare [[code abort: mod0_uint]]
 
 definition wivs_overflow_uint :: uint 
   where "wivs_overflow_uint \<equiv> 1 << (dflt_size - 1)"
 
 (* TODO: Move to Word *)
 lemma dflt_size_word_pow_ne_zero [simp]:
   "(2 :: 'a word) ^ (LENGTH('a::len) - Suc 0) \<noteq> 0"
 proof
   assume "(2 :: 'a word) ^ (LENGTH('a::len) - Suc 0) = 0"
   then have "unat ((2 :: 'a word) ^ (LENGTH('a::len) - Suc 0)) = unat 0"
     by simp
   then show False by (simp add: unat_p2)
 qed
 
 lemma uint_divmod_code [code]:
   "uint_divmod x y =
   (if wivs_overflow_uint \<le> y then if x < y then (0, x) else (1, x - y)
    else if y = 0 then (div0_uint x, mod0_uint x)
    else let q = (uint_sdiv (x >> 1) y) << 1;
             r = x - q * y
         in if r \<ge> y then (q + 1, r - y) else (q, r))"
   including undefined_transfer 
   unfolding uint_divmod_def uint_sdiv_def div0_uint_def mod0_uint_def
     wivs_overflow_uint_def
   by transfer (simp add: divmod_via_sdivmod)
 
 lemma uint_sdiv_code [code abstract]:
   "Rep_uint (uint_sdiv x y) =
    (if y = 0 then Rep_uint (undefined ((div) :: uint \<Rightarrow> _) x (0 :: uint))
     else Rep_uint x sdiv Rep_uint y)"
 unfolding uint_sdiv_def by(simp add: Abs_uint_inverse)
 
 text \<open>
   Note that we only need a translation for signed division, but not for the remainder
   because @{thm uint_divmod_code} computes both with division only.
 \<close>
 
 code_printing
   constant uint_div \<rightharpoonup>
   (SML) "Word.div ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.div ((_), (_))" and
   (Haskell) "Prelude.div"
 | constant uint_mod \<rightharpoonup>
   (SML) "Word.mod ((_), (_))" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Word.mod ((_), (_))" and
   (Haskell) "Prelude.mod"
 | constant uint_divmod \<rightharpoonup>
   (Haskell) "divmod"
 | constant uint_sdiv \<rightharpoonup>
   (OCaml) "Pervasives.('/)" and
   (Scala) "_ '/ _"
 
 definition uint_test_bit :: "uint \<Rightarrow> integer \<Rightarrow> bool"
 where [code del]:
   "uint_test_bit x n =
   (if n < 0 \<or> dflt_size_integer \<le> n then undefined (test_bit :: uint \<Rightarrow> _) x n
    else x !! (nat_of_integer n))"
 
 lemma test_bit_eq_bit_uint [code]:
   \<open>test_bit = (bit :: uint \<Rightarrow> _)\<close>
   by (rule ext)+ (transfer, transfer, simp)
 
 lemma test_bit_uint_code [code]:
   "test_bit x n \<longleftrightarrow> n < dflt_size \<and> uint_test_bit x (integer_of_nat n)"
   including undefined_transfer integer.lifting unfolding uint_test_bit_def
   by (transfer, simp, transfer, simp)
 
 lemma uint_test_bit_code [code]:
   "uint_test_bit w n =
   (if n < 0 \<or> dflt_size_integer \<le> n then undefined (test_bit :: uint \<Rightarrow> _) w n else Rep_uint w !! nat_of_integer n)"
 unfolding uint_test_bit_def
 by(simp add: test_bit_uint.rep_eq)
 
 code_printing constant uint_test_bit \<rightharpoonup>
   (SML) "Uint.test'_bit" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.test'_bit" and
   (Haskell) "Data'_Bits.testBitBounded" and
   (OCaml) "Uint.test'_bit" and
   (Scala) "Uint.test'_bit"
 
 definition uint_set_bit :: "uint \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> uint"
 where [code del]:
   "uint_set_bit x n b =
   (if n < 0 \<or> dflt_size_integer \<le> n then undefined (set_bit :: uint \<Rightarrow> _) x n b
    else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_uint_code [code]:
   "set_bit x n b = (if n < dflt_size then uint_set_bit x (integer_of_nat n) b else x)"
   including undefined_transfer integer.lifting unfolding uint_set_bit_def
   by (transfer) (auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
 
 lemma uint_set_bit_code [code abstract]:
   "Rep_uint (uint_set_bit w n b) = 
   (if n < 0 \<or> dflt_size_integer \<le> n then Rep_uint (undefined (set_bit :: uint \<Rightarrow> _) w n b)
    else set_bit (Rep_uint w) (nat_of_integer n) b)"
 including undefined_transfer integer.lifting unfolding uint_set_bit_def by transfer simp
 
 code_printing constant uint_set_bit \<rightharpoonup>
   (SML) "Uint.set'_bit" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.set'_bit" and
   (Haskell) "Data'_Bits.setBitBounded" and
   (OCaml) "Uint.set'_bit" and
   (Scala) "Uint.set'_bit"
 
 lift_definition uint_set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> uint \<Rightarrow> nat \<Rightarrow> uint" is set_bits_aux .
 
 lemma uint_set_bits_code [code]:
   "uint_set_bits f w n =
   (if n = 0 then w 
    else let n' = n - 1 in uint_set_bits f ((w << 1) OR (if f n' then 1 else 0)) n')"
 by(transfer fixing: n)(cases n, simp_all)
 
 lemma set_bits_uint [code]:
   "(BITS n. f n) = uint_set_bits f 0 dflt_size"
   by transfer (simp add: set_bits_conv_set_bits_aux)
 
 lemma lsb_code [code]: fixes x :: uint shows "lsb x = x !! 0"
 by transfer(simp add: word_lsb_def word_test_bit_def)
 
 definition uint_shiftl :: "uint \<Rightarrow> integer \<Rightarrow> uint"
 where [code del]:
   "uint_shiftl x n = (if n < 0 \<or> dflt_size_integer \<le> n then undefined (shiftl :: uint \<Rightarrow> _) x n else x << (nat_of_integer n))"
 
 lemma shiftl_uint_code [code]: "x << n = (if n < dflt_size then uint_shiftl x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint_shiftl_def
 by transfer(simp add: not_less shiftl_zero_size word_size)
 
 lemma uint_shiftl_code [code abstract]:
   "Rep_uint (uint_shiftl w n) =
   (if n < 0 \<or> dflt_size_integer \<le> n then Rep_uint (undefined (shiftl :: uint \<Rightarrow> _) w n) else Rep_uint w << (nat_of_integer n))"
 including undefined_transfer integer.lifting unfolding uint_shiftl_def by transfer simp
 
 code_printing constant uint_shiftl \<rightharpoonup>
   (SML) "Uint.shiftl" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.shiftl" and
   (Haskell) "Data'_Bits.shiftlBounded" and
   (OCaml) "Uint.shiftl" and
   (Scala) "Uint.shiftl"
 
 definition uint_shiftr :: "uint \<Rightarrow> integer \<Rightarrow> uint"
 where [code del]:
   "uint_shiftr x n = (if n < 0 \<or> dflt_size_integer \<le> n then undefined (shiftr :: uint \<Rightarrow> _) x n else x >> (nat_of_integer n))"
 
 lemma shiftr_uint_code [code]: "x >> n = (if n < dflt_size then uint_shiftr x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint_shiftr_def
 by transfer(simp add: not_less shiftr_zero_size word_size)
 
 lemma uint_shiftr_code [code abstract]:
   "Rep_uint (uint_shiftr w n) =
   (if n < 0 \<or> dflt_size_integer \<le> n then Rep_uint (undefined (shiftr :: uint \<Rightarrow> _) w n) else Rep_uint w >> nat_of_integer n)"
 including undefined_transfer unfolding uint_shiftr_def by transfer simp
 
 code_printing constant uint_shiftr \<rightharpoonup>
   (SML) "Uint.shiftr" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.shiftr" and
   (Haskell) "Data'_Bits.shiftrBounded" and
   (OCaml) "Uint.shiftr" and
   (Scala) "Uint.shiftr"
 
 definition uint_sshiftr :: "uint \<Rightarrow> integer \<Rightarrow> uint"
 where [code del]:
   "uint_sshiftr x n =
   (if n < 0 \<or> dflt_size_integer \<le> n then undefined sshiftr_uint x n else sshiftr_uint x (nat_of_integer n))"
 
 lemma sshiftr_beyond: fixes x :: "'a :: len word" shows
   "size x \<le> n \<Longrightarrow> x >>> n = (if x !! (size x - 1) then -1 else 0)"
 by(rule word_eqI)(simp add: nth_sshiftr word_size)
 
 lemma sshiftr_uint_code [code]:
   "x >>> n = 
   (if n < dflt_size then uint_sshiftr x (integer_of_nat n) else 
     if x !! wivs_index then -1 else 0)"
 including undefined_transfer integer.lifting unfolding uint_sshiftr_def
 by transfer(simp add: not_less sshiftr_beyond word_size wivs_index_def)
 
 lemma uint_sshiftr_code [code abstract]:
   "Rep_uint (uint_sshiftr w n) =
   (if n < 0 \<or> dflt_size_integer \<le> n then Rep_uint (undefined sshiftr_uint w n) else Rep_uint w >>> (nat_of_integer n))"
 including undefined_transfer unfolding uint_sshiftr_def by transfer simp
 
 code_printing constant uint_sshiftr \<rightharpoonup>
   (SML) "Uint.shiftr'_signed" and
   (Eval) "(raise (Fail \"Machine dependent code\"))" and
   (Quickcheck) "Uint.shiftr'_signed" and
   (Haskell) 
     "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint.Int) _)) :: Uint.Word)" and
   (OCaml) "Uint.shiftr'_signed" and
   (Scala) "Uint.shiftr'_signed"
 
 lemma uint_msb_test_bit: "msb x \<longleftrightarrow> (x :: uint) !! wivs_index"
 by transfer(simp add: msb_nth wivs_index_def)
 
 lemma msb_uint_code [code]: "msb x \<longleftrightarrow> uint_test_bit x wivs_index_integer"
   apply(simp add: uint_test_bit_def uint_msb_test_bit 
   wivs_index_integer_code dflt_size_integer_def wivs_index_def)
   by (metis (full_types) One_nat_def dflt_size(2) less_iff_diff_less_0 
     nat_of_integer_of_nat of_nat_1 of_nat_diff of_nat_less_0_iff wivs_index_def)
 
 lemma uint_of_int_code [code]: "uint_of_int i = (BITS n. i !! n)"
 by transfer(simp add: word_of_int_conv_set_bits test_bit_int_def[abs_def])
 
 section \<open>Quickcheck setup\<close>
 
 definition uint_of_natural :: "natural \<Rightarrow> uint"
 where "uint_of_natural x \<equiv> Uint (integer_of_natural x)"
 
 instantiation uint :: "{random, exhaustive, full_exhaustive}" begin
 definition "random_uint \<equiv> qc_random_cnv uint_of_natural"
 definition "exhaustive_uint \<equiv> qc_exhaustive_cnv uint_of_natural"
 definition "full_exhaustive_uint \<equiv> qc_full_exhaustive_cnv uint_of_natural"
 instance ..
 end
 
 instantiation uint :: narrowing begin
 
 interpretation quickcheck_narrowing_samples
   "\<lambda>i. (Uint i, Uint (- i))" "0"
   "Typerep.Typerep (STR ''Uint.uint'') []" .
 
 definition "narrowing_uint d = qc_narrowing_drawn_from (narrowing_samples d) d"
 declare [[code drop: "partial_term_of :: uint itself \<Rightarrow> _"]]
 lemmas partial_term_of_uint [code] = partial_term_of_code
 
 instance ..
 end
 
 no_notation sshiftr_uint (infixl ">>>" 55)
 
 end
diff --git a/thys/Native_Word/Uint32.thy b/thys/Native_Word/Uint32.thy
--- a/thys/Native_Word/Uint32.thy
+++ b/thys/Native_Word/Uint32.thy
@@ -1,720 +1,716 @@
 (*  Title:      Uint32.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Unsigned words of 32 bits\<close>
 
 theory Uint32 imports
   Code_Target_Word_Base
 begin
 
 declare prod.Quotient[transfer_rule]
 
 section \<open>Type definition and primitive operations\<close>
 
 typedef uint32 = "UNIV :: 32 word set" .. 
 
 setup_lifting type_definition_uint32
 
 text \<open>Use an abstract type for code generation to disable pattern matching on @{term Abs_uint32}.\<close>
 declare Rep_uint32_inverse[code abstype]
 
 declare Quotient_uint32[transfer_rule]
 
 instantiation uint32 :: comm_ring_1
 begin
 lift_definition zero_uint32 :: uint32 is "0 :: 32 word" .
 lift_definition one_uint32 :: uint32 is "1" .
 lift_definition plus_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(+) :: 32 word \<Rightarrow> _" .
 lift_definition minus_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(-)" .
 lift_definition uminus_uint32 :: "uint32 \<Rightarrow> uint32" is uminus .
 lift_definition times_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(*)" .
 instance by (standard; transfer) (simp_all add: algebra_simps)
 end
 
 instantiation uint32 :: semiring_modulo
 begin
 lift_definition divide_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(div)" .
 lift_definition modulo_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(mod)" .
 instance by (standard; transfer) (fact word_mod_div_equality)
 end
 
 instantiation uint32 :: linorder begin
 lift_definition less_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> bool" is "(<)" .
 lift_definition less_eq_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> bool" is "(\<le>)" .
 instance by (standard; transfer) (simp_all add: less_le_not_le linear)
 end
 
 lemmas [code] = less_uint32.rep_eq less_eq_uint32.rep_eq
 
 context
   includes lifting_syntax
   notes
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> cr_uint32) of_bool of_bool"
   by transfer_prover
 
 lemma transfer_rule_numeral_uint [transfer_rule]:
   "((=) ===> cr_uint32) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   \<open>(cr_uint32 ===> (\<longleftrightarrow>)) even ((dvd) 2 :: uint32 \<Rightarrow> bool)\<close>
   by (unfold dvd_def) transfer_prover
 
 end
 
 instantiation uint32:: semiring_bits
 begin
 
 lift_definition bit_uint32 :: \<open>uint32 \<Rightarrow> nat \<Rightarrow> bool\<close> is bit .
 
 instance
   by (standard; transfer)
     (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
        bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
        even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
        div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+
 
 end
 
 instantiation uint32 :: semiring_bit_shifts
 begin
 lift_definition push_bit_uint32 :: \<open>nat \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is push_bit .
 lift_definition drop_bit_uint32 :: \<open>nat \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is drop_bit .
 lift_definition take_bit_uint32 :: \<open>nat \<Rightarrow> uint32 \<Rightarrow> uint32\<close> is take_bit .
 instance by (standard; transfer)
   (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 end
 
 instantiation uint32 :: ring_bit_operations
 begin
 lift_definition not_uint32 :: "uint32 \<Rightarrow> uint32" is NOT .
 lift_definition and_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is \<open>(AND)\<close> .
 lift_definition or_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is \<open>(OR)\<close> .
 lift_definition xor_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is \<open>(XOR)\<close> .
 instance by (standard; transfer)
   (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1)
 end
 
 instantiation uint32 :: bit_operations
 begin
 lift_definition test_bit_uint32 :: "uint32 \<Rightarrow> nat \<Rightarrow> bool" is test_bit .
 lift_definition set_bit_uint32 :: "uint32 \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint32" is set_bit .
 lift_definition lsb_uint32 :: "uint32 \<Rightarrow> bool" is lsb .
 lift_definition shiftl_uint32 :: "uint32 \<Rightarrow> nat \<Rightarrow> uint32" is shiftl .
 lift_definition shiftr_uint32 :: "uint32 \<Rightarrow> nat \<Rightarrow> uint32" is shiftr .
 lift_definition msb_uint32 :: "uint32 \<Rightarrow> bool" is msb .
 instance ..
 end
 
 instantiation uint32 :: bit_comprehension begin
 lift_definition set_bits_uint32 :: "(nat \<Rightarrow> bool) \<Rightarrow> uint32" is "set_bits" .
 instance ..
 end
 
 lemmas [code] = test_bit_uint32.rep_eq lsb_uint32.rep_eq msb_uint32.rep_eq
 
 instantiation uint32 :: equal begin
 lift_definition equal_uint32 :: "uint32 \<Rightarrow> uint32 \<Rightarrow> bool" is "equal_class.equal" .
 instance by standard (transfer, simp add: equal_eq)
 end
 
 lemmas [code] = equal_uint32.rep_eq
 
 instantiation uint32 :: size begin
 lift_definition size_uint32 :: "uint32 \<Rightarrow> nat" is "size" .
 instance ..
 end
 
 lemmas [code] = size_uint32.rep_eq                                                    
 
 lift_definition sshiftr_uint32 :: "uint32 \<Rightarrow> nat \<Rightarrow> uint32" (infixl ">>>" 55) is sshiftr .
 
 lift_definition uint32_of_int :: "int \<Rightarrow> uint32" is "word_of_int" .
 
 definition uint32_of_nat :: "nat \<Rightarrow> uint32"
 where "uint32_of_nat = uint32_of_int \<circ> int"
 
 lift_definition int_of_uint32 :: "uint32 \<Rightarrow> int" is "uint" .
 lift_definition nat_of_uint32 :: "uint32 \<Rightarrow> nat" is "unat" .
 
 definition integer_of_uint32 :: "uint32 \<Rightarrow> integer"
 where "integer_of_uint32 = integer_of_int o int_of_uint32"
 
-lemma bitval_integer_transfer [transfer_rule]:
-  "(rel_fun (=) pcr_integer) of_bool of_bool"
-by(auto simp add: of_bool_def integer.pcr_cr_eq cr_integer_def split: bit.split)
-
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 context includes integer.lifting begin
 
 lift_definition Uint32 :: "integer \<Rightarrow> uint32" is "word_of_int" .
 
 lemma Rep_uint32_numeral [simp]: "Rep_uint32 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint32_def Abs_uint32_inverse numeral.simps plus_uint32_def)
 
 lemma numeral_uint32_transfer [transfer_rule]:
   "(rel_fun (=) cr_uint32) numeral numeral"
 by(auto simp add: cr_uint32_def)
 
 lemma numeral_uint32 [code_unfold]: "numeral n = Uint32 (numeral n)"
 by transfer simp
 
 lemma Rep_uint32_neg_numeral [simp]: "Rep_uint32 (- numeral n) = - numeral n"
 by(simp only: uminus_uint32_def)(simp add: Abs_uint32_inverse)
 
 lemma neg_numeral_uint32 [code_unfold]: "- numeral n = Uint32 (- numeral n)"
 by transfer(simp add: cr_uint32_def)
 
 end
 
 lemma Abs_uint32_numeral [code_post]: "Abs_uint32 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint32_def numeral.simps plus_uint32_def Abs_uint32_inverse)
 
 lemma Abs_uint32_0 [code_post]: "Abs_uint32 0 = 0"
 by(simp add: zero_uint32_def)
 
 lemma Abs_uint32_1 [code_post]: "Abs_uint32 1 = 1"
 by(simp add: one_uint32_def)
 
 section \<open>Code setup\<close>
 
 code_printing code_module Uint32 \<rightharpoonup> (SML)
 \<open>(* Test that words can handle numbers between 0 and 31 *)
 val _ = if 5 <= Word.wordSize then () else raise (Fail ("wordSize less than 5"));
 
 structure Uint32 : sig
   val set_bit : Word32.word -> IntInf.int -> bool -> Word32.word
   val shiftl : Word32.word -> IntInf.int -> Word32.word
   val shiftr : Word32.word -> IntInf.int -> Word32.word
   val shiftr_signed : Word32.word -> IntInf.int -> Word32.word
   val test_bit : Word32.word -> IntInf.int -> bool
 end = struct
 
 fun set_bit x n b =
   let val mask = Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
   in if b then Word32.orb (x, mask)
      else Word32.andb (x, Word32.notb mask)
   end
 
 fun shiftl x n =
   Word32.<< (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr x n =
   Word32.>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun shiftr_signed x n =
   Word32.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
 
 fun test_bit x n =
   Word32.andb (x, Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word32.fromInt 0
 
 end; (* struct Uint32 *)\<close>
 code_reserved SML Uint32
 
 code_printing code_module Uint32 \<rightharpoonup> (Haskell)
  \<open>module Uint32(Int32, Word32) where
 
   import Data.Int(Int32)
   import Data.Word(Word32)\<close>
 code_reserved Haskell Uint32
 
 text \<open>
   OCaml and Scala provide only signed 32bit numbers, so we use these and 
   implement sign-sensitive operations like comparisons manually.
 \<close>
 code_printing code_module "Uint32" \<rightharpoonup> (OCaml)
 \<open>module Uint32 : sig
   val less : int32 -> int32 -> bool
   val less_eq : int32 -> int32 -> bool
   val set_bit : int32 -> Z.t -> bool -> int32
   val shiftl : int32 -> Z.t -> int32
   val shiftr : int32 -> Z.t -> int32
   val shiftr_signed : int32 -> Z.t -> int32
   val test_bit : int32 -> Z.t -> bool
 end = struct
 
 (* negative numbers have their highest bit set, 
    so they are greater than positive ones *)
 let less x y =
   if Int32.compare x Int32.zero < 0 then
     Int32.compare y Int32.zero < 0 && Int32.compare x y < 0
   else Int32.compare y Int32.zero < 0 || Int32.compare x y < 0;;
 
 let less_eq x y =
   if Int32.compare x Int32.zero < 0 then
     Int32.compare y Int32.zero < 0 && Int32.compare x y <= 0
   else Int32.compare y Int32.zero < 0 || Int32.compare x y <= 0;;
 
 let set_bit x n b =
   let mask = Int32.shift_left Int32.one (Z.to_int n)
   in if b then Int32.logor x mask
      else Int32.logand x (Int32.lognot mask);;
 
 let shiftl x n = Int32.shift_left x (Z.to_int n);;
 
 let shiftr x n = Int32.shift_right_logical x (Z.to_int n);;
 
 let shiftr_signed x n = Int32.shift_right x (Z.to_int n);;
 
 let test_bit x n =
   Int32.compare 
     (Int32.logand x (Int32.shift_left Int32.one (Z.to_int n)))
     Int32.zero
   <> 0;;
 
 end;; (*struct Uint32*)\<close>
 code_reserved OCaml Uint32
 
 code_printing code_module Uint32 \<rightharpoonup> (Scala)
 \<open>object Uint32 {
 
 def less(x: Int, y: Int) : Boolean =
   if (x < 0) y < 0 && x < y
   else y < 0 || x < y
 
 def less_eq(x: Int, y: Int) : Boolean =
   if (x < 0) y < 0 && x <= y
   else y < 0 || x <= y
 
 def set_bit(x: Int, n: BigInt, b: Boolean) : Int =
   if (b)
     x | (1 << n.intValue)
   else
     x & (1 << n.intValue).unary_~
 
 def shiftl(x: Int, n: BigInt) : Int = x << n.intValue
 
 def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue
 
 def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue
 
 def test_bit(x: Int, n: BigInt) : Boolean =
   (x & (1 << n.intValue)) != 0
 
 } /* object Uint32 */\<close>
 code_reserved Scala Uint32
 
 text \<open>
   OCaml's conversion from Big\_int to int32 demands that the value fits int a signed 32-bit integer.
   The following justifies the implementation.
 \<close>
 
 definition Uint32_signed :: "integer \<Rightarrow> uint32" 
 where "Uint32_signed i = (if i < -(0x80000000) \<or> i \<ge> 0x80000000 then undefined Uint32 i else Uint32 i)"
 
 lemma Uint32_code [code]:
   "Uint32 i = 
   (let i' = i AND 0xFFFFFFFF
    in if i' !! 31 then Uint32_signed (i' - 0x100000000) else Uint32_signed i')"
 including undefined_transfer integer.lifting unfolding Uint32_signed_def
 by transfer(rule word_of_int_via_signed, simp_all add: bin_mask_numeral)
 
 lemma Uint32_signed_code [code abstract]:
   "Rep_uint32 (Uint32_signed i) = 
   (if i < -(0x80000000) \<or> i \<ge> 0x80000000 then Rep_uint32 (undefined Uint32 i) else word_of_int (int_of_integer_symbolic i))"
 unfolding Uint32_signed_def Uint32_def int_of_integer_symbolic_def word_of_integer_def
 by(simp add: Abs_uint32_inverse)
 
 text \<open>
   Avoid @{term Abs_uint32} in generated code, use @{term Rep_uint32'} instead. 
   The symbolic implementations for code\_simp use @{term Rep_uint32}.
 
   The new destructor @{term Rep_uint32'} is executable.
   As the simplifier is given the [code abstract] equations literally, 
   we cannot implement @{term Rep_uint32} directly, because that makes code\_simp loop.
 
   If code generation raises Match, some equation probably contains @{term Rep_uint32} 
   ([code abstract] equations for @{typ uint32} may use @{term Rep_uint32} because
   these instances will be folded away.)
 
   To convert @{typ "32 word"} values into @{typ uint32}, use @{term "Abs_uint32'"}.
 \<close>
 
 definition Rep_uint32' where [simp]: "Rep_uint32' = Rep_uint32"
 
 lemma Rep_uint32'_transfer [transfer_rule]:
   "rel_fun cr_uint32 (=) (\<lambda>x. x) Rep_uint32'"
 unfolding Rep_uint32'_def by(rule uint32.rep_transfer)
 
 lemma Rep_uint32'_code [code]: "Rep_uint32' x = (BITS n. x !! n)"
 by transfer simp
 
 lift_definition Abs_uint32' :: "32 word \<Rightarrow> uint32" is "\<lambda>x :: 32 word. x" .
 
 lemma Abs_uint32'_code [code]:
   "Abs_uint32' x = Uint32 (integer_of_int (uint x))"
 including integer.lifting by transfer simp
 
 declare [[code drop: "term_of_class.term_of :: uint32 \<Rightarrow> _"]]
 
 lemma term_of_uint32_code [code]:
   defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" 
   shows
   "term_of_class.term_of x = 
    Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
        (term_of_class.term_of (Rep_uint32' x))"
 by(simp add: term_of_anything)
 
 code_printing
   type_constructor uint32 \<rightharpoonup>
   (SML) "Word32.word" and
   (Haskell) "Uint32.Word32" and
   (OCaml) "int32" and
   (Scala) "Int" and
   (Eval) "Word32.word"
 | constant Uint32 \<rightharpoonup>
   (SML) "Word32.fromLargeInt (IntInf.toLarge _)" and
   (Haskell) "(Prelude.fromInteger _ :: Uint32.Word32)" and
   (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Word32)" and
   (Scala) "_.intValue"
 | constant Uint32_signed \<rightharpoonup>
   (OCaml) "Z.to'_int32"
 | constant "0 :: uint32" \<rightharpoonup>
   (SML) "(Word32.fromInt 0)" and
   (Haskell) "(0 :: Uint32.Word32)" and
   (OCaml) "Int32.zero" and
   (Scala) "0"
 | constant "1 :: uint32" \<rightharpoonup>
   (SML) "(Word32.fromInt 1)" and
   (Haskell) "(1 :: Uint32.Word32)" and
   (OCaml) "Int32.one" and
   (Scala) "1"
 | constant "plus :: uint32 \<Rightarrow> _ " \<rightharpoonup>
   (SML) "Word32.+ ((_), (_))" and
   (Haskell) infixl 6 "+" and
   (OCaml) "Int32.add" and
   (Scala) infixl 7 "+"
 | constant "uminus :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.~" and
   (Haskell) "negate" and
   (OCaml) "Int32.neg" and
   (Scala) "!(- _)"
 | constant "minus :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.- ((_), (_))" and
   (Haskell) infixl 6 "-" and
   (OCaml) "Int32.sub" and
   (Scala) infixl 7 "-"
 | constant "times :: uint32 \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.* ((_), (_))" and
   (Haskell) infixl 7 "*" and
   (OCaml) "Int32.mul" and
   (Scala) infixl 8 "*"
 | constant "HOL.equal :: uint32 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "!((_ : Word32.word) = _)" and
   (Haskell) infix 4 "==" and
   (OCaml) "(Int32.compare _ _ = 0)" and
   (Scala) infixl 5 "=="
 | class_instance uint32 :: equal \<rightharpoonup>
   (Haskell) -
 | constant "less_eq :: uint32 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word32.<= ((_), (_))" and
   (Haskell) infix 4 "<=" and
   (OCaml) "Uint32.less'_eq" and
   (Scala) "Uint32.less'_eq"
 | constant "less :: uint32 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Word32.< ((_), (_))" and
   (Haskell) infix 4 "<" and
   (OCaml) "Uint32.less" and
   (Scala) "Uint32.less"
 | constant "NOT :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.notb" and
   (Haskell) "Data'_Bits.complement" and
   (OCaml) "Int32.lognot" and
   (Scala) "_.unary'_~"
 | constant "(AND) :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.andb ((_),/ (_))" and
   (Haskell) infixl 7 "Data_Bits..&." and
   (OCaml) "Int32.logand" and
   (Scala) infixl 3 "&"
 | constant "(OR) :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.orb ((_),/ (_))" and
   (Haskell) infixl 5 "Data_Bits..|." and
   (OCaml) "Int32.logor" and
   (Scala) infixl 1 "|"
 | constant "(XOR) :: uint32 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Word32.xorb ((_),/ (_))" and
   (Haskell) "Data'_Bits.xor" and
   (OCaml) "Int32.logxor" and
   (Scala) infixl 2 "^"
 
 definition uint32_divmod :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32 \<times> uint32" where
   "uint32_divmod x y = 
   (if y = 0 then (undefined ((div) :: uint32 \<Rightarrow> _) x (0 :: uint32), undefined ((mod) :: uint32 \<Rightarrow> _) x (0 :: uint32)) 
   else (x div y, x mod y))"
 
 definition uint32_div :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" 
 where "uint32_div x y = fst (uint32_divmod x y)"
 
 definition uint32_mod :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" 
 where "uint32_mod x y = snd (uint32_divmod x y)"
 
 lemma div_uint32_code [code]: "x div y = (if y = 0 then 0 else uint32_div x y)"
 including undefined_transfer unfolding uint32_divmod_def uint32_div_def
 by transfer (simp add: word_div_def)
 
 lemma mod_uint32_code [code]: "x mod y = (if y = 0 then x else uint32_mod x y)"
 including undefined_transfer unfolding uint32_mod_def uint32_divmod_def
 by transfer (simp add: word_mod_def)
 
 definition uint32_sdiv :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32"
 where [code del]:
   "uint32_sdiv x y =
    (if y = 0 then undefined ((div) :: uint32 \<Rightarrow> _) x (0 :: uint32)
     else Abs_uint32 (Rep_uint32 x sdiv Rep_uint32 y))"
 
 definition div0_uint32 :: "uint32 \<Rightarrow> uint32"
 where [code del]: "div0_uint32 x = undefined ((div) :: uint32 \<Rightarrow> _) x (0 :: uint32)"
 declare [[code abort: div0_uint32]]
 
 definition mod0_uint32 :: "uint32 \<Rightarrow> uint32"
 where [code del]: "mod0_uint32 x = undefined ((mod) :: uint32 \<Rightarrow> _) x (0 :: uint32)"
 declare [[code abort: mod0_uint32]]
 
 lemma uint32_divmod_code [code]:
   "uint32_divmod x y =
   (if 0x80000000 \<le> y then if x < y then (0, x) else (1, x - y)
    else if y = 0 then (div0_uint32 x, mod0_uint32 x)
    else let q = (uint32_sdiv (x >> 1) y) << 1;
             r = x - q * y
         in if r \<ge> y then (q + 1, r - y) else (q, r))"
 including undefined_transfer unfolding uint32_divmod_def uint32_sdiv_def div0_uint32_def mod0_uint32_def
 by transfer(simp add: divmod_via_sdivmod)
 
 lemma uint32_sdiv_code [code abstract]:
   "Rep_uint32 (uint32_sdiv x y) =
    (if y = 0 then Rep_uint32 (undefined ((div) :: uint32 \<Rightarrow> _) x (0 :: uint32))
     else Rep_uint32 x sdiv Rep_uint32 y)"
 unfolding uint32_sdiv_def by(simp add: Abs_uint32_inverse)
 
 text \<open>
   Note that we only need a translation for signed division, but not for the remainder
   because @{thm uint32_divmod_code} computes both with division only.
 \<close>
 
 code_printing
   constant uint32_div \<rightharpoonup>
   (SML) "Word32.div ((_), (_))" and
   (Haskell) "Prelude.div"
 | constant uint32_mod \<rightharpoonup>
   (SML) "Word32.mod ((_), (_))" and
   (Haskell) "Prelude.mod"
 | constant uint32_divmod \<rightharpoonup>
   (Haskell) "divmod"
 | constant uint32_sdiv \<rightharpoonup>
   (OCaml) "Int32.div" and
   (Scala) "_ '/ _"
 
 definition uint32_test_bit :: "uint32 \<Rightarrow> integer \<Rightarrow> bool"
 where [code del]:
   "uint32_test_bit x n =
   (if n < 0 \<or> 31 < n then undefined (test_bit :: uint32 \<Rightarrow> _) x n
    else x !! (nat_of_integer n))"
 
 lemma test_bit_eq_bit_uint32 [code]:
   \<open>test_bit = (bit :: uint32 \<Rightarrow> _)\<close>
   by (rule ext)+ (transfer, transfer, simp)
 
 lemma test_bit_uint32_code [code]:
   "bit x n \<longleftrightarrow> n < 32 \<and> uint32_test_bit x (integer_of_nat n)"
   including undefined_transfer integer.lifting unfolding uint32_test_bit_def
   by (transfer, simp, transfer, simp)
 
 lemma uint32_test_bit_code [code]:
   "uint32_test_bit w n =
   (if n < 0 \<or> 31 < n then undefined (test_bit :: uint32 \<Rightarrow> _) w n else Rep_uint32 w !! nat_of_integer n)"
 unfolding uint32_test_bit_def
 by(simp add: test_bit_uint32.rep_eq)
 
 code_printing constant uint32_test_bit \<rightharpoonup>
   (SML) "Uint32.test'_bit" and
   (Haskell) "Data'_Bits.testBitBounded" and
   (OCaml) "Uint32.test'_bit" and
   (Scala) "Uint32.test'_bit" and
   (Eval) "(fn w => fn n => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_test'_bit out of bounds\") else Uint32.test'_bit w n)"
 
 definition uint32_set_bit :: "uint32 \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> uint32"
 where [code del]:
   "uint32_set_bit x n b =
   (if n < 0 \<or> 31 < n then undefined (set_bit :: uint32 \<Rightarrow> _) x n b
    else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_uint32_code [code]:
   "set_bit x n b = (if n < 32 then uint32_set_bit x (integer_of_nat n) b else x)"
 including undefined_transfer integer.lifting unfolding uint32_set_bit_def
 by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
 
 lemma uint32_set_bit_code [code abstract]:
   "Rep_uint32 (uint32_set_bit w n b) = 
   (if n < 0 \<or> 31 < n then Rep_uint32 (undefined (set_bit :: uint32 \<Rightarrow> _) w n b)
    else set_bit (Rep_uint32 w) (nat_of_integer n) b)"
 including undefined_transfer unfolding uint32_set_bit_def by transfer simp
 
 code_printing constant uint32_set_bit \<rightharpoonup>
   (SML) "Uint32.set'_bit" and
   (Haskell) "Data'_Bits.setBitBounded" and
   (OCaml) "Uint32.set'_bit" and
   (Scala) "Uint32.set'_bit" and
   (Eval) "(fn w => fn n => fn b => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_set'_bit out of bounds\") else Uint32.set'_bit x n b)"
 
 lift_definition uint32_set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> uint32 \<Rightarrow> nat \<Rightarrow> uint32" is set_bits_aux .
 
 lemma uint32_set_bits_code [code]:
   "uint32_set_bits f w n =
   (if n = 0 then w 
    else let n' = n - 1 in uint32_set_bits f ((w << 1) OR (if f n' then 1 else 0)) n')"
 by(transfer fixing: n)(cases n, simp_all)
 
 lemma set_bits_uint32 [code]:
   "(BITS n. f n) = uint32_set_bits f 0 32"
 by transfer(simp add: set_bits_conv_set_bits_aux)
 
 
 lemma lsb_code [code]: fixes x :: uint32 shows "lsb x = x !! 0"
 by transfer(simp add: word_lsb_def word_test_bit_def)
 
 
 definition uint32_shiftl :: "uint32 \<Rightarrow> integer \<Rightarrow> uint32"
 where [code del]:
   "uint32_shiftl x n = (if n < 0 \<or> 32 \<le> n then undefined (shiftl :: uint32 \<Rightarrow> _) x n else x << (nat_of_integer n))"
 
 lemma shiftl_uint32_code [code]: "x << n = (if n < 32 then uint32_shiftl x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint32_shiftl_def
 by transfer(simp add: not_less shiftl_zero_size word_size)
 
 lemma uint32_shiftl_code [code abstract]:
   "Rep_uint32 (uint32_shiftl w n) =
   (if n < 0 \<or> 32 \<le> n then Rep_uint32 (undefined (shiftl :: uint32 \<Rightarrow> _) w n) else Rep_uint32 w << (nat_of_integer n))"
 including undefined_transfer unfolding uint32_shiftl_def by transfer simp
 
 code_printing constant uint32_shiftl \<rightharpoonup>
   (SML) "Uint32.shiftl" and
   (Haskell) "Data'_Bits.shiftlBounded" and
   (OCaml) "Uint32.shiftl" and
   (Scala) "Uint32.shiftl" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftl out of bounds\" else Uint32.shiftl x i)"
 
 definition uint32_shiftr :: "uint32 \<Rightarrow> integer \<Rightarrow> uint32"
 where [code del]:
   "uint32_shiftr x n = (if n < 0 \<or> 32 \<le> n then undefined (shiftr :: uint32 \<Rightarrow> _) x n else x >> (nat_of_integer n))"
 
 lemma shiftr_uint32_code [code]: "x >> n = (if n < 32 then uint32_shiftr x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint32_shiftr_def
 by transfer(simp add: not_less shiftr_zero_size word_size)
 
 lemma uint32_shiftr_code [code abstract]:
   "Rep_uint32 (uint32_shiftr w n) =
   (if n < 0 \<or> 32 \<le> n then Rep_uint32 (undefined (shiftr :: uint32 \<Rightarrow> _) w n) else Rep_uint32 w >> nat_of_integer n)"
 including undefined_transfer unfolding uint32_shiftr_def by transfer simp
 
 code_printing constant uint32_shiftr \<rightharpoonup>
   (SML) "Uint32.shiftr" and
   (Haskell) "Data'_Bits.shiftrBounded" and
   (OCaml) "Uint32.shiftr" and
   (Scala) "Uint32.shiftr" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr out of bounds\" else Uint32.shiftr x i)"
 
 definition uint32_sshiftr :: "uint32 \<Rightarrow> integer \<Rightarrow> uint32"
 where [code del]:
   "uint32_sshiftr x n =
   (if n < 0 \<or> 32 \<le> n then undefined sshiftr_uint32 x n else sshiftr_uint32 x (nat_of_integer n))"
 
 lemma sshiftr_beyond: fixes x :: "'a :: len word" shows
   "size x \<le> n \<Longrightarrow> x >>> n = (if x !! (size x - 1) then -1 else 0)"
 by(rule word_eqI)(simp add: nth_sshiftr word_size)
 
 lemma sshiftr_uint32_code [code]:
   "x >>> n = 
   (if n < 32 then uint32_sshiftr x (integer_of_nat n) else if x !! 31 then -1 else 0)"
 including undefined_transfer integer.lifting unfolding uint32_sshiftr_def
 by transfer(simp add: not_less sshiftr_beyond word_size)
 
 lemma uint32_sshiftr_code [code abstract]:
   "Rep_uint32 (uint32_sshiftr w n) =
   (if n < 0 \<or> 32 \<le> n then Rep_uint32 (undefined sshiftr_uint32 w n) else Rep_uint32 w >>> (nat_of_integer n))"
 including undefined_transfer unfolding uint32_sshiftr_def by transfer simp
 
 code_printing constant uint32_sshiftr \<rightharpoonup>
   (SML) "Uint32.shiftr'_signed" and
   (Haskell) 
     "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Int32) _)) :: Uint32.Word32)" and
   (OCaml) "Uint32.shiftr'_signed" and
   (Scala) "Uint32.shiftr'_signed" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr'_signed out of bounds\" else Uint32.shiftr'_signed x i)"
 
 lemma uint32_msb_test_bit: "msb x \<longleftrightarrow> (x :: uint32) !! 31"
 by transfer(simp add: msb_nth)
 
 lemma msb_uint32_code [code]: "msb x \<longleftrightarrow> uint32_test_bit x 31"
 by(simp add: uint32_test_bit_def uint32_msb_test_bit)
 
 lemma uint32_of_int_code [code]: "uint32_of_int i = Uint32 (integer_of_int i)"
 including integer.lifting by transfer simp
 
 lemma int_of_uint32_code [code]:
   "int_of_uint32 x = int_of_integer (integer_of_uint32 x)"
 by(simp add: integer_of_uint32_def)
 
 lemma nat_of_uint32_code [code]:
   "nat_of_uint32 x = nat_of_integer (integer_of_uint32 x)"
 unfolding integer_of_uint32_def including integer.lifting by transfer (simp add: unat_def)
 
 definition integer_of_uint32_signed :: "uint32 \<Rightarrow> integer"
 where
   "integer_of_uint32_signed n = (if n !! 31 then undefined integer_of_uint32 n else integer_of_uint32 n)"
 
 lemma integer_of_uint32_signed_code [code]:
   "integer_of_uint32_signed n =
   (if n !! 31 then undefined integer_of_uint32 n else integer_of_int (uint (Rep_uint32' n)))"
 unfolding integer_of_uint32_signed_def integer_of_uint32_def
 including undefined_transfer by transfer simp
 
 lemma integer_of_uint32_code [code]:
   "integer_of_uint32 n =
   (if n !! 31 then integer_of_uint32_signed (n AND 0x7FFFFFFF) OR 0x80000000 else integer_of_uint32_signed n)"
 unfolding integer_of_uint32_def integer_of_uint32_signed_def o_def
 including undefined_transfer integer.lifting
 by transfer(auto simp add: word_ao_nth uint_and_mask_or_full mask_numeral mask_Suc_0 intro!: uint_and_mask_or_full[symmetric])
 
 code_printing
   constant "integer_of_uint32" \<rightharpoonup>
   (SML) "IntInf.fromLarge (Word32.toLargeInt _) : IntInf.int" and
   (Haskell) "Prelude.toInteger"
 | constant "integer_of_uint32_signed" \<rightharpoonup>
   (OCaml) "Z.of'_int32" and
   (Scala) "BigInt"
 
 section \<open>Quickcheck setup\<close>
 
 definition uint32_of_natural :: "natural \<Rightarrow> uint32"
 where "uint32_of_natural x \<equiv> Uint32 (integer_of_natural x)"
 
 instantiation uint32 :: "{random, exhaustive, full_exhaustive}" begin
 definition "random_uint32 \<equiv> qc_random_cnv uint32_of_natural"
 definition "exhaustive_uint32 \<equiv> qc_exhaustive_cnv uint32_of_natural"
 definition "full_exhaustive_uint32 \<equiv> qc_full_exhaustive_cnv uint32_of_natural"
 instance ..
 end
 
 instantiation uint32 :: narrowing begin
 
 interpretation quickcheck_narrowing_samples
   "\<lambda>i. let x = Uint32 i in (x, 0xFFFFFFFF - x)" "0"
   "Typerep.Typerep (STR ''Uint32.uint32'') []" .
 
 definition "narrowing_uint32 d = qc_narrowing_drawn_from (narrowing_samples d) d"
 declare [[code drop: "partial_term_of :: uint32 itself \<Rightarrow> _"]]
 lemmas partial_term_of_uint32 [code] = partial_term_of_code
 
 instance ..
 end
 
 no_notation sshiftr_uint32 (infixl ">>>" 55)
 
 end
diff --git a/thys/Native_Word/Uint64.thy b/thys/Native_Word/Uint64.thy
--- a/thys/Native_Word/Uint64.thy
+++ b/thys/Native_Word/Uint64.thy
@@ -1,921 +1,917 @@
 (*  Title:      Uint64.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Unsigned words of 64 bits\<close>
 
 theory Uint64 imports
   Code_Target_Word_Base
 begin
 
 text \<open>
   PolyML (in version 5.7) provides a Word64 structure only when run in 64-bit mode.
   Therefore, we by default provide an implementation of 64-bit words using \verb$IntInf.int$ and
   masking. The code target \texttt{SML\_word} replaces this implementation and maps the operations
   directly to the \verb$Word64$ structure provided by the Standard ML implementations.
 
   The \verb$Eval$ target used by @{command value} and @{method eval} dynamically tests at
   runtime for the version of PolyML and uses PolyML's Word64 structure if it detects a 64-bit 
   version which does not suffer from a division bug found in PolyML 5.6.
 \<close>
 
 declare prod.Quotient[transfer_rule]
 
 section \<open>Type definition and primitive operations\<close>
 
 typedef uint64 = "UNIV :: 64 word set" .. 
 
 setup_lifting type_definition_uint64
 
 text \<open>Use an abstract type for code generation to disable pattern matching on @{term Abs_uint64}.\<close>
 declare Rep_uint64_inverse[code abstype]
 
 declare Quotient_uint64[transfer_rule]
 
 instantiation uint64 :: comm_ring_1
 begin
 lift_definition zero_uint64 :: uint64 is "0 :: 64 word" .
 lift_definition one_uint64 :: uint64 is "1" .
 lift_definition plus_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(+) :: 64 word \<Rightarrow> _" .
 lift_definition minus_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(-)" .
 lift_definition uminus_uint64 :: "uint64 \<Rightarrow> uint64" is uminus .
 lift_definition times_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(*)" .
 instance by (standard; transfer) (simp_all add: algebra_simps)
 end
 
 instantiation uint64 :: semiring_modulo
 begin
 lift_definition divide_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(div)" .
 lift_definition modulo_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is "(mod)" .
 instance by (standard; transfer) (fact word_mod_div_equality)
 end
 
 instantiation uint64 :: linorder begin
 lift_definition less_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> bool" is "(<)" .
 lift_definition less_eq_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> bool" is "(\<le>)" .
 instance by (standard; transfer) (simp_all add: less_le_not_le linear)
 end
 
 lemmas [code] = less_uint64.rep_eq less_eq_uint64.rep_eq
 
 context
   includes lifting_syntax
   notes
     transfer_rule_of_bool [transfer_rule]
     transfer_rule_numeral [transfer_rule]
 begin
 
 lemma [transfer_rule]:
   "((=) ===> cr_uint64) of_bool of_bool"
   by transfer_prover
 
 lemma transfer_rule_numeral_uint [transfer_rule]:
   "((=) ===> cr_uint64) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   \<open>(cr_uint64 ===> (\<longleftrightarrow>)) even ((dvd) 2 :: uint64 \<Rightarrow> bool)\<close>
   by (unfold dvd_def) transfer_prover
 
 end
 
 instantiation uint64 :: semiring_bits
 begin
 
 lift_definition bit_uint64 :: \<open>uint64 \<Rightarrow> nat \<Rightarrow> bool\<close> is bit .
 
 instance
   by (standard; transfer)
     (fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
        bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
        even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
        div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+
 
 end
 
 instantiation uint64 :: semiring_bit_shifts
 begin
 lift_definition push_bit_uint64 :: \<open>nat \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is push_bit .
 lift_definition drop_bit_uint64 :: \<open>nat \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is drop_bit .
 lift_definition take_bit_uint64 :: \<open>nat \<Rightarrow> uint64 \<Rightarrow> uint64\<close> is take_bit .
 instance by (standard; transfer)
   (fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
 end
 
 instantiation uint64 :: ring_bit_operations
 begin
 lift_definition not_uint64 :: "uint64 \<Rightarrow> uint64" is NOT .
 lift_definition and_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is \<open>(AND)\<close> .
 lift_definition or_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is \<open>(OR)\<close> .
 lift_definition xor_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" is \<open>(XOR)\<close> .
 instance by (standard; transfer)
   (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1)
 end
 
 instantiation uint64 :: bit_operations
 begin
 lift_definition test_bit_uint64 :: "uint64 \<Rightarrow> nat \<Rightarrow> bool" is test_bit .
 lift_definition set_bit_uint64 :: "uint64 \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> uint64" is set_bit .
 lift_definition lsb_uint64 :: "uint64 \<Rightarrow> bool" is lsb .
 lift_definition shiftl_uint64 :: "uint64 \<Rightarrow> nat \<Rightarrow> uint64" is shiftl .
 lift_definition shiftr_uint64 :: "uint64 \<Rightarrow> nat \<Rightarrow> uint64" is shiftr .
 lift_definition msb_uint64 :: "uint64 \<Rightarrow> bool" is msb .
 instance ..
 end
 
 instantiation uint64 :: bit_comprehension begin
 lift_definition set_bits_uint64 :: "(nat \<Rightarrow> bool) \<Rightarrow> uint64" is "set_bits" .
 instance ..
 end
 
 lemmas [code] = test_bit_uint64.rep_eq lsb_uint64.rep_eq msb_uint64.rep_eq
 
 instantiation uint64 :: equal begin
 lift_definition equal_uint64 :: "uint64 \<Rightarrow> uint64 \<Rightarrow> bool" is "equal_class.equal" .
 instance by standard (transfer, simp add: equal_eq)
 end
 
 lemmas [code] = equal_uint64.rep_eq
 
 instantiation uint64 :: size begin
 lift_definition size_uint64 :: "uint64 \<Rightarrow> nat" is "size" .
 instance ..
 end
 
 lemmas [code] = size_uint64.rep_eq
 
 lift_definition sshiftr_uint64 :: "uint64 \<Rightarrow> nat \<Rightarrow> uint64" (infixl ">>>" 55) is sshiftr .
 
 lift_definition uint64_of_int :: "int \<Rightarrow> uint64" is "word_of_int" .
 
 definition uint64_of_nat :: "nat \<Rightarrow> uint64"
 where "uint64_of_nat = uint64_of_int \<circ> int"
 
 lift_definition int_of_uint64 :: "uint64 \<Rightarrow> int" is "uint" .
 lift_definition nat_of_uint64 :: "uint64 \<Rightarrow> nat" is "unat" .
 
 definition integer_of_uint64 :: "uint64 \<Rightarrow> integer"
 where "integer_of_uint64 = integer_of_int o int_of_uint64"
 
-lemma bitval_integer_transfer [transfer_rule]:
-  "(rel_fun (=) pcr_integer) of_bool of_bool"
-by(auto simp add: of_bool_def integer.pcr_cr_eq cr_integer_def split: bit.split)
-
 text \<open>Use pretty numerals from integer for pretty printing\<close>
 
 context includes integer.lifting begin
 
 lift_definition Uint64 :: "integer \<Rightarrow> uint64" is "word_of_int" .
 
 lemma Rep_uint64_numeral [simp]: "Rep_uint64 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint64_def Abs_uint64_inverse numeral.simps plus_uint64_def)
 
 lemma numeral_uint64_transfer [transfer_rule]:
   "(rel_fun (=) cr_uint64) numeral numeral"
 by(auto simp add: cr_uint64_def)
 
 lemma numeral_uint64 [code_unfold]: "numeral n = Uint64 (numeral n)"
 by transfer simp
 
 lemma Rep_uint64_neg_numeral [simp]: "Rep_uint64 (- numeral n) = - numeral n"
 by(simp only: uminus_uint64_def)(simp add: Abs_uint64_inverse)
 
 lemma neg_numeral_uint64 [code_unfold]: "- numeral n = Uint64 (- numeral n)"
 by transfer(simp add: cr_uint64_def)
 
 end
 
 lemma Abs_uint64_numeral [code_post]: "Abs_uint64 (numeral n) = numeral n"
 by(induction n)(simp_all add: one_uint64_def numeral.simps plus_uint64_def Abs_uint64_inverse)
 
 lemma Abs_uint64_0 [code_post]: "Abs_uint64 0 = 0"
 by(simp add: zero_uint64_def)
 
 lemma Abs_uint64_1 [code_post]: "Abs_uint64 1 = 1"
 by(simp add: one_uint64_def)
 
 section \<open>Code setup\<close>
 
 text \<open> For SML, we generate an implementation of unsigned 64-bit words using \verb$IntInf.int$.
   If @{ML "LargeWord.wordSize > 63"} of the Isabelle/ML runtime environment holds, then we assume
   that there is also a \<open>Word64\<close> structure available and accordingly replace the implementation
   for the target \verb$Eval$.
 \<close>
 code_printing code_module "Uint64" \<rightharpoonup> (SML) \<open>(* Test that words can handle numbers between 0 and 63 *)
 val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6"));
 
 structure Uint64 : sig
   eqtype uint64;
   val zero : uint64;
   val one : uint64;
   val fromInt : IntInf.int -> uint64;
   val toInt : uint64 -> IntInf.int;
   val toLarge : uint64 -> LargeWord.word;
   val fromLarge : LargeWord.word -> uint64
   val plus : uint64 -> uint64 -> uint64;
   val minus : uint64 -> uint64 -> uint64;
   val times : uint64 -> uint64 -> uint64;
   val divide : uint64 -> uint64 -> uint64;
   val modulus : uint64 -> uint64 -> uint64;
   val negate : uint64 -> uint64;
   val less_eq : uint64 -> uint64 -> bool;
   val less : uint64 -> uint64 -> bool;
   val notb : uint64 -> uint64;
   val andb : uint64 -> uint64 -> uint64;
   val orb : uint64 -> uint64 -> uint64;
   val xorb : uint64 -> uint64 -> uint64;
   val shiftl : uint64 -> IntInf.int -> uint64;
   val shiftr : uint64 -> IntInf.int -> uint64;
   val shiftr_signed : uint64 -> IntInf.int -> uint64;
   val set_bit : uint64 -> IntInf.int -> bool -> uint64;
   val test_bit : uint64 -> IntInf.int -> bool;
 end = struct
 
 type uint64 = IntInf.int;
 
 val mask = 0xFFFFFFFFFFFFFFFF : IntInf.int;
 
 val zero = 0 : IntInf.int;
 
 val one = 1 : IntInf.int;
 
 fun fromInt x = IntInf.andb(x, mask);
 
 fun toInt x = x
 
 fun toLarge x = LargeWord.fromLargeInt (IntInf.toLarge x);
 
 fun fromLarge x = IntInf.fromLarge (LargeWord.toLargeInt x);
 
 fun plus x y = IntInf.andb(IntInf.+(x, y), mask);
 
 fun minus x y = IntInf.andb(IntInf.-(x, y), mask);
 
 fun negate x = IntInf.andb(IntInf.~(x), mask);
 
 fun times x y = IntInf.andb(IntInf.*(x, y), mask);
 
 fun divide x y = IntInf.div(x, y);
 
 fun modulus x y = IntInf.mod(x, y);
 
 fun less_eq x y = IntInf.<=(x, y);
 
 fun less x y = IntInf.<(x, y);
 
 fun notb x = IntInf.andb(IntInf.notb(x), mask);
 
 fun orb x y = IntInf.orb(x, y);
 
 fun andb x y = IntInf.andb(x, y);
 
 fun xorb x y = IntInf.xorb(x, y);
 
 val maxWord = IntInf.pow (2, Word.wordSize);
 
 fun shiftl x n = 
   if n < maxWord then IntInf.andb(IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)), mask)
   else 0;
 
 fun shiftr x n =
   if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
   else 0;
 
 val msb_mask = 0x8000000000000000 : IntInf.int;
 
 fun shiftr_signed x i =
   if IntInf.andb(x, msb_mask) = 0 then shiftr x i
   else if i >= 64 then 0xFFFFFFFFFFFFFFFF
   else let
     val x' = shiftr x i
     val m' = IntInf.andb(IntInf.<<(mask, Word.max(0w64 - Word.fromLargeInt (IntInf.toLarge i), 0w0)), mask)
   in IntInf.orb(x', m') end;
 
 fun test_bit x n =
   if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
   else false;
 
 fun set_bit x n b =
   if n < 64 then
     if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))
     else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))))
   else x;
 
 end
 \<close>
 code_reserved SML Uint64
 
 setup \<open>
 let
   val polyml64 = LargeWord.wordSize > 63;
   (* PolyML 5.6 has bugs in its Word64 implementation. We test for one such bug and refrain
      from using Word64 in that case. Testing is done with dynamic code evaluation such that
      the compiler does not choke on the Word64 structure, which need not be present in a 32bit
      environment. *)
   val error_msg = "Buggy Word64 structure";
   val test_code = 
    "val _ = if Word64.div (0w18446744073709551611 : Word64.word, 0w3) = 0w6148914691236517203 then ()\n" ^
    "else raise (Fail \"" ^ error_msg ^ "\");";
   val f = Exn.interruptible_capture (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code))
   val use_Word64 = polyml64 andalso
     (case f () of 
        Exn.Res _ => true
      | Exn.Exn (e as ERROR m) => if String.isSuffix error_msg m then false else Exn.reraise e
      | Exn.Exn e => Exn.reraise e)
     ;
 
   val newline = "\n";
   val content = 
     "structure Uint64 : sig" ^ newline ^
     "  eqtype uint64;" ^ newline ^
     "  val zero : uint64;" ^ newline ^
     "  val one : uint64;" ^ newline ^
     "  val fromInt : IntInf.int -> uint64;" ^ newline ^
     "  val toInt : uint64 -> IntInf.int;" ^ newline ^
     "  val toLarge : uint64 -> LargeWord.word;" ^ newline ^
     "  val fromLarge : LargeWord.word -> uint64" ^ newline ^
     "  val plus : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val minus : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val times : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val divide : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val modulus : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val negate : uint64 -> uint64;" ^ newline ^
     "  val less_eq : uint64 -> uint64 -> bool;" ^ newline ^
     "  val less : uint64 -> uint64 -> bool;" ^ newline ^
     "  val notb : uint64 -> uint64;" ^ newline ^
     "  val andb : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val orb : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val xorb : uint64 -> uint64 -> uint64;" ^ newline ^
     "  val shiftl : uint64 -> IntInf.int -> uint64;" ^ newline ^
     "  val shiftr : uint64 -> IntInf.int -> uint64;" ^ newline ^
     "  val shiftr_signed : uint64 -> IntInf.int -> uint64;" ^ newline ^
     "  val set_bit : uint64 -> IntInf.int -> bool -> uint64;" ^ newline ^
     "  val test_bit : uint64 -> IntInf.int -> bool;" ^ newline ^
     "end = struct" ^ newline ^
     "" ^ newline ^
     "type uint64 = Word64.word;" ^ newline ^
     "" ^ newline ^
     "val zero = (0wx0 : uint64);" ^ newline ^
     "" ^ newline ^
     "val one = (0wx1 : uint64);" ^ newline ^
     "" ^ newline ^
     "fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);" ^ newline ^
     "" ^ newline ^
     "fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);"  ^ newline ^
     "" ^ newline ^
     "fun fromLarge x = Word64.fromLarge x;" ^ newline ^
     "" ^ newline ^
     "fun toLarge x = Word64.toLarge x;"  ^ newline ^
     "" ^ newline ^
     "fun plus x y = Word64.+(x, y);" ^ newline ^
     "" ^ newline ^
     "fun minus x y = Word64.-(x, y);" ^ newline ^
     "" ^ newline ^
     "fun negate x = Word64.~(x);" ^ newline ^
     "" ^ newline ^
     "fun times x y = Word64.*(x, y);" ^ newline ^
     "" ^ newline ^
     "fun divide x y = Word64.div(x, y);" ^ newline ^
     "" ^ newline ^
     "fun modulus x y = Word64.mod(x, y);" ^ newline ^
     "" ^ newline ^
     "fun less_eq x y = Word64.<=(x, y);" ^ newline ^
     "" ^ newline ^
     "fun less x y = Word64.<(x, y);" ^ newline ^
     "" ^ newline ^
     "fun set_bit x n b =" ^ newline ^
     "  let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
     "  in if b then Word64.orb (x, mask)" ^ newline ^
     "     else Word64.andb (x, Word64.notb mask)" ^ newline ^
     "  end" ^ newline ^
     "" ^ newline ^
     "fun shiftl x n =" ^ newline ^
     "  Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
     "" ^ newline ^
     "fun shiftr x n =" ^ newline ^
     "  Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
     "" ^ newline ^
     "fun shiftr_signed x n =" ^ newline ^
     "  Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
     "" ^ newline ^
     "fun test_bit x n =" ^ newline ^
     "  Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0" ^ newline ^
     "" ^ newline ^
     "val notb = Word64.notb" ^ newline ^
     "" ^ newline ^
     "fun andb x y = Word64.andb(x, y);" ^ newline ^
     "" ^ newline ^
     "fun orb x y = Word64.orb(x, y);" ^ newline ^
     "" ^ newline ^
     "fun xorb x y = Word64.xorb(x, y);" ^ newline ^
     "" ^ newline ^
     "end (*struct Uint64*)"
   val target_SML64 = "SML_word";
 in
   (if use_Word64 then Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(Code_Runtime.target, SOME (content, []))])) else I)
   #> Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(target_SML64, SOME (content, []))]))
 end
 \<close>
 
 code_printing code_module Uint64 \<rightharpoonup> (Haskell)
  \<open>module Uint64(Int64, Word64) where
 
   import Data.Int(Int64)
   import Data.Word(Word64)\<close>
 code_reserved Haskell Uint64
 
 text \<open>
   OCaml and Scala provide only signed 64bit numbers, so we use these and 
   implement sign-sensitive operations like comparisons manually.
 \<close>
 code_printing code_module "Uint64" \<rightharpoonup> (OCaml)
 \<open>module Uint64 : sig
   val less : int64 -> int64 -> bool
   val less_eq : int64 -> int64 -> bool
   val set_bit : int64 -> Z.t -> bool -> int64
   val shiftl : int64 -> Z.t -> int64
   val shiftr : int64 -> Z.t -> int64
   val shiftr_signed : int64 -> Z.t -> int64
   val test_bit : int64 -> Z.t -> bool
 end = struct
 
 (* negative numbers have their highest bit set, 
    so they are greater than positive ones *)
 let less x y =
   if Int64.compare x Int64.zero < 0 then
     Int64.compare y Int64.zero < 0 && Int64.compare x y < 0
   else Int64.compare y Int64.zero < 0 || Int64.compare x y < 0;;
 
 let less_eq x y =
   if Int64.compare x Int64.zero < 0 then
     Int64.compare y Int64.zero < 0 && Int64.compare x y <= 0
   else Int64.compare y Int64.zero < 0 || Int64.compare x y <= 0;;
 
 let set_bit x n b =
   let mask = Int64.shift_left Int64.one (Z.to_int n)
   in if b then Int64.logor x mask
      else Int64.logand x (Int64.lognot mask);;
 
 let shiftl x n = Int64.shift_left x (Z.to_int n);;
 
 let shiftr x n = Int64.shift_right_logical x (Z.to_int n);;
 
 let shiftr_signed x n = Int64.shift_right x (Z.to_int n);;
 
 let test_bit x n =
   Int64.compare 
     (Int64.logand x (Int64.shift_left Int64.one (Z.to_int n)))
     Int64.zero
   <> 0;;
 
 end;; (*struct Uint64*)\<close>
 code_reserved OCaml Uint64
 
 code_printing code_module Uint64 \<rightharpoonup> (Scala)
 \<open>object Uint64 {
 
 def less(x: Long, y: Long) : Boolean =
   if (x < 0) y < 0 && x < y
   else y < 0 || x < y
 
 def less_eq(x: Long, y: Long) : Boolean =
   if (x < 0) y < 0 && x <= y
   else y < 0 || x <= y
 
 def set_bit(x: Long, n: BigInt, b: Boolean) : Long =
   if (b)
     x | (1L << n.intValue)
   else
     x & (1L << n.intValue).unary_~
 
 def shiftl(x: Long, n: BigInt) : Long = x << n.intValue
 
 def shiftr(x: Long, n: BigInt) : Long = x >>> n.intValue
 
 def shiftr_signed(x: Long, n: BigInt) : Long = x >> n.intValue
 
 def test_bit(x: Long, n: BigInt) : Boolean =
   (x & (1L << n.intValue)) != 0
 
 } /* object Uint64 */\<close>
 code_reserved Scala Uint64
 
 text \<open>
   OCaml's conversion from Big\_int to int64 demands that the value fits int a signed 64-bit integer.
   The following justifies the implementation.
 \<close>
 
 definition Uint64_signed :: "integer \<Rightarrow> uint64" 
 where "Uint64_signed i = (if i < -(0x8000000000000000) \<or> i \<ge> 0x8000000000000000 then undefined Uint64 i else Uint64 i)"
 
 lemma Uint64_code [code]:
   "Uint64 i = 
   (let i' = i AND 0xFFFFFFFFFFFFFFFF
    in if i' !! 63 then Uint64_signed (i' - 0x10000000000000000) else Uint64_signed i')"
 including undefined_transfer integer.lifting unfolding Uint64_signed_def
 by transfer(rule word_of_int_via_signed, simp_all add: bin_mask_numeral)
 
 lemma Uint64_signed_code [code abstract]:
   "Rep_uint64 (Uint64_signed i) = 
   (if i < -(0x8000000000000000) \<or> i \<ge> 0x8000000000000000 then Rep_uint64 (undefined Uint64 i) else word_of_int (int_of_integer_symbolic i))"
 unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def word_of_integer_def
 by(simp add: Abs_uint64_inverse)
 
 text \<open>
   Avoid @{term Abs_uint64} in generated code, use @{term Rep_uint64'} instead. 
   The symbolic implementations for code\_simp use @{term Rep_uint64}.
 
   The new destructor @{term Rep_uint64'} is executable.
   As the simplifier is given the [code abstract] equations literally, 
   we cannot implement @{term Rep_uint64} directly, because that makes code\_simp loop.
 
   If code generation raises Match, some equation probably contains @{term Rep_uint64} 
   ([code abstract] equations for @{typ uint64} may use @{term Rep_uint64} because
   these instances will be folded away.)
 
   To convert @{typ "64 word"} values into @{typ uint64}, use @{term "Abs_uint64'"}.
 \<close>
 
 definition Rep_uint64' where [simp]: "Rep_uint64' = Rep_uint64"
 
 lemma Rep_uint64'_transfer [transfer_rule]:
   "rel_fun cr_uint64 (=) (\<lambda>x. x) Rep_uint64'"
 unfolding Rep_uint64'_def by(rule uint64.rep_transfer)
 
 lemma Rep_uint64'_code [code]: "Rep_uint64' x = (BITS n. x !! n)"
 by transfer simp
 
 lift_definition Abs_uint64' :: "64 word \<Rightarrow> uint64" is "\<lambda>x :: 64 word. x" .
 
 lemma Abs_uint64'_code [code]:
   "Abs_uint64' x = Uint64 (integer_of_int (uint x))"
 including integer.lifting by transfer simp
 
 declare [[code drop: "term_of_class.term_of :: uint64 \<Rightarrow> _"]]
 
 lemma term_of_uint64_code [code]:
   defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" 
   shows
   "term_of_class.term_of x = 
    Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint64.uint64.Abs_uint64'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]]], TR (STR ''Uint64.uint64'') []]))
        (term_of_class.term_of (Rep_uint64' x))"
 by(simp add: term_of_anything)
 
 code_printing
   type_constructor uint64 \<rightharpoonup>
   (SML) "Uint64.uint64" and
   (Haskell) "Uint64.Word64" and
   (OCaml) "int64" and
   (Scala) "Long"
 | constant Uint64 \<rightharpoonup>
   (SML) "Uint64.fromInt" and
   (Haskell) "(Prelude.fromInteger _ :: Uint64.Word64)" and
   (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Word64)" and
   (Scala) "_.longValue"
 | constant Uint64_signed \<rightharpoonup>
   (OCaml) "Z.to'_int64"
 | constant "0 :: uint64" \<rightharpoonup>
   (SML) "Uint64.zero" and
   (Haskell) "(0 :: Uint64.Word64)" and
   (OCaml) "Int64.zero" and
   (Scala) "0"
 | constant "1 :: uint64" \<rightharpoonup>
   (SML) "Uint64.one" and
   (Haskell) "(1 :: Uint64.Word64)" and
   (OCaml) "Int64.one" and
   (Scala) "1"
 | constant "plus :: uint64 \<Rightarrow> _ " \<rightharpoonup>
   (SML) "Uint64.plus" and
   (Haskell) infixl 6 "+" and
   (OCaml) "Int64.add" and
   (Scala) infixl 7 "+"
 | constant "uminus :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.negate" and
   (Haskell) "negate" and
   (OCaml) "Int64.neg" and
   (Scala) "!(- _)"
 | constant "minus :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.minus" and
   (Haskell) infixl 6 "-" and
   (OCaml) "Int64.sub" and
   (Scala) infixl 7 "-"
 | constant "times :: uint64 \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.times" and
   (Haskell) infixl 7 "*" and
   (OCaml) "Int64.mul" and
   (Scala) infixl 8 "*"
 | constant "HOL.equal :: uint64 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "!((_ : Uint64.uint64) = _)" and
   (Haskell) infix 4 "==" and
   (OCaml) "(Int64.compare _ _ = 0)" and
   (Scala) infixl 5 "=="
 | class_instance uint64 :: equal \<rightharpoonup>
   (Haskell) -
 | constant "less_eq :: uint64 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Uint64.less'_eq" and
   (Haskell) infix 4 "<=" and
   (OCaml) "Uint64.less'_eq" and
   (Scala) "Uint64.less'_eq"
 | constant "less :: uint64 \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   (SML) "Uint64.less" and
   (Haskell) infix 4 "<" and
   (OCaml) "Uint64.less" and
   (Scala) "Uint64.less"
 | constant "NOT :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.notb" and
   (Haskell) "Data'_Bits.complement" and
   (OCaml) "Int64.lognot" and
   (Scala) "_.unary'_~"
 | constant "(AND) :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.andb" and
   (Haskell) infixl 7 "Data_Bits..&." and
   (OCaml) "Int64.logand" and
   (Scala) infixl 3 "&"
 | constant "(OR) :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.orb" and
   (Haskell) infixl 5 "Data_Bits..|." and
   (OCaml) "Int64.logor" and
   (Scala) infixl 1 "|"
 | constant "(XOR) :: uint64 \<Rightarrow> _" \<rightharpoonup>
   (SML) "Uint64.xorb" and
   (Haskell) "Data'_Bits.xor" and
   (OCaml) "Int64.logxor" and
   (Scala) infixl 2 "^"
 
 definition uint64_divmod :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64 \<times> uint64" where
   "uint64_divmod x y = 
   (if y = 0 then (undefined ((div) :: uint64 \<Rightarrow> _) x (0 :: uint64), undefined ((mod) :: uint64 \<Rightarrow> _) x (0 :: uint64)) 
   else (x div y, x mod y))"
 
 definition uint64_div :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" 
 where "uint64_div x y = fst (uint64_divmod x y)"
 
 definition uint64_mod :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64" 
 where "uint64_mod x y = snd (uint64_divmod x y)"
 
 lemma div_uint64_code [code]: "x div y = (if y = 0 then 0 else uint64_div x y)"
 including undefined_transfer unfolding uint64_divmod_def uint64_div_def
 by transfer (simp add: word_div_def)
 
 lemma mod_uint64_code [code]: "x mod y = (if y = 0 then x else uint64_mod x y)"
 including undefined_transfer unfolding uint64_mod_def uint64_divmod_def
 by transfer (simp add: word_mod_def)
 
 definition uint64_sdiv :: "uint64 \<Rightarrow> uint64 \<Rightarrow> uint64"
 where [code del]:
   "uint64_sdiv x y =
    (if y = 0 then undefined ((div) :: uint64 \<Rightarrow> _) x (0 :: uint64)
     else Abs_uint64 (Rep_uint64 x sdiv Rep_uint64 y))"
 
 definition div0_uint64 :: "uint64 \<Rightarrow> uint64"
 where [code del]: "div0_uint64 x = undefined ((div) :: uint64 \<Rightarrow> _) x (0 :: uint64)"
 declare [[code abort: div0_uint64]]
 
 definition mod0_uint64 :: "uint64 \<Rightarrow> uint64"
 where [code del]: "mod0_uint64 x = undefined ((mod) :: uint64 \<Rightarrow> _) x (0 :: uint64)"
 declare [[code abort: mod0_uint64]]
 
 lemma uint64_divmod_code [code]:
   "uint64_divmod x y =
   (if 0x8000000000000000 \<le> y then if x < y then (0, x) else (1, x - y)
    else if y = 0 then (div0_uint64 x, mod0_uint64 x)
    else let q = (uint64_sdiv (x >> 1) y) << 1;
             r = x - q * y
         in if r \<ge> y then (q + 1, r - y) else (q, r))"
 including undefined_transfer unfolding uint64_divmod_def uint64_sdiv_def div0_uint64_def mod0_uint64_def
 by transfer(simp add: divmod_via_sdivmod)
 
 lemma uint64_sdiv_code [code abstract]:
   "Rep_uint64 (uint64_sdiv x y) =
    (if y = 0 then Rep_uint64 (undefined ((div) :: uint64 \<Rightarrow> _) x (0 :: uint64))
     else Rep_uint64 x sdiv Rep_uint64 y)"
 unfolding uint64_sdiv_def by(simp add: Abs_uint64_inverse)
 
 text \<open>
   Note that we only need a translation for signed division, but not for the remainder
   because @{thm uint64_divmod_code} computes both with division only.
 \<close>
 
 code_printing
   constant uint64_div \<rightharpoonup>
   (SML) "Uint64.divide" and
   (Haskell) "Prelude.div"
 | constant uint64_mod \<rightharpoonup>
   (SML) "Uint64.modulus" and
   (Haskell) "Prelude.mod"
 | constant uint64_divmod \<rightharpoonup>
   (Haskell) "divmod"
 | constant uint64_sdiv \<rightharpoonup>
   (OCaml) "Int64.div" and
   (Scala) "_ '/ _"
 
 definition uint64_test_bit :: "uint64 \<Rightarrow> integer \<Rightarrow> bool"
 where [code del]:
   "uint64_test_bit x n =
   (if n < 0 \<or> 63 < n then undefined (test_bit :: uint64 \<Rightarrow> _) x n
    else x !! (nat_of_integer n))"
 
 lemma test_bit_eq_bit_uint64 [code]:
   \<open>test_bit = (bit :: uint64 \<Rightarrow> _)\<close>
   by (rule ext)+ (transfer, transfer, simp)
 
 lemma bit_uint64_code [code]:
   "bit x n \<longleftrightarrow> n < 64 \<and> uint64_test_bit x (integer_of_nat n)"
   including undefined_transfer integer.lifting unfolding uint64_test_bit_def
   by (transfer, simp, transfer, simp)
 
 lemma uint64_test_bit_code [code]:
   "uint64_test_bit w n =
   (if n < 0 \<or> 63 < n then undefined (test_bit :: uint64 \<Rightarrow> _) w n else Rep_uint64 w !! nat_of_integer n)"
 unfolding uint64_test_bit_def
 by(simp add: test_bit_uint64.rep_eq)
 
 code_printing constant uint64_test_bit \<rightharpoonup>
   (SML) "Uint64.test'_bit" and
   (Haskell) "Data'_Bits.testBitBounded" and
   (OCaml) "Uint64.test'_bit" and
   (Scala) "Uint64.test'_bit" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_test'_bit out of bounds\") else Uint64.test'_bit x i)"
 
 definition uint64_set_bit :: "uint64 \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> uint64"
 where [code del]:
   "uint64_set_bit x n b =
   (if n < 0 \<or> 63 < n then undefined (set_bit :: uint64 \<Rightarrow> _) x n b
    else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_uint64_code [code]:
   "set_bit x n b = (if n < 64 then uint64_set_bit x (integer_of_nat n) b else x)"
 including undefined_transfer integer.lifting unfolding uint64_set_bit_def
 by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
 
 lemma uint64_set_bit_code [code abstract]:
   "Rep_uint64 (uint64_set_bit w n b) = 
   (if n < 0 \<or> 63 < n then Rep_uint64 (undefined (set_bit :: uint64 \<Rightarrow> _) w n b)
    else set_bit (Rep_uint64 w) (nat_of_integer n) b)"
 including undefined_transfer unfolding uint64_set_bit_def by transfer simp
 
 code_printing constant uint64_set_bit \<rightharpoonup>
   (SML) "Uint64.set'_bit" and
   (Haskell) "Data'_Bits.setBitBounded" and
   (OCaml) "Uint64.set'_bit" and
   (Scala) "Uint64.set'_bit" and
   (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_set'_bit out of bounds\") else Uint64.set'_bit x i b)"
 
 lift_definition uint64_set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> uint64 \<Rightarrow> nat \<Rightarrow> uint64" is set_bits_aux .
 
 lemma uint64_set_bits_code [code]:
   "uint64_set_bits f w n =
   (if n = 0 then w 
    else let n' = n - 1 in uint64_set_bits f ((w << 1) OR (if f n' then 1 else 0)) n')"
 by(transfer fixing: n)(cases n, simp_all)
 
 lemma set_bits_uint64 [code]:
   "(BITS n. f n) = uint64_set_bits f 0 64"
 by transfer(simp add: set_bits_conv_set_bits_aux)
 
 
 lemma lsb_code [code]: fixes x :: uint64 shows "lsb x = x !! 0"
 by transfer(simp add: word_lsb_def word_test_bit_def)
 
 
 definition uint64_shiftl :: "uint64 \<Rightarrow> integer \<Rightarrow> uint64"
 where [code del]:
   "uint64_shiftl x n = (if n < 0 \<or> 64 \<le> n then undefined (shiftl :: uint64 \<Rightarrow> _) x n else x << (nat_of_integer n))"
 
 lemma shiftl_uint64_code [code]: "x << n = (if n < 64 then uint64_shiftl x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint64_shiftl_def
 by transfer(simp add: not_less shiftl_zero_size word_size)
 
 lemma uint64_shiftl_code [code abstract]:
   "Rep_uint64 (uint64_shiftl w n) =
   (if n < 0 \<or> 64 \<le> n then Rep_uint64 (undefined (shiftl :: uint64 \<Rightarrow> _) w n) else Rep_uint64 w << (nat_of_integer n))"
 including undefined_transfer unfolding uint64_shiftl_def by transfer simp
 
 code_printing constant uint64_shiftl \<rightharpoonup>
   (SML) "Uint64.shiftl" and
   (Haskell) "Data'_Bits.shiftlBounded" and
   (OCaml) "Uint64.shiftl" and
   (Scala) "Uint64.shiftl" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftl out of bounds\") else Uint64.shiftl x i)"
 
 
 definition uint64_shiftr :: "uint64 \<Rightarrow> integer \<Rightarrow> uint64"
 where [code del]:
   "uint64_shiftr x n = (if n < 0 \<or> 64 \<le> n then undefined (shiftr :: uint64 \<Rightarrow> _) x n else x >> (nat_of_integer n))"
 
 lemma shiftr_uint64_code [code]: "x >> n = (if n < 64 then uint64_shiftr x (integer_of_nat n) else 0)"
 including undefined_transfer integer.lifting unfolding uint64_shiftr_def
 by transfer(simp add: not_less shiftr_zero_size word_size)
 
 lemma uint64_shiftr_code [code abstract]:
   "Rep_uint64 (uint64_shiftr w n) =
   (if n < 0 \<or> 64 \<le> n then Rep_uint64 (undefined (shiftr :: uint64 \<Rightarrow> _) w n) else Rep_uint64 w >> nat_of_integer n)"
 including undefined_transfer unfolding uint64_shiftr_def by transfer simp
 
 code_printing constant uint64_shiftr \<rightharpoonup>
   (SML) "Uint64.shiftr" and
   (Haskell) "Data'_Bits.shiftrBounded" and
   (OCaml) "Uint64.shiftr" and
   (Scala) "Uint64.shiftr" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr out of bounds\") else Uint64.shiftr x i)"
 
 
 definition uint64_sshiftr :: "uint64 \<Rightarrow> integer \<Rightarrow> uint64"
 where [code del]:
   "uint64_sshiftr x n =
   (if n < 0 \<or> 64 \<le> n then undefined sshiftr_uint64 x n else sshiftr_uint64 x (nat_of_integer n))"
 
 lemma sshiftr_beyond: fixes x :: "'a :: len word" shows
   "size x \<le> n \<Longrightarrow> x >>> n = (if x !! (size x - 1) then -1 else 0)"
 by(rule word_eqI)(simp add: nth_sshiftr word_size)
 
 lemma sshiftr_uint64_code [code]:
   "x >>> n = 
   (if n < 64 then uint64_sshiftr x (integer_of_nat n) else if x !! 63 then -1 else 0)"
 including undefined_transfer integer.lifting unfolding uint64_sshiftr_def
 by transfer(simp add: not_less sshiftr_beyond word_size)
 
 lemma uint64_sshiftr_code [code abstract]:
   "Rep_uint64 (uint64_sshiftr w n) =
   (if n < 0 \<or> 64 \<le> n then Rep_uint64 (undefined sshiftr_uint64 w n) else Rep_uint64 w >>> (nat_of_integer n))"
 including undefined_transfer unfolding uint64_sshiftr_def by transfer simp
 
 code_printing constant uint64_sshiftr \<rightharpoonup>
   (SML) "Uint64.shiftr'_signed" and
   (Haskell) 
     "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Int64) _)) :: Uint64.Word64)" and
   (OCaml) "Uint64.shiftr'_signed" and
   (Scala) "Uint64.shiftr'_signed" and
   (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr'_signed out of bounds\") else Uint64.shiftr'_signed x i)"
 
 
 lemma uint64_msb_test_bit: "msb x \<longleftrightarrow> (x :: uint64) !! 63"
 by transfer(simp add: msb_nth)
 
 lemma msb_uint64_code [code]: "msb x \<longleftrightarrow> uint64_test_bit x 63"
 by(simp add: uint64_test_bit_def uint64_msb_test_bit)
 
 lemma uint64_of_int_code [code]: "uint64_of_int i = Uint64 (integer_of_int i)"
 including integer.lifting by transfer simp
 
 lemma int_of_uint64_code [code]:
   "int_of_uint64 x = int_of_integer (integer_of_uint64 x)"
 by(simp add: integer_of_uint64_def)
 
 lemma nat_of_uint64_code [code]:
   "nat_of_uint64 x = nat_of_integer (integer_of_uint64 x)"
 unfolding integer_of_uint64_def including integer.lifting by transfer (simp add: unat_def)
 
 definition integer_of_uint64_signed :: "uint64 \<Rightarrow> integer"
 where
   "integer_of_uint64_signed n = (if n !! 63 then undefined integer_of_uint64 n else integer_of_uint64 n)"
 
 lemma integer_of_uint64_signed_code [code]:
   "integer_of_uint64_signed n =
   (if n !! 63 then undefined integer_of_uint64 n else integer_of_int (uint (Rep_uint64' n)))"
 unfolding integer_of_uint64_signed_def integer_of_uint64_def
 including undefined_transfer by transfer simp
 
 lemma integer_of_uint64_code [code]:
   "integer_of_uint64 n =
   (if n !! 63 then integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 else integer_of_uint64_signed n)"
 unfolding integer_of_uint64_def integer_of_uint64_signed_def o_def
 including undefined_transfer integer.lifting
 by transfer(auto simp add: word_ao_nth uint_and_mask_or_full mask_numeral mask_Suc_0 intro!: uint_and_mask_or_full[symmetric])
 
 code_printing
   constant "integer_of_uint64" \<rightharpoonup>
   (SML) "Uint64.toInt" and
   (Haskell) "Prelude.toInteger"
 | constant "integer_of_uint64_signed" \<rightharpoonup>
   (OCaml) "Z.of'_int64" and
   (Scala) "BigInt"
 
 section \<open>Quickcheck setup\<close>
 
 definition uint64_of_natural :: "natural \<Rightarrow> uint64"
 where "uint64_of_natural x \<equiv> Uint64 (integer_of_natural x)"
 
 instantiation uint64 :: "{random, exhaustive, full_exhaustive}" begin
 definition "random_uint64 \<equiv> qc_random_cnv uint64_of_natural"
 definition "exhaustive_uint64 \<equiv> qc_exhaustive_cnv uint64_of_natural"
 definition "full_exhaustive_uint64 \<equiv> qc_full_exhaustive_cnv uint64_of_natural"
 instance ..
 end
 
 instantiation uint64 :: narrowing begin
 
 interpretation quickcheck_narrowing_samples
   "\<lambda>i. let x = Uint64 i in (x, 0xFFFFFFFFFFFFFFFF - x)" "0"
   "Typerep.Typerep (STR ''Uint64.uint64'') []" .
 
 definition "narrowing_uint64 d = qc_narrowing_drawn_from (narrowing_samples d) d"
 declare [[code drop: "partial_term_of :: uint64 itself \<Rightarrow> _"]]
 lemmas partial_term_of_uint64 [code] = partial_term_of_code
 
 instance ..
 end
 
 no_notation sshiftr_uint64 (infixl ">>>" 55)
 
 end