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:
Groupdefines 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).
FiniteProductextends commutative groups by a product operator for finite sets (provided by Clemens Ballarin).
Cosetdefines the factorization of a group and shows that the factorization a normal subgroup is a group.
Bijdefines bijections over sets and operations on them and shows that they are a group. It shows that automorphisms form a group.
Exponentthe combinatorial argument underlying Sylow's first theorem.
Sylowcontains a proof of the first Sylow theorem.
CRingdefines 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.
Moduleintroduces the notion of a R-left-module over an Abelian group, where R is a ring.
UnivPolyconstructs univariate polynomials over rings and integral domains. Degree function. Universal Property.
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:
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: FieldsAlso, some facts about ring homomorphisms and ideals are mechanised.
Polynomials: Polynomials have a natural, mathematical representation. Facts about the following topics are provided:
[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$