# HG changeset patch
# User haftmann
# Date 1215759744 -7200
# Node ID 9bf0a22f8bcda3cda506a833dcca49186d10f346
# Parent  9e585e99b494284dfd48d30acce25b38a18817f7
class instead of axclass

diff -r 9e585e99b494 -r 9bf0a22f8bcd src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Jul 11 09:02:23 2008 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Jul 11 09:02:24 2008 +0200
@@ -5,71 +5,63 @@
   Copyright: Clemens Ballarin
 *)
 
-header {* The algebraic hierarchy of rings as axiomatic classes *}
-
-theory Ring2 imports Main
-begin
-
-section {* Constants *}
+header {* The algebraic hierarchy of rings as type classes *}
 
-text {* Most constants are already declared by HOL. *}
-
-consts
-  assoc         :: "['a::Divides.div, 'a] => bool"              (infixl "assoc" 50)
-  irred         :: "'a::{zero, one, Divides.div} => bool"
-  prime         :: "'a::{zero, one, Divides.div} => bool"
-
-section {* Axioms *}
+theory Ring2
+imports Main
+begin
 
 subsection {* Ring axioms *}
 
-axclass ring < zero, one, plus, minus, uminus, times, inverse, power, Divides.div
-
-  a_assoc:      "(a + b) + c = a + (b + c)"
-  l_zero:       "0 + a = a"
-  l_neg:        "(-a) + a = 0"
-  a_comm:       "a + b = b + a"
+class ring = zero + one + plus + minus + uminus + times + inverse + power + Divides.dvd +
+  assumes a_assoc:      "(a + b) + c = a + (b + c)"
+  and l_zero:           "0 + a = a"
+  and l_neg:            "(-a) + a = 0"
+  and a_comm:           "a + b = b + a"
 
-  m_assoc:      "(a * b) * c = a * (b * c)"
-  l_one:        "1 * a = a"
+  assumes m_assoc:      "(a * b) * c = a * (b * c)"
+  and l_one:            "1 * a = a"
 
-  l_distr:      "(a + b) * c = a * c + b * c"
+  assumes l_distr:      "(a + b) * c = a * c + b * c"
 
-  m_comm:       "a * b = b * a"
+  assumes m_comm:       "a * b = b * a"
 
-  -- {* Definition of derived operations *}
+  assumes minus_def:    "a - b = a + (-b)"
+  and inverse_def:      "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
+  and divide_def:       "a / b = a * inverse b"
+  and power_0 [simp]:   "a ^ 0 = 1"
+  and power_Suc [simp]: "a ^ Suc n = a ^ n * a"
+begin
 
-  minus_def:    "a - b = a + (-b)"
-  inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
-  divide_def:   "a / b = a * inverse b"
-  power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
+definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where
+  assoc_def: "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
 
-defs
-  assoc_def:    "a assoc b == a dvd b & b dvd a"
-  irred_def:    "irred a == a ~= 0 & ~ a dvd 1
+definition irred :: "'a \<Rightarrow> bool" where
+  irred_def: "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1
                           & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
-  prime_def:    "prime p == p ~= 0 & ~ p dvd 1
+
+definition prime :: "'a \<Rightarrow> bool" where
+  prime_def: "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1
                           & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
 
+end
+
+
 subsection {* Integral domains *}
 
-axclass
-  "domain" < ring
-
-  one_not_zero: "1 ~= 0"
-  integral:     "a * b = 0 ==> a = 0 | b = 0"
+class "domain" = ring +
+  assumes one_not_zero: "1 ~= 0"
+  and integral: "a * b = 0 ==> a = 0 | b = 0"
 
 subsection {* Factorial domains *}
 
-axclass
-  factorial < "domain"
-
+class factorial = "domain" +
 (*
   Proper definition using divisor chain condition currently not supported.
   factorial_divisor:    "wf {(a, b). a dvd b & ~ (b dvd a)}"
 *)
-  factorial_divisor:	"True"
-  factorial_prime:      "irred a ==> prime a"
+  assumes factorial_divisor: "True"
+  and factorial_prime: "irred a ==> prime a"
 
 subsection {* Euclidean domains *}
 
@@ -94,13 +86,11 @@
 
 subsection {* Fields *}
 
-axclass
-  field < ring
-
-  field_one_not_zero:    "1 ~= 0"
+class field = ring +
+  assumes field_one_not_zero: "1 ~= 0"
                 (* Avoid a common superclass as the first thing we will
                    prove about fields is that they are domains. *)
-  field_ax:        "a ~= 0 ==> a dvd 1"
+  and field_ax: "a ~= 0 ==> a dvd 1"
 
 
 section {* Basic facts *}
@@ -275,12 +265,12 @@
 
 (* Facts specific to rings *)
 
-instance ring < comm_monoid_add
+subclass (in ring) comm_monoid_add
 proof
   fix x y z
-  show "(x::'a::ring) + y = y + x" by (rule a_comm)
-  show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc)
-  show "0 + (x::'a::ring) = x" by (rule l_zero)
+  show "x + y = y + x" by (rule a_comm)
+  show "(x + y) + z = x + (y + z)" by (rule a_assoc)
+  show "0 + x = x" by (rule l_zero)
 qed
 
 ML {*
@@ -358,11 +348,7 @@
   "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
 by (simp add: m_lcancel)
 
-lemma power_0 [simp]:
-  "(a::'a::ring) ^ 0 = 1" unfolding power_def by simp
-
-lemma power_Suc [simp]:
-  "(a::'a::ring) ^ Suc n = a ^ n * a" unfolding power_def by simp
+declare power_Suc [simp]
 
 lemma power_one [simp]:
   "1 ^ n = (1::'a::ring)" by (induct n) simp_all