# HG changeset patch
# User haftmann
# Date 1743167620 -3600
# Node ID 003bef1acb2c5980da46294c17c6af31da4dacb9
# Parent  1972ae7da0d2cc751c24026c69de799da703e645
tuned

diff -r 1972ae7da0d2 -r 003bef1acb2c src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Mar 28 14:13:38 2025 +0100
+++ b/src/HOL/Library/Word.thy	Fri Mar 28 14:13:40 2025 +0100
@@ -1630,6 +1630,67 @@
 
 subsection \<open>Ordering\<close>
 
+instance word :: (len) wellorder
+proof
+  fix P :: "'a word \<Rightarrow> bool" and a
+  assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)"
+  have "wf (measure unat)" ..
+  moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat"
+    by (auto simp add: word_less_iff_unsigned [where ?'a = nat])
+  ultimately have "wf {(a, b :: ('a::len) word). a < b}"
+    by (rule wf_subset)
+  then show "P a" using *
+    by induction blast
+qed
+
+lemma word_m1_ge [simp]: (* FIXME: delete *)
+  "word_pred 0 \<ge> y"
+  by transfer (simp add: mask_eq_exp_minus_1)
+
+lemma word_less_alt:
+  "a < b \<longleftrightarrow> uint a < uint b"
+  by (fact word_less_def)
+
+lemma word_zero_le [simp]:
+  "0 \<le> y" for y :: "'a::len word"
+  by (fact word_coorder.extremum)
+
+lemma word_n1_ge [simp]:
+  "y \<le> - 1" for y :: "'a::len word"
+  by (fact word_order.extremum)
+
+lemmas word_not_simps [simp] =
+  word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
+
+lemma word_gt_0:
+  "0 < y \<longleftrightarrow> 0 \<noteq> y"
+  for y :: "'a::len word"
+  by (simp add: less_le)
+
+lemma word_gt_0_no [simp]:
+  \<open>(0 :: 'a::len word) < numeral y \<longleftrightarrow> (0 :: 'a::len word) \<noteq> numeral y\<close>
+  by (fact word_gt_0)
+
+lemma word_le_nat_alt:
+  "a \<le> b \<longleftrightarrow> unat a \<le> unat b"
+  by transfer (simp add: nat_le_eq_zle)
+
+lemma word_less_nat_alt:
+  "a < b \<longleftrightarrow> unat a < unat b"
+  by transfer (auto simp: less_le [of 0])
+
+lemmas unat_mono = word_less_nat_alt [THEN iffD1]
+
+lemma wi_less:
+  "(word_of_int n < (word_of_int m :: 'a::len word)) =
+    (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))"
+  by (simp add: uint_word_of_int word_less_def)
+
+lemma wi_le:
+  "(word_of_int n \<le> (word_of_int m :: 'a::len word)) =
+    (n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))"
+  by (simp add: uint_word_of_int word_le_def)
+
 lift_definition word_sle :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>
   is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - Suc 0) k \<le> signed_take_bit (LENGTH('a) - Suc 0) l\<close>
   by (simp flip: signed_take_bit_decr_length_iff)
@@ -1651,13 +1712,12 @@
   \<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close>
   by transfer simp
 
-lemma [code]:
-  \<open>a <s b \<longleftrightarrow> sint a < sint b\<close>
+lemma word_sless_alt [code]:
+  "a <s b \<longleftrightarrow> sint a < sint b"
   by transfer simp
 
 lemma signed_ordering: \<open>ordering word_sle word_sless\<close>
-  apply (standard; transfer)
-  using signed_take_bit_decr_length_iff by force+
+  by (standard; transfer) (auto simp flip: signed_take_bit_decr_length_iff)
 
 lemma signed_linorder: \<open>class.linorder word_sle word_sless\<close>
   by (standard; transfer) (auto simp: signed_take_bit_decr_length_iff)
@@ -1669,63 +1729,6 @@
   \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
   by (fact signed.less_le)
 
-lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b"
-  by (fact word_less_def)
-
-lemma word_zero_le [simp]: "0 \<le> y"
-  for y :: "'a::len word"
-  by (fact word_coorder.extremum)
-
-lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
-  by transfer (simp add: mask_eq_exp_minus_1)
-
-lemma word_n1_ge [simp]: "y \<le> -1"
-  for y :: "'a::len word"
-  by (fact word_order.extremum)
-
-lemmas word_not_simps [simp] =
-  word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
-
-lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y"
-  for y :: "'a::len word"
-  by (simp add: less_le)
-
-lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y
-
-lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b"
-  by transfer simp
-
-lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b"
-  by transfer (simp add: nat_le_eq_zle)
-
-lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b"
-  by transfer (auto simp: less_le [of 0])
-
-lemmas unat_mono = word_less_nat_alt [THEN iffD1]
-
-instance word :: (len) wellorder
-proof
-  fix P :: "'a word \<Rightarrow> bool" and a
-  assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)"
-  have "wf (measure unat)" ..
-  moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat"
-    by (auto simp: word_less_nat_alt)
-  ultimately have "wf {(a, b :: ('a::len) word). a < b}"
-    by (rule wf_subset)
-  then show "P a" using *
-    by induction blast
-qed
-
-lemma wi_less:
-  "(word_of_int n < (word_of_int m :: 'a::len word)) =
-    (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))"
-  by (simp add: uint_word_of_int word_less_def)
-
-lemma wi_le:
-  "(word_of_int n \<le> (word_of_int m :: 'a::len word)) =
-    (n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))"
-  by (simp add: uint_word_of_int word_le_def)
-
 
 subsection \<open>Bit-wise operations\<close>