# HG changeset patch
# User haftmann
# Date 1737016016 -3600
# Node ID 8df58b532ecb5fc75b2f84784ca38706a31dfb50
# Parent  232ccd03d9afff7c4742cc9074c05c1c18817990
theory to rewrite arithmetic operations to bit shifts

diff -r 232ccd03d9af -r 8df58b532ecb NEWS
--- a/NEWS	Wed Jan 15 17:48:38 2025 +0100
+++ b/NEWS	Thu Jan 16 09:26:56 2025 +0100
@@ -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
diff -r 232ccd03d9af -r 8df58b532ecb src/HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy	Thu Jan 16 09:26:56 2025 +0100
@@ -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