# HG changeset patch
# User haftmann
# Date 1699542711 0
# Node ID 5e788ff7a48980a0b2ed6499ad102249e2d43ed2
# Parent  5553a86a1091f5f7418cf549cd1362abff1202f7
explicit type class for discrete linordered semidoms

diff -r 5553a86a1091 -r 5e788ff7a489 NEWS
--- a/NEWS	Thu Nov 09 19:06:50 2023 +0100
+++ b/NEWS	Thu Nov 09 15:11:51 2023 +0000
@@ -15,6 +15,9 @@
   by Sledgehammer and should be used instead. For more information, see
   Sledgehammer's documentation relating to "preplay_timeout". INCOMPATIBILITY.
 
+* Explicit type class for discrete_linear_ordered_semidom for integral
+  semidomains with a discrete linear order.
+
 
 *** ML ***
 
diff -r 5553a86a1091 -r 5e788ff7a489 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Nov 09 19:06:50 2023 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Nov 09 15:11:51 2023 +0000
@@ -178,46 +178,59 @@
   "integer_of_num (Num.Bit0 Num.One) = 2"
   by simp_all
 
-instantiation integer :: "{linordered_idom, equal}"
+instantiation integer :: equal
 begin
 
-lift_definition abs_integer :: "integer \<Rightarrow> integer"
-  is "abs :: int \<Rightarrow> int"
+lift_definition equal_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> bool\<close>
+  is \<open>HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool\<close>
+  .
+
+instance
+  by (standard; transfer) (fact equal_eq)
+
+end
+
+instantiation integer :: linordered_idom
+begin
+
+lift_definition abs_integer :: \<open>integer \<Rightarrow> integer\<close>
+  is \<open>abs :: int \<Rightarrow> int\<close>
   .
 
 declare abs_integer.rep_eq [simp]
 
-lift_definition sgn_integer :: "integer \<Rightarrow> integer"
-  is "sgn :: int \<Rightarrow> int"
+lift_definition sgn_integer :: \<open>integer \<Rightarrow> integer\<close>
+  is \<open>sgn :: int \<Rightarrow> int\<close>
   .
 
 declare sgn_integer.rep_eq [simp]
 
-lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
-  is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
+lift_definition less_eq_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> bool\<close>
+  is \<open>less_eq :: int \<Rightarrow> int \<Rightarrow> bool\<close>
   .
 
 lemma integer_less_eq_iff:
-  "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
+  \<open>k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l\<close>
   by (fact less_eq_integer.rep_eq)
 
-lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
-  is "less :: int \<Rightarrow> int \<Rightarrow> bool"
+lift_definition less_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> bool\<close>
+  is \<open>less :: int \<Rightarrow> int \<Rightarrow> bool\<close>
   .
 
 lemma integer_less_iff:
-  "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
+  \<open>k < l \<longleftrightarrow> int_of_integer k < int_of_integer l\<close>
   by (fact less_integer.rep_eq)
 
-lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
-  is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
-  .
-
 instance
-  by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
+  by (standard; transfer)
+    (simp_all add: algebra_simps less_le_not_le [symmetric] mult_strict_right_mono linear)
 
 end
 
+instance integer :: discrete_linordered_semidom
+  by (standard; transfer)
+    (fact less_iff_succ_less_eq)
+
 context
   includes lifting_syntax
 begin
@@ -1051,7 +1064,7 @@
   "division_segment (n::natural) = 1"
   by (simp add: natural_eq_iff)
 
-instance natural :: linordered_semidom
+instance natural :: discrete_linordered_semidom
   by (standard; transfer) simp_all
 
 instance natural :: unique_euclidean_semiring_with_nat
diff -r 5553a86a1091 -r 5e788ff7a489 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Nov 09 19:06:50 2023 +0100
+++ b/src/HOL/Divides.thy	Thu Nov 09 15:11:51 2023 +0000
@@ -7,7 +7,7 @@
 imports Parity
 begin
 
-class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + linordered_semidom +
+class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + discrete_linordered_semidom +
   assumes div_less [no_atp]: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
     and mod_less [no_atp]: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
     and div_positive [no_atp]: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
@@ -16,9 +16,8 @@
     and pos_mod_sign [no_atp]: "0 < b \<Longrightarrow> 0 \<le> a mod b"
     and mod_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
     and div_mult2_eq [no_atp]: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
-  assumes discrete [no_atp]: "a < b \<longleftrightarrow> a + 1 \<le> b"
 
-hide_fact (open) div_less mod_less div_positive mod_less_eq_dividend pos_mod_bound pos_mod_sign mod_mult2_eq div_mult2_eq discrete
+hide_fact (open) div_less mod_less div_positive mod_less_eq_dividend pos_mod_bound pos_mod_sign mod_mult2_eq div_mult2_eq
 
 context unique_euclidean_semiring_numeral
 begin
@@ -26,6 +25,10 @@
 context
 begin
 
+qualified lemma discrete [no_atp]:
+  "a < b \<longleftrightarrow> a + 1 \<le> b"
+  by (fact less_iff_succ_less_eq)
+
 qualified lemma divmod_digit_1 [no_atp]:
   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
diff -r 5553a86a1091 -r 5e788ff7a489 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Thu Nov 09 19:06:50 2023 +0100
+++ b/src/HOL/Groups_List.thy	Thu Nov 09 15:11:51 2023 +0000
@@ -421,7 +421,7 @@
 
 end
 
-context unique_euclidean_semiring_numeral
+context discrete_linordered_semidom
 begin
 
 lemma horner_sum_bound:
@@ -435,11 +435,16 @@
   moreover define a where \<open>a = 2 ^ length bs - horner_sum of_bool 2 bs\<close>
   ultimately have *: \<open>2 ^ length bs = horner_sum of_bool 2 bs + a\<close>
     by simp
-  have \<open>1 < a * 2\<close> if \<open>0 < a\<close>
-    using that add_mono [of 1 a 1 a]
-    by (simp add: mult_2_right discrete)
+  have \<open>0 < a\<close>
+    using Cons * by simp
+  moreover have \<open>1 \<le> a\<close>
+    using \<open>0 < a\<close> by (simp add: less_eq_iff_succ_less)
+  ultimately have \<open>0 + 1 < a + a\<close>
+    by (rule add_less_le_mono)
+  then have \<open>1 < a * 2\<close>
+    by (simp add: mult_2_right)
   with Cons show ?case
-    by (simp add: algebra_simps *)
+    by (simp add: * algebra_simps)
 qed
 
 end
@@ -448,7 +453,7 @@
   \<open>nat (horner_sum of_bool 2 bs) = horner_sum of_bool 2 bs\<close>
   by (induction bs) (auto simp add: nat_add_distrib horner_sum_nonnegative)
 
-context unique_euclidean_semiring_numeral
+context discrete_linordered_semidom
 begin
 
 lemma horner_sum_less_eq_iff_lexordp_eq:
diff -r 5553a86a1091 -r 5e788ff7a489 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Nov 09 19:06:50 2023 +0100
+++ b/src/HOL/Int.thy	Thu Nov 09 15:11:51 2023 +0000
@@ -181,6 +181,31 @@
 
 end
 
+instance int :: discrete_linordered_semidom
+proof
+  fix k l :: int
+  show \<open>k < l \<longleftrightarrow> k + 1 \<le> l\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  proof
+    assume ?Q
+    then show ?P
+      by simp
+  next
+    assume ?P
+    then have \<open>l - k > 0\<close>
+      by simp
+    with zero_less_imp_eq_int obtain n where \<open>l - k = int n\<close>
+      by blast
+    then have \<open>n > 0\<close>
+      using \<open>l - k > 0\<close> by simp
+    then have \<open>n \<ge> 1\<close>
+      by simp
+    then have \<open>int n \<ge> int 1\<close>
+      by (rule of_nat_mono)
+    with \<open>l - k = int n\<close> show ?Q
+      by simp
+  qed
+qed
+
 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + 1 \<le> z"
   for w z :: int
   by transfer clarsimp
diff -r 5553a86a1091 -r 5e788ff7a489 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Nov 09 19:06:50 2023 +0100
+++ b/src/HOL/Nat.thy	Thu Nov 09 15:11:51 2023 +0000
@@ -846,19 +846,21 @@
 
 text \<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>.\<close>
 
-instance nat :: linordered_semidom
+instance nat :: discrete_linordered_semidom
 proof
   fix m n q :: nat
-  show "0 < (1::nat)"
+  show \<open>0 < (1::nat)\<close>
     by simp
-  show "m \<le> n \<Longrightarrow> q + m \<le> q + n"
+  show \<open>m \<le> n \<Longrightarrow> q + m \<le> q + n\<close>
     by simp
-  show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n"
+  show \<open>m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n\<close>
     by (simp add: mult_less_mono2)
-  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0"
+  show \<open>m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0\<close>
     by simp
-  show "n \<le> m \<Longrightarrow> (m - n) + n = m"
+  show \<open>n \<le> m \<Longrightarrow> (m - n) + n = m\<close>
     by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
+  show \<open>m < n \<longleftrightarrow> m + 1 \<le> n\<close>
+    by (simp add: Suc_le_eq)
 qed
 
 instance nat :: dioid
diff -r 5553a86a1091 -r 5e788ff7a489 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Nov 09 19:06:50 2023 +0100
+++ b/src/HOL/Rings.thy	Thu Nov 09 15:11:51 2023 +0000
@@ -2679,6 +2679,16 @@
 
 end
 
+class discrete_linordered_semidom = linordered_semidom +
+  assumes less_iff_succ_less_eq: \<open>a < b \<longleftrightarrow> a + 1 \<le> b\<close>
+begin
+
+lemma less_eq_iff_succ_less:
+  \<open>a \<le> b \<longleftrightarrow> a < b + 1\<close>
+  using less_iff_succ_less_eq [of a \<open>b + 1\<close>] by simp
+
+end
+
 text \<open>Reasoning about inequalities with division\<close>
 
 context linordered_semidom