Abstract Algebra Specs

Number Systems: Concepts, Issues, and Designs

Abstract Algebra Specs

Monoid-Sig

Signature for monoids:
Sort E;
op binop : E, E -> E
const unit : E

MONOID

ASSOCIATIVE and BIN-OP-UNIT

COMMUTATIVE-MONOID

Commutative MONOID

GROUP

MONOID and INVERSE for binop

RING-DIAGRAM

Sharing for rings: two copies of BIN-OP (e.g., plus and times); arcs are morphisms from the BIN-OPs into GROUP, MONOID, and DISTRIBUTIVITY.

RING

Imports (the sharing diagram) Ring-Diagram and renames the group unit to zero and the monoid unit to one.

COMMUTATIVE-RING-DIAGRAM

Similar to Ring-Diagram except that it uses COMMUTATIVE-MONOID instead of MONOID

COMMUTATIVE-RING

Similar to Ring except that it uses COMMUTATIVE-RING-DIAGRAM

INTEGRAL-DOMAIN

Imports COMMUTATIVE-RING and adds the axioms:
nontrivial: (not (equal zero one))
cancellation-for-times:
(implies (and (not (equal x zero)) (equal (times x y) (times x z))) (equal y z))

ORDERED-INTEGRAL-DOMAIN

Imports merge of INTEGRAL-DOMAIN and STRICT-TOTAL-ORDER sharing E.
Adds axioms relating the order and the ring operations:
lt-plus: (implies (lt x y) (lt (plus x z) (plus y z)))
lt-times: (implies (lt x y) (lt (times x z) (times y z)))
Then defines pos? [via: (iff (pos? x) (lt zero x))], neg? and abs

ORDERED-INTEGRAL-DOMAIN-POS

Imports INTEGRAL-DOMAIN and defines the lt relation via:
succ: (equal (succ x) (plus x one))
minus: (equal (minus x y) (plus x (inv-plus y)))
pred: (equal (pred x) (minus x one))
pos?:
(not (pos? zero))
(pos? one)
(implies (pos? x) (pos? (succ x)))
(implies (pos? x) (not (pos? (inv-plus x))))

lt is then defined via: (iff (lt x y) (pos? (minus y x)))

FIELD

Imports INTEGRAL-DOMAIN and adds the divisiblity axiom:
divisiblity: (implies (not (equal y zero)) (Ex (z) (equal (times y z) x)))
Then defines the sort nonzero and the op div : E, nonzero -> E via
(iff (equal (div x y) z) (equal x (times ((relax nonzero?) y) z)))

ORDERED-FIELD

Merges ORDERED-INTEGRAL-DOMAIN and FIELD sharing INTEGRAL-DOMAIN

ORDERED-FIELD-AXM

Imports ORDERED-INTEGRAL-DOMAIN adds the divisiblity axiom etc

SpecWeb Index

Specs