# HG changeset patch
# User wenzelm
# Date 974573232 -3600
# Node ID 107c7db021a9201ab546678fc65538df5a50c967
# Parent  e4a4087280126a5de4e28c87f6f6602843daf540
axclass ordered_ring;
instance int :: ordered_ring;

diff -r e4a408728012 -r 107c7db021a9 src/HOL/Library/Ring_and_Field.thy
--- a/src/HOL/Library/Ring_and_Field.thy	Sat Nov 18 19:46:48 2000 +0100
+++ b/src/HOL/Library/Ring_and_Field.thy	Sat Nov 18 19:47:12 2000 +0100
@@ -10,16 +10,14 @@
 
 theory Ring_and_Field = Main: 
 
-text {*
- The class @{text ring} models commutative ring structures with $1$.
-*}
+subsection {* Abstract algebraic structures *}
 
 axclass ring < zero, plus, minus, times, number
   add_assoc: "(a + b) + c = a + (b + c)"
   add_commute: "a + b = b + a"
   left_zero: "0 + a = a"
-  left_minus: "(- a) + a = 0"
-  diff_minus: "a - b = a + (- b)"
+  left_minus: "(-a) + a = 0"
+  diff_minus: "a - b = a + (-b)"
   zero_number: "0 = #0"
 
   mult_assoc: "(a * b) * c = a * (b * c)"
@@ -28,14 +26,36 @@
 
   left_distrib: "(a + b) * c = a * c + b * c"
 
+axclass ordered_ring < ring, linorder
+  add_left_mono: "a \<le> b ==> c + a \<le> c + b"
+  mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
+  abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
 
 axclass field < ring, inverse
   left_inverse: "a \<noteq> 0 ==> inverse a * a = #1"
   divides_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
 
+axclass ordered_field < ordered_ring, field
 
-axclass ordered_field < field, linorder
-  add_left_mono: "a \<le> b ==> c + a \<le> c + b"
-  mult_left_mono: "a \<le> b ==> 0 < c ==> c * a \<le> c * b"
+
+subsection {* The ordered ring of integers *}
+
+instance int :: ordered_ring
+proof
+  fix i j k :: int
+  show "(i + j) + k = i + (j + k)" by simp
+  show "i + j = j + i" by simp
+  show "0 + i = i" by simp
+  show "(-i) + i = 0" by simp
+  show "i - j = i + (-j)" by simp
+  show "(i * j) * k = i * (j * k)" by simp
+  show "i * j = j * i" by simp
+  show "#1 * i = i" by simp
+  show "0 = (#0::int)" by simp
+  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
+  show "i \<le> j ==> k + i \<le> k + j" by simp
+  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
+  show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
+qed
 
 end