webertj@15283: webertj@15283: webertj@15582: webertj@15582: webertj@15582: webertj@15582: webertj@15582: HOL/Algebra/README.html webertj@15582: webertj@15582: webertj@15582: paulson@7998: ballarin@13949:

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

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

GroupTheory, including Sylow's Theorem

ballarin@13949: blanchet@37435:

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:

ballarin@13949: ballarin@13949:

Rings and Polynomials

ballarin@13949: ballarin@51516: ballarin@13949: ballarin@51517:

Development of Polynomials using Type Classes

paulson@7998: ballarin@51517:

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: