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