summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Algebra/README.html

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$ --> +<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>