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

src/HOL/Algebra/README.html

author | paulson |

Thu, 01 May 2003 11:54:18 +0200 | |

changeset 13944 | 9b34607cd83e |

parent 7998 | 3d0c34795831 |

child 13949 | 0ce528cd6f19 |

permissions | -rw-r--r-- |

new proofs about direct products, etc.

<!-- $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. <H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2> <P>This directory presents proofs about group theory, by Florian Kammüller. (Later, Larry Paulson simplified some of the proofs.) These theories use locales and were indeed the original motivation for locales. However, this treatment of groups must still be regarded as experimental. We can expect to see refinements in the future. Here is an outline of the directory's contents: <UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, groups, homomorphisms and the subgroup relation. It also defines the product of two groups. It defines the factorization of a group and shows that the factorization a normal subgroup is a group. <LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A> defines bijections over sets and operations on them and shows that they are a group. It shows that automorphisms form a group. <LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves a few basic theorems. Ring automorphisms are shown to form a group. <LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A> contains a proof of the first Sylow theorem. <LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends abelian groups by a summation operator for finite sets (provided by Clemens Ballarin). </UL> <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>