src/HOL/Algebra/README.html
author paulson
Fri Nov 05 11:14:26 1999 +0100 (1999-11-05)
changeset 7998 3d0c34795831
child 13944 9b34607cd83e
permissions -rw-r--r--
Algebra and Polynomial theories, by Clemens Ballarin
paulson@7998
     1
<!-- $Id$ -->
paulson@7998
     2
<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
paulson@7998
     3
paulson@7998
     4
<H2>Algebra: Theories of Rings and Polynomials</H2>
paulson@7998
     5
paulson@7998
     6
<P>This development of univariate polynomials is separated into an
paulson@7998
     7
abstract development of rings and the development of polynomials
paulson@7998
     8
itself. The formalisation is based on [Jacobson1985], and polynomials
paulson@7998
     9
have a sparse, mathematical representation. These theories were
paulson@7998
    10
developed as a base for the integration of a computer algebra system
paulson@7998
    11
to Isabelle [Ballarin1999], and was designed to match implementations
paulson@7998
    12
of these domains in some typed computer algebra systems.  Summary:
paulson@7998
    13
paulson@7998
    14
<P><EM>Rings:</EM>
paulson@7998
    15
  Classes of rings are represented by axiomatic type classes. The
paulson@7998
    16
  following are available:
paulson@7998
    17
paulson@7998
    18
<PRE>
paulson@7998
    19
  ringS:	Syntactic class
paulson@7998
    20
  ring:		Commutative rings with one (including a summation
paulson@7998
    21
		operator, which is needed for the polynomials)
paulson@7998
    22
  domain:	Integral domains
paulson@7998
    23
  factorial:	Factorial domains (divisor chain condition is missing)
paulson@7998
    24
  pid:		Principal ideal domains
paulson@7998
    25
  field:	Fields
paulson@7998
    26
</PRE>
paulson@7998
    27
paulson@7998
    28
  Also, some facts about ring homomorphisms and ideals are mechanised.
paulson@7998
    29
paulson@7998
    30
<P><EM>Polynomials:</EM>
paulson@7998
    31
  Polynomials have a natural, mathematical representation. Facts about
paulson@7998
    32
  the following topics are provided:
paulson@7998
    33
paulson@7998
    34
<MENU>
paulson@7998
    35
<LI>Degree function
paulson@7998
    36
<LI> Universal Property, evaluation homomorphism
paulson@7998
    37
<LI>Long division (existence and uniqueness)
paulson@7998
    38
<LI>Polynomials over a ring form a ring
paulson@7998
    39
<LI>Polynomials over an integral domain form an integral domain
paulson@7998
    40
</MENU>
paulson@7998
    41
paulson@7998
    42
 <P>Still missing are
paulson@7998
    43
    Polynomials over a factorial domain form a factorial domain
paulson@7998
    44
    (difficult), and polynomials over a field form a pid.
paulson@7998
    45
paulson@7998
    46
<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
paulson@7998
    47
paulson@7998
    48
<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
paulson@7998
    49
  Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
paulson@7998
    50
paulson@7998
    51
<HR>
paulson@7998
    52
<P>Last modified on $Date$
paulson@7998
    53
paulson@7998
    54
<ADDRESS>
paulson@7998
    55
<P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>.  Karlsruhe, October 1999
paulson@7998
    56
paulson@7998
    57
<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>
paulson@7998
    58
</ADDRESS>
paulson@7998
    59
</BODY></HTML>