--- a/NEWS Mon Oct 30 13:18:41 2017 +0000
+++ b/NEWS Mon Oct 30 13:18:44 2017 +0000
@@ -63,6 +63,9 @@
* Session HOL-Analysis: Moebius functions and the Riemann mapping
theorem.
+* Class linordered_semiring_1 covers zero_less_one also, ruling out
+pathologic instances. Minor INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Rings.thy Mon Oct 30 13:18:41 2017 +0000
+++ b/src/HOL/Rings.thy Mon Oct 30 13:18:44 2017 +0000
@@ -1738,7 +1738,10 @@
end
-class linordered_semiring_1 = linordered_semiring + semiring_1
+class zero_less_one = order + zero + one +
+ assumes zero_less_one [simp]: "0 < 1"
+
+class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
begin
lemma convex_bound_le:
@@ -1847,7 +1850,7 @@
end
-class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
+class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one
begin
subclass linordered_semiring_1 ..
@@ -2124,9 +2127,6 @@
end
-class zero_less_one = order + zero + one +
- assumes zero_less_one [simp]: "0 < 1"
-
class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
begin
@@ -2200,22 +2200,26 @@
end
-class linordered_idom =
- comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn +
+class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict +
+ ordered_ab_group_add + abs_if + sgn +
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
begin
-subclass linordered_semiring_1_strict ..
subclass linordered_ring_strict ..
+
+subclass linordered_semiring_1_strict
+proof
+ have "0 \<le> 1 * 1"
+ by (fact zero_le_square)
+ then show "0 < 1"
+ by (simp add: le_less)
+qed
+
subclass ordered_comm_ring ..
subclass idom ..
subclass linordered_semidom
-proof
- have "0 \<le> 1 * 1" by (rule zero_le_square)
- then show "0 < 1" by (simp add: le_less)
- show "b \<le> a \<Longrightarrow> a - b + b = a" for a b by simp
-qed
+ by standard simp
subclass idom_abs_sgn
by standard