src/HOL/Algebra/README.html
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15582 7219facb3fd0
child 35849 b5522b51cb1e
permissions -rw-r--r--
Constant "If" is now local
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <!-- $Id$ -->
     4 
     5 <HTML>
     6 
     7 <HEAD>
     8   <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
     9   <TITLE>HOL/Algebra/README.html</TITLE>
    10 </HEAD>
    11 
    12 <BODY>
    13 
    14 <H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
    15 
    16 This directory contains proofs in classical algebra.  It is intended
    17 as a base for any algebraic development in Isabelle.  Emphasis is on
    18 reusability.  This is achieved by modelling algebraic structures
    19 as first-class citizens of the logic (not axiomatic type classes, say).
    20 The library is expected to grow in future releases of Isabelle.
    21 Contributions are welcome.
    22 
    23 <H2>GroupTheory, including Sylow's Theorem</H2>
    24 
    25 <P>These proofs are mainly by Florian Kammller.  (Later, Larry
    26 Paulson simplified some of the proofs.)  These theories were indeed
    27 the original motivation for locales.
    28 
    29 Here is an outline of the directory's contents: <UL> <LI>Theory <A
    30 HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
    31 groups, commutative monoids, commutative groups, homomorphisms and the
    32 subgroup relation.  It also defines the product of two groups
    33 (This theory was reimplemented by Clemens Ballarin).
    34 
    35 <LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends
    36 commutative groups by a product operator for finite sets (provided by
    37 Clemens Ballarin).
    38 
    39 <LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> defines
    40 the factorization of a group and shows that the factorization a normal
    41 subgroup is a group.
    42 
    43 <LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
    44 defines bijections over sets and operations on them and shows that they
    45 are a group.  It shows that automorphisms form a group.
    46 
    47 <LI>Theory <A HREF="Exponent.html"><CODE>Exponent</CODE></A> the
    48 	    combinatorial argument underlying Sylow's first theorem.
    49 
    50 <LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
    51 contains a proof of the first Sylow theorem.
    52 </UL>
    53 
    54 <H2>Rings and Polynomials</H2>
    55 
    56 <UL><LI>Theory <A HREF="CRing.html"><CODE>CRing</CODE></A>
    57 defines Abelian monoids and groups.  The difference to commutative
    58       structures is merely notational:  the binary operation is
    59       addition rather than multiplication.  Commutative rings are
    60       obtained by inheriting properties from Abelian groups and
    61       commutative monoids.  Further structures in the algebraic
    62       hierarchy of rings: integral domain.
    63 
    64 <LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>
    65 introduces the notion of a R-left-module over an Abelian group, where
    66 	R is a ring.
    67 
    68 <LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>
    69 constructs univariate polynomials over rings and integral domains.
    70 	  Degree function.  Universal Property.
    71 </UL>
    72 
    73 <H2>Legacy Development of Rings using Axiomatic Type Classes</H2>
    74 
    75 <P>This development of univariate polynomials is separated into an
    76 abstract development of rings and the development of polynomials
    77 itself. The formalisation is based on [Jacobson1985], and polynomials
    78 have a sparse, mathematical representation. These theories were
    79 developed as a base for the integration of a computer algebra system
    80 to Isabelle [Ballarin1999], and was designed to match implementations
    81 of these domains in some typed computer algebra systems.  Summary:
    82 
    83 <P><EM>Rings:</EM>
    84   Classes of rings are represented by axiomatic type classes. The
    85   following are available:
    86 
    87 <PRE>
    88   ring:		Commutative rings with one (including a summation
    89 		operator, which is needed for the polynomials)
    90   domain:	Integral domains
    91   factorial:	Factorial domains (divisor chain condition is missing)
    92   pid:		Principal ideal domains
    93   field:	Fields
    94 </PRE>
    95 
    96   Also, some facts about ring homomorphisms and ideals are mechanised.
    97 
    98 <P><EM>Polynomials:</EM>
    99   Polynomials have a natural, mathematical representation. Facts about
   100   the following topics are provided:
   101 
   102 <MENU>
   103 <LI>Degree function
   104 <LI> Universal Property, evaluation homomorphism
   105 <LI>Long division (existence and uniqueness)
   106 <LI>Polynomials over a ring form a ring
   107 <LI>Polynomials over an integral domain form an integral domain
   108 </MENU>
   109 
   110 <P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
   111 
   112 <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
   113   Author's <A HREF="http://www4.in.tum.de/~ballarin/publications.html">PhD thesis</A>, 1999.
   114 
   115 <HR>
   116 <P>Last modified on $Date$
   117 
   118 <ADDRESS>
   119 <P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.
   120 </ADDRESS>
   121 </BODY>
   122 </HTML>