src/HOL/Algebra/README.html
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 51517 7957d26c3334
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
webertj@15582
     3
<HTML>
webertj@15582
     4
webertj@15582
     5
<HEAD>
webertj@15582
     6
  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
webertj@15582
     7
  <TITLE>HOL/Algebra/README.html</TITLE>
webertj@15582
     8
</HEAD>
webertj@15582
     9
webertj@15582
    10
<BODY>
paulson@7998
    11
ballarin@13949
    12
<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
ballarin@13949
    13
ballarin@13975
    14
This directory contains proofs in classical algebra.  It is intended
ballarin@13975
    15
as a base for any algebraic development in Isabelle.  Emphasis is on
ballarin@13975
    16
reusability.  This is achieved by modelling algebraic structures
ballarin@13975
    17
as first-class citizens of the logic (not axiomatic type classes, say).
ballarin@13975
    18
The library is expected to grow in future releases of Isabelle.
ballarin@13975
    19
Contributions are welcome.
ballarin@13949
    20
ballarin@13949
    21
<H2>GroupTheory, including Sylow's Theorem</H2>
ballarin@13949
    22
blanchet@37435
    23
<P>These proofs are mainly by Florian Kamm&uuml;ller.  (Later, Larry
ballarin@13949
    24
Paulson simplified some of the proofs.)  These theories were indeed
ballarin@13949
    25
the original motivation for locales.
ballarin@13949
    26
ballarin@13949
    27
Here is an outline of the directory's contents: <UL> <LI>Theory <A
ballarin@13949
    28
HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
ballarin@13949
    29
groups, commutative monoids, commutative groups, homomorphisms and the
ballarin@13949
    30
subgroup relation.  It also defines the product of two groups
ballarin@13949
    31
(This theory was reimplemented by Clemens Ballarin).
ballarin@13949
    32
ballarin@13949
    33
<LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends
ballarin@13949
    34
commutative groups by a product operator for finite sets (provided by
ballarin@13949
    35
Clemens Ballarin).
ballarin@13949
    36
ballarin@13949
    37
<LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> defines
ballarin@13949
    38
the factorization of a group and shows that the factorization a normal
ballarin@13949
    39
subgroup is a group.
ballarin@13949
    40
ballarin@13949
    41
<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
ballarin@13949
    42
defines bijections over sets and operations on them and shows that they
ballarin@13949
    43
are a group.  It shows that automorphisms form a group.
ballarin@13949
    44
ballarin@13949
    45
<LI>Theory <A HREF="Exponent.html"><CODE>Exponent</CODE></A> the
ballarin@13949
    46
	    combinatorial argument underlying Sylow's first theorem.
ballarin@13949
    47
ballarin@13949
    48
<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
ballarin@13949
    49
contains a proof of the first Sylow theorem.
ballarin@13949
    50
</UL>
ballarin@13949
    51
ballarin@13949
    52
<H2>Rings and Polynomials</H2>
ballarin@13949
    53
ballarin@51516
    54
<UL><LI>Theory <A HREF="Ring.html"><CODE>CRing</CODE></A>
ballarin@13949
    55
defines Abelian monoids and groups.  The difference to commutative
ballarin@13949
    56
      structures is merely notational:  the binary operation is
ballarin@13949
    57
      addition rather than multiplication.  Commutative rings are
ballarin@13949
    58
      obtained by inheriting properties from Abelian groups and
ballarin@13949
    59
      commutative monoids.  Further structures in the algebraic
ballarin@13949
    60
      hierarchy of rings: integral domain.
ballarin@13949
    61
ballarin@13949
    62
<LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>
ballarin@13949
    63
introduces the notion of a R-left-module over an Abelian group, where
ballarin@13949
    64
	R is a ring.
ballarin@13949
    65
ballarin@13949
    66
<LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>
ballarin@13949
    67
constructs univariate polynomials over rings and integral domains.
ballarin@13949
    68
	  Degree function.  Universal Property.
ballarin@13949
    69
</UL>
ballarin@13949
    70
ballarin@51517
    71
<H2>Development of Polynomials using Type Classes</H2>
paulson@7998
    72
ballarin@51517
    73
<P>A development of univariate polynomials for HOL's ring classes
ballarin@51517
    74
is available at <CODE>HOL/Library/Polynomial</CODE>.
paulson@7998
    75
paulson@7998
    76
<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
paulson@7998
    77
paulson@7998
    78
<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
ballarin@51516
    79
  Author's PhD thesis, 1999.  Also University of Cambridge, Computer Laboratory Technical Report number 473.
paulson@13944
    80
paulson@7998
    81
<ADDRESS>
ballarin@51516
    82
<P><A HREF="http://www21.in.tum.de/~ballarin">Clemens Ballarin</A>.
paulson@7998
    83
</ADDRESS>
webertj@15582
    84
</BODY>
webertj@15582
    85
</HTML>