author ballarin Fri, 02 May 2003 20:02:50 +0200 changeset 13949 0ce528cd6f19 parent 13944 9b34607cd83e child 13975 c8e9a89883ce permissions -rw-r--r--
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
```
<!-- \$Id\$ -->

<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>

This directory presents proofs in classical algebra.

<H2>GroupTheory, including Sylow's Theorem</H2>

<P>These proofs are mainly by Florian Kammüller.  (Later, Larry
Paulson simplified some of the proofs.)  These theories were indeed
the original motivation for locales.

Here is an outline of the directory's contents: <UL> <LI>Theory <A
HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
groups, commutative monoids, commutative groups, homomorphisms and the
subgroup relation.  It also defines the product of two groups
(This theory was reimplemented by Clemens Ballarin).

<LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends
commutative groups by a product operator for finite sets (provided by
Clemens Ballarin).

<LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> 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="Exponent.html"><CODE>Exponent</CODE></A> the
combinatorial argument underlying Sylow's first theorem.

<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
contains a proof of the first Sylow theorem.
</UL>

<H2>Rings and Polynomials</H2>

<UL><LI>Theory <A HREF="CRing.html"><CODE>CRing</CODE></A>
defines Abelian monoids and groups.  The difference to commutative
structures is merely notational:  the binary operation is
addition rather than multiplication.  Commutative rings are
obtained by inheriting properties from Abelian groups and
commutative monoids.  Further structures in the algebraic
hierarchy of rings: integral domain.

<LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>
introduces the notion of a R-left-module over an Abelian group, where
R is a ring.

<LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>
constructs univariate polynomials over rings and integral domains.
Degree function.  Universal Property.
</UL>

<H2>Legacy Development of Rings using Axiomatic Type Classes</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>
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:

<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>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.

<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
Author's <A HREF="http://www4.in.tum.de/~ballarin/publications.html">PhD thesis</A>, 1999.

<HR>