7998

1 
<! $Id$ >


2 
<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>


3 


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


5 


6 
<P>This development of univariate polynomials is separated into an


7 
abstract development of rings and the development of polynomials


8 
itself. The formalisation is based on [Jacobson1985], and polynomials


9 
have a sparse, mathematical representation. These theories were


10 
developed as a base for the integration of a computer algebra system


11 
to Isabelle [Ballarin1999], and was designed to match implementations


12 
of these domains in some typed computer algebra systems. Summary:


13 


14 
<P><EM>Rings:</EM>


15 
Classes of rings are represented by axiomatic type classes. The


16 
following are available:


17 


18 
<PRE>


19 
ringS: Syntactic class


20 
ring: Commutative rings with one (including a summation


21 
operator, which is needed for the polynomials)


22 
domain: Integral domains


23 
factorial: Factorial domains (divisor chain condition is missing)


24 
pid: Principal ideal domains


25 
field: Fields


26 
</PRE>


27 


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


29 


30 
<P><EM>Polynomials:</EM>


31 
Polynomials have a natural, mathematical representation. Facts about


32 
the following topics are provided:


33 


34 
<MENU>


35 
<LI>Degree function


36 
<LI> Universal Property, evaluation homomorphism


37 
<LI>Long division (existence and uniqueness)


38 
<LI>Polynomials over a ring form a ring


39 
<LI>Polynomials over an integral domain form an integral domain


40 
</MENU>


41 


42 
<P>Still missing are


43 
Polynomials over a factorial domain form a factorial domain


44 
(difficult), and polynomials over a field form a pid.


45 


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


47 


48 
<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,


49 
Author's <A HREF="http://iakswww.ira.uka.de/iakscalmet/ballarin/publications.html">PhD thesis</A>, 1999.


50 


51 
<HR>


52 
<P>Last modified on $Date$


53 


54 
<ADDRESS>


55 
<P><A HREF="http://iakswww.ira.uka.de/iakscalmet/ballarin">Clemens Ballarin</A>. Karlsruhe, October 1999


56 


57 
<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>


58 
</ADDRESS>


59 
</BODY></HTML>
