# HG changeset patch
# User haftmann
# Date 1743159378 -3600
# Node ID 07e95760a612dd34067fe8cabdbe17384ea13b53
# Parent  7816e7be7bc7dc4e418590ca49052348d7b47511
simplified implementation of the_signed_int

diff -r 7816e7be7bc7 -r 07e95760a612 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Mar 28 08:56:13 2025 +0100
+++ b/src/HOL/Library/Word.thy	Fri Mar 28 11:56:18 2025 +0100
@@ -475,9 +475,10 @@
   by (rule; transfer) simp
 
 lemma [code]:
-  \<open>Word.the_signed_int w = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)\<close>
+  \<open>Word.the_signed_int w = (let k = Word.the_int w
+    in if bit k (LENGTH('a) - Suc 0) then k + push_bit LENGTH('a) (- 1) else k)\<close>
   for w :: \<open>'a::len word\<close>
-  by transfer (simp add: signed_take_bit_take_bit)
+  by transfer (simp add: bit_simps signed_take_bit_eq_take_bit_add)
 
 lemma [code_abbrev, simp]:
   \<open>Word.the_signed_int = sint\<close>