src/HOL/Rings.thy
changeset 66937 a1a4a5e2933a
parent 66816 212a3334e7da
child 67051 e7e54a0b9197
     1.1 --- a/src/HOL/Rings.thy	Mon Oct 30 13:18:41 2017 +0000
     1.2 +++ b/src/HOL/Rings.thy	Mon Oct 30 13:18:44 2017 +0000
     1.3 @@ -1738,7 +1738,10 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class linordered_semiring_1 = linordered_semiring + semiring_1
     1.8 +class zero_less_one = order + zero + one +
     1.9 +  assumes zero_less_one [simp]: "0 < 1"
    1.10 +
    1.11 +class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
    1.12  begin
    1.13  
    1.14  lemma convex_bound_le:
    1.15 @@ -1847,7 +1850,7 @@
    1.16  
    1.17  end
    1.18  
    1.19 -class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
    1.20 +class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one
    1.21  begin
    1.22  
    1.23  subclass linordered_semiring_1 ..
    1.24 @@ -2124,9 +2127,6 @@
    1.25  
    1.26  end
    1.27  
    1.28 -class zero_less_one = order + zero + one +
    1.29 -  assumes zero_less_one [simp]: "0 < 1"
    1.30 -
    1.31  class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
    1.32  begin
    1.33  
    1.34 @@ -2200,22 +2200,26 @@
    1.35  
    1.36  end
    1.37  
    1.38 -class linordered_idom =
    1.39 -  comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn +
    1.40 +class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict +
    1.41 +  ordered_ab_group_add + abs_if + sgn +
    1.42    assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    1.43  begin
    1.44  
    1.45 -subclass linordered_semiring_1_strict ..
    1.46  subclass linordered_ring_strict ..
    1.47 +
    1.48 +subclass linordered_semiring_1_strict
    1.49 +proof
    1.50 +  have "0 \<le> 1 * 1"
    1.51 +    by (fact zero_le_square)
    1.52 +  then show "0 < 1" 
    1.53 +    by (simp add: le_less)
    1.54 +qed
    1.55 +
    1.56  subclass ordered_comm_ring ..
    1.57  subclass idom ..
    1.58  
    1.59  subclass linordered_semidom
    1.60 -proof
    1.61 -  have "0 \<le> 1 * 1" by (rule zero_le_square)
    1.62 -  then show "0 < 1" by (simp add: le_less)
    1.63 -  show "b \<le> a \<Longrightarrow> a - b + b = a" for a b by simp
    1.64 -qed
    1.65 +  by standard simp
    1.66  
    1.67  subclass idom_abs_sgn
    1.68    by standard