src/HOL/Algebra/abstract/Ring.thy

use inverse, divide from basic HOL;

(*
    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, inverse

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

translations
  "a -- b" 	== "a + (-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! *)

  inverse_ax    "inverse a = (if a dvd <1> then @x. a*x = <1> else <0>)"
  divide_ax     "a / b = a * inverse b"
  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)"

(* 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