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