# HG changeset patch
# User haftmann
# Date 1745077146 -7200
# Node ID df5b2785abd62810490bed9bd2b380029314a8ea
# Parent  e4207dfa36b55876547e5344c453114d1aa46e3c
more lemmas

diff -r e4207dfa36b5 -r df5b2785abd6 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Fri Apr 18 14:19:41 2025 +0200
+++ b/src/HOL/Bit_Operations.thy	Sat Apr 19 17:39:06 2025 +0200
@@ -778,6 +778,14 @@
     by (simp add: mask_eq_exp_minus_1)
 qed
 
+lemma mask_eq_iff_eq_exp:
+  \<open>mask n = a \<longleftrightarrow> a + 1 = 2 ^ n\<close>
+  by (auto simp flip: inc_mask_eq_exp)
+
+lemma eq_mask_iff_eq_exp:
+  \<open>a = mask n \<longleftrightarrow> a + 1 = 2 ^ n\<close>
+  by (auto simp flip: inc_mask_eq_exp)
+
 lemma mask_Suc_double:
   \<open>mask (Suc n) = 1 OR 2 * mask n\<close>
 proof -
@@ -3832,6 +3840,10 @@
   using that take_bit_int_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
   by (simp add: signed_take_bit_eq_take_bit_shift)
 
+lemma signed_take_bit_Suc_sgn_eq [simp]:
+  \<open>signed_take_bit (Suc n) (sgn k) = sgn k\<close> for k :: int
+  by (simp add: sgn_if)
+
 lemma signed_take_bit_Suc_bit0 [simp]:
   \<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
diff -r e4207dfa36b5 -r df5b2785abd6 src/HOL/Library/Type_Length.thy
--- a/src/HOL/Library/Type_Length.thy	Fri Apr 18 14:19:41 2025 +0200
+++ b/src/HOL/Library/Type_Length.thy	Sat Apr 19 17:39:06 2025 +0200
@@ -101,10 +101,22 @@
 
 end
 
+lemma length_less_eq_Suc_0_iff [simp]:
+  \<open>LENGTH('a::len) \<le> Suc 0 \<longleftrightarrow> LENGTH('a) = Suc 0\<close>
+  by (simp add: le_Suc_eq)
+
 lemma length_not_greater_eq_2_iff [simp]:
-  \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
+  \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = Suc 0\<close>
   by (auto simp add: not_le dest: less_2_cases)
 
+lemma less_eq_decr_length_iff [simp]:
+  \<open>n \<le> LENGTH('a::len) - Suc 0 \<longleftrightarrow> n < LENGTH('a)\<close>
+  by (cases \<open>LENGTH('a)\<close>) (simp_all add: less_Suc_eq le_less)
+
+lemma decr_length_less_iff [simp]:
+  \<open>LENGTH('a::len) - Suc 0 < n \<longleftrightarrow> LENGTH('a) \<le> n\<close>
+  by (cases \<open>LENGTH('a)\<close>) auto
+
 context linordered_idom
 begin
 
@@ -115,12 +127,4 @@
 
 end
 
-lemma less_eq_decr_length_iff [simp]:
-  \<open>n \<le> LENGTH('a::len) - Suc 0 \<longleftrightarrow> n < LENGTH('a)\<close>
-  by (cases \<open>LENGTH('a)\<close>) (simp_all add: less_Suc_eq le_less)
-
-lemma decr_length_less_iff [simp]:
-  \<open>LENGTH('a::len) - Suc 0 < n \<longleftrightarrow> LENGTH('a) \<le> n\<close>
-  by (cases \<open>LENGTH('a)\<close>) auto
-
 end
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>