# HG changeset patch
# User haftmann
# Date 1749066193 0
# Node ID 97b9ac57751e8f24dd4b8d783c6f2c7781518823
# Parent  e6f299c5dec6ef3f7fa95e87359f926e62fd50f6
some more lemmas

diff -r e6f299c5dec6 -r 97b9ac57751e src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Jun 04 19:43:13 2025 +0000
+++ b/src/HOL/Library/Word.thy	Wed Jun 04 19:43:13 2025 +0000
@@ -3180,6 +3180,40 @@
   for i m :: "'a::len word"
   by uint_arith
 
+lemma less_imp_less_eq_dec:
+  \<open>v \<le> w - 1\<close> if \<open>v < w\<close> for v w :: \<open>'a::len word\<close>
+using that proof transfer
+  show \<open>take_bit LENGTH('a) k \<le> take_bit LENGTH('a) (l - 1)\<close>
+    if \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
+    for k l :: int
+    using that by (cases \<open>take_bit LENGTH('a) l = 0\<close>)
+      (auto simp add: take_bit_decr_eq)
+qed
+
+lemma inc_less_eq_triv_imp:
+  \<open>w = - 1\<close> if \<open>w + 1 \<le> w\<close> for w :: \<open>'a::len word\<close>
+proof (rule ccontr)
+  assume \<open>w \<noteq> - 1\<close>
+  with that show False
+    by transfer (auto simp add: take_bit_eq_mask_iff dest: take_bit_decr_eq)
+qed
+
+lemma less_eq_dec_triv_imp:
+  \<open>w = 0\<close> if \<open>w \<le> w - 1\<close> for w :: \<open>'a::len word\<close>
+proof (rule ccontr)
+  assume \<open>w \<noteq> 0\<close>
+  with that show False
+    by transfer (auto simp add: take_bit_eq_mask_iff dest: take_bit_decr_eq)
+qed
+
+lemma inc_less_eq_iff:
+  \<open>v + 1 \<le> w \<longleftrightarrow> v = - 1 \<or> v < w\<close> for v w :: \<open>'a::len word\<close>
+  by (auto intro: inc_less_eq_triv_imp inc_le)
+
+lemma less_eq_dec_iff:
+  \<open>v \<le> w - 1 \<longleftrightarrow> w = 0 \<or> v < w\<close> for v w :: \<open>'a::len word\<close>
+  by (auto intro: less_eq_dec_triv_imp less_imp_less_eq_dec)
+
 lemma inc_i: "1 \<le> i \<Longrightarrow> i < m \<Longrightarrow> 1 \<le> i + 1 \<and> i + 1 \<le> m"
   for i m :: "'a::len word"
   by uint_arith