# HG changeset patch
# User wenzelm
# Date 1735325875 -3600
# Node ID ece4941f0f1786e9c0c268ca3f62e46ff797fd82
# Parent  0ca0a47235e53ec93bce681e2a149726b829db61# Parent  70d2f72098df74a3781d46fd7ba60d652ba4c4b9
merged

diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Fri Dec 27 19:49:45 2024 +0100
+++ b/src/HOL/Bit_Operations.thy	Fri Dec 27 19:57:55 2024 +0100
@@ -1237,14 +1237,6 @@
   \<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
   by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_flip_bit_iff)
 
-lemma bit_1_0 [simp]:
-  \<open>bit 1 0\<close>
-  by (simp add: bit_0)
-
-lemma not_bit_1_Suc [simp]:
-  \<open>\<not> bit 1 (Suc n)\<close>
-  by (simp add: bit_Suc)
-
 lemma push_bit_Suc_numeral [simp]:
   \<open>push_bit (Suc n) (numeral k) = push_bit n (numeral (Num.Bit0 k))\<close>
   by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
@@ -1387,7 +1379,7 @@
 
 lemma not_one_eq [simp]:
   \<open>NOT 1 = - 2\<close>
-  by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
+  by (rule bit_eqI, simp add: bit_simps)
 
 sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
   by standard (rule bit_eqI, simp add: bit_and_iff)
@@ -2695,6 +2687,18 @@
 context semiring_bits
 begin
 
+lemma bit_1_0 [simp]:
+  \<open>bit 1 0\<close>
+  by (simp add: bit_0)
+
+lemma not_bit_1_Suc [simp]:
+  \<open>\<not> bit 1 (Suc n)\<close>
+  by (simp add: bit_Suc)
+
+lemma not_bit_1_numeral [simp]:
+  \<open>\<not> bit 1 (numeral m)\<close>
+  by (simp add: numeral_eq_Suc)
+
 lemma not_bit_numeral_Bit0_0 [simp]:
   \<open>\<not> bit (numeral (Num.Bit0 m)) 0\<close>
   by (simp add: bit_0)
@@ -2770,7 +2774,6 @@
   by (cases n; simp add: bit_0)+
 
 lemma bit_numeral_simps [simp]:
-  \<open>\<not> bit 1 (numeral n)\<close>
   \<open>bit (numeral (Num.Bit0 w)) (numeral n) \<longleftrightarrow> bit (numeral w) (pred_numeral n)\<close>
   \<open>bit (numeral (Num.Bit1 w)) (numeral n) \<longleftrightarrow> bit (numeral w) (pred_numeral n)\<close>
   by (simp_all add: bit_1_iff numeral_eq_Suc)
@@ -2923,7 +2926,8 @@
   \<open>numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\<close>
   \<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\<close>
   \<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
-  by (simp_all add: bit_eq_iff) (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split)
+  by (simp_all add: bit_eq_iff)
+    (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split)
 
 fun and_not_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
 where
diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Dec 27 19:49:45 2024 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Dec 27 19:57:55 2024 +0100
@@ -872,6 +872,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
diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Codegenerator_Test/Code_Test_GHC.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri Dec 27 19:49:45 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri Dec 27 19:57:55 2024 +0100
@@ -1,10 +1,15 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_GHC.thy
     Author:     Andreas Lochbihler, ETH Zurich
-
-Test case for test_code on GHC
+    Author:     Florian Haftmann, TU Muenchen
 *)
 
-theory Code_Test_GHC imports "HOL-Library.Code_Test" Code_Lazy_Test begin
+theory Code_Test_GHC
+imports
+  "HOL-Library.Code_Test"
+  Code_Lazy_Test
+begin
+
+text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
 
 test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
 
@@ -22,4 +27,163 @@
 
 test_code "stake 10 (cycle ''ab'') = ''ababababab''" in GHC
 
+text \<open>Test cases for bit operations on target language numerals\<close>
+
+unbundle bit_operations_syntax
+
+lemma \<open>bit (473514 :: integer) 5\<close>
+  by normalization
+
+test_code \<open>bit (473514 :: integer) 5\<close> in GHC
+
+lemma \<open>bit (- 805167 :: integer) 7\<close>
+  by normalization
+
+test_code \<open>bit (- 805167 :: integer) 7\<close> in GHC
+
+lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
+  by normalization
+
+test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in GHC
+
+lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
+  by normalization
+
+test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in GHC
+
+lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
+  by normalization
+
+test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in GHC
+
+lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
+  by normalization
+
+test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in GHC
+
+lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
+  by normalization
+
+test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in GHC
+
+lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
+  by normalization
+
+test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in GHC
+
+lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
+  by normalization
+
+test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in GHC
+
+lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
+  by normalization
+
+test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in GHC
+
+lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
+  by normalization
+
+test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in GHC
+
+lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
+  by normalization
+
+test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in GHC
+
+lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
+  by normalization
+
+test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in GHC
+
+lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
+  by normalization
+
+test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in GHC
+
+lemma \<open>NOT (473513 :: integer) = - 473514\<close>
+  by normalization
+
+test_code \<open>NOT (473513 :: integer) = - 473514\<close> in GHC
+
+lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
+  by normalization
+
+test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in GHC
+
+lemma \<open>(mask 39 :: integer) = 549755813887\<close>
+  by normalization
+
+test_code \<open>(mask 39 :: integer) = 549755813887\<close> in GHC
+
+lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
+  by normalization
+
+test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in GHC
+
+lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
+  by normalization
+
+test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in GHC
+
+lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
+  by normalization
+
+test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in GHC
+
+lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
+  by normalization
+
+test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in GHC
+
+lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
+  by normalization
+
+test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in GHC
+
+lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
+  by normalization
+
+test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in GHC
+
+lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
+  by normalization
+
+test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in GHC
+
+lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
+  by normalization
+
+test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in GHC
+
+lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
+  by normalization
+
+test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in GHC
+
+lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
+  by normalization
+
+test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in GHC
+
+lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
+  by normalization
+
+test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in GHC
+
+lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
+  by normalization
+
+test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in GHC
+
+lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
+  by normalization
+
+test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in GHC
+
+lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
+  by normalization
+
+test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in GHC
+
 end
diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri Dec 27 19:49:45 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri Dec 27 19:57:55 2024 +0100
@@ -1,10 +1,15 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_OCaml.thy
     Author:     Andreas Lochbihler, ETH Zurich
-
-Test case for test_code on OCaml
+    Author:     Florian Haftmann, TU Muenchen
 *)
 
-theory Code_Test_OCaml imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
+theory Code_Test_OCaml
+imports
+  "HOL-Library.Code_Test"
+  Code_Lazy_Test
+begin
+
+text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
 
@@ -22,4 +27,163 @@
 
 test_code "stake 10 (cycle ''ab'') = ''ababababab''" in OCaml
 
+text \<open>Test cases for bit operations on target language numerals\<close>
+
+unbundle bit_operations_syntax
+
+lemma \<open>bit (473514 :: integer) 5\<close>
+  by normalization
+
+test_code \<open>bit (473514 :: integer) 5\<close> in OCaml
+
+lemma \<open>bit (- 805167 :: integer) 7\<close>
+  by normalization
+
+test_code \<open>bit (- 805167 :: integer) 7\<close> in OCaml
+
+lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
+  by normalization
+
+test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in OCaml
+
+lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
+  by normalization
+
+test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in OCaml
+
+lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
+  by normalization
+
+test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in OCaml
+
+lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
+  by normalization
+
+test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in OCaml
+
+lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
+  by normalization
+
+test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in OCaml
+
+lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
+  by normalization
+
+test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in OCaml
+
+lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
+  by normalization
+
+test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in OCaml
+
+lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
+  by normalization
+
+test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in OCaml
+
+lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
+  by normalization
+
+test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in OCaml
+
+lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
+  by normalization
+
+test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in OCaml
+
+lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
+  by normalization
+
+test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in OCaml
+
+lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
+  by normalization
+
+test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in OCaml
+
+lemma \<open>NOT (473513 :: integer) = - 473514\<close>
+  by normalization
+
+test_code \<open>NOT (473513 :: integer) = - 473514\<close> in OCaml
+
+lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
+  by normalization
+
+test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in OCaml
+
+lemma \<open>(mask 39 :: integer) = 549755813887\<close>
+  by normalization
+
+test_code \<open>(mask 39 :: integer) = 549755813887\<close> in OCaml
+
+lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
+  by normalization
+
+test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in OCaml
+
+lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
+  by normalization
+
+test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in OCaml
+
+lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
+  by normalization
+
+test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in OCaml
+
+lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
+  by normalization
+
+test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in OCaml
+
+lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
+  by normalization
+
+test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in OCaml
+
+lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
+  by normalization
+
+test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in OCaml
+
+lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
+  by normalization
+
+test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in OCaml
+
+lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
+  by normalization
+
+test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in OCaml
+
+lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
+  by normalization
+
+test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in OCaml
+
+lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
+  by normalization
+
+test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in OCaml
+
+lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
+  by normalization
+
+test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in OCaml
+
+lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
+  by normalization
+
+test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in OCaml
+
+lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
+  by normalization
+
+test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in OCaml
+
+lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
+  by normalization
+
+test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in OCaml
+
 end
diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri Dec 27 19:49:45 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri Dec 27 19:57:55 2024 +0100
@@ -1,10 +1,15 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_PolyML.thy
     Author:     Andreas Lochbihler, ETH Zurich
-
-Test case for test_code on PolyML
+    Author:     Florian Haftmann, TU Muenchen
 *)
 
-theory Code_Test_PolyML imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
+theory Code_Test_PolyML
+imports 
+  "HOL-Library.Code_Test"
+  Code_Lazy_Test
+begin
+
+text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
 
@@ -12,4 +17,163 @@
 
 test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML
 
+text \<open>Test cases for bit operations on target language numerals\<close>
+
+unbundle bit_operations_syntax
+
+lemma \<open>bit (473514 :: integer) 5\<close>
+  by normalization
+
+test_code \<open>bit (473514 :: integer) 5\<close> in PolyML
+
+lemma \<open>bit (- 805167 :: integer) 7\<close>
+  by normalization
+
+test_code \<open>bit (- 805167 :: integer) 7\<close> in PolyML
+
+lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
+  by normalization
+
+test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in PolyML
+
+lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
+  by normalization
+
+test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in PolyML
+
+lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
+  by normalization
+
+test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in PolyML
+
+lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
+  by normalization
+
+test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in PolyML
+
+lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
+  by normalization
+
+test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in PolyML
+
+lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
+  by normalization
+
+test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in PolyML
+
+lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
+  by normalization
+
+test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in PolyML
+
+lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
+  by normalization
+
+test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in PolyML
+
+lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
+  by normalization
+
+test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in PolyML
+
+lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
+  by normalization
+
+test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in PolyML
+
+lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
+  by normalization
+
+test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in PolyML
+
+lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
+  by normalization
+
+test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in PolyML
+
+lemma \<open>NOT (473513 :: integer) = - 473514\<close>
+  by normalization
+
+test_code \<open>NOT (473513 :: integer) = - 473514\<close> in PolyML
+
+lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
+  by normalization
+
+test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in PolyML
+
+lemma \<open>(mask 39 :: integer) = 549755813887\<close>
+  by normalization
+
+test_code \<open>(mask 39 :: integer) = 549755813887\<close> in PolyML
+
+lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
+  by normalization
+
+test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in PolyML
+
+lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
+  by normalization
+
+test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in PolyML
+
+lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
+  by normalization
+
+test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in PolyML
+
+lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
+  by normalization
+
+test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in PolyML
+
+lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
+  by normalization
+
+test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in PolyML
+
+lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
+  by normalization
+
+test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in PolyML
+
+lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
+  by normalization
+
+test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in PolyML
+
+lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
+  by normalization
+
+test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in PolyML
+
+lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
+  by normalization
+
+test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in PolyML
+
+lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
+  by normalization
+
+test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in PolyML
+
+lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
+  by normalization
+
+test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in PolyML
+
+lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
+  by normalization
+
+test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in PolyML
+
+lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
+  by normalization
+
+test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in PolyML
+
+lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
+  by normalization
+
+test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in PolyML
+
 end
diff -r 70d2f72098df -r ece4941f0f17 src/HOL/Codegenerator_Test/Code_Test_Scala.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri Dec 27 19:49:45 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri Dec 27 19:57:55 2024 +0100
@@ -1,10 +1,14 @@
 (*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
     Author:     Andreas Lochbihler, ETH Zurich
-
-Test case for test_code on Scala
+    Author:     Florian Haftmann, TU Muenchen
 *)
 
-theory Code_Test_Scala imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
+theory Code_Test_Scala imports
+  "HOL-Library.Code_Test"
+  Code_Lazy_Test
+begin
+
+text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
 
@@ -22,4 +26,163 @@
 
 test_code "stake 10 (cycle ''ab'') = ''ababababab''" in Scala
 
+text \<open>Test cases for bit operations on target language numerals\<close>
+
+unbundle bit_operations_syntax
+
+lemma \<open>bit (473514 :: integer) 5\<close>
+  by normalization
+
+test_code \<open>bit (473514 :: integer) 5\<close> in Scala
+
+lemma \<open>bit (- 805167 :: integer) 7\<close>
+  by normalization
+
+test_code \<open>bit (- 805167 :: integer) 7\<close> in Scala
+
+lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
+  by normalization
+
+test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in Scala
+
+lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
+  by normalization
+
+test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in Scala
+
+lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
+  by normalization
+
+test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in Scala
+
+lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
+  by normalization
+
+test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in Scala
+
+lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
+  by normalization
+
+test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in Scala
+
+lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
+  by normalization
+
+test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in Scala
+
+lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
+  by normalization
+
+test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in Scala
+
+lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
+  by normalization
+
+test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in Scala
+
+lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
+  by normalization
+
+test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in Scala
+
+lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
+  by normalization
+
+test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in Scala
+
+lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
+  by normalization
+
+test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in Scala
+
+lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
+  by normalization
+
+test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in Scala
+
+lemma \<open>NOT (473513 :: integer) = - 473514\<close>
+  by normalization
+
+test_code \<open>NOT (473513 :: integer) = - 473514\<close> in Scala
+
+lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
+  by normalization
+
+test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in Scala
+
+lemma \<open>(mask 39 :: integer) = 549755813887\<close>
+  by normalization
+
+test_code \<open>(mask 39 :: integer) = 549755813887\<close> in Scala
+
+lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
+  by normalization
+
+test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in Scala
+
+lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
+  by normalization
+
+test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in Scala
+
+lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
+  by normalization
+
+test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in Scala
+
+lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
+  by normalization
+
+test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in Scala
+
+lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
+  by normalization
+
+test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in Scala
+
+lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
+  by normalization
+
+test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in Scala
+
+lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
+  by normalization
+
+test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in Scala
+
+lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
+  by normalization
+
+test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in Scala
+
+lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
+  by normalization
+
+test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in Scala
+
+lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
+  by normalization
+
+test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in Scala
+
+lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
+  by normalization
+
+test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in Scala
+
+lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
+  by normalization
+
+test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in Scala
+
+lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
+  by normalization
+
+test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in Scala
+
+lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
+  by normalization
+
+test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in Scala
+
 end
diff -r 70d2f72098df -r ece4941f0f17 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Dec 27 19:49:45 2024 +0100
+++ b/src/Tools/Code/code_haskell.ML	Fri Dec 27 19:57:55 2024 +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