diff -r e4207dfa36b5 -r df5b2785abd6 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Apr 18 14:19:41 2025 +0200
+++ b/src/HOL/Library/Word.thy	Sat Apr 19 17:39:06 2025 +0200
@@ -759,10 +759,8 @@
     for a :: \<open>'a::len word\<close>
 proof (cases \<open>2 \<le> LENGTH('a::len)\<close>)
   case False
-  have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
-    by auto
-  with False that show ?thesis
-    by transfer (simp add: eq_iff)
+  with that show ?thesis
+    by transfer simp
 next
   case True
   obtain n where length: \<open>LENGTH('a) = Suc n\<close>
@@ -1245,9 +1243,7 @@
 lemma signed_push_bit_eq:
   \<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\<close>
   for w :: \<open>'b::len word\<close>
-  apply (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj)
-  apply (cases n, simp_all add: min_def)
-  done
+  by (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj) auto
 
 lemma signed_take_bit_eq:
   \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
@@ -1729,6 +1725,14 @@
   \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
   by (fact signed.less_le)
 
+lemma minus_1_sless_0 [simp]:
+  \<open>- 1 <s 0\<close>
+  by transfer simp
+
+lemma minus_1_sless_eq_0 [simp]:
+  \<open>- 1 \<le>s 0\<close>
+  by transfer simp
+
 
 subsection \<open>Bit-wise operations\<close>