merged
authorpaulson
Thu, 16 Jan 2025 10:09:42 +0000
changeset 81817 e31120ed89c9
parent 81815 0b31f0909060 (diff)
parent 81816 bee084ecd18c (current diff)
child 81818 1085eb118dc7
merged
--- a/NEWS	Thu Jan 16 10:09:33 2025 +0000
+++ b/NEWS	Thu Jan 16 10:09:42 2025 +0000
@@ -235,6 +235,9 @@
 types by target-language operations; this is also used by
 HOL-Library.Code_Target_Numeral.
 
+* Theory HOL-Library.Code_Bit_Shifts_for_Arithmetic rewrites certain
+arithmetic operations on numerals to bit shifts.
+
 * Sledgehammer:
   - Update of bundled provers:
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Thu Jan 16 10:09:33 2025 +0000
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Thu Jan 16 10:09:42 2025 +0000
@@ -26,163 +26,4 @@
 
 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
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Thu Jan 16 10:09:33 2025 +0000
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Thu Jan 16 10:09:42 2025 +0000
@@ -26,163 +26,4 @@
 
 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
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Thu Jan 16 10:09:33 2025 +0000
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Thu Jan 16 10:09:42 2025 +0000
@@ -16,163 +16,4 @@
 
 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
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Thu Jan 16 10:09:33 2025 +0000
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Thu Jan 16 10:09:42 2025 +0000
@@ -26,163 +26,4 @@
 
 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
--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Jan 16 10:09:33 2025 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Jan 16 10:09:42 2025 +0000
@@ -60,4 +60,25 @@
 test_code check in GHC
 test_code check in Scala
 
+text \<open>Checking the index maximum for \<text>\<open>SML\<close>\<close>
+
+ML \<open>
+fun check_max max =
+  let
+    val _ = IntInf.~>> (0, max);
+    val _ = \<^assert> ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); false) handle Size => true)
+  in () end;
+\<close>
+
+definition \<open>check_max = ()\<close>
+
+code_printing constant check \<rightharpoonup>
+  (Eval) "check'_max Bit'_Shifts.word'_max'_index"
+
+definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+
+ML \<open>
+\<^code>\<open>anchor\<close>;
+\<close>
+
 end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy	Thu Jan 16 10:09:42 2025 +0000
@@ -0,0 +1,62 @@
+(*  Title:      HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Rewrite arithmetic operations to bit-shifts if feasible\<close>
+
+theory Code_Bit_Shifts_for_Arithmetic
+  imports Main
+begin
+
+context semiring_bit_operations
+begin
+
+context
+  includes bit_operations_syntax
+begin
+
+lemma [code_unfold]:
+  \<open>of_bool (odd a) = a AND 1\<close>
+  by (simp add: and_one_eq mod2_eq_if)
+
+lemma [code_unfold]:
+  \<open>even a \<longleftrightarrow> a AND 1 = 0\<close>
+  by (simp add: and_one_eq mod2_eq_if)
+
+lemma [code_unfold]:
+  \<open>2 * a = push_bit 1 a\<close>
+  by (simp add: ac_simps)
+
+lemma [code_unfold]:
+  \<open>a * 2 = push_bit 1 a\<close>
+  by simp
+
+lemma [code_unfold]:
+  \<open>2 ^ n * a = push_bit n a\<close>
+  by (simp add: push_bit_eq_mult ac_simps)
+
+lemma [code_unfold]:
+  \<open>a * 2 ^ n = push_bit n a\<close>
+  by (simp add: push_bit_eq_mult)
+
+lemma [code_unfold]:
+  \<open>a div 2 = drop_bit 1 a\<close>
+  by (simp add: drop_bit_eq_div)
+
+lemma [code_unfold]:
+  \<open>a div 2 ^ n = drop_bit n a\<close>
+  by (simp add: drop_bit_eq_div)
+
+lemma [code_unfold]:
+  \<open>a mod 2 = take_bit 1 a\<close>
+  by (simp add: take_bit_eq_mod)
+
+lemma [code_unfold]:
+  \<open>a mod 2 ^ n  = take_bit n a\<close>
+  by (simp add: take_bit_eq_mod)
+
+end
+
+end
+
+end
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Thu Jan 16 10:09:33 2025 +0000
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Thu Jan 16 10:09:42 2025 +0000
@@ -41,6 +41,7 @@
   type int = IntInf.int
   val push : int -> int -> int
   val drop : int -> int -> int
+  val word_max_index : Word.word (*only for validation*)
 end = struct
 
 type int = IntInf.int;