Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/README.html
author paulson
Fri, 05 Nov 1999 11:14:26 +0100
changeset 7998 3d0c34795831
child 13944 9b34607cd83e
permissions -rw-r--r--
Algebra and Polynomial theories, by Clemens Ballarin

<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>

<H2>Algebra: Theories of Rings and Polynomials</H2>

<P>This development of univariate polynomials is separated into an
abstract development of rings and the development of polynomials
itself. The formalisation is based on [Jacobson1985], and polynomials
have a sparse, mathematical representation. These theories were
developed as a base for the integration of a computer algebra system
to Isabelle [Ballarin1999], and was designed to match implementations
of these domains in some typed computer algebra systems.  Summary:

<P><EM>Rings:</EM>
  Classes of rings are represented by axiomatic type classes. The
  following are available:

<PRE>
  ringS:	Syntactic class
  ring:		Commutative rings with one (including a summation
		operator, which is needed for the polynomials)
  domain:	Integral domains
  factorial:	Factorial domains (divisor chain condition is missing)
  pid:		Principal ideal domains
  field:	Fields
</PRE>

  Also, some facts about ring homomorphisms and ideals are mechanised.

<P><EM>Polynomials:</EM>
  Polynomials have a natural, mathematical representation. Facts about
  the following topics are provided:

<MENU>
<LI>Degree function
<LI> Universal Property, evaluation homomorphism
<LI>Long division (existence and uniqueness)
<LI>Polynomials over a ring form a ring
<LI>Polynomials over an integral domain form an integral domain
</MENU>

 <P>Still missing are
    Polynomials over a factorial domain form a factorial domain
    (difficult), and polynomials over a field form a pid.

<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.

<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
  Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.

<HR>
<P>Last modified on $Date$

<ADDRESS>
<P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>.  Karlsruhe, October 1999

<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>
</ADDRESS>
</BODY></HTML>
isabelle