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