new Ring_and_Field hierarchy, eliminating redundant axioms
authorpaulson
Mon Mar 01 13:51:21 2004 +0100 (2004-03-01)
changeset 14421ee97b6463cb4
parent 14420 4e72cd222e0b
child 14422 b8da5f258b04
new Ring_and_Field hierarchy, eliminating redundant axioms
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/Lim.ML
src/HOL/Integ/IntDef.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Complex/Complex.thy	Mon Mar 01 11:52:59 2004 +0100
     1.2 +++ b/src/HOL/Complex/Complex.thy	Mon Mar 01 13:51:21 2004 +0100
     1.3 @@ -246,13 +246,8 @@
     1.4    show "0 \<noteq> (1::complex)"
     1.5      by (simp add: complex_zero_def complex_one_def)
     1.6    show "(u + v) * w = u * w + v * w"
     1.7 -    by (simp add: complex_mult_def complex_add_def left_distrib real_diff_def add_ac)
     1.8 -  show "z+u = z+v ==> u=v"
     1.9 -    proof -
    1.10 -      assume eq: "z+u = z+v"
    1.11 -      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)
    1.12 -      thus "u = v" by (simp add: complex_add_minus_left complex_add_zero_left)
    1.13 -    qed
    1.14 +    by (simp add: complex_mult_def complex_add_def left_distrib 
    1.15 +                  diff_minus add_ac)
    1.16    assume neq: "w \<noteq> 0"
    1.17    thus "z / w = z * inverse w"
    1.18      by (simp add: complex_divide_def)
     2.1 --- a/src/HOL/Complex/NSComplex.thy	Mon Mar 01 11:52:59 2004 +0100
     2.2 +++ b/src/HOL/Complex/NSComplex.thy	Mon Mar 01 13:51:21 2004 +0100
     2.3 @@ -394,13 +394,6 @@
     2.4      by (rule hcomplex_zero_not_eq_one)
     2.5    show "(u + v) * w = u * w + v * w"
     2.6      by (simp add: hcomplex_add_mult_distrib)
     2.7 -  show "z+u = z+v ==> u=v"
     2.8 -    proof -
     2.9 -      assume eq: "z+u = z+v"
    2.10 -      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc)
    2.11 -      thus "u = v"
    2.12 -        by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left)
    2.13 -    qed
    2.14    assume neq: "w \<noteq> 0"
    2.15    thus "z / w = z * inverse w"
    2.16      by (simp add: hcomplex_divide_def)
     3.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Mon Mar 01 11:52:59 2004 +0100
     3.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Mar 01 13:51:21 2004 +0100
     3.3 @@ -477,24 +477,16 @@
     3.4    show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
     3.5    show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
     3.6    show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
     3.7 -  assume eq: "z+x = z+y" 
     3.8 -    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq hypreal_add_assoc)
     3.9 -    thus "x = y" by (simp add: hypreal_add_minus_left)
    3.10  qed
    3.11  
    3.12  
    3.13 -lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)"
    3.14 -by (simp add: hypreal_inverse hypreal_zero_def)
    3.15 -
    3.16 -lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0"
    3.17 -by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO 
    3.18 -              hypreal_mult_commute [of a])
    3.19 -
    3.20  instance hypreal :: division_by_zero
    3.21  proof
    3.22    fix x :: hypreal
    3.23 -  show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO)
    3.24 -  show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) 
    3.25 +  show inv: "inverse 0 = (0::hypreal)" 
    3.26 +    by (simp add: hypreal_inverse hypreal_zero_def)
    3.27 +  show "x/0 = 0" 
    3.28 +    by (simp add: hypreal_divide_def inv hypreal_mult_commute [of a])
    3.29  qed
    3.30  
    3.31  
    3.32 @@ -569,9 +561,6 @@
    3.33  instance hypreal :: ordered_field
    3.34  proof
    3.35    fix x y z :: hypreal
    3.36 -  show "0 < (1::hypreal)" 
    3.37 -    by (simp add: hypreal_zero_def hypreal_one_def linorder_not_le [symmetric],
    3.38 -        simp add: hypreal_le)
    3.39    show "x \<le> y ==> z + x \<le> z + y" 
    3.40      by (rule hypreal_add_left_mono)
    3.41    show "x < y ==> 0 < z ==> z * x < z * y" 
     4.1 --- a/src/HOL/Hyperreal/Lim.ML	Mon Mar 01 11:52:59 2004 +0100
     4.2 +++ b/src/HOL/Hyperreal/Lim.ML	Mon Mar 01 13:51:21 2004 +0100
     4.3 @@ -2051,7 +2051,7 @@
     4.4  Goal "f a - (f b - f a)/(b - a) * a = \
     4.5  \     f b - (f b - f a)/(b - a) * (b::real)";
     4.6  by (case_tac "a = b" 1);
     4.7 -by (asm_full_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1); 
     4.8 +by (Asm_full_simp_tac 1); 
     4.9  by (res_inst_tac [("c1","b - a")] (real_mult_left_cancel RS iffD1) 1);
    4.10  by (arith_tac 1);
    4.11  by (auto_tac (claset(), simpset() addsimps [right_diff_distrib]));
     5.1 --- a/src/HOL/Integ/IntDef.thy	Mon Mar 01 11:52:59 2004 +0100
     5.2 +++ b/src/HOL/Integ/IntDef.thy	Mon Mar 01 13:51:21 2004 +0100
     5.3 @@ -325,9 +325,6 @@
     5.4    show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
     5.5    show "0 \<noteq> (1::int)" 
     5.6      by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
     5.7 -  assume eq: "k+i = k+j" 
     5.8 -    hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc)
     5.9 -    thus "i = j" by simp
    5.10  qed
    5.11  
    5.12  
    5.13 @@ -484,7 +481,6 @@
    5.14  instance int :: ordered_ring
    5.15  proof
    5.16    fix i j k :: int
    5.17 -  show "0 < (1::int)" by (rule int_0_less_1)
    5.18    show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
    5.19    show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
    5.20    show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
     6.1 --- a/src/HOL/Real/Rational.thy	Mon Mar 01 11:52:59 2004 +0100
     6.2 +++ b/src/HOL/Real/Rational.thy	Mon Mar 01 13:51:21 2004 +0100
     6.3 @@ -516,9 +516,6 @@
     6.4         (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
     6.5    show "0 \<noteq> (1::rat)"
     6.6      by (simp add: zero_rat one_rat eq_rat) 
     6.7 -  assume eq: "s+q = s+r" 
     6.8 -    hence "(-s + s) + q = (-s + s) + r" by (simp only: eq rat_add_assoc)
     6.9 -    thus "q = r" by (simp add: rat_left_minus rat_add_0)
    6.10  qed
    6.11  
    6.12  instance rat :: linorder
    6.13 @@ -592,8 +589,6 @@
    6.14  instance rat :: ordered_field
    6.15  proof
    6.16    fix q r s :: rat
    6.17 -  show "0 < (1::rat)" 
    6.18 -    by (simp add: zero_rat one_rat less_rat) 
    6.19    show "q \<le> r ==> s + q \<le> s + r"
    6.20    proof (induct q, induct r, induct s)
    6.21      fix a b c d e f :: int
     7.1 --- a/src/HOL/Real/RealDef.thy	Mon Mar 01 11:52:59 2004 +0100
     7.2 +++ b/src/HOL/Real/RealDef.thy	Mon Mar 01 13:51:21 2004 +0100
     7.3 @@ -352,9 +352,6 @@
     7.4    show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
     7.5    show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
     7.6    show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
     7.7 -  assume eq: "z+x = z+y" 
     7.8 -    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq real_add_assoc)
     7.9 -    thus "x = y" by (simp add: real_add_minus_left)
    7.10  qed
    7.11  
    7.12  
    7.13 @@ -366,14 +363,11 @@
    7.14  apply (auto simp add: zero_neq_one)
    7.15  done
    7.16  
    7.17 -lemma DIVISION_BY_ZERO: "a / (0::real) = 0"
    7.18 -  by (simp add: real_divide_def INVERSE_ZERO)
    7.19 -
    7.20  instance real :: division_by_zero
    7.21  proof
    7.22    fix x :: real
    7.23    show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
    7.24 -  show "x/0 = 0" by (rule DIVISION_BY_ZERO) 
    7.25 +  show "x/0 = 0" by (simp add: real_divide_def INVERSE_ZERO)
    7.26  qed
    7.27  
    7.28  
    7.29 @@ -524,8 +518,6 @@
    7.30  instance real :: ordered_field
    7.31  proof
    7.32    fix x y z :: real
    7.33 -  show "0 < (1::real)"
    7.34 -    by (simp add: real_less_def real_zero_le_one real_zero_not_eq_one)  
    7.35    show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
    7.36    show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
    7.37    show "\<bar>x\<bar> = (if x < 0 then -x else x)"
     8.1 --- a/src/HOL/Ring_and_Field.thy	Mon Mar 01 11:52:59 2004 +0100
     8.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Mar 01 13:51:21 2004 +0100
     8.3 @@ -14,16 +14,11 @@
     8.4  
     8.5  subsection {* Abstract algebraic structures *}
     8.6  
     8.7 -axclass semiring \<subseteq> zero, one, plus, times
     8.8 +text{*This class underlies both @{text semiring} and @{text ring}*}
     8.9 +axclass almost_semiring \<subseteq> zero, one, plus, times
    8.10    add_assoc: "(a + b) + c = a + (b + c)"
    8.11    add_commute: "a + b = b + a"
    8.12    add_0 [simp]: "0 + a = a"
    8.13 -  add_left_imp_eq: "a + b = a + c ==> b=c"
    8.14 -    --{*This axiom is needed for semirings only: for rings, etc., it is
    8.15 -        redundant. Including it allows many more of the following results
    8.16 -        to be proved for semirings too. The drawback is that this redundant
    8.17 -        axiom must be proved for instances of rings.*}
    8.18 -
    8.19    mult_assoc: "(a * b) * c = a * (b * c)"
    8.20    mult_commute: "a * b = b * a"
    8.21    mult_1 [simp]: "1 * a = a"
    8.22 @@ -31,16 +26,35 @@
    8.23    left_distrib: "(a + b) * c = a * c + b * c"
    8.24    zero_neq_one [simp]: "0 \<noteq> 1"
    8.25  
    8.26 -axclass ring \<subseteq> semiring, minus
    8.27 +axclass semiring \<subseteq> almost_semiring
    8.28 +  add_left_imp_eq: "a + b = a + c ==> b=c"
    8.29 +    --{*This axiom is needed for semirings only: for rings, etc., it is
    8.30 +        redundant. Including it allows many more of the following results
    8.31 +        to be proved for semirings too.*}
    8.32 +
    8.33 +axclass ring \<subseteq> almost_semiring, minus
    8.34    left_minus [simp]: "- a + a = 0"
    8.35    diff_minus: "a - b = a + (-b)"
    8.36  
    8.37 -axclass ordered_semiring \<subseteq> semiring, linorder
    8.38 -  zero_less_one [simp]: "0 < 1" --{*This too is needed for semirings only.*}
    8.39 +text{*Proving axiom @{text add_left_imp_eq} makes all @{text semiring}
    8.40 +      theorems available to members of @{term ring} *}
    8.41 +instance ring \<subseteq> semiring
    8.42 +proof
    8.43 +  fix a b c :: 'a
    8.44 +  assume "a + b = a + c"
    8.45 +  hence  "-a + a + b = -a + a + c" by (simp only: add_assoc)
    8.46 +  thus "b = c" by simp
    8.47 +qed
    8.48 +
    8.49 +text{*This class underlies @{text ordered_semiring} and @{text ordered_ring}*}
    8.50 +axclass almost_ordered_semiring \<subseteq> semiring, linorder
    8.51    add_left_mono: "a \<le> b ==> c + a \<le> c + b"
    8.52    mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
    8.53  
    8.54 -axclass ordered_ring \<subseteq> ordered_semiring, ring
    8.55 +axclass ordered_semiring \<subseteq> almost_ordered_semiring
    8.56 +  zero_less_one [simp]: "0 < 1" --{*This too is needed for semirings only.*}
    8.57 +
    8.58 +axclass ordered_ring \<subseteq> almost_ordered_semiring, ring
    8.59    abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
    8.60  
    8.61  axclass field \<subseteq> ring, inverse
    8.62 @@ -56,14 +70,14 @@
    8.63  
    8.64  subsection {* Derived Rules for Addition *}
    8.65  
    8.66 -lemma add_0_right [simp]: "a + 0 = (a::'a::semiring)"
    8.67 +lemma add_0_right [simp]: "a + 0 = (a::'a::almost_semiring)"
    8.68  proof -
    8.69    have "a + 0 = 0 + a" by (simp only: add_commute)
    8.70    also have "... = a" by simp
    8.71    finally show ?thesis .
    8.72  qed
    8.73  
    8.74 -lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::semiring))"
    8.75 +lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::almost_semiring))"
    8.76    by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
    8.77  
    8.78  theorems add_ac = add_assoc add_commute add_left_commute
    8.79 @@ -153,14 +167,14 @@
    8.80  
    8.81  subsection {* Derived rules for multiplication *}
    8.82  
    8.83 -lemma mult_1_right [simp]: "a * (1::'a::semiring) = a"
    8.84 +lemma mult_1_right [simp]: "a * (1::'a::almost_semiring) = a"
    8.85  proof -
    8.86    have "a * 1 = 1 * a" by (simp add: mult_commute)
    8.87    also have "... = a" by simp
    8.88    finally show ?thesis .
    8.89  qed
    8.90  
    8.91 -lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::semiring))"
    8.92 +lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::almost_semiring))"
    8.93    by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
    8.94  
    8.95  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    8.96 @@ -178,7 +192,7 @@
    8.97  
    8.98  subsection {* Distribution rules *}
    8.99  
   8.100 -lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::semiring)"
   8.101 +lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::almost_semiring)"
   8.102  proof -
   8.103    have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
   8.104    also have "... = b * a + c * a" by (simp only: left_distrib)
   8.105 @@ -189,7 +203,8 @@
   8.106  theorems ring_distrib = right_distrib left_distrib
   8.107  
   8.108  text{*For the @{text combine_numerals} simproc*}
   8.109 -lemma combine_common_factor: "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
   8.110 +lemma combine_common_factor:
   8.111 +     "a*e + (b*e + c) = (a+b)*e + (c::'a::almost_semiring)"
   8.112  by (simp add: left_distrib add_ac)
   8.113  
   8.114  lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)"
   8.115 @@ -226,43 +241,44 @@
   8.116  
   8.117  subsection {* Ordering Rules for Addition *}
   8.118  
   8.119 -lemma add_right_mono: "a \<le> (b::'a::ordered_semiring) ==> a + c \<le> b + c"
   8.120 +lemma add_right_mono: "a \<le> (b::'a::almost_ordered_semiring) ==> a + c \<le> b + c"
   8.121  by (simp add: add_commute [of _ c] add_left_mono)
   8.122  
   8.123  text {* non-strict, in both arguments *}
   8.124 -lemma add_mono: "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::ordered_semiring)"
   8.125 +lemma add_mono:
   8.126 +     "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::almost_ordered_semiring)"
   8.127    apply (erule add_right_mono [THEN order_trans])
   8.128    apply (simp add: add_commute add_left_mono)
   8.129    done
   8.130  
   8.131  lemma add_strict_left_mono:
   8.132 -     "a < b ==> c + a < c + (b::'a::ordered_semiring)"
   8.133 +     "a < b ==> c + a < c + (b::'a::almost_ordered_semiring)"
   8.134   by (simp add: order_less_le add_left_mono) 
   8.135  
   8.136  lemma add_strict_right_mono:
   8.137 -     "a < b ==> a + c < b + (c::'a::ordered_semiring)"
   8.138 +     "a < b ==> a + c < b + (c::'a::almost_ordered_semiring)"
   8.139   by (simp add: add_commute [of _ c] add_strict_left_mono)
   8.140  
   8.141  text{*Strict monotonicity in both arguments*}
   8.142 -lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_semiring)"
   8.143 +lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::almost_ordered_semiring)"
   8.144  apply (erule add_strict_right_mono [THEN order_less_trans])
   8.145  apply (erule add_strict_left_mono)
   8.146  done
   8.147  
   8.148  lemma add_less_le_mono:
   8.149 -     "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::ordered_semiring)"
   8.150 +     "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::almost_ordered_semiring)"
   8.151  apply (erule add_strict_right_mono [THEN order_less_le_trans])
   8.152  apply (erule add_left_mono) 
   8.153  done
   8.154  
   8.155  lemma add_le_less_mono:
   8.156 -     "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::ordered_semiring)"
   8.157 +     "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::almost_ordered_semiring)"
   8.158  apply (erule add_right_mono [THEN order_le_less_trans])
   8.159  apply (erule add_strict_left_mono) 
   8.160  done
   8.161  
   8.162  lemma add_less_imp_less_left:
   8.163 -      assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_semiring)"
   8.164 +      assumes less: "c + a < c + b"  shows "a < (b::'a::almost_ordered_semiring)"
   8.165  proof (rule ccontr)
   8.166    assume "~ a < b"
   8.167    hence "b \<le> a" by (simp add: linorder_not_less)
   8.168 @@ -272,36 +288,36 @@
   8.169  qed
   8.170  
   8.171  lemma add_less_imp_less_right:
   8.172 -      "a + c < b + c ==> a < (b::'a::ordered_semiring)"
   8.173 +      "a + c < b + c ==> a < (b::'a::almost_ordered_semiring)"
   8.174  apply (rule add_less_imp_less_left [of c])
   8.175  apply (simp add: add_commute)  
   8.176  done
   8.177  
   8.178  lemma add_less_cancel_left [simp]:
   8.179 -    "(c+a < c+b) = (a < (b::'a::ordered_semiring))"
   8.180 +    "(c+a < c+b) = (a < (b::'a::almost_ordered_semiring))"
   8.181  by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   8.182  
   8.183  lemma add_less_cancel_right [simp]:
   8.184 -    "(a+c < b+c) = (a < (b::'a::ordered_semiring))"
   8.185 +    "(a+c < b+c) = (a < (b::'a::almost_ordered_semiring))"
   8.186  by (blast intro: add_less_imp_less_right add_strict_right_mono)
   8.187  
   8.188  lemma add_le_cancel_left [simp]:
   8.189 -    "(c+a \<le> c+b) = (a \<le> (b::'a::ordered_semiring))"
   8.190 +    "(c+a \<le> c+b) = (a \<le> (b::'a::almost_ordered_semiring))"
   8.191  by (simp add: linorder_not_less [symmetric]) 
   8.192  
   8.193  lemma add_le_cancel_right [simp]:
   8.194 -    "(a+c \<le> b+c) = (a \<le> (b::'a::ordered_semiring))"
   8.195 +    "(a+c \<le> b+c) = (a \<le> (b::'a::almost_ordered_semiring))"
   8.196  by (simp add: linorder_not_less [symmetric]) 
   8.197  
   8.198  lemma add_le_imp_le_left:
   8.199 -      "c + a \<le> c + b ==> a \<le> (b::'a::ordered_semiring)"
   8.200 +      "c + a \<le> c + b ==> a \<le> (b::'a::almost_ordered_semiring)"
   8.201  by simp
   8.202  
   8.203  lemma add_le_imp_le_right:
   8.204 -      "a + c \<le> b + c ==> a \<le> (b::'a::ordered_semiring)"
   8.205 +      "a + c \<le> b + c ==> a \<le> (b::'a::almost_ordered_semiring)"
   8.206  by simp
   8.207  
   8.208 -lemma add_increasing: "[|0\<le>a; b\<le>c|] ==> b \<le> a + (c::'a::ordered_semiring)"
   8.209 +lemma add_increasing: "[|0\<le>a; b\<le>c|] ==> b \<le> a + (c::'a::almost_ordered_semiring)"
   8.210  by (insert add_mono [of 0 a b c], simp)
   8.211  
   8.212  
   8.213 @@ -477,33 +493,33 @@
   8.214  subsection {* Ordering Rules for Multiplication *}
   8.215  
   8.216  lemma mult_strict_right_mono:
   8.217 -     "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_semiring)"
   8.218 +     "[|a < b; 0 < c|] ==> a * c < b * (c::'a::almost_ordered_semiring)"
   8.219  by (simp add: mult_commute [of _ c] mult_strict_left_mono)
   8.220  
   8.221  lemma mult_left_mono:
   8.222 -     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
   8.223 +     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::almost_ordered_semiring)"
   8.224    apply (case_tac "c=0", simp)
   8.225    apply (force simp add: mult_strict_left_mono order_le_less) 
   8.226    done
   8.227  
   8.228  lemma mult_right_mono:
   8.229 -     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
   8.230 +     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::almost_ordered_semiring)"
   8.231    by (simp add: mult_left_mono mult_commute [of _ c]) 
   8.232  
   8.233  lemma mult_left_le_imp_le:
   8.234 -     "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
   8.235 +     "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::almost_ordered_semiring)"
   8.236    by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
   8.237   
   8.238  lemma mult_right_le_imp_le:
   8.239 -     "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
   8.240 +     "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::almost_ordered_semiring)"
   8.241    by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
   8.242  
   8.243  lemma mult_left_less_imp_less:
   8.244 -     "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   8.245 +     "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::almost_ordered_semiring)"
   8.246    by (force simp add: mult_left_mono linorder_not_le [symmetric])
   8.247   
   8.248  lemma mult_right_less_imp_less:
   8.249 -     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   8.250 +     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::almost_ordered_semiring)"
   8.251    by (force simp add: mult_right_mono linorder_not_le [symmetric])
   8.252  
   8.253  lemma mult_strict_left_mono_neg:
   8.254 @@ -521,17 +537,17 @@
   8.255  
   8.256  subsection{* Products of Signs *}
   8.257  
   8.258 -lemma mult_pos: "[| (0::'a::ordered_semiring) < a; 0 < b |] ==> 0 < a*b"
   8.259 +lemma mult_pos: "[| (0::'a::almost_ordered_semiring) < a; 0 < b |] ==> 0 < a*b"
   8.260  by (drule mult_strict_left_mono [of 0 b], auto)
   8.261  
   8.262 -lemma mult_pos_neg: "[| (0::'a::ordered_semiring) < a; b < 0 |] ==> a*b < 0"
   8.263 +lemma mult_pos_neg: "[| (0::'a::almost_ordered_semiring) < a; b < 0 |] ==> a*b < 0"
   8.264  by (drule mult_strict_left_mono [of b 0], auto)
   8.265  
   8.266  lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b"
   8.267  by (drule mult_strict_right_mono_neg, auto)
   8.268  
   8.269  lemma zero_less_mult_pos:
   8.270 -     "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring)"
   8.271 +     "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::almost_ordered_semiring)"
   8.272  apply (case_tac "b\<le>0") 
   8.273   apply (auto simp add: order_le_less linorder_not_less)
   8.274  apply (drule_tac mult_pos_neg [of a b]) 
   8.275 @@ -574,6 +590,14 @@
   8.276  lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"
   8.277  by (simp add: zero_le_mult_iff linorder_linear) 
   8.278  
   8.279 +text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semiring}
   8.280 +      theorems available to members of @{term ordered_ring} *}
   8.281 +instance ordered_ring \<subseteq> ordered_semiring
   8.282 +proof
   8.283 +  have "(0::'a) \<le> 1*1" by (rule zero_le_square)
   8.284 +  thus "(0::'a) < 1" by (simp add: order_le_less ) 
   8.285 +qed
   8.286 +
   8.287  text{*All three types of comparision involving 0 and 1 are covered.*}
   8.288  
   8.289  declare zero_neq_one [THEN not_sym, simp]