rule out pathologic instances
authorhaftmann
Mon Oct 30 13:18:44 2017 +0000 (19 months ago)
changeset 66937a1a4a5e2933a
parent 66936 cf8d8fc23891
child 66938 c78ff0aeba4c
rule out pathologic instances
NEWS
src/HOL/Rings.thy
     1.1 --- a/NEWS	Mon Oct 30 13:18:41 2017 +0000
     1.2 +++ b/NEWS	Mon Oct 30 13:18:44 2017 +0000
     1.3 @@ -63,6 +63,9 @@
     1.4  * Session HOL-Analysis: Moebius functions and the Riemann mapping
     1.5  theorem.
     1.6  
     1.7 +* Class linordered_semiring_1 covers zero_less_one also, ruling out
     1.8 +pathologic instances. Minor INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/HOL/Rings.thy	Mon Oct 30 13:18:41 2017 +0000
     2.2 +++ b/src/HOL/Rings.thy	Mon Oct 30 13:18:44 2017 +0000
     2.3 @@ -1738,7 +1738,10 @@
     2.4  
     2.5  end
     2.6  
     2.7 -class linordered_semiring_1 = linordered_semiring + semiring_1
     2.8 +class zero_less_one = order + zero + one +
     2.9 +  assumes zero_less_one [simp]: "0 < 1"
    2.10 +
    2.11 +class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
    2.12  begin
    2.13  
    2.14  lemma convex_bound_le:
    2.15 @@ -1847,7 +1850,7 @@
    2.16  
    2.17  end
    2.18  
    2.19 -class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
    2.20 +class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one
    2.21  begin
    2.22  
    2.23  subclass linordered_semiring_1 ..
    2.24 @@ -2124,9 +2127,6 @@
    2.25  
    2.26  end
    2.27  
    2.28 -class zero_less_one = order + zero + one +
    2.29 -  assumes zero_less_one [simp]: "0 < 1"
    2.30 -
    2.31  class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
    2.32  begin
    2.33  
    2.34 @@ -2200,22 +2200,26 @@
    2.35  
    2.36  end
    2.37  
    2.38 -class linordered_idom =
    2.39 -  comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn +
    2.40 +class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict +
    2.41 +  ordered_ab_group_add + abs_if + sgn +
    2.42    assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    2.43  begin
    2.44  
    2.45 -subclass linordered_semiring_1_strict ..
    2.46  subclass linordered_ring_strict ..
    2.47 +
    2.48 +subclass linordered_semiring_1_strict
    2.49 +proof
    2.50 +  have "0 \<le> 1 * 1"
    2.51 +    by (fact zero_le_square)
    2.52 +  then show "0 < 1" 
    2.53 +    by (simp add: le_less)
    2.54 +qed
    2.55 +
    2.56  subclass ordered_comm_ring ..
    2.57  subclass idom ..
    2.58  
    2.59  subclass linordered_semidom
    2.60 -proof
    2.61 -  have "0 \<le> 1 * 1" by (rule zero_le_square)
    2.62 -  then show "0 < 1" by (simp add: le_less)
    2.63 -  show "b \<le> a \<Longrightarrow> a - b + b = a" for a b by simp
    2.64 -qed
    2.65 +  by standard simp
    2.66  
    2.67  subclass idom_abs_sgn
    2.68    by standard