# HG changeset patch
# User haftmann
# Date 1509369524 0
# Node ID a1a4a5e2933a76b0c585f0c2d4583e89dbb6387b
# Parent  cf8d8fc2389125e380d149af4e6830fcd7c20392
rule out pathologic instances

diff -r cf8d8fc23891 -r a1a4a5e2933a NEWS
--- 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 ***
 
diff -r cf8d8fc23891 -r a1a4a5e2933a src/HOL/Rings.thy
--- 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