Algebra --- Classical Algebra, using Explicit Structures and Locales

This directory contains proofs in classical algebra. It is intended as a base for any algebraic development in Isabelle. Emphasis is on reusability. This is achieved by modelling algebraic structures as first-class citizens of the logic (not axiomatic type classes, say). The library is expected to grow in future releases of Isabelle. Contributions are welcome.

GroupTheory, including Sylow's Theorem

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:

Rings and Polynomials

Development of Polynomials using Type Classes

A development of univariate polynomials for HOL's ring classes is available at HOL/Library/Polynomial.

[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.

[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving, Author's PhD thesis, 1999. Also University of Cambridge, Computer Laboratory Technical Report number 473.

Clemens Ballarin.