more lemmas and instances

--- a/src/HOL/Bit_Operations.thy	Sun Oct 19 11:36:36 2025 +0900
+++ b/src/HOL/Bit_Operations.thy	Sat Oct 18 18:43:09 2025 +0200
@@ -2405,6 +2405,10 @@
   by (auto simp: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
     intro: order_trans [of 0 \<open>2 ^ n\<close> k])
 
+lemma take_bit_int_less_eq_mask:
+  \<open>take_bit n k \<le> mask n\<close> for k :: int
+  using take_bit_int_less_exp [of n k] by (simp add: mask_eq_exp_minus_1)
+
 lemma take_bit_int_greater_self_iff:
   \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close> for k :: int
   using take_bit_int_less_eq_self_iff [of n k] by auto
@@ -2748,6 +2752,11 @@
     by simp
 qed
 
+lemma take_bit_nat_less_eq_mask:
+  \<open>take_bit n m \<le> mask n\<close> for m :: nat
+  using take_bit_nat_less_exp [of n m]
+  by (simp flip: Suc_mask_eq_exp)
+
 lemma take_bit_tightened_less_eq_nat:
   \<open>take_bit m q \<le> take_bit n q\<close> if \<open>m \<le> n\<close> for q :: nat
 proof -

--- a/src/HOL/Library/Word.thy	Sun Oct 19 11:36:36 2025 +0900
+++ b/src/HOL/Library/Word.thy	Sat Oct 18 18:43:09 2025 +0200
@@ -600,6 +600,35 @@
   \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
   by transfer rule
 
+instantiation word :: (len) order_bot
+begin
+
+lift_definition bot_word :: \<open>'a word\<close>
+  is 0 .
+
+instance
+  by (standard; transfer) simp
+
+end
+
+lemma bot_word_eq:
+  \<open>bot = (0 :: 'a::len word)\<close>
+  by transfer rule
+
+instantiation word :: (len) order_top
+begin
+
+lift_definition top_word :: \<open>'a word\<close>
+  is \<open>- 1\<close> .
+
+instance
+  by (standard; transfer) (simp add: take_bit_int_less_eq_mask)
+
+end
+
+lemma top_word_eq:
+  \<open>top = (- 1 :: 'a::len word)\<close>
+  by transfer rule
 
 
 subsection \<open>Enumeration\<close>
@@ -3218,6 +3247,22 @@
   for i m :: "'a::len word"
   by uint_arith
 
+lemma dec_less_imp_less_eq:
+  \<open>v \<le> w\<close> if \<open>v - 1 < w\<close> for v w :: \<open>'a::len word\<close>
+  using that inc_le [of \<open>v - 1\<close> w] by simp
+
+lemma less_inc_imp_less_eq:
+  \<open>v \<le> w\<close> if \<open>v < w + 1\<close> for v w :: \<open>'a::len word\<close>
+  using that less_imp_less_eq_dec [of v \<open>w + 1\<close>] by simp
+
+lemma less_eq_dec_self_iff_eq:
+  \<open>w \<le> w - 1 \<longleftrightarrow> w = 0\<close> for w :: \<open>'a::len word\<close>
+  using less_eq_dec_iff [of w w] by simp
+
+lemma inc_less_eq_self_iff_eq:
+  \<open>w + 1 \<le> w \<longleftrightarrow> w = - 1\<close> for w :: \<open>'a::len word\<close>
+  using inc_less_eq_triv_imp [of w] by auto
+
 lemma udvd_incr_lem:
   "\<lbrakk>up < uq; up = ua + n * uint K; uq = ua + n' * uint K\<rbrakk>
     \<Longrightarrow> up + uint K \<le> uq"