| author | ballarin |
| Wed, 11 Dec 2002 10:12:48 +0100 | |
| changeset 13745 | a31e04831dd1 |
| parent 13583 | 5fcc8bf538ee |
| permissions | -rw-r--r-- |
| 11443 | 1 |
<!-- $Id$ --> |
2 |
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY> |
|
3 |
||
4 |
<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2> |
|
5 |
||
6 |
<P>This directory presents proofs about group theory, by |
|
7 |
Florian Kammüller. (Later, Larry Paulson simplified some of the proofs.) |
|
8 |
These theories use locales and were indeed the original motivation for |
|
9 |
locales. However, this treatment of groups must still be regarded as |
|
10 |
experimental. We can expect to see refinements in the future. |
|
11 |
||
12 |
Here is an outline of the directory's contents: |
|
13 |
||
|
13583
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
12254
diff
changeset
|
14 |
<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines |
|
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
12254
diff
changeset
|
15 |
semigroups, groups, homomorphisms and the subgroup relation. It also defines |
|
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
12254
diff
changeset
|
16 |
the product of two groups. It defines the factorization of a group and shows |
|
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
12254
diff
changeset
|
17 |
that the factorization a normal subgroup is a group. |
|
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
12254
diff
changeset
|
18 |
|
| 12254 | 19 |
<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A> |
| 11443 | 20 |
defines bijections over sets and operations on them and shows that they |
|
13583
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
12254
diff
changeset
|
21 |
are a group. It shows that automorphisms form a group. |
| 11443 | 22 |
|
|
13583
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
12254
diff
changeset
|
23 |
<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves |
|
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
12254
diff
changeset
|
24 |
a few basic theorems. Ring automorphisms are shown to form a group. |
| 11443 | 25 |
|
| 12254 | 26 |
<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A> |
| 11443 | 27 |
contains a proof of the first Sylow theorem. |
|
13745
a31e04831dd1
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
ballarin
parents:
13583
diff
changeset
|
28 |
|
|
a31e04831dd1
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
ballarin
parents:
13583
diff
changeset
|
29 |
<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends |
|
a31e04831dd1
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
ballarin
parents:
13583
diff
changeset
|
30 |
abelian groups by a summation operator for finite sets (provided by |
|
a31e04831dd1
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
ballarin
parents:
13583
diff
changeset
|
31 |
Clemens Ballarin). |
| 11443 | 32 |
</UL> |
33 |
||
34 |
<HR> |
|
35 |
<P>Last modified on $Date$ |
|
36 |
||
37 |
<ADDRESS> |
|
38 |
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
39 |
</ADDRESS> |
|
40 |
</BODY></HTML> |