# HG changeset patch
# User paulson
# Date 1078145481 -3600
# Node ID ee97b6463cb4d772768f43f8c91287b8a2622d2b
# Parent  4e72cd222e0b42ea79baf44f57e5f1b85bcbd004
new Ring_and_Field hierarchy, eliminating redundant axioms

diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Complex/Complex.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -246,13 +246,8 @@
   show "0 \<noteq> (1::complex)"
     by (simp add: complex_zero_def complex_one_def)
   show "(u + v) * w = u * w + v * w"
-    by (simp add: complex_mult_def complex_add_def left_distrib real_diff_def add_ac)
-  show "z+u = z+v ==> u=v"
-    proof -
-      assume eq: "z+u = z+v"
-      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)
-      thus "u = v" by (simp add: complex_add_minus_left complex_add_zero_left)
-    qed
+    by (simp add: complex_mult_def complex_add_def left_distrib 
+                  diff_minus add_ac)
   assume neq: "w \<noteq> 0"
   thus "z / w = z * inverse w"
     by (simp add: complex_divide_def)
diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -394,13 +394,6 @@
     by (rule hcomplex_zero_not_eq_one)
   show "(u + v) * w = u * w + v * w"
     by (simp add: hcomplex_add_mult_distrib)
-  show "z+u = z+v ==> u=v"
-    proof -
-      assume eq: "z+u = z+v"
-      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc)
-      thus "u = v"
-        by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left)
-    qed
   assume neq: "w \<noteq> 0"
   thus "z / w = z * inverse w"
     by (simp add: hcomplex_divide_def)
diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -477,24 +477,16 @@
   show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
   show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
   show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
-  assume eq: "z+x = z+y" 
-    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq hypreal_add_assoc)
-    thus "x = y" by (simp add: hypreal_add_minus_left)
 qed
 
 
-lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)"
-by (simp add: hypreal_inverse hypreal_zero_def)
-
-lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0"
-by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO 
-              hypreal_mult_commute [of a])
-
 instance hypreal :: division_by_zero
 proof
   fix x :: hypreal
-  show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO)
-  show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) 
+  show inv: "inverse 0 = (0::hypreal)" 
+    by (simp add: hypreal_inverse hypreal_zero_def)
+  show "x/0 = 0" 
+    by (simp add: hypreal_divide_def inv hypreal_mult_commute [of a])
 qed
 
 
@@ -569,9 +561,6 @@
 instance hypreal :: ordered_field
 proof
   fix x y z :: hypreal
-  show "0 < (1::hypreal)" 
-    by (simp add: hypreal_zero_def hypreal_one_def linorder_not_le [symmetric],
-        simp add: hypreal_le)
   show "x \<le> y ==> z + x \<le> z + y" 
     by (rule hypreal_add_left_mono)
   show "x < y ==> 0 < z ==> z * x < z * y" 
diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Hyperreal/Lim.ML
--- a/src/HOL/Hyperreal/Lim.ML	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Hyperreal/Lim.ML	Mon Mar 01 13:51:21 2004 +0100
@@ -2051,7 +2051,7 @@
 Goal "f a - (f b - f a)/(b - a) * a = \
 \     f b - (f b - f a)/(b - a) * (b::real)";
 by (case_tac "a = b" 1);
-by (asm_full_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1); 
+by (Asm_full_simp_tac 1); 
 by (res_inst_tac [("c1","b - a")] (real_mult_left_cancel RS iffD1) 1);
 by (arith_tac 1);
 by (auto_tac (claset(), simpset() addsimps [right_diff_distrib]));
diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -325,9 +325,6 @@
   show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
   show "0 \<noteq> (1::int)" 
     by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
-  assume eq: "k+i = k+j" 
-    hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc)
-    thus "i = j" by simp
 qed
 
 
@@ -484,7 +481,6 @@
 instance int :: ordered_ring
 proof
   fix i j k :: int
-  show "0 < (1::int)" by (rule int_0_less_1)
   show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
   show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Real/Rational.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -516,9 +516,6 @@
        (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
   show "0 \<noteq> (1::rat)"
     by (simp add: zero_rat one_rat eq_rat) 
-  assume eq: "s+q = s+r" 
-    hence "(-s + s) + q = (-s + s) + r" by (simp only: eq rat_add_assoc)
-    thus "q = r" by (simp add: rat_left_minus rat_add_0)
 qed
 
 instance rat :: linorder
@@ -592,8 +589,6 @@
 instance rat :: ordered_field
 proof
   fix q r s :: rat
-  show "0 < (1::rat)" 
-    by (simp add: zero_rat one_rat less_rat) 
   show "q \<le> r ==> s + q \<le> s + r"
   proof (induct q, induct r, induct s)
     fix a b c d e f :: int
diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -352,9 +352,6 @@
   show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
   show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
   show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
-  assume eq: "z+x = z+y" 
-    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq real_add_assoc)
-    thus "x = y" by (simp add: real_add_minus_left)
 qed
 
 
@@ -366,14 +363,11 @@
 apply (auto simp add: zero_neq_one)
 done
 
-lemma DIVISION_BY_ZERO: "a / (0::real) = 0"
-  by (simp add: real_divide_def INVERSE_ZERO)
-
 instance real :: division_by_zero
 proof
   fix x :: real
   show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
-  show "x/0 = 0" by (rule DIVISION_BY_ZERO) 
+  show "x/0 = 0" by (simp add: real_divide_def INVERSE_ZERO)
 qed
 
 
@@ -524,8 +518,6 @@
 instance real :: ordered_field
 proof
   fix x y z :: real
-  show "0 < (1::real)"
-    by (simp add: real_less_def real_zero_le_one real_zero_not_eq_one)  
   show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
   show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
   show "\<bar>x\<bar> = (if x < 0 then -x else x)"
diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -14,16 +14,11 @@
 
 subsection {* Abstract algebraic structures *}
 
-axclass semiring \<subseteq> zero, one, plus, times
+text{*This class underlies both @{text semiring} and @{text ring}*}
+axclass almost_semiring \<subseteq> zero, one, plus, times
   add_assoc: "(a + b) + c = a + (b + c)"
   add_commute: "a + b = b + a"
   add_0 [simp]: "0 + a = a"
-  add_left_imp_eq: "a + b = a + c ==> b=c"
-    --{*This axiom is needed for semirings only: for rings, etc., it is
-        redundant. Including it allows many more of the following results
-        to be proved for semirings too. The drawback is that this redundant
-        axiom must be proved for instances of rings.*}
-
   mult_assoc: "(a * b) * c = a * (b * c)"
   mult_commute: "a * b = b * a"
   mult_1 [simp]: "1 * a = a"
@@ -31,16 +26,35 @@
   left_distrib: "(a + b) * c = a * c + b * c"
   zero_neq_one [simp]: "0 \<noteq> 1"
 
-axclass ring \<subseteq> semiring, minus
+axclass semiring \<subseteq> almost_semiring
+  add_left_imp_eq: "a + b = a + c ==> b=c"
+    --{*This axiom is needed for semirings only: for rings, etc., it is
+        redundant. Including it allows many more of the following results
+        to be proved for semirings too.*}
+
+axclass ring \<subseteq> almost_semiring, minus
   left_minus [simp]: "- a + a = 0"
   diff_minus: "a - b = a + (-b)"
 
-axclass ordered_semiring \<subseteq> semiring, linorder
-  zero_less_one [simp]: "0 < 1" --{*This too is needed for semirings only.*}
+text{*Proving axiom @{text add_left_imp_eq} makes all @{text semiring}
+      theorems available to members of @{term ring} *}
+instance ring \<subseteq> semiring
+proof
+  fix a b c :: 'a
+  assume "a + b = a + c"
+  hence  "-a + a + b = -a + a + c" by (simp only: add_assoc)
+  thus "b = c" by simp
+qed
+
+text{*This class underlies @{text ordered_semiring} and @{text ordered_ring}*}
+axclass almost_ordered_semiring \<subseteq> semiring, linorder
   add_left_mono: "a \<le> b ==> c + a \<le> c + b"
   mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
 
-axclass ordered_ring \<subseteq> ordered_semiring, ring
+axclass ordered_semiring \<subseteq> almost_ordered_semiring
+  zero_less_one [simp]: "0 < 1" --{*This too is needed for semirings only.*}
+
+axclass ordered_ring \<subseteq> almost_ordered_semiring, ring
   abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
 
 axclass field \<subseteq> ring, inverse
@@ -56,14 +70,14 @@
 
 subsection {* Derived Rules for Addition *}
 
-lemma add_0_right [simp]: "a + 0 = (a::'a::semiring)"
+lemma add_0_right [simp]: "a + 0 = (a::'a::almost_semiring)"
 proof -
   have "a + 0 = 0 + a" by (simp only: add_commute)
   also have "... = a" by simp
   finally show ?thesis .
 qed
 
-lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::semiring))"
+lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::almost_semiring))"
   by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
 
 theorems add_ac = add_assoc add_commute add_left_commute
@@ -153,14 +167,14 @@
 
 subsection {* Derived rules for multiplication *}
 
-lemma mult_1_right [simp]: "a * (1::'a::semiring) = a"
+lemma mult_1_right [simp]: "a * (1::'a::almost_semiring) = a"
 proof -
   have "a * 1 = 1 * a" by (simp add: mult_commute)
   also have "... = a" by simp
   finally show ?thesis .
 qed
 
-lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::semiring))"
+lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::almost_semiring))"
   by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
@@ -178,7 +192,7 @@
 
 subsection {* Distribution rules *}
 
-lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::semiring)"
+lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::almost_semiring)"
 proof -
   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
   also have "... = b * a + c * a" by (simp only: left_distrib)
@@ -189,7 +203,8 @@
 theorems ring_distrib = right_distrib left_distrib
 
 text{*For the @{text combine_numerals} simproc*}
-lemma combine_common_factor: "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
+lemma combine_common_factor:
+     "a*e + (b*e + c) = (a+b)*e + (c::'a::almost_semiring)"
 by (simp add: left_distrib add_ac)
 
 lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)"
@@ -226,43 +241,44 @@
 
 subsection {* Ordering Rules for Addition *}
 
-lemma add_right_mono: "a \<le> (b::'a::ordered_semiring) ==> a + c \<le> b + c"
+lemma add_right_mono: "a \<le> (b::'a::almost_ordered_semiring) ==> a + c \<le> b + c"
 by (simp add: add_commute [of _ c] add_left_mono)
 
 text {* non-strict, in both arguments *}
-lemma add_mono: "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::ordered_semiring)"
+lemma add_mono:
+     "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::almost_ordered_semiring)"
   apply (erule add_right_mono [THEN order_trans])
   apply (simp add: add_commute add_left_mono)
   done
 
 lemma add_strict_left_mono:
-     "a < b ==> c + a < c + (b::'a::ordered_semiring)"
+     "a < b ==> c + a < c + (b::'a::almost_ordered_semiring)"
  by (simp add: order_less_le add_left_mono) 
 
 lemma add_strict_right_mono:
-     "a < b ==> a + c < b + (c::'a::ordered_semiring)"
+     "a < b ==> a + c < b + (c::'a::almost_ordered_semiring)"
  by (simp add: add_commute [of _ c] add_strict_left_mono)
 
 text{*Strict monotonicity in both arguments*}
-lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_semiring)"
+lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::almost_ordered_semiring)"
 apply (erule add_strict_right_mono [THEN order_less_trans])
 apply (erule add_strict_left_mono)
 done
 
 lemma add_less_le_mono:
-     "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::ordered_semiring)"
+     "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::almost_ordered_semiring)"
 apply (erule add_strict_right_mono [THEN order_less_le_trans])
 apply (erule add_left_mono) 
 done
 
 lemma add_le_less_mono:
-     "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::ordered_semiring)"
+     "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::almost_ordered_semiring)"
 apply (erule add_right_mono [THEN order_le_less_trans])
 apply (erule add_strict_left_mono) 
 done
 
 lemma add_less_imp_less_left:
-      assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_semiring)"
+      assumes less: "c + a < c + b"  shows "a < (b::'a::almost_ordered_semiring)"
 proof (rule ccontr)
   assume "~ a < b"
   hence "b \<le> a" by (simp add: linorder_not_less)
@@ -272,36 +288,36 @@
 qed
 
 lemma add_less_imp_less_right:
-      "a + c < b + c ==> a < (b::'a::ordered_semiring)"
+      "a + c < b + c ==> a < (b::'a::almost_ordered_semiring)"
 apply (rule add_less_imp_less_left [of c])
 apply (simp add: add_commute)  
 done
 
 lemma add_less_cancel_left [simp]:
-    "(c+a < c+b) = (a < (b::'a::ordered_semiring))"
+    "(c+a < c+b) = (a < (b::'a::almost_ordered_semiring))"
 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
 
 lemma add_less_cancel_right [simp]:
-    "(a+c < b+c) = (a < (b::'a::ordered_semiring))"
+    "(a+c < b+c) = (a < (b::'a::almost_ordered_semiring))"
 by (blast intro: add_less_imp_less_right add_strict_right_mono)
 
 lemma add_le_cancel_left [simp]:
-    "(c+a \<le> c+b) = (a \<le> (b::'a::ordered_semiring))"
+    "(c+a \<le> c+b) = (a \<le> (b::'a::almost_ordered_semiring))"
 by (simp add: linorder_not_less [symmetric]) 
 
 lemma add_le_cancel_right [simp]:
-    "(a+c \<le> b+c) = (a \<le> (b::'a::ordered_semiring))"
+    "(a+c \<le> b+c) = (a \<le> (b::'a::almost_ordered_semiring))"
 by (simp add: linorder_not_less [symmetric]) 
 
 lemma add_le_imp_le_left:
-      "c + a \<le> c + b ==> a \<le> (b::'a::ordered_semiring)"
+      "c + a \<le> c + b ==> a \<le> (b::'a::almost_ordered_semiring)"
 by simp
 
 lemma add_le_imp_le_right:
-      "a + c \<le> b + c ==> a \<le> (b::'a::ordered_semiring)"
+      "a + c \<le> b + c ==> a \<le> (b::'a::almost_ordered_semiring)"
 by simp
 
-lemma add_increasing: "[|0\<le>a; b\<le>c|] ==> b \<le> a + (c::'a::ordered_semiring)"
+lemma add_increasing: "[|0\<le>a; b\<le>c|] ==> b \<le> a + (c::'a::almost_ordered_semiring)"
 by (insert add_mono [of 0 a b c], simp)
 
 
@@ -477,33 +493,33 @@
 subsection {* Ordering Rules for Multiplication *}
 
 lemma mult_strict_right_mono:
-     "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_semiring)"
+     "[|a < b; 0 < c|] ==> a * c < b * (c::'a::almost_ordered_semiring)"
 by (simp add: mult_commute [of _ c] mult_strict_left_mono)
 
 lemma mult_left_mono:
-     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
+     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::almost_ordered_semiring)"
   apply (case_tac "c=0", simp)
   apply (force simp add: mult_strict_left_mono order_le_less) 
   done
 
 lemma mult_right_mono:
-     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
+     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::almost_ordered_semiring)"
   by (simp add: mult_left_mono mult_commute [of _ c]) 
 
 lemma mult_left_le_imp_le:
-     "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
+     "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::almost_ordered_semiring)"
   by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
  
 lemma mult_right_le_imp_le:
-     "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
+     "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::almost_ordered_semiring)"
   by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
 
 lemma mult_left_less_imp_less:
-     "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
+     "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::almost_ordered_semiring)"
   by (force simp add: mult_left_mono linorder_not_le [symmetric])
  
 lemma mult_right_less_imp_less:
-     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
+     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::almost_ordered_semiring)"
   by (force simp add: mult_right_mono linorder_not_le [symmetric])
 
 lemma mult_strict_left_mono_neg:
@@ -521,17 +537,17 @@
 
 subsection{* Products of Signs *}
 
-lemma mult_pos: "[| (0::'a::ordered_semiring) < a; 0 < b |] ==> 0 < a*b"
+lemma mult_pos: "[| (0::'a::almost_ordered_semiring) < a; 0 < b |] ==> 0 < a*b"
 by (drule mult_strict_left_mono [of 0 b], auto)
 
-lemma mult_pos_neg: "[| (0::'a::ordered_semiring) < a; b < 0 |] ==> a*b < 0"
+lemma mult_pos_neg: "[| (0::'a::almost_ordered_semiring) < a; b < 0 |] ==> a*b < 0"
 by (drule mult_strict_left_mono [of b 0], auto)
 
 lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b"
 by (drule mult_strict_right_mono_neg, auto)
 
 lemma zero_less_mult_pos:
-     "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring)"
+     "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::almost_ordered_semiring)"
 apply (case_tac "b\<le>0") 
  apply (auto simp add: order_le_less linorder_not_less)
 apply (drule_tac mult_pos_neg [of a b]) 
@@ -574,6 +590,14 @@
 lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"
 by (simp add: zero_le_mult_iff linorder_linear) 
 
+text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semiring}
+      theorems available to members of @{term ordered_ring} *}
+instance ordered_ring \<subseteq> ordered_semiring
+proof
+  have "(0::'a) \<le> 1*1" by (rule zero_le_square)
+  thus "(0::'a) < 1" by (simp add: order_le_less ) 
+qed
+
 text{*All three types of comparision involving 0 and 1 are covered.*}
 
 declare zero_neq_one [THEN not_sym, simp]