official theory for using bit shift operations for ordinary arithmetic if feasible

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Basic_Setup.thy	Tue Apr 15 23:04:44 2025 +0200
@@ -0,0 +1,33 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Basic setup\<close>
+
+theory Basic_Setup
+imports
+  Complex_Main
+begin
+
+text \<open>Drop technical stuff from \<^theory>\<open>HOL.Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>
+
+ML \<open>
+structure Codegenerator_Test =
+struct
+
+fun drop_partial_term_of thy =
+  let
+    val tycos = Sign.logical_types thy;
+    val consts = map_filter (try (curry (Axclass.param_of_inst thy)
+      \<^const_name>\<open>Quickcheck_Narrowing.partial_term_of\<close>)) tycos;
+  in
+    thy
+    |> fold Code.declare_unimplemented_global consts
+  end;
+
+end;
+\<close>
+
+text \<open>Avoid popular infix.\<close>
+
+code_reserved (SML) upto
+
+end

--- a/src/HOL/Codegenerator_Test/Candidates.thy	Tue Apr 15 19:40:42 2025 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Apr 15 23:04:44 2025 +0200
@@ -5,7 +5,7 @@
 
 theory Candidates
 imports
-  Complex_Main
+  Basic_Setup
   "HOL-Library.Library"
   "HOL-Library.Sorting_Algorithms"
   "HOL-Library.Subseq_Order"
@@ -19,16 +19,7 @@
   "HOL-Examples.Gauss_Numbers"
 begin
 
-text \<open>Drop technical stuff from \<^theory>\<open>HOL.Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>
-
-setup \<open>
-fn thy =>
-let
-  val tycos = Sign.logical_types thy;
-  val consts = map_filter (try (curry (Axclass.param_of_inst thy)
-    \<^const_name>\<open>Quickcheck_Narrowing.partial_term_of\<close>)) tycos;
-in fold Code.declare_unimplemented_global consts thy end
-\<close>
+setup \<open>Codegenerator_Test.drop_partial_term_of\<close>
 
 text \<open>Simple example for the predicate compiler.\<close>
 
@@ -40,10 +31,6 @@
 
 code_pred sublist .
 
-text \<open>Avoid popular infix.\<close>
-
-code_reserved (SML) upto
-
 text \<open>Explicit check in \<open>OCaml\<close> for correct precedence of let expressions in list expressions\<close>
 
 definition funny_list :: "bool list"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Rewrites_To_Bit_Operations.thy	Tue Apr 15 23:04:44 2025 +0200
@@ -0,0 +1,21 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Test of arithmetic using target-language bit operations\<close>
+
+theory Generate_Target_Rewrites_To_Bit_Operations
+imports
+  Basic_Setup
+  "HOL-Library.Code_Bit_Shifts_for_Arithmetic"
+  "HOL-Library.Code_Test"
+begin
+
+setup \<open>Codegenerator_Test.drop_partial_term_of\<close>
+
+text \<open>
+  If any of the checks fails, inspect the code generated
+  by a corresponding \<open>export_code\<close> command.
+\<close>
+
+export_code _ checking SML OCaml? Haskell? Scala
+
+end