explicit check for computations on word type

--- a/src/HOL/Library/Word.thy	Thu Apr 17 22:57:26 2025 +0100
+++ b/src/HOL/Library/Word.thy	Fri Apr 18 14:19:41 2025 +0200
@@ -2122,12 +2122,11 @@
 declare word_neg_numeral_alt [symmetric, code_abbrev]
 
 lemma uint_bintrunc [simp]:
-  "uint (numeral bin :: 'a word) =
-    take_bit (LENGTH('a::len)) (numeral bin)"
+  "uint (numeral bin :: 'a word) = take_bit LENGTH('a::len) (numeral bin)"
   by transfer rule
 
 lemma uint_bintrunc_neg [simp]:
-  "uint (- numeral bin :: 'a word) = take_bit (LENGTH('a::len)) (- numeral bin)"
+  "uint (- numeral bin :: 'a word) = take_bit LENGTH('a::len) (- numeral bin)"
   by transfer rule
 
 lemma sint_sbintrunc [simp]:
@@ -2139,11 +2138,11 @@
   by transfer simp
 
 lemma unat_bintrunc [simp]:
-  "unat (numeral bin :: 'a::len word) = nat (take_bit (LENGTH('a)) (numeral bin))"
+  "unat (numeral bin :: 'a::len word) = take_bit LENGTH('a) (numeral bin)"
   by transfer simp
 
 lemma unat_bintrunc_neg [simp]:
-  "unat (- numeral bin :: 'a::len word) = nat (take_bit (LENGTH('a)) (- numeral bin))"
+  "unat (- numeral bin :: 'a::len word) = nat (take_bit LENGTH('a) (- numeral bin))"
   by transfer simp
 
 lemma size_0_eq: "size w = 0 \<Longrightarrow> v = w"
@@ -4429,6 +4428,84 @@
 end
 
 
+subsection \<open>Some more naive computations rules\<close>
+
+lemma drop_bit_of_minus_1_eq [simp]:
+  \<open>drop_bit n (- 1 :: 'a::len word) = mask (LENGTH('a) - n)\<close>
+  by (rule bit_word_eqI) (auto simp add: bit_simps)
+
+context
+  includes bit_operations_syntax
+begin
+
+lemma word_cat_eq_push_bit_or:
+  \<open>word_cat v w = (push_bit LENGTH('b) (ucast v) OR ucast w :: 'c::len word)\<close>
+  for v :: \<open>'a::len word\<close> and w :: \<open>'b::len word\<close>
+  by transfer (simp add: concat_bit_def ac_simps)
+
+end
+
+context semiring_bit_operations
+begin
+
+lemma of_nat_take_bit_numeral_eq [simp]:
+  \<open>of_nat (take_bit m (numeral n)) = take_bit m (numeral n)\<close>
+  by (simp add: of_nat_take_bit)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma signed_take_bit_of_int:
+  \<open>signed_take_bit n (of_int k) = of_int (signed_take_bit n k)\<close>
+  by (rule bit_eqI) (simp add: bit_simps)
+
+lemma of_int_signed_take_bit:
+  \<open>of_int (signed_take_bit n k) = signed_take_bit n (of_int k)\<close>
+  by (simp add: signed_take_bit_of_int)
+
+lemma of_int_take_bit_minus_numeral_eq [simp]:
+  \<open>of_int (take_bit m (numeral n)) = take_bit m (numeral n)\<close>
+  \<open>of_int (take_bit m (- numeral n)) = take_bit m (- numeral n)\<close>
+  by (simp_all add: of_int_take_bit)
+
+end
+
+context
+  includes bit_operations_syntax
+begin
+
+lemma concat_bit_numeral_of_one_1 [simp]:
+  \<open>concat_bit (numeral m) 1 l = 1 OR push_bit (numeral m) l\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma concat_bit_of_one_2 [simp]:
+  \<open>concat_bit n k 1 = set_bit n (take_bit n k)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma concat_bit_numeral_of_minus_one_1 [simp]:
+  \<open>concat_bit (numeral m) (- 1) l = push_bit (numeral m) l OR mask (numeral m)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma concat_bit_numeral_of_minus_one_2 [simp]:
+  \<open>concat_bit (numeral m) k (- 1) = take_bit (numeral m) k OR NOT (mask (numeral m))\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma concat_bit_numeral [simp]:
+  \<open>concat_bit (numeral m) (numeral n) (numeral q) = take_bit (numeral m) (numeral n) OR push_bit (numeral m) (numeral q)\<close>
+  \<open>concat_bit (numeral m) (- numeral n) (numeral q) = take_bit (numeral m) (- numeral n) OR push_bit (numeral m) (numeral q)\<close>
+  \<open>concat_bit (numeral m) (numeral n) (- numeral q) = take_bit (numeral m) (numeral n) OR push_bit (numeral m) (- numeral q)\<close>
+  \<open>concat_bit (numeral m) (- numeral n) (- numeral q) = take_bit (numeral m) (- numeral n) OR push_bit (numeral m) (- numeral q)\<close>
+  by (fact concat_bit_def)+
+
+end
+
+lemma word_cat_0_left [simp]:
+  \<open>word_cat 0 w = ucast w\<close>
+  by (simp add: word_cat_eq)
+
+
 subsection \<open>Tool support\<close>
 
 ML_file \<open>Tools/smt_word.ML\<close>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Word_Computations.thy	Fri Apr 18 14:19:41 2025 +0200
@@ -0,0 +1,76 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Tests for simplifying word operations on ground terms\<close>
+
+theory Word_Computations
+  imports
+    "HOL.Bit_Operations"
+    "HOL-Library.Word"
+begin
+
+unbundle bit_operations_syntax
+
+named_theorems eval
+
+declare mask_numeral [eval]
+
+type_synonym word16 = \<open>16 word\<close>
+type_synonym word32 = \<open>32 word\<close>
+
+definition computations_arith where
+  [eval]: \<open>computations_arith = (
+    [473514 + - 763, - 5324 - 7892 :: word16],
+    [3131 * - 42, - 2342 div 1213, 2152 mod - 235 :: word16],
+    [12323 \<le> (- 12132 :: word16), - 123 < (321312 :: word16), 12323 \<le>s (- 12132 :: word16), - 123 <s (321312 :: word16)]
+  )\<close>
+
+definition results_arith where
+  [eval]: \<open>results_arith = (
+    [472751, - 13216 :: word16],
+    [- 131502, 52, 2152 :: word16],
+    [True, False, False, False]
+  )\<close>
+
+lemma \<open>computations_arith = results_arith\<close>
+  by (simp add: eval)
+ 
+definition computations_bit where
+  [eval]: \<open>computations_bit = (
+    [bit (473514 :: word16) 5, bit (- 805167 :: word16) 7],
+    [NOT 473513, NOT (- 805167) :: word16],
+    [473514 AND 767063, - 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: word16],
+    [473514 OR 767063, - 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: word16],
+    [473514 XOR 767063, - 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: word16],
+    mask 11 :: word16,
+    [set_bit 15 473514, set_bit 11 (- 805167)  :: word16],
+    [unset_bit 13 473514, unset_bit 12 (- 805167) :: word16],
+    [flip_bit 15 473514, flip_bit 12 (- 805167) :: word16],
+    [push_bit 12 473514, push_bit 12 (- 805167) :: word16],
+    [drop_bit 12 65344, drop_bit 12 (- 17405) :: word16],
+    [signed_drop_bit 12 (- 17405) :: word16],
+    [take_bit 12 473514, take_bit 12 (- 805167) :: word16],
+    [signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: word16]
+  )\<close>
+
+definition results_bit where
+  [eval]: \<open>results_bit = (
+    [True, True],
+    [- 473514, 805166 :: word16],
+    [208898, 242769, 209184, - 839103 :: word16],
+    [1031679, - 280873, - 50197, - 280591 :: word16],
+    [822781, - 523642, - 259381, 558512 :: word16],
+    2047 :: word16,
+    [506282, - 803119 :: word16],
+    [465322, - 809263 :: word16],
+    [506282, - 809263 :: word16],
+    [1939513344, - 3297964032 :: word16],
+    [15, 11 :: word16],
+    [- 5 :: word16],
+    [2474, 1745 :: word16],
+    [- 1622, - 2351 :: word16]
+  )\<close>
+
+lemma \<open>computations_bit = results_bit\<close>
+  by (simp add: eval)
+
+end