webertj@15283: webertj@15283: paulson@7998: webertj@15582: 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: webertj@15283:

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:

ballarin@13949: ballarin@13949:

Rings and Polynomials

ballarin@13949: ballarin@13949: ballarin@13949: ballarin@13949:

Legacy Development of Rings using Axiomatic Type Classes

paulson@7998: paulson@7998:

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: 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:

  • Degree function paulson@7998:
  • Universal Property, evaluation homomorphism paulson@7998:
  • Long division (existence and uniqueness) paulson@7998:
  • Polynomials over a ring form a ring paulson@7998:
  • Polynomials over an integral domain form an integral domain paulson@7998:
  • 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:


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


    Clemens Ballarin. paulson@7998:

    webertj@15582: webertj@15582: