These proofs are mainly by Florian Kammüller. (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:

A development of univariate polynomials for HOL's ring classes
ballarin@51517: is available at `HOL/Library/Polynomial`

.
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@51516: Author's PhD thesis, 1999. Also University of Cambridge, Computer Laboratory Technical Report number 473. paulson@13944: paulson@7998:

ballarin@51516:Clemens Ballarin. paulson@7998:

webertj@15582: webertj@15582: