diff --git a/thys/Native_Word/Code_Target_Integer_Bit.thy b/thys/Native_Word/Code_Target_Integer_Bit.thy
--- a/thys/Native_Word/Code_Target_Integer_Bit.thy
+++ b/thys/Native_Word/Code_Target_Integer_Bit.thy
@@ -1,680 +1,635 @@
 (*  Title:      Code_Target_Integer_Bit.thy
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
 chapter \<open>Bit operations for target language integers\<close>
 
 theory Code_Target_Integer_Bit
   imports
     "HOL-Library.Word"
     "Code_Int_Integer_Conversion"
     "Word_Lib.Most_significant_bit"
     "Word_Lib.Least_significant_bit"
     "Word_Lib.Generic_set_bit"
     "Word_Lib.Bit_Comprehension"
 begin
 
 text \<open>TODO: separate\<close>
 
 lemmas [transfer_rule] =
   identity_quotient
   fun_quotient
   Quotient_integer[folded integer.pcr_cr_eq]
 
 lemma undefined_transfer:
   assumes "Quotient R Abs Rep T"
   shows "T (Rep undefined) undefined"
 using assms unfolding Quotient_alt_def by blast
 
 bundle undefined_transfer = undefined_transfer[transfer_rule]
 
+
 section \<open>More lemmas about @{typ integer}s\<close>
 
 context
-includes integer.lifting
+  includes integer.lifting
 begin
 
-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)
-
 lemma integer_of_nat_less_0_conv [simp]: "\<not> integer_of_nat n < 0"
-by(transfer) simp
+  by transfer simp
 
 lemma int_of_integer_pow: "int_of_integer (x ^ n) = int_of_integer x ^ n"
-by(induct n) simp_all
-
-lemma pow_integer_transfer [transfer_rule]:
-  "(rel_fun pcr_integer (rel_fun (=) pcr_integer)) (^) (^)"
-by(auto 4 3 simp add: integer.pcr_cr_eq cr_integer_def int_of_integer_pow)
+  by transfer rule
 
 lemma sub1_lt_0_iff [simp]: "Code_Numeral.sub n num.One < 0 \<longleftrightarrow> False"
-by(cases n)(simp_all add: Code_Numeral.sub_code)
+  by transfer (simp add: sub_negative)
 
 lemma nat_of_integer_numeral [simp]: "nat_of_integer (numeral n) = numeral n"
-by transfer simp
+  by transfer simp
 
 lemma nat_of_integer_sub1_conv_pred_numeral [simp]:
   "nat_of_integer (Code_Numeral.sub n num.One) = pred_numeral n"
-by(cases n)(simp_all add: Code_Numeral.sub_code)
+  by transfer (simp only: pred_numeral_def int_nat_eq numeral_One int_minus flip: int_int_eq, simp)
 
 lemma nat_of_integer_1 [simp]: "nat_of_integer 1 = 1"
-by transfer simp
+  by transfer simp
 
 lemma dup_1 [simp]: "Code_Numeral.dup 1 = 2"
-by transfer simp
-
-
-section \<open>Bit operations on @{typ integer}\<close>
-
-text \<open>Bit operations on @{typ integer} are the same as on @{typ int}\<close>
+  by transfer simp
 
 lift_definition bin_rest_integer :: "integer \<Rightarrow> integer" is \<open>\<lambda>k . k div 2\<close> .
+
 lift_definition bin_last_integer :: "integer \<Rightarrow> bool" is odd .
+
 lift_definition Bit_integer :: "integer \<Rightarrow> bool \<Rightarrow> integer" is \<open>\<lambda>k b. of_bool b + 2 * k\<close> .
 
 end
 
-instantiation integer :: lsb begin
-context includes integer.lifting begin
-
-lift_definition lsb_integer :: "integer \<Rightarrow> bool" is lsb .
-
-instance
-  by (standard; transfer) (fact lsb_odd)
-
-end
-end
-
-instantiation integer :: msb begin
-context includes integer.lifting begin
-
-lift_definition msb_integer :: "integer \<Rightarrow> bool" is msb .
-
-instance ..
-
-end
-end
-
-instantiation integer :: set_bit begin
-context includes integer.lifting begin
-
-lift_definition set_bit_integer :: "integer \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> integer" is set_bit .
-
-instance
-  apply standard
-  apply transfer
-  apply (simp add: bit_simps)
-  done
-
-end
-end
-
 
 section \<open>Target language implementations\<close>
 
 text \<open>
   Unfortunately, this is not straightforward,
   because these API functions have different signatures and preconditions on the parameters:
 
   \begin{description}
   \item[Standard ML] Shifts in IntInf are given as word, but not IntInf.
   \item[Haskell] In the Data.Bits.Bits type class, shifts and bit indices are given as Int rather than Integer.
   \end{description}
 
   Additional constants take only parameters of type @{typ integer} rather than @{typ nat}
   and check the preconditions as far as possible (e.g., being non-negative) in a portable way.
   Manual implementations inside code\_printing perform the remaining range checks and convert
   these @{typ integer}s into the right type.
 
   For normalisation by evaluation, we derive custom code equations, because NBE
   does not know these code\_printing serialisations and would otherwise loop.
 \<close>
 
 code_printing code_module Integer_Bit \<rightharpoonup> (SML)
 \<open>structure Integer_Bit : sig
   val test_bit : IntInf.int -> IntInf.int -> bool
   val set_bit : IntInf.int -> IntInf.int -> bool -> IntInf.int
   val shiftl : IntInf.int -> IntInf.int -> IntInf.int
   val shiftr : IntInf.int -> IntInf.int -> IntInf.int
 end = struct
 
 val maxWord = IntInf.pow (2, Word.wordSize);
 
 fun test_bit x n =
   if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
   else raise (Fail ("Bit index too large: " ^ IntInf.toString n));
 
 fun set_bit x n b =
   if n < maxWord 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 raise (Fail ("Bit index too large: " ^ IntInf.toString n));
 
 fun shiftl x n =
   if n < maxWord then IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n))
   else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));
 
 fun shiftr x n =
   if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
   else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));
 
 end; (*struct Integer_Bit*)\<close>
 code_reserved SML Integer_Bit
 
 code_printing code_module Integer_Bit \<rightharpoonup> (OCaml)
 \<open>module Integer_Bit : sig
   val test_bit : Z.t -> Z.t -> bool
   val shiftl : Z.t -> Z.t -> Z.t
   val shiftr : Z.t -> Z.t -> Z.t
 end = struct
 
 (* We do not need an explicit range checks here,
    because Big_int.int_of_big_int raises Failure
    if the argument does not fit into an int. *)
 let test_bit x n =  Z.testbit x (Z.to_int n);;
 
 let shiftl x n = Z.shift_left x (Z.to_int n);;
 
 let shiftr x n = Z.shift_right x (Z.to_int n);;
 
 end;; (*struct Integer_Bit*)\<close>
 code_reserved OCaml Integer_Bit
 
 code_printing code_module Data_Bits \<rightharpoonup> (Haskell)
 \<open>
 module Data_Bits where {
 
 import qualified Data.Bits;
 
 {-
   The ...Bounded functions assume that the Integer argument for the shift
   or bit index fits into an Int, is non-negative and (for types of fixed bit width)
   less than bitSize
 -}
 
 infixl 7 .&.;
 infixl 6 `xor`;
 infixl 5 .|.;
 
 (.&.) :: Data.Bits.Bits a => a -> a -> a;
 (.&.) = (Data.Bits..&.);
 
 xor :: Data.Bits.Bits a => a -> a -> a;
 xor = Data.Bits.xor;
 
 (.|.) :: Data.Bits.Bits a => a -> a -> a;
 (.|.) = (Data.Bits..|.);
 
 complement :: Data.Bits.Bits a => a -> a;
 complement = Data.Bits.complement;
 
 testBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool;
 testBitUnbounded x b
   | b <= toInteger (Prelude.maxBound :: Int) = Data.Bits.testBit x (fromInteger b)
   | otherwise = error ("Bit index too large: " ++ show b)
 ;
 
 testBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool;
 testBitBounded x b = Data.Bits.testBit x (fromInteger b);
 
 setBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a;
 setBitUnbounded x n b
   | n <= toInteger (Prelude.maxBound :: Int) =
     if b then Data.Bits.setBit x (fromInteger n) else Data.Bits.clearBit x (fromInteger n)
   | otherwise = error ("Bit index too large: " ++ show n)
 ;
 
 setBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a;
 setBitBounded x n True = Data.Bits.setBit x (fromInteger n);
 setBitBounded x n False = Data.Bits.clearBit x (fromInteger n);
 
 shiftlUnbounded :: Data.Bits.Bits a => a -> Integer -> a;
 shiftlUnbounded x n
   | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftL x (fromInteger n)
   | otherwise = error ("Shift operand too large: " ++ show n)
 ;
 
 shiftlBounded :: Data.Bits.Bits a => a -> Integer -> a;
 shiftlBounded x n = Data.Bits.shiftL x (fromInteger n);
 
 shiftrUnbounded :: Data.Bits.Bits a => a -> Integer -> a;
 shiftrUnbounded x n
   | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftR x (fromInteger n)
   | otherwise = error ("Shift operand too large: " ++ show n)
 ;
 
 shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Integer -> a;
 shiftrBounded x n = Data.Bits.shiftR x (fromInteger n);
 
 }\<close>
 
   and \<comment> \<open>@{theory HOL.Quickcheck_Narrowing} maps @{typ integer} to
             Haskell's Prelude.Int type instead of Integer. For compatibility
             with the Haskell target, we nevertheless provide bounded and
             unbounded functions.\<close>
   (Haskell_Quickcheck)
 \<open>
 module Data_Bits where {
 
 import qualified Data.Bits;
 
 {-
   The functions assume that the Int argument for the shift or bit index is
   non-negative and (for types of fixed bit width) less than bitSize
 -}
 
 infixl 7 .&.;
 infixl 6 `xor`;
 infixl 5 .|.;
 
 (.&.) :: Data.Bits.Bits a => a -> a -> a;
 (.&.) = (Data.Bits..&.);
 
 xor :: Data.Bits.Bits a => a -> a -> a;
 xor = Data.Bits.xor;
 
 (.|.) :: Data.Bits.Bits a => a -> a -> a;
 (.|.) = (Data.Bits..|.);
 
 complement :: Data.Bits.Bits a => a -> a;
 complement = Data.Bits.complement;
 
 testBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool;
 testBitUnbounded = Data.Bits.testBit;
 
 testBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool;
 testBitBounded = Data.Bits.testBit;
 
 setBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a;
 setBitUnbounded x n True = Data.Bits.setBit x n;
 setBitUnbounded x n False = Data.Bits.clearBit x n;
 
 setBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a;
 setBitBounded x n True = Data.Bits.setBit x n;
 setBitBounded x n False = Data.Bits.clearBit x n;
 
 shiftlUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
 shiftlUnbounded = Data.Bits.shiftL;
 
 shiftlBounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
 shiftlBounded = Data.Bits.shiftL;
 
 shiftrUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
 shiftrUnbounded = Data.Bits.shiftR;
 
 shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Prelude.Int -> a;
 shiftrBounded = Data.Bits.shiftR;
 
 }\<close>
 code_reserved Haskell Data_Bits
 
 code_printing code_module Integer_Bit \<rightharpoonup> (Scala)
 \<open>object Integer_Bit {
 
 def testBit(x: BigInt, n: BigInt) : Boolean =
   if (n.isValidInt)
     x.testBit(n.toInt)
   else
     sys.error("Bit index too large: " + n.toString)
 
 def setBit(x: BigInt, n: BigInt, b: Boolean) : BigInt =
   if (n.isValidInt)
     if (b)
       x.setBit(n.toInt)
     else
       x.clearBit(n.toInt)
   else
     sys.error("Bit index too large: " + n.toString)
 
 def shiftl(x: BigInt, n: BigInt) : BigInt =
   if (n.isValidInt)
     x << n.toInt
   else
     sys.error("Shift index too large: " + n.toString)
 
 def shiftr(x: BigInt, n: BigInt) : BigInt =
   if (n.isValidInt)
     x << n.toInt
   else
     sys.error("Shift index too large: " + n.toString)
 
 } /* object Integer_Bit */\<close>
 
 code_printing
   constant "Bit_Operations.and :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
   (SML) "IntInf.andb ((_),/ (_))" and
   (OCaml) "Z.logand" and
   (Haskell) "((Data'_Bits..&.) :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "((Data'_Bits..&.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) infixl 3 "&"
 | constant "Bit_Operations.or :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
   (SML) "IntInf.orb ((_),/ (_))" and
   (OCaml) "Z.logor" and
   (Haskell) "((Data'_Bits..|.) :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "((Data'_Bits..|.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) infixl 1 "|"
 | constant "Bit_Operations.xor :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
   (SML) "IntInf.xorb ((_),/ (_))" and
   (OCaml) "Z.logxor" and
   (Haskell) "(Data'_Bits.xor :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.xor :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) infixl 2 "^"
 | constant "Bit_Operations.not :: integer \<Rightarrow> integer" \<rightharpoonup>
   (SML) "IntInf.notb" and
   (OCaml) "Z.lognot" and
   (Haskell) "(Data'_Bits.complement :: Integer -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.complement :: Prelude.Int -> Prelude.Int)" and
   (Scala) "_.unary'_~"
 
 code_printing constant bin_rest_integer \<rightharpoonup>
   (SML) "IntInf.div ((_), 2)" and
   (OCaml) "Z.shift'_right/ _/ 1" and
   (Haskell) "(Data'_Bits.shiftrUnbounded _ 1 :: Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded _ 1 :: Prelude.Int)" and
   (Scala) "_ >> 1"
 
 context
   includes integer.lifting bit_operations_syntax
 begin
 
 lemma bitNOT_integer_code [code]:
   fixes i :: integer shows
   "NOT i = - i - 1"
   by transfer (simp add: not_int_def)
 
 lemma bin_rest_integer_code [code nbe]:
   "bin_rest_integer i = i div 2"
   by transfer rule
 
 lemma bin_last_integer_code [code]:
   "bin_last_integer i \<longleftrightarrow> i AND 1 \<noteq> 0"
   by transfer (simp add: and_one_eq odd_iff_mod_2_eq_one)
 
 lemma bin_last_integer_nbe [code nbe]:
   "bin_last_integer i \<longleftrightarrow> i mod 2 \<noteq> 0"
   by transfer (simp add: odd_iff_mod_2_eq_one)
 
 lemma bitval_bin_last_integer [code_unfold]:
   "of_bool (bin_last_integer i) = i AND 1"
   by transfer (simp add: and_one_eq mod_2_eq_odd)
 
 end
 
 definition integer_test_bit :: "integer \<Rightarrow> integer \<Rightarrow> bool"
   where "integer_test_bit x n = (if n < 0 then undefined x n else bit x (nat_of_integer n))"
 
 declare [[code drop: \<open>bit :: integer \<Rightarrow> nat \<Rightarrow> bool\<close>]]
 
 lemma bit_integer_code [code]:
   "bit x n \<longleftrightarrow> integer_test_bit x (integer_of_nat n)"
   by (simp add: integer_test_bit_def)
 
 lemma integer_test_bit_code [code]:
   "integer_test_bit x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
   "integer_test_bit 0 0 = False"
   "integer_test_bit 0 (Code_Numeral.Pos n) = False"
   "integer_test_bit (Code_Numeral.Pos num.One)      0 = True"
   "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) 0 = False"
   "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) 0 = True"
   "integer_test_bit (Code_Numeral.Pos num.One)      (Code_Numeral.Pos n') = False"
   "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) (Code_Numeral.Pos n') =
    integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)"
   "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) (Code_Numeral.Pos n') =
    integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)"
   "integer_test_bit (Code_Numeral.Neg num.One)      0 = True"
   "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) 0 = False"
   "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) 0 = True"
   "integer_test_bit (Code_Numeral.Neg num.One)      (Code_Numeral.Pos n') = True"
   "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) (Code_Numeral.Pos n') =
    integer_test_bit (Code_Numeral.Neg n) (Code_Numeral.sub n' num.One)"
   "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) (Code_Numeral.Pos n') =
    integer_test_bit (Code_Numeral.Neg (n + num.One)) (Code_Numeral.sub n' num.One)"
   by (simp_all add: integer_test_bit_def bit_integer_def bit_0 flip: bit_not_int_iff')
 
 code_printing constant integer_test_bit \<rightharpoonup>
   (SML) "Integer'_Bit.test'_bit" and
   (OCaml) "Integer'_Bit.test'_bit" and
   (Haskell) "(Data'_Bits.testBitUnbounded :: Integer -> Integer -> Bool)" and
   (Haskell_Quickcheck) "(Data'_Bits.testBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool)" and
   (Scala) "Integer'_Bit.testBit"
 
 context
   includes integer.lifting bit_operations_syntax
 begin
 
 lemma lsb_integer_code [code]:
   fixes x :: integer shows
   "lsb x = bit x 0"
 by transfer(simp add: lsb_int_def)
 
 definition integer_set_bit :: "integer \<Rightarrow> integer \<Rightarrow> bool \<Rightarrow> integer"
 where [code del]: "integer_set_bit x n b = (if n < 0 then undefined x n b else set_bit x (nat_of_integer n) b)"
 
 lemma set_bit_integer_code [code]:
   "set_bit x i b = integer_set_bit x (integer_of_nat i) b"
 by(simp add: integer_set_bit_def)
 
 lemma set_bit_integer_conv_masks:
   fixes x :: integer shows
   "set_bit x i b = (if b then x OR (push_bit i 1) else x AND NOT (push_bit i 1))"
   by (transfer; rule bit_eqI) (simp add: bit_simps)
 
 end
 
 code_printing constant integer_set_bit \<rightharpoonup>
   (SML) "Integer'_Bit.set'_bit" and
   (Haskell) "(Data'_Bits.setBitUnbounded :: Integer -> Integer -> Bool -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.setBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool -> Prelude.Int)" and
   (Scala) "Integer'_Bit.setBit"
 
 text \<open>
   OCaml.Big\_int does not have a method for changing an individual bit, so we emulate that with masks.
   We prefer an Isabelle implementation, because this then takes care of the signs for AND and OR.
 \<close>
 
 context
   includes bit_operations_syntax
 begin
 
 lemma integer_set_bit_code [code]:
   "integer_set_bit x n b =
   (if n < 0 then undefined x n b else
    if b then x OR (push_bit (nat_of_integer n) 1)
    else x AND NOT (push_bit (nat_of_integer n) 1))"
   by (auto simp add: integer_set_bit_def not_less set_bit_eq set_bit_def unset_bit_def)
 
 end
 
 definition integer_shiftl :: "integer \<Rightarrow> integer \<Rightarrow> integer"
 where [code del]: "integer_shiftl x n = (if n < 0 then undefined x n else push_bit (nat_of_integer n) x)"
 
 declare [[code drop: \<open>push_bit :: nat \<Rightarrow> integer \<Rightarrow> integer\<close>]]
 
 lemma shiftl_integer_code [code]:
   fixes x :: integer shows
   "push_bit n x = integer_shiftl x (integer_of_nat n)"
 by(auto simp add: integer_shiftl_def)
 
 context
 includes integer.lifting
 begin
 
 lemma shiftl_integer_conv_mult_pow2:
   fixes x :: integer shows
   "push_bit n x = x * 2 ^ n"
   by (fact push_bit_eq_mult)
 
 lemma integer_shiftl_code [code]:
   "integer_shiftl x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
   "integer_shiftl x 0 = x"
   "integer_shiftl x (Code_Numeral.Pos n) = integer_shiftl (Code_Numeral.dup x) (Code_Numeral.sub n num.One)"
   "integer_shiftl 0 (Code_Numeral.Pos n) = 0"
      apply (simp_all add: integer_shiftl_def numeral_eq_Suc)
   apply transfer
   apply (simp add: ac_simps)
   done
 
 end
 
 code_printing constant integer_shiftl \<rightharpoonup>
   (SML) "Integer'_Bit.shiftl" and
   (OCaml) "Integer'_Bit.shiftl" and
   (Haskell) "(Data'_Bits.shiftlUnbounded :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.shiftlUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) "Integer'_Bit.shiftl"
 
 definition integer_shiftr :: "integer \<Rightarrow> integer \<Rightarrow> integer"
 where [code del]: "integer_shiftr x n = (if n < 0 then undefined x n else drop_bit (nat_of_integer n) x)"
 
 declare [[code drop: \<open>drop_bit :: nat \<Rightarrow> integer \<Rightarrow> integer\<close>]]
 
 lemma shiftr_integer_conv_div_pow2:
   includes integer.lifting fixes x :: integer shows
   "drop_bit n x = x div 2 ^ n"
   by (fact drop_bit_eq_div)
 
 lemma shiftr_integer_code [code]:
   fixes x :: integer shows
   "drop_bit n x = integer_shiftr x (integer_of_nat n)"
 by(auto simp add: integer_shiftr_def)
 
 code_printing constant integer_shiftr \<rightharpoonup>
   (SML) "Integer'_Bit.shiftr" and
   (OCaml) "Integer'_Bit.shiftr" and
   (Haskell) "(Data'_Bits.shiftrUnbounded :: Integer -> Integer -> Integer)" and
   (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
   (Scala) "Integer'_Bit.shiftr"
 
 lemma integer_shiftr_code [code]:
   includes integer.lifting
   shows
   "integer_shiftr x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
   "integer_shiftr x 0 = x"
   "integer_shiftr 0 (Code_Numeral.Pos n) = 0"
   "integer_shiftr (Code_Numeral.Pos num.One) (Code_Numeral.Pos n) = 0"
   "integer_shiftr (Code_Numeral.Pos (num.Bit0 n')) (Code_Numeral.Pos n) =
    integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)"
   "integer_shiftr (Code_Numeral.Pos (num.Bit1 n')) (Code_Numeral.Pos n) =
    integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)"
   "integer_shiftr (Code_Numeral.Neg num.One) (Code_Numeral.Pos n) = -1"
   "integer_shiftr (Code_Numeral.Neg (num.Bit0 n')) (Code_Numeral.Pos n) =
    integer_shiftr (Code_Numeral.Neg n') (Code_Numeral.sub n num.One)"
   "integer_shiftr (Code_Numeral.Neg (num.Bit1 n')) (Code_Numeral.Pos n) =
    integer_shiftr (Code_Numeral.Neg (Num.inc n')) (Code_Numeral.sub n num.One)"
           apply (simp_all add: integer_shiftr_def numeral_eq_Suc drop_bit_Suc)
     apply transfer apply simp
    apply transfer apply simp
   apply transfer apply (simp add: add_One)
   done
 
 context
 includes integer.lifting
 begin
 
 lemma Bit_integer_code [code]:
   "Bit_integer i False = push_bit 1 i"
   "Bit_integer i True = push_bit 1 i + 1"
   by (transfer; simp)+
 
 lemma msb_integer_code [code]:
   "msb (x :: integer) \<longleftrightarrow> x < 0"
   by transfer (simp add: msb_int_def)
 
 end
 
 context
-  includes integer.lifting natural.lifting bit_operations_syntax
+  includes integer.lifting bit_operations_syntax
 begin
 
 lemma bitAND_integer_unfold [code]:
   "x AND y =
    (if x = 0 then 0
     else if x = - 1 then y
     else Bit_integer (bin_rest_integer x AND bin_rest_integer y) (bin_last_integer x \<and> bin_last_integer y))"
   by transfer
     (auto simp add: algebra_simps
       and_int_rec [of _ \<open>_ * 2\<close>] and_int_rec [of \<open>_ * 2\<close>] and_int_rec [of \<open>1 + _ * 2\<close>]
       elim!: evenE oddE)
 
 lemma bitOR_integer_unfold [code]:
   "x OR y =
    (if x = 0 then y
     else if x = - 1 then - 1
     else Bit_integer (bin_rest_integer x OR bin_rest_integer y) (bin_last_integer x \<or> bin_last_integer y))"
   by transfer
     (auto simp add: algebra_simps
       or_int_rec [of _ \<open>_ * 2\<close>] or_int_rec [of _ \<open>1 + _ * 2\<close>] or_int_rec [of \<open>1 + _ * 2\<close>]
       elim!: evenE oddE)
 
 lemma bitXOR_integer_unfold [code]:
   "x XOR y =
    (if x = 0 then y
     else if x = - 1 then NOT y
     else Bit_integer (bin_rest_integer x XOR bin_rest_integer y)
       (\<not> bin_last_integer x \<longleftrightarrow> bin_last_integer y))"
   by transfer
     (auto simp add: algebra_simps
       xor_int_rec [of _ \<open>_ * 2\<close>] xor_int_rec [of \<open>_ * 2\<close>] xor_int_rec [of \<open>1 + _ * 2\<close>]
       elim!: evenE oddE)
 
 end
 
 
 section \<open>Test code generator setup\<close>
 
 context
   includes bit_operations_syntax
 begin
 
 definition bit_integer_test :: "bool" where
   "bit_integer_test =
   (([ -1 AND 3, 1 AND -3, 3 AND 5, -3 AND (- 5)
     , -3 OR 1, 1 OR -3, 3 OR 5, -3 OR (- 5)
     , NOT 1, NOT (- 3)
     , -1 XOR 3, 1 XOR (- 3), 3 XOR 5, -5 XOR (- 3)
     , set_bit 5 4 True, set_bit (- 5) 2 True, set_bit 5 0 False, set_bit (- 5) 1 False
     , push_bit 2 1, push_bit 3 (- 1)
     , drop_bit 3 100, drop_bit 3 (- 100)] :: integer list)
   = [ 3, 1, 1, -7
     , -3, -3, 7, -1
     , -2, 2
     , -4, -4, 6, 6
     , 21, -1, 4, -7
     , 4, -8
     , 12, -13] \<and>
     [ bit (5 :: integer) 4, bit (5 :: integer) 2, bit (-5 :: integer) 4, bit (-5 :: integer) 2
     , lsb (5 :: integer), lsb (4 :: integer), lsb (-1 :: integer), lsb (-2 :: integer),
       msb (5 :: integer), msb (0 :: integer), msb (-1 :: integer), msb (-2 :: integer)]
   = [ False, True, True, False,
       True, False, True, False,
       False, False, True, True])"
 
 export_code bit_integer_test checking SML Haskell? Haskell_Quickcheck? OCaml? Scala
 
 notepad begin
 have bit_integer_test by eval
 have bit_integer_test by normalization
 have bit_integer_test by code_simp
 end
 ML_val \<open>val true = @{code bit_integer_test}\<close>
 
 lemma "x AND y = x OR (y :: integer)"
 quickcheck[random, expect=counterexample]
 quickcheck[exhaustive, expect=counterexample]
 oops
 
 lemma "(x :: integer) AND x = x OR x"
 quickcheck[narrowing, expect=no_counterexample]
 oops
 
 lemma "(f :: integer \<Rightarrow> unit) = g"
 quickcheck[narrowing, size=3, expect=no_counterexample]
 by(simp add: fun_eq_iff)
 
 end
 
 hide_const bit_integer_test
 hide_fact bit_integer_test_def
 
 end
diff --git a/thys/Word_Lib/Generic_set_bit.thy b/thys/Word_Lib/Generic_set_bit.thy
--- a/thys/Word_Lib/Generic_set_bit.thy
+++ b/thys/Word_Lib/Generic_set_bit.thy
@@ -1,136 +1,152 @@
 (*
  * Copyright Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 (* Author: Jeremy Dawson, NICTA *)
 
 section \<open>Operation variant for setting and unsetting bits\<close>
 
 theory Generic_set_bit
   imports
     "HOL-Library.Word"
     Most_significant_bit
 begin
 
 class set_bit = semiring_bits +
   fixes set_bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a\<close>
   assumes bit_set_bit_iff_2n:
     \<open>bit (set_bit a m b) n \<longleftrightarrow>
       (if m = n then b else bit a n) \<and> 2 ^ n \<noteq> 0\<close>
 
 lemmas bit_set_bit_iff[bit_simps] = bit_set_bit_iff_2n[simplified fold_possible_bit simp_thms]
 
 lemma set_bit_eq:
   \<open>set_bit a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\<close>
   for a :: \<open>'a::{ring_bit_operations, set_bit}\<close>
   by (rule bit_eqI) (simp add: bit_simps)
 
 instantiation int :: set_bit
 begin
 
 definition set_bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> int\<close>
   where \<open>set_bit_int i n b = (if b then Bit_Operations.set_bit else Bit_Operations.unset_bit) n i\<close>
 
 instance
   by standard (simp_all add: set_bit_int_def bit_simps)
 
 end
 
 context
   includes bit_operations_syntax
 begin
 
 lemma fixes i :: int
   shows int_set_bit_True_conv_OR [code]: "Generic_set_bit.set_bit i n True = i OR push_bit n 1"
   and int_set_bit_False_conv_NAND [code]: "Generic_set_bit.set_bit i n False = i AND NOT (push_bit n 1)"
   and int_set_bit_conv_ops: "Generic_set_bit.set_bit i n b = (if b then i OR (push_bit n 1) else i AND NOT (push_bit n 1))"
   by (simp_all add: bit_eq_iff) (auto simp add: bit_simps)
 
 end
 
 instantiation word :: (len) set_bit
 begin
 
 definition set_bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a word\<close>
   where set_bit_unfold: \<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close>
   for w :: \<open>'a::len word\<close>
 
 instance
   by standard (auto simp add: set_bit_unfold bit_simps dest: bit_imp_le_length)
 
 end
 
 lemma bit_set_bit_word_iff [bit_simps]:
   \<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close>
   for w :: \<open>'a::len word\<close>
   by (auto simp add: bit_simps dest: bit_imp_le_length)
 
 lemma test_bit_set_gen:
   "bit (set_bit w n x) m \<longleftrightarrow> (if m = n then n < size w \<and> x else bit w m)"
   for w :: "'a::len word"
   by (simp add: bit_set_bit_word_iff word_size)
 
 lemma test_bit_set:
   "bit (set_bit w n x) n \<longleftrightarrow> n < size w \<and> x"
   for w :: "'a::len word"
   by (auto simp add: bit_simps word_size)
 
 lemma word_set_nth: "set_bit w n (bit w n) = w"
   for w :: "'a::len word"
   by (rule bit_word_eqI) (simp add: bit_simps)
 
 lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
   for w :: "'a::len word"
   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
 
 lemma word_set_set_diff:
   fixes w :: "'a::len word"
   assumes "m \<noteq> n"
   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
   by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
 
 lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> bit w n = b \<or> n \<ge> size w"
   for w :: "'a::len word"
   apply (rule iffI)
    apply (rule disjCI)
    apply (drule word_eqD)
    apply (erule sym [THEN trans])
    apply (simp add: test_bit_set)
   apply (erule disjE)
    apply clarsimp
   apply (rule word_eqI)
    apply (clarsimp simp add : test_bit_set_gen)
    apply (auto simp add: word_size)
   apply (rule bit_eqI)
   apply (simp add: bit_simps)
   done
 
 lemma word_clr_le: "w \<ge> set_bit w n False"
   for w :: "'a::len word"
   apply (simp add: set_bit_unfold)
   apply transfer
   apply (simp add: take_bit_unset_bit_eq unset_bit_less_eq)
   done
 
 lemma word_set_ge: "w \<le> set_bit w n True"
   for w :: "'a::len word"
   apply (simp add: set_bit_unfold)
   apply transfer
   apply (simp add: take_bit_set_bit_eq set_bit_greater_eq)
   done
 
 lemma set_bit_beyond:
   "size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len word"
   by (simp add: word_set_nth_iff)
 
 lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n"
   apply (rule word_eqI)
   apply (auto simp add: word_size bit_simps)
   done
 
 lemma one_bit_pow: "set_bit 0 n True = (2 :: 'a :: len word) ^ n"
   by (simp add: one_bit_shiftl shiftl_def)
 
+instantiation integer :: set_bit
+begin
+
+context
+  includes integer.lifting
+begin
+
+lift_definition set_bit_integer :: \<open>integer \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> integer\<close> is set_bit .
+
+instance
+  by (standard; transfer) (simp add: bit_simps)
+
 end
+
+end
+
+end
diff --git a/thys/Word_Lib/Least_significant_bit.thy b/thys/Word_Lib/Least_significant_bit.thy
--- a/thys/Word_Lib/Least_significant_bit.thy
+++ b/thys/Word_Lib/Least_significant_bit.thy
@@ -1,94 +1,110 @@
 (*
  * Copyright Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 (* Author: Jeremy Dawson, NICTA *)
 
 section \<open>Operation variant for the least significant bit\<close>
 
 theory Least_significant_bit
   imports
     "HOL-Library.Word"
     More_Word
 begin
 
 class lsb = semiring_bits +
   fixes lsb :: \<open>'a \<Rightarrow> bool\<close>
   assumes lsb_odd: \<open>lsb = odd\<close>
 
 instantiation int :: lsb
 begin
 
 definition lsb_int :: \<open>int \<Rightarrow> bool\<close>
   where \<open>lsb i = bit i 0\<close> for i :: int
 
 instance
   by standard (simp add: fun_eq_iff lsb_int_def bit_0)
 
 end
 
 lemma bin_last_conv_lsb: "odd = (lsb :: int \<Rightarrow> bool)"
   by (simp add: lsb_odd)
 
 lemma int_lsb_numeral [simp]:
   "lsb (0 :: int) = False"
   "lsb (1 :: int) = True"
   "lsb (Numeral1 :: int) = True"
   "lsb (- 1 :: int) = True"
   "lsb (- Numeral1 :: int) = True"
   "lsb (numeral (num.Bit0 w) :: int) = False"
   "lsb (numeral (num.Bit1 w) :: int) = True"
   "lsb (- numeral (num.Bit0 w) :: int) = False"
   "lsb (- numeral (num.Bit1 w) :: int) = True"
   by (simp_all add: lsb_int_def bit_0)
 
 instantiation word :: (len) lsb
 begin
 
 definition lsb_word :: \<open>'a word \<Rightarrow> bool\<close>
   where word_lsb_def: \<open>lsb a \<longleftrightarrow> odd (uint a)\<close> for a :: \<open>'a word\<close>
 
 instance
   apply standard
   apply (simp add: fun_eq_iff word_lsb_def)
   apply transfer apply simp
   done
 
 end
 
 lemma lsb_word_eq:
   \<open>lsb = (odd :: 'a word \<Rightarrow> bool)\<close> for w :: \<open>'a::len word\<close>
   by (fact lsb_odd)
 
 lemma word_lsb_alt: "lsb w = bit w 0"
   for w :: "'a::len word"
   by (simp add: lsb_word_eq bit_0)
 
 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)"
   unfolding word_lsb_def by simp
 
 lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
   apply (simp add: lsb_odd flip: odd_iff_mod_2_eq_one)
   apply transfer
   apply simp
   done
 
 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
 
 lemma word_lsb_numeral [simp]:
   "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> odd (numeral bin :: int)"
   by (simp only: lsb_odd, transfer) rule
 
 lemma word_lsb_neg_numeral [simp]:
   "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> odd (- numeral bin :: int)"
   by (simp only: lsb_odd, transfer) rule
 
 lemma word_lsb_nat:"lsb w = (unat w mod 2 = 1)"
   apply (simp add: word_lsb_def Groebner_Basis.algebra(31))
   apply transfer
   apply (simp add: even_nat_iff)
   done
 
+instantiation integer :: lsb
+begin
+
+context
+  includes integer.lifting
+begin
+
+lift_definition lsb_integer :: \<open>integer \<Rightarrow> bool\<close> is lsb .
+
+instance
+  by (standard; transfer) (fact lsb_odd)
+
 end
+
+end
+
+end
diff --git a/thys/Word_Lib/Most_significant_bit.thy b/thys/Word_Lib/Most_significant_bit.thy
--- a/thys/Word_Lib/Most_significant_bit.thy
+++ b/thys/Word_Lib/Most_significant_bit.thy
@@ -1,194 +1,209 @@
 (*
  * Copyright Data61, CSIRO (ABN 41 687 119 230)
  *
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
 (* Author: Jeremy Dawson, NICTA *)
 
 section \<open>Dedicated operation for the most significant bit\<close>
 
 theory Most_significant_bit
   imports
     "HOL-Library.Word"
     Bit_Shifts_Infix_Syntax
     More_Word
     More_Arithmetic
 begin
 
 class msb =
   fixes msb :: \<open>'a \<Rightarrow> bool\<close>
 
 instantiation int :: msb
 begin
 
 definition \<open>msb x \<longleftrightarrow> x < 0\<close> for x :: int
 
 instance ..
 
 end
 
 lemma msb_bin_rest [simp]: "msb (x div 2) = msb x"
   for x :: int
   by (simp add: msb_int_def)
 
 context
   includes bit_operations_syntax
 begin
 
 lemma int_msb_and [simp]: "msb ((x :: int) AND y) \<longleftrightarrow> msb x \<and> msb y"
 by(simp add: msb_int_def)
 
 lemma int_msb_or [simp]: "msb ((x :: int) OR y) \<longleftrightarrow> msb x \<or> msb y"
 by(simp add: msb_int_def)
 
 lemma int_msb_xor [simp]: "msb ((x :: int) XOR y) \<longleftrightarrow> msb x \<noteq> msb y"
 by(simp add: msb_int_def)
 
 lemma int_msb_not [simp]: "msb (NOT (x :: int)) \<longleftrightarrow> \<not> msb x"
 by(simp add: msb_int_def not_less)
 
 end
 
 lemma msb_shiftl [simp]: "msb ((x :: int) << n) \<longleftrightarrow> msb x"
   by (simp add: msb_int_def shiftl_def)
 
 lemma msb_shiftr [simp]: "msb ((x :: int) >> r) \<longleftrightarrow> msb x"
   by (simp add: msb_int_def shiftr_def)
 
 lemma msb_0 [simp]: "msb (0 :: int) = False"
 by(simp add: msb_int_def)
 
 lemma msb_1 [simp]: "msb (1 :: int) = False"
 by(simp add: msb_int_def)
 
 lemma msb_numeral [simp]:
   "msb (numeral n :: int) = False"
   "msb (- numeral n :: int) = True"
 by(simp_all add: msb_int_def)
 
 instantiation word :: (len) msb
 begin
 
 definition msb_word :: \<open>'a word \<Rightarrow> bool\<close>
   where msb_word_iff_bit: \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - Suc 0)\<close> for w :: \<open>'a::len word\<close>
 
 instance ..
 
 end
 
 lemma msb_word_eq:
   \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
   by (simp add: msb_word_iff_bit)
 
 lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
   by (simp add: msb_word_eq bit_last_iff)
 
 lemma msb_word_iff_sless_0:
   \<open>msb w \<longleftrightarrow> w <s 0\<close>
   by (simp add: word_msb_sint word_sless_alt)
 
 lemma msb_word_of_int:
   "msb (word_of_int x::'a::len word) = bit x (LENGTH('a) - 1)"
   by (simp add: msb_word_iff_bit bit_simps)
 
 lemma word_msb_numeral [simp]:
   "msb (numeral w::'a::len word) = bit (numeral w :: int) (LENGTH('a) - 1)"
   unfolding word_numeral_alt by (rule msb_word_of_int)
 
 lemma word_msb_neg_numeral [simp]:
   "msb (- numeral w::'a::len word) = bit (- numeral w :: int) (LENGTH('a) - 1)"
   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
 
 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
   by (simp add: msb_word_iff_bit)
 
 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1"
   by (simp add: msb_word_iff_bit le_Suc_eq)
 
 lemma word_msb_nth: "msb w = bit (uint w) (LENGTH('a) - 1)"
   for w :: "'a::len word"
   by (simp add: msb_word_iff_bit bit_simps)
 
 lemma msb_nth: "msb w = bit w (LENGTH('a) - 1)"
   for w :: "'a::len word"
   by (fact msb_word_eq)
 
 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
   by (simp add: msb_word_eq not_le)
 
 lemma msb_shift: "msb w \<longleftrightarrow> w >> LENGTH('a) - 1 \<noteq> 0"
   for w :: "'a::len word"
   by (simp add: drop_bit_eq_zero_iff_not_bit_last msb_word_eq shiftr_def)
 
 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
 
 lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)"
   apply (cases \<open>LENGTH('a)\<close>)
   apply (simp_all add: msb_word_iff_bit word_size)
   apply transfer
   apply (simp add: signed_take_bit_eq_take_bit_minus)
   done
 
 lemma word_sle_msb_le: "x <=s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> y)"
   apply (simp add: word_sle_eq word_sint_msb_eq word_size word_le_def)
   apply safe
    apply (rule order_trans[OF _ uint_ge_0])
    apply (simp add: order_less_imp_le)
   apply (erule notE[OF leD])
   apply (rule order_less_le_trans[OF _ uint_ge_0])
   apply simp
   done
 
 lemma word_sless_msb_less: "x <s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x < y)"
   by (auto simp add: word_sless_eq word_sle_msb_le)
 
 lemma not_msb_from_less:
   "(v :: 'a word) < 2 ^ (LENGTH('a :: len) - 1) \<Longrightarrow> \<not> msb v"
   apply (clarsimp simp add: msb_nth)
   apply (drule less_mask_eq)
   apply (drule word_eqD, drule(1) iffD2)
   apply (simp add: bit_simps)
   done
 
 lemma sint_eq_uint:
   "\<not> msb x \<Longrightarrow> sint x = uint x"
   apply (cases \<open>LENGTH('a)\<close>)
   apply (simp_all add: msb_word_iff_bit)
   apply transfer
   apply (simp add: signed_take_bit_eq_take_bit_minus)
   done
 
 lemma scast_eq_ucast:
   "\<not> msb x \<Longrightarrow> scast x = ucast x"
   apply (cases \<open>LENGTH('a)\<close>)
   apply simp
   apply (rule bit_word_eqI)
   apply (auto simp add: bit_signed_iff bit_unsigned_iff min_def msb_word_eq)
   apply (erule notE)
   apply (metis le_less_Suc_eq test_bit_bin)
   done
 
 lemma msb_ucast_eq:
     "LENGTH('a) = LENGTH('b) \<Longrightarrow>
          msb (ucast x :: ('a::len) word) = msb (x :: ('b::len) word)"
   by (simp add: msb_word_eq bit_simps)
 
 lemma msb_big:
   \<open>msb a \<longleftrightarrow> 2 ^ (LENGTH('a) - Suc 0) \<le> a\<close>
   for a :: \<open>'a::len word\<close>
   using bang_is_le [of a \<open>LENGTH('a) - Suc 0\<close>]
   apply (auto simp add: msb_nth word_le_not_less)
   apply (rule ccontr)
   apply (erule notE)
   apply (rule ccontr)
   apply (clarsimp simp: not_less)
   apply (subgoal_tac "a = take_bit (LENGTH('a) - Suc 0) a")
    apply (cut_tac and_mask_less' [where w=a and n="LENGTH('a) - Suc 0"])
     apply auto
   apply (simp flip: take_bit_eq_mask)
   apply (rule sym)
   apply (simp add: take_bit_eq_self_iff_drop_bit_eq_0 drop_bit_eq_zero_iff_not_bit_last)
   done
 
+instantiation integer :: msb
+begin
+
+context
+  includes integer.lifting
+begin
+
+lift_definition msb_integer :: \<open>integer \<Rightarrow> bool\<close> is msb .
+
+instance ..
+
 end
+
+end
+
+end