src/HOL/Algebra/abstract/Ring.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/abstract/Ring.thy	Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,111 @@
+(*
+    Abstract class ring (commutative, with 1)
+    $Id$
+    Author: Clemens Ballarin, started 9 December 1996
+*)
+
+Ring = Main +
+
+(* Syntactic class ring *)
+
+axclass
+  ringS < plus, minus, times, power
+
+consts
+  (* Basic rings *)
+  "<0>"		:: 'a::ringS				("<0>")
+  "<1>"		:: 'a::ringS				("<1>")
+  "--"		:: ['a, 'a] => 'a::ringS		(infixl 65)
+
+  (* Divisibility *)
+  assoc		:: ['a::times, 'a] => bool		(infixl 70)
+  irred		:: 'a::ringS => bool
+  prime		:: 'a::ringS => bool
+
+  (* Fields *)
+  inverse	:: 'a::ringS => 'a
+  "'/'/"	:: ['a, 'a] => 'a::ringS		(infixl 70)
+
+translations
+  "a -- b" 	== "a + (-b)"
+  "a // b"	== "a * inverse b"
+
+(* Class ring and ring axioms *)
+
+axclass
+  ring < ringS
+
+  a_assoc	"(a + b) + c = a + (b + c)"
+  l_zero	"<0> + a = a"
+  l_neg		"(-a) + a = <0>"
+  a_comm	"a + b = b + a"
+
+  m_assoc	"(a * b) * c = a * (b * c)"
+  l_one		"<1> * a = a"
+
+  l_distr	"(a + b) * c = a * c + b * c"
+
+  m_comm	"a * b = b * a"
+
+  one_not_zero	"<1> ~= <0>"
+  		(* if <1> = <0>, then the ring has only one element! *)
+
+  power_ax	"a ^ n = nat_rec <1> (%u b. b * a) n"
+
+defs
+  assoc_def	"a assoc b == a dvd b & b dvd a"
+  irred_def	"irred a == 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>
+                          & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
+
+  inverse_def	"inverse a == if a dvd <1> then @x. a*x = <1> else <0>"
+
+(* Integral domains *)
+
+axclass
+  domain < ring
+
+  integral	"a * b = <0> ==> a = <0> | b = <0>"
+
+(* Factorial domains *)
+
+axclass
+  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"
+
+(* Euclidean domains *)
+
+(*
+axclass
+  euclidean < domain
+
+  euclidean_ax	"b ~= <0> ==> Ex (% (q, r, e_size::('a::ringS)=>nat).
+                   a = b * q + r & e_size r < e_size b)"
+
+  Nothing has been proved about euclidean domains, yet.
+  Design question:
+    Fix quo, rem and e_size as constants that are axiomatised with
+    euclidean_ax?
+    - advantage: more pragmatic and easier to use
+    - disadvantage: for every type, one definition of quo and rem will
+        be fixed, users may want to use differing ones;
+        also, it seems not possible to prove that fields are euclidean
+        domains, because that would require generic (type-independent)
+        definitions of quo and rem.
+*)
+
+(* Fields *)
+
+axclass
+  field < ring
+
+  field_ax	"a ~= <0> ==> a dvd <1>"
+
+end