changeset 7998 3d0c34795831
child 13944 9b34607cd83e
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/README.html	Fri Nov 05 11:14:26 1999 +0100
@@ -0,0 +1,59 @@
+<!-- $Id$ -->
+<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:
+  Classes of rings are represented by axiomatic type classes. The
+  following are available:
+  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
+  Also, some facts about ring homomorphisms and ideals are mechanised.
+  Polynomials have a natural, mathematical representation. Facts about
+  the following topics are provided:
+<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
+ <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="">PhD thesis</A>, 1999.
+<P>Last modified on $Date$
+<P><A HREF="">Clemens Ballarin</A>.  Karlsruhe, October 1999
+<A NAME="" HREF=""></A>