# HG changeset patch
# User wenzelm
# Date 1736087404 -3600
# Node ID b836e9ac0cf3a081aeef13cfba474ec6c9b98b7e
# Parent  658f1b5168f26488c50612ab77d65e56bb576941# Parent  560a069a537f0dc38972b1a0d4874102f0e4b572
merged

diff -r 560a069a537f -r b836e9ac0cf3 NEWS
--- a/NEWS	Sun Jan 05 15:18:54 2025 +0100
+++ b/NEWS	Sun Jan 05 15:30:04 2025 +0100
@@ -225,6 +225,10 @@
 * Code generator: command 'code_reserved' now uses parentheses for
 target languages, similar to 'code_printing'.
 
+* Theory HOL-Library.Code_Target_Bit_Shifts implemented bit shifts on numeric
+types by target-language operations; this is also used by
+HOL-Library.Code_Target_Numeral.
+
 * Sledgehammer:
   - Update of bundled provers:
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
diff -r 560a069a537f -r b836e9ac0cf3 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/Doc/Codegen/Adaptation.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -204,13 +204,17 @@
        Pattern matching with \<^term>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated
        by a preprocessor.
 
+    \item[\<open>Code_Target_Bit_Shifts\<close>] implements bit shifts on \<^typ>\<open>integer\<close>
+       by target-language operations. Combined with \<open>Code_Target_Int\<close>
+       or \<open>Code_Target_Nat\<close>, bit shifts on \<^typ>\<open>int\<close> or \<^type>\<open>nat\<close> can
+       be implemented by target-language operations.
+
     \item[\<open>Code_Target_Numeral\<close>] is a convenience theory
-       containing both \<open>Code_Target_Nat\<close> and
-       \<open>Code_Target_Int\<close>.
+       containing \<open>Code_Target_Nat\<close>, \<open>Code_Target_Int\<close> and \<open>Code_Target_Bit_Shifts\<close>-
 
     \item[\<open>Code_Abstract_Char\<close>] implements type \<^typ>\<open>char\<close> by target language
        integers, sacrificing pattern patching in exchange for dramatically
-       increased performance for comparisions.
+       increased performance for comparisons.
 
     \item[\<^theory>\<open>HOL-Library.IArray\<close>] provides a type \<^typ>\<open>'a iarray\<close>
        isomorphic to lists but implemented by (effectively immutable)
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/HOL/Bit_Operations.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -2491,6 +2491,18 @@
   \<open>of_nat (mask n) = mask n\<close>
   by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq)
 
+lemma of_nat_set_bit_eq:
+  \<open>of_nat (set_bit n m) = set_bit n (of_nat m)\<close>
+  by (simp add: set_bit_eq_or Bit_Operations.set_bit_eq_or of_nat_or_eq Bit_Operations.push_bit_eq_mult)
+
+lemma of_nat_unset_bit_eq:
+  \<open>of_nat (unset_bit n m) = unset_bit n (of_nat m)\<close>
+  by (simp add: unset_bit_eq_or_xor Bit_Operations.unset_bit_eq_or_xor of_nat_or_eq of_nat_xor_eq Bit_Operations.push_bit_eq_mult)
+
+lemma of_nat_flip_bit_eq:
+  \<open>of_nat (flip_bit n m) = flip_bit n (of_nat m)\<close>
+  by (simp add: flip_bit_eq_xor Bit_Operations.flip_bit_eq_xor of_nat_xor_eq Bit_Operations.push_bit_eq_mult)
+
 end
 
 context linordered_euclidean_semiring_bit_operations
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/HOL/Code_Numeral.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -377,19 +377,6 @@
 begin
 
 lemma [code]:
-  \<open>bit k n \<longleftrightarrow> odd (drop_bit n k)\<close>
-  \<open>NOT k = - k - 1\<close>
-  \<open>mask n = 2 ^ n - (1 :: integer)\<close>
-  \<open>set_bit n k = k OR push_bit n 1\<close>
-  \<open>unset_bit n k = k AND NOT (push_bit n 1)\<close>
-  \<open>flip_bit n k = k XOR push_bit n 1\<close>
-  \<open>push_bit n k = k * 2 ^ n\<close>
-  \<open>drop_bit n k = k div 2 ^ n\<close>
-  \<open>take_bit n k = k mod 2 ^ n\<close> for k :: integer
-  by (fact bit_iff_odd_drop_bit not_eq_complement mask_eq_exp_minus_1
-    set_bit_eq_or unset_bit_eq_and_not flip_bit_eq_xor push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
-
-lemma [code]:
   \<open>k AND l = (if k = 0 \<or> l = 0 then 0 else if k = - 1 then l else if l = - 1 then k
     else (k mod 2) * (l mod 2) + 2 * ((k div 2) AND (l div 2)))\<close> for k l :: integer
   by transfer (fact and_int_unfold) 
@@ -404,6 +391,42 @@
     else \<bar>k mod 2 - l mod 2\<bar> + 2 * ((k div 2) XOR (l div 2)))\<close> for k l :: integer
   by transfer (fact xor_int_unfold)
 
+lemma [code]:
+  \<open>NOT k = - k - 1\<close> for k :: integer
+  by (fact not_eq_complement)
+
+lemma [code]:
+  \<open>bit k n \<longleftrightarrow> k AND push_bit n 1 \<noteq> (0 :: integer)\<close>
+  by (simp add: and_exp_eq_0_iff_not_bit)
+
+lemma [code]:
+  \<open>mask n = push_bit n 1 - (1 :: integer)\<close>
+  by (simp add: mask_eq_exp_minus_1)
+
+lemma [code]:
+  \<open>set_bit n k = k OR push_bit n 1\<close> for k :: integer
+  by (fact set_bit_def)
+
+lemma [code]:
+  \<open>unset_bit n k = k AND NOT (push_bit n 1)\<close> for k :: integer
+  by (fact unset_bit_def)
+
+lemma [code]:
+  \<open>flip_bit n k = k XOR push_bit n 1\<close> for k :: integer
+  by (fact flip_bit_def)
+
+lemma [code]:
+  \<open>push_bit n k = k * 2 ^ n\<close> for k :: integer
+  by (fact push_bit_eq_mult)
+
+lemma [code]:
+  \<open>drop_bit n k = k div  2 ^ n\<close> for k :: integer
+  by (fact drop_bit_eq_div)
+
+lemma [code]:
+  \<open>take_bit n k = k AND mask n\<close> for k :: integer
+  by (fact take_bit_eq_mask)
+
 end
 
 instantiation integer :: linordered_euclidean_semiring_division
@@ -873,6 +896,26 @@
     and (Haskell) "Prelude.abs"
     and (Scala) "_.abs"
     and (Eval) "abs"
+| constant "Bit_Operations.and :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+    (SML) "IntInf.andb ((_),/ (_))"
+    and (OCaml) "Z.logand"
+    and (Haskell) infixl 7 ".&."
+    and (Scala) infixl 3 "&"
+| constant "Bit_Operations.or :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+    (SML) "IntInf.orb ((_),/ (_))"
+    and (OCaml) "Z.logor"
+    and (Haskell) infixl 5 ".|."
+    and (Scala) infixl 1 "|"
+| constant "Bit_Operations.xor :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
+    (SML) "IntInf.xorb ((_),/ (_))"
+    and (OCaml) "Z.logxor"
+    and (Haskell) infixl 6 ".^."
+    and (Scala) infixl 2 "^"
+| constant "Bit_Operations.not :: integer \<Rightarrow> integer" \<rightharpoonup>
+    (SML) "IntInf.notb"
+    and (OCaml) "Z.lognot"
+    and (Haskell) "Data.Bits.complement"
+    and (Scala) "_.unary'_~"
 
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
@@ -1131,43 +1174,6 @@
 
 instance natural :: linordered_euclidean_semiring_bit_operations ..
 
-context
-  includes bit_operations_syntax
-begin
-
-lemma [code]:
-  \<open>bit m n \<longleftrightarrow> odd (drop_bit n m)\<close>
-  \<open>mask n = 2 ^ n - (1 :: natural)\<close>
-  \<open>set_bit n m = m OR push_bit n 1\<close>
-  \<open>flip_bit n m = m XOR push_bit n 1\<close>
-  \<open>push_bit n m = m * 2 ^ n\<close>
-  \<open>drop_bit n m = m div 2 ^ n\<close>
-  \<open>take_bit n m = m mod 2 ^ n\<close> for m :: natural
-  by (fact bit_iff_odd_drop_bit mask_eq_exp_minus_1
-    set_bit_eq_or flip_bit_eq_xor push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
-
-lemma [code]:
-  \<open>m AND n = (if m = 0 \<or> n = 0 then 0
-    else (m mod 2) * (n mod 2) + 2 * ((m div 2) AND (n div 2)))\<close> for m n :: natural
-  by transfer (fact and_nat_unfold)
-
-lemma [code]:
-  \<open>m OR n = (if m = 0 then n else if n = 0 then m
-    else max (m mod 2) (n mod 2) + 2 * ((m div 2) OR (n div 2)))\<close> for m n :: natural
-  by transfer (fact or_nat_unfold)
-
-lemma [code]:
-  \<open>m XOR n = (if m = 0 then n else if n = 0 then m
-    else (m mod 2 + n mod 2) mod 2 + 2 * ((m div 2) XOR (n div 2)))\<close> for m n :: natural
-  by transfer (fact xor_nat_unfold)
-
-lemma [code]:
-  \<open>unset_bit 0 m = 2 * (m div 2)\<close>
-  \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close> for m :: natural
-  by (transfer; simp add: unset_bit_Suc)+
-
-end
-
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"
   .
@@ -1323,6 +1329,56 @@
 lemma [code]: "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
   by transfer simp
 
+context
+  includes bit_operations_syntax
+begin
+
+lemma [code]:
+  \<open>bit m n \<longleftrightarrow> bit (integer_of_natural m) n\<close>
+  by transfer (simp add: bit_simps)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (m AND n) = integer_of_natural m AND integer_of_natural n\<close>
+  by transfer (simp add: of_nat_and_eq)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (m OR n) = integer_of_natural m OR integer_of_natural n\<close>
+  by transfer (simp add: of_nat_or_eq)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (m XOR n) = integer_of_natural m XOR integer_of_natural n\<close>
+  by transfer (simp add: of_nat_xor_eq)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (mask n) = mask n\<close>
+  by transfer (simp add: of_nat_mask_eq)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (set_bit n m) = set_bit n (integer_of_natural m)\<close>
+  by transfer (simp add: of_nat_set_bit_eq)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (unset_bit n m) = unset_bit n (integer_of_natural m)\<close>
+  by transfer (simp add: of_nat_unset_bit_eq)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (flip_bit n m) = flip_bit n (integer_of_natural m)\<close>
+  by transfer (simp add: of_nat_flip_bit_eq)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (push_bit n m) = push_bit n (integer_of_natural m)\<close>
+  by transfer (simp add: of_nat_push_bit)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (drop_bit n m) = drop_bit n (integer_of_natural m)\<close>
+  by transfer (simp add: of_nat_drop_bit)
+
+lemma [code abstract]:
+  \<open>integer_of_natural (take_bit n m) = take_bit n (integer_of_natural m)\<close>
+  by transfer (simp add: of_nat_take_bit)
+
+end
+
 hide_const (open) Nat
 
 code_reflect Code_Numeral
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Codegenerator_Test/Code_Test_GHC.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_GHC.thy
     Author:     Andreas Lochbihler, ETH Zurich
-    Author:     Florian Haftmann, TU Muenchen
 *)
 
 theory Code_Test_GHC
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_OCaml.thy
     Author:     Andreas Lochbihler, ETH Zurich
-    Author:     Florian Haftmann, TU Muenchen
 *)
 
 theory Code_Test_OCaml
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_PolyML.thy
     Author:     Andreas Lochbihler, ETH Zurich
-    Author:     Florian Haftmann, TU Muenchen
 *)
 
 theory Code_Test_PolyML
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Codegenerator_Test/Code_Test_Scala.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
     Author:     Andreas Lochbihler, ETH Zurich
-    Author:     Florian Haftmann, TU Muenchen
 *)
 
-theory Code_Test_Scala imports
+theory Code_Test_Scala
+imports
   "HOL-Library.Code_Test"
   Code_Lazy_Test
 begin
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -0,0 +1,63 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Test of target-language bit operations\<close>
+
+theory Generate_Target_Bit_Operations
+imports
+  "HOL-Library.Code_Test"
+  "HOL-Library.Code_Target_Bit_Shifts"
+begin
+
+unbundle bit_operations_syntax
+
+definition computations where
+  \<open>computations = (
+    [bit (473514 :: integer) 5, bit (- 805167 :: integer) 7],
+    [473514 AND 767063, - 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: integer],
+    [473514 OR 767063, - 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: integer],
+    [473514 XOR 767063, - 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: integer],
+    [NOT 473513, NOT (- 805167) :: integer],
+    mask 39 :: integer,
+    [set_bit 15 473514, set_bit 11 (- 805167) :: integer],
+    [unset_bit 13 473514, unset_bit 12 (- 805167) :: integer],
+    [flip_bit 15 473514, flip_bit 12 (- 805167) :: integer],
+    [push_bit 12 473514, push_bit 12 (- 805167) :: integer],
+    [drop_bit 12 473514, drop_bit 12 (- 805167) :: integer],
+    [take_bit 12 473514, take_bit 12 (- 805167) :: integer],
+    [signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: integer]
+  )\<close>
+
+definition results where
+  \<open>results = (
+    [True, True],
+    [208898, 242769, 209184, - 839103 :: integer],
+    [1031679, - 280873, - 50197, - 280591 :: integer],
+    [822781, - 523642, - 259381, 558512 :: integer],
+    [- 473514, 805166 :: integer],
+    549755813887 :: integer,
+    [506282, - 803119 :: integer],
+    [465322, - 809263 :: integer],
+    [506282, - 809263 :: integer],
+    [1939513344, - 3297964032 :: integer],
+    [115, - 197 :: integer],
+    [2474, 1745 :: integer],
+    [- 1622, - 2351 :: integer]
+  )\<close>
+
+definition check where
+  \<open>check \<longleftrightarrow> computations = results\<close>
+
+lemma check
+  by code_simp
+
+lemma check
+  by normalization
+
+lemma check
+  by eval
+
+test_code check in OCaml
+test_code check in GHC
+test_code check in Scala
+
+end
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Library/Code_Target_Bit_Shifts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -0,0 +1,186 @@
+(*  Title:      HOL/Library/Code_Target_Bit_Shifts.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Implementation of bit-shifts on target-language integers by built-in operations\<close>
+
+theory Code_Target_Bit_Shifts
+imports Main
+begin
+
+context
+begin
+
+qualified definition push_bit :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+  where \<open>push_bit i k = Bit_Operations.push_bit (nat_of_integer \<bar>i\<bar>) k\<close>
+
+qualified lemma push_bit_code [code]:
+  \<open>push_bit i k = k * 2 ^ nat_of_integer \<bar>i\<bar>\<close>
+  by (simp add: push_bit_def push_bit_eq_mult)
+
+lemma push_bit_integer_code [code]:
+  \<open>Bit_Operations.push_bit n k = push_bit (of_nat n) k\<close>
+  by (simp add: push_bit_def)
+
+qualified definition drop_bit :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+  where \<open>drop_bit i k = Bit_Operations.drop_bit (nat_of_integer \<bar>i\<bar>) k\<close>
+
+qualified lemma drop_bit_code [code]:
+  \<open>drop_bit i k = k div 2 ^ nat_of_integer \<bar>i\<bar>\<close>
+  by (simp add: drop_bit_def drop_bit_eq_div)
+
+lemma drop_bit_integer_code [code]:
+  \<open>Bit_Operations.drop_bit n k = drop_bit (of_nat n) k\<close>
+  by (simp add: drop_bit_def)
+
+end
+
+code_printing code_module Bit_Shifts \<rightharpoonup>
+    (SML) \<open>
+structure Bit_Shifts : sig
+  type int = IntInf.int
+  val push : int -> int -> int
+  val drop : int -> int -> int
+end = struct
+
+type int = IntInf.int;
+
+fun curry f x y = f (x, y);
+
+fun fold _ [] y = y
+  | fold f (x :: xs) y = fold f xs (f x y);
+
+fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x);
+
+val exp = curry IntInf.pow 2;
+
+val div_mod = curry IntInf.divMod;
+
+val max_index = exp (Word.wordSize - 3) - 1; (*experimentally determined*)
+
+val word_of_int = Word.fromLargeInt o IntInf.toLarge;
+
+val word_max_index = word_of_int max_index;
+
+fun words_of_int k = case div_mod k max_index
+  of (b, s) => word_of_int s :: (replicate b word_max_index);
+
+fun push' i k = IntInf.<< (k, i);
+
+fun drop' i k = IntInf.~>> (k, i);
+
+(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
+
+fun push i = fold push' (words_of_int (IntInf.abs i));
+
+fun drop i = fold drop' (words_of_int (IntInf.abs i));
+
+end;\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
+    and (OCaml) \<open>
+module Bit_Shifts : sig
+  val push : Z.t -> Z.t -> Z.t
+  val drop : Z.t -> Z.t -> Z.t
+end = struct
+
+let curry f x y = f (x, y);;
+
+let rec fold f xs y = match xs with
+  [] -> y
+  | (x :: xs) -> fold f xs (f x y);;
+
+let rec replicate n x = (if Z.leq n Z.zero then [] else x :: replicate (Z.pred n) x);;
+
+let max_index = Z.of_int max_int;;
+
+let splitIndex i = let (b, s) = Z.div_rem i max_index
+  in Z.to_int s :: (replicate b max_int);;
+
+let push' i k = Z.shift_left k i;;
+
+let drop' i k = Z.shift_right k i;;
+
+(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
+
+let push i = fold push' (splitIndex (Z.abs i));;
+
+let drop i = fold drop' (splitIndex (Z.abs i));;
+
+end;;
+\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
+    and (Haskell) \<open>
+module Bit_Shifts where
+
+import Prelude (Int, Integer, toInteger, fromInteger, maxBound, divMod, (-), (<=), abs, flip)
+import GHC.Bits (Bits)
+import Data.Bits (shiftL, shiftR)
+
+fold :: (a -> b -> b) -> [a] -> b -> b
+fold _ [] y = y
+fold f (x : xs) y = fold f xs (f x y)
+
+replicate :: Integer -> a -> [a]
+replicate k x = if k <= 0 then [] else x : replicate (k - 1) x
+
+maxIndex :: Integer
+maxIndex = toInteger (maxBound :: Int)
+
+splitIndex :: Integer -> [Int]
+splitIndex i = fromInteger s : replicate (fromInteger b) maxBound
+  where (b, s) = i `divMod` maxIndex
+
+{- The implementations are formally total, though indices >~ maxIndex will produce heavy computation load -}
+
+push' :: Int -> Int -> Int
+push' i = flip shiftL (abs i)
+
+push :: Integer -> Integer -> Integer
+push i = fold (flip shiftL) (splitIndex (abs i))
+
+drop' :: Int -> Int -> Int
+drop' i = flip shiftR (abs i)
+
+drop :: Integer -> Integer -> Integer
+drop i = fold (flip shiftR) (splitIndex (abs i))
+\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
+    and (Scala) \<open>
+object Bit_Shifts {
+
+private val maxIndex : BigInt = BigInt(Int.MaxValue);
+
+private def replicate[A](i : BigInt, x : A) : List[A] =
+  if (i <= 0) Nil else x :: replicate[A](i - 1, x)
+
+private def splitIndex(i : BigInt) : List[Int] = {
+  val (b, s) = i /% maxIndex
+  return s.intValue :: replicate(b, Int.MaxValue)
+}
+
+/* The implementations are formally total, though indices >~ maxIndex will produce heavy computation load */
+
+def push(i: BigInt, k: BigInt) : BigInt =
+  splitIndex(i).foldLeft(k) { (l, j) => l << j }
+
+def drop(i: BigInt, k: BigInt) : BigInt =
+  splitIndex(i).foldLeft(k) { (l, j) => l >> j }
+
+}
+\<close> for constant Code_Target_Bit_Shifts.push_bit Code_Target_Bit_Shifts.drop_bit
+| constant Code_Target_Bit_Shifts.push_bit \<rightharpoonup>
+    (SML) "Bit'_Shifts.push"
+    and (OCaml) "Bit'_Shifts.push"
+    and (Haskell) "Bit'_Shifts.push"
+    and (Haskell_Quickcheck) "Bit'_Shifts.push'"
+    and (Scala) "Bit'_Shifts.push"
+| constant Code_Target_Bit_Shifts.drop_bit \<rightharpoonup>
+    (SML) "Bit'_Shifts.drop"
+    and (OCaml) "Bit'_Shifts.drop"
+    and (Haskell) "Bit'_Shifts.drop"
+    and (Haskell_Quickcheck) "Bit'_Shifts.drop'"
+    and (Scala) "Bit'_Shifts.drop"
+
+code_reserved
+  (SML) Bit_Shifts
+  and (Haskell) Bit_Shifts
+  and (Scala) Bit_Shifts
+
+end
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/Library/Code_Target_Numeral.thy
--- a/src/HOL/Library/Code_Target_Numeral.thy	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/HOL/Library/Code_Target_Numeral.thy	Sun Jan 05 15:30:04 2025 +0100
@@ -5,7 +5,7 @@
 section \<open>Implementation of natural and integer numbers by target-language integers\<close>
 
 theory Code_Target_Numeral
-imports Code_Target_Int Code_Target_Nat
+imports Code_Target_Nat Code_Target_Int Code_Target_Bit_Shifts
 begin
 
 end
diff -r 560a069a537f -r b836e9ac0cf3 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/HOL/ROOT	Sun Jan 05 15:30:04 2025 +0100
@@ -373,6 +373,7 @@
     Generate_Target_Nat
     Generate_Abstract_Char
     Generate_Efficient_Datastructures
+    Generate_Target_Bit_Operations
     Code_Lazy_Test
     Code_Test_PolyML
     Code_Test_Scala
diff -r 560a069a537f -r b836e9ac0cf3 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sun Jan 05 15:18:54 2025 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sun Jan 05 15:30:04 2025 +0100
@@ -330,6 +330,10 @@
   ("Maybe", ["Nothing", "Just"])
 ];
 
+val data_bits_import_operators = [
+  ".&.", ".|.", ".^."
+];
+
 fun serialize_haskell module_prefix string_classes ctxt { module_name,
     reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports =
   let
@@ -379,7 +383,10 @@
       enclose "import Prelude (" ");" (commas (map str
         (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
           @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
+      :: enclose "import Data.Bits (" ");" (commas
+        (map (str o Library.enclose "(" ")") data_bits_import_operators))
       :: print_qualified_import "Prelude"
+      :: print_qualified_import "Data.Bits"
       :: map (print_qualified_import o fst) includes;
     fun print_module module_name (gr, imports) =
       let