These proofs are mainly by Florian Kammller. (Later, Larry ballarin@13949: Paulson simplified some of the proofs.) These theories were indeed ballarin@13949: the original motivation for locales. ballarin@13949: ballarin@13949: Here is an outline of the directory's contents:

- Theory
`Group`

defines semigroups, monoids, ballarin@13949: groups, commutative monoids, commutative groups, homomorphisms and the ballarin@13949: subgroup relation. It also defines the product of two groups ballarin@13949: (This theory was reimplemented by Clemens Ballarin). ballarin@13949: ballarin@13949: - Theory
`FiniteProduct`

extends ballarin@13949: commutative groups by a product operator for finite sets (provided by ballarin@13949: Clemens Ballarin). ballarin@13949: ballarin@13949: - Theory
`Coset`

defines ballarin@13949: the factorization of a group and shows that the factorization a normal ballarin@13949: subgroup is a group. ballarin@13949: ballarin@13949: - Theory
`Bij`

ballarin@13949: defines bijections over sets and operations on them and shows that they ballarin@13949: are a group. It shows that automorphisms form a group. ballarin@13949: ballarin@13949: - Theory
`Exponent`

the ballarin@13949: combinatorial argument underlying Sylow's first theorem. ballarin@13949: ballarin@13949: - Theory
`Sylow`

ballarin@13949: contains a proof of the first Sylow theorem. ballarin@13949:

- Theory
`CRing`

ballarin@13949: defines Abelian monoids and groups. The difference to commutative ballarin@13949: structures is merely notational: the binary operation is ballarin@13949: addition rather than multiplication. Commutative rings are ballarin@13949: obtained by inheriting properties from Abelian groups and ballarin@13949: commutative monoids. Further structures in the algebraic ballarin@13949: hierarchy of rings: integral domain. ballarin@13949: ballarin@13949: - Theory
`Module`

ballarin@13949: introduces the notion of a R-left-module over an Abelian group, where ballarin@13949: R is a ring. ballarin@13949: ballarin@13949: - Theory
`UnivPoly`

ballarin@13949: constructs univariate polynomials over rings and integral domains. ballarin@13949: Degree function. Universal Property. ballarin@13949:

This development of univariate polynomials is separated into an paulson@7998: abstract development of rings and the development of polynomials paulson@7998: itself. The formalisation is based on [Jacobson1985], and polynomials paulson@7998: have a sparse, mathematical representation. These theories were paulson@7998: developed as a base for the integration of a computer algebra system paulson@7998: to Isabelle [Ballarin1999], and was designed to match implementations paulson@7998: of these domains in some typed computer algebra systems. Summary: paulson@7998: paulson@7998:

*Rings:*
paulson@7998: Classes of rings are represented by axiomatic type classes. The
paulson@7998: following are available:
paulson@7998:
paulson@7998:

paulson@7998: ring: Commutative rings with one (including a summation paulson@7998: operator, which is needed for the polynomials) paulson@7998: domain: Integral domains paulson@7998: factorial: Factorial domains (divisor chain condition is missing) paulson@7998: pid: Principal ideal domains paulson@7998: field: Fields paulson@7998:paulson@7998: paulson@7998: Also, some facts about ring homomorphisms and ideals are mechanised. paulson@7998: paulson@7998:

*Polynomials:*
paulson@7998: Polynomials have a natural, mathematical representation. Facts about
paulson@7998: the following topics are provided:
paulson@7998:
paulson@7998:

[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985. paulson@7998: paulson@7998:

[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving, ballarin@13949: Author's PhD thesis, 1999. paulson@13944: paulson@7998:

paulson@7998:

Last modified on $Date$ paulson@7998: paulson@7998:

ballarin@13949:Clemens Ballarin. paulson@7998:

webertj@15582: webertj@15582: