--- 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 ***
--- 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
--- 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")
--- 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:
--- 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
--- 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
--- 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