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