# HG changeset patch
# User haftmann
# Date 1737407711 -3600
# Node ID ac0716ca151be9262503156441c2de3870cdb01f
# Parent  7fe20d39459332629652bcbffae130fa283b47e8
systematic checks for bit operations and more rules on symbolic terms

diff -r 7fe20d394593 -r ac0716ca151b src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Mon Jan 20 22:15:11 2025 +0100
+++ b/src/HOL/Bit_Operations.thy	Mon Jan 20 22:15:11 2025 +0100
@@ -132,6 +132,17 @@
   using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] div_mult_mod_eq [of a \<open>2 ^ n\<close>] that
   by simp (metis (full_types) add.left_commute add_left_imp_eq)
 
+lemma half_numeral_Bit1_eq [simp]:
+  \<open>numeral (num.Bit1 m) div 2 = numeral (num.Bit0 m) div 2\<close>
+  using even_half_succ_eq [of \<open>2 * numeral m\<close>]
+  by simp
+
+lemma double_half_numeral_Bit_0_eq [simp]:
+  \<open>2 * (numeral (num.Bit0 m) div 2) = numeral (num.Bit0 m)\<close>
+  \<open>(numeral (num.Bit0 m) div 2) * 2 = numeral (num.Bit0 m)\<close>
+  using mod_mult_div_eq [of \<open>numeral (Num.Bit0 m)\<close> 2]
+  by (simp_all add: mod2_eq_if ac_simps)
+
 named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>
 
 definition possible_bit :: \<open>'a itself \<Rightarrow> nat \<Rightarrow> bool\<close>
@@ -1195,7 +1206,7 @@
     by (cases n) (auto simp: bit_0 bit_double_iff even_bit_succ_iff)
 qed
 
-lemma set_bit_0 [simp]:
+lemma set_bit_0:
   \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)
 
@@ -1204,7 +1215,7 @@
   by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
     elim: possible_bit_less_imp)
 
-lemma unset_bit_0 [simp]:
+lemma unset_bit_0:
   \<open>unset_bit 0 a = 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps simp flip: bit_Suc)
 
@@ -1212,7 +1223,7 @@
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)
 
-lemma flip_bit_0 [simp]:
+lemma flip_bit_0:
   \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
   by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)
 
@@ -1557,7 +1568,7 @@
 
 lemma drop_bit_Suc_bit1 [simp]:
   \<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit1_div_2)
+  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
 
 lemma drop_bit_numeral_bit0 [simp]:
   \<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
@@ -1565,7 +1576,7 @@
 
 lemma drop_bit_numeral_bit1 [simp]:
   \<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
-  by (simp add: drop_bit_rec numeral_Bit1_div_2)
+  by (simp add: drop_bit_rec numeral_Bit0_div_2)
 
 lemma take_bit_Suc_1 [simp]:
   \<open>take_bit (Suc n) 1 = 1\<close>
@@ -1577,7 +1588,7 @@
 
 lemma take_bit_Suc_bit1:
   \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
+  by (simp add: take_bit_Suc numeral_Bit0_div_2 mod_2_eq_odd)
 
 lemma take_bit_numeral_1 [simp]:
   \<open>take_bit (numeral l) 1 = 1\<close>
@@ -1589,7 +1600,7 @@
 
 lemma take_bit_numeral_bit1:
   \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
+  by (simp add: take_bit_rec numeral_Bit0_div_2 mod_2_eq_odd)
 
 lemma bit_of_nat_iff_bit [bit_simps]:
   \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
@@ -2600,7 +2611,7 @@
 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 n :: nat
-  by (simp_all add: unset_bit_Suc)
+  by (simp_all add: unset_bit_0 unset_bit_Suc)
 
 lemma push_bit_of_Suc_0 [simp]:
   \<open>push_bit n (Suc 0) = 2 ^ n\<close>
@@ -2778,7 +2789,7 @@
 
 lemma bit_numeral_Bit1_Suc_iff [simp]:
   \<open>bit (numeral (Num.Bit1 m)) (Suc n) \<longleftrightarrow> bit (numeral m) n\<close>
-  by (simp add: bit_Suc numeral_Bit1_div_2)
+  by (simp add: bit_Suc numeral_Bit0_div_2)
 
 lemma bit_numeral_rec:
   \<open>bit (numeral (Num.Bit0 w)) n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc m \<Rightarrow> bit (numeral w) m)\<close>
@@ -3278,6 +3289,86 @@
 
 end
 
+context semiring_bit_operations
+begin
+
+lemma push_bit_eq_pow:
+  \<open>push_bit (numeral n) 1 = numeral (Num.pow (Num.Bit0 Num.One) n)\<close>
+  by simp
+
+lemma set_bit_of_0 [simp]:
+  \<open>set_bit n 0 = 2 ^ n\<close>
+  by (simp add: set_bit_eq_or)
+
+lemma unset_bit_of_0 [simp]:
+  \<open>unset_bit n 0 = 0\<close>
+  by (simp add: unset_bit_eq_or_xor)
+
+lemma flip_bit_of_0 [simp]:
+  \<open>flip_bit n 0 = 2 ^ n\<close>
+  by (simp add: flip_bit_eq_xor)
+
+lemma set_bit_0_numeral_eq [simp]:
+  \<open>set_bit 0 (numeral Num.One) = 1\<close>
+  \<open>set_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit1 m)\<close>
+  \<open>set_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit1 m)\<close>
+  by (simp_all add: set_bit_0)
+
+lemma set_bit_numeral_eq_or [simp]:
+  \<open>set_bit (numeral n) (numeral m) = numeral m OR push_bit (numeral n) 1\<close>
+  by (fact set_bit_eq_or)
+
+lemma unset_bit_0_numeral_eq_and_not' [simp]:
+  \<open>unset_bit 0 (numeral Num.One) = 0\<close>
+  \<open>unset_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit0 m)\<close>
+  \<open>unset_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit0 m)\<close>
+  by (simp_all add: unset_bit_0)
+
+lemma unset_bit_numeral_eq_or [simp]:
+  \<open>unset_bit (numeral n) (numeral m) =
+    (case and_not_num m (Num.pow (Num.Bit0 Num.One) n)
+     of None \<Rightarrow> 0
+      | Some q \<Rightarrow> numeral q)\<close> (is \<open>?lhs = _\<close>)
+proof -
+  have \<open>?lhs = of_nat (unset_bit (numeral n) (numeral m))\<close>
+    by (simp add: of_nat_unset_bit_eq)
+  also have \<open>unset_bit (numeral n) (numeral m) = nat (unset_bit (numeral n) (numeral m))\<close>
+    by (simp flip: int_int_eq add: Bit_Operations.of_nat_unset_bit_eq)
+  finally have *: \<open>?lhs = of_nat (nat (unset_bit (numeral n) (numeral m)))\<close> .
+  show ?thesis
+    by (simp only: * unset_bit_eq_and_not Bit_Operations.push_bit_eq_pow int_numeral_and_not_num)
+      (auto split: option.splits)
+qed
+
+lemma flip_bit_0_numeral_eq_or [simp]:
+  \<open>flip_bit 0 (numeral Num.One) = 0\<close>
+  \<open>flip_bit 0 (numeral (Num.Bit0 m)) = numeral (Num.Bit1 m)\<close>
+  \<open>flip_bit 0 (numeral (Num.Bit1 m)) = numeral (Num.Bit0 m)\<close>
+  by (simp_all add: flip_bit_0)
+
+lemma flip_bit_numeral_eq_xor [simp]:
+  \<open>flip_bit (numeral n) (numeral m) = numeral m XOR push_bit (numeral n) 1\<close>
+  by (fact flip_bit_eq_xor)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma set_bit_minus_numeral_eq_or [simp]:
+  \<open>set_bit (numeral n) (- numeral m) = - numeral m OR push_bit (numeral n) 1\<close>
+  by (fact set_bit_eq_or)
+
+lemma unset_bit_minus_numeral_eq_and_not [simp]:
+  \<open>unset_bit (numeral n) (- numeral m) = - numeral m AND NOT (push_bit (numeral n) 1)\<close>
+  by (fact unset_bit_eq_and_not)
+
+lemma flip_bit_minus_numeral_eq_xor [simp]:
+  \<open>flip_bit (numeral n) (- numeral m) = - numeral m XOR push_bit (numeral n) 1\<close>
+  by (fact flip_bit_eq_xor)
+
+end
+
 lemma xor_int_code [code]:
   fixes i j :: int shows
   \<open>0 XOR j = j\<close>
diff -r 7fe20d394593 -r ac0716ca151b src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jan 20 22:15:11 2025 +0100
+++ b/src/HOL/ROOT	Mon Jan 20 22:15:11 2025 +0100
@@ -694,6 +694,7 @@
     BigO
     BinEx
     Birthday_Paradox
+    Bit_Operation_Calculations
     Bubblesort
     CTL
     Cartouche_Examples
diff -r 7fe20d394593 -r ac0716ca151b src/HOL/ex/Bit_Operation_Calculations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Bit_Operation_Calculations.thy	Mon Jan 20 22:15:11 2025 +0100
@@ -0,0 +1,145 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Tests for simplifying bit operations on ground terms\<close>
+
+theory Bit_Operation_Calculations
+  imports
+    "HOL.Bit_Operations"
+    "HOL-Library.Word"
+begin
+
+unbundle bit_operations_syntax
+
+subsection \<open>Generic unsigned computations\<close>
+
+locale unsigned_computations =
+  fixes type :: \<open>'a::semiring_bit_operations itself\<close>
+begin
+
+definition computations where
+  \<open>computations = (
+    [bit (473514 :: 'a) 5],
+    [473514 AND 767063 :: 'a],
+    [473514 OR 767063 :: 'a],
+    [473514 XOR 767063 :: 'a],
+    mask 11 :: 'a,
+    [set_bit 15 473514 :: 'a],
+    [unset_bit 13 473514 :: 'a],
+    [flip_bit 15 473514 :: 'a],
+    [push_bit 12 473514 :: 'a],
+    [drop_bit 12 65344 :: 'a],
+    [take_bit 12 473514 :: 'a]
+  )\<close>
+
+definition results where
+  \<open>results = (
+    [True],
+    [208898 :: 'a::semiring_bit_operations],
+    [1031679 :: 'a],
+    [822781 :: 'a],
+    2047 :: 'a,
+    [506282 :: 'a],
+    [465322 :: 'a],
+    [506282 :: 'a],
+    [1939513344 :: 'a],
+    [15 :: 'a],
+    [2474 :: 'a]
+  )\<close>
+
+lemmas evaluation_simps = computations_def results_def mask_numeral
+   \<comment> \<open>Expressions like \<term>\<open>mask 42\<close> are deliberately not simplified by default\<close>
+
+end
+
+global_interpretation unsigned_computations_nat: unsigned_computations \<open>TYPE(nat)\<close>
+  defines unsigned_computations_nat = unsigned_computations_nat.computations
+    and unsigned_results_nat = unsigned_computations_nat.results .
+
+lemma \<open>unsigned_computations_nat.computations = unsigned_computations_nat.results\<close>
+  by (simp add: unsigned_computations_nat.evaluation_simps)
+
+global_interpretation unsigned_computations_int: unsigned_computations \<open>TYPE(int)\<close>
+  defines unsigned_computations_int = unsigned_computations_int.computations
+    and unsigned_results_int = unsigned_computations_int.results .
+
+lemma \<open>unsigned_computations_int.computations = unsigned_computations_int.results\<close>
+  by (simp add: unsigned_computations_int.evaluation_simps)
+
+global_interpretation unsigned_computations_word16: unsigned_computations \<open>TYPE(16 word)\<close>
+  defines unsigned_computations_word16 = unsigned_computations_word16.computations
+    and unsigned_results_word16 = unsigned_computations_word16.results .
+
+lemma \<open>unsigned_computations_word16 = unsigned_results_word16\<close>
+  by (simp add: unsigned_computations_word16.evaluation_simps)
+
+
+subsection \<open>Generic unsigned computations\<close>
+
+locale signed_computations =
+  fixes type :: \<open>'a::ring_bit_operations itself\<close>
+begin
+
+definition computations where
+  \<open>computations = (
+    [bit (- 805167 :: 'a) 7],
+    [- 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: 'a],
+    [- 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: 'a],
+    [- 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: 'a],
+    [NOT 473513, NOT (- 805167) :: 'a],
+    [set_bit 11 (- 805167) :: 'a],
+    [unset_bit 12 (- 805167) :: 'a],
+    [flip_bit 12 (- 805167) :: 'a],
+    [push_bit 12 (- 805167) :: 'a],
+    [take_bit 12 (- 805167) :: 'a],
+    [signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: 'a]
+  )\<close>
+
+definition results where
+  \<open>results = (
+    [True],
+    [242769, 209184, - 839103 :: 'a],
+    [- 280873, - 50197, - 280591 :: 'a],
+    [- 523642, - 259381, 558512 :: 'a],
+    [- 473514, 805166 :: 'a],
+    [- 803119 :: 'a],
+    [- 809263 :: 'a],
+    [- 809263 :: 'a],
+    [- 3297964032 :: 'a],
+    [1745 :: 'a],
+    [- 1622, - 2351 :: 'a]
+  )\<close>
+
+lemmas evaluation_simps = computations_def results_def
+
+end
+
+global_interpretation signed_computations_int: signed_computations \<open>TYPE(int)\<close>
+  defines signed_computations_int = signed_computations_int.computations
+    and signed_results_int = signed_computations_int.results .
+
+lemma \<open>signed_computations_int.computations = signed_computations_int.results\<close>
+  by (simp add: signed_computations_int.evaluation_simps)
+
+global_interpretation signed_computations_word16: signed_computations \<open>TYPE(16 word)\<close>
+  defines signed_computations_word16 = signed_computations_word16.computations
+    and signed_results_word16 = signed_computations_word16.results .
+
+lemma \<open>signed_computations_word16 = signed_results_word16\<close>
+  by (simp add: signed_computations_word16.evaluation_simps)
+
+
+subsection \<open>Special cases on particular type instances\<close>
+
+lemma
+  \<open>drop_bit 12 (- 17405 :: int) = - 5\<close>
+  by simp
+
+lemma
+  \<open>signed_drop_bit 12 (- 17405 :: 16 word) = - 5\<close>
+  by simp
+
+lemma
+  \<open>drop_bit 12 (- 17405 :: 16 word) = 11\<close>
+  by simp
+
+end