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: + +
Rings: + 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: + Polynomials have a natural, mathematical representation. Facts about + the following topics are provided: + +
+ +Still missing are + Polynomials over a factorial domain form a factorial domain + (difficult), and polynomials over a field form a pid. + +
[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985. + +
[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving, + Author's PhD thesis, 1999. + +
Last modified on $Date$ + +
+Clemens Ballarin. Karlsruhe, October 1999 + +ballarin@ira.uka.de +
+