isabelle: src/HOL/Algebra/README.html@da3fefcb43c3 (annotated)

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
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	3	<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	4
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	5	<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	6	<meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	7	<TITLE>HOL/Algebra/README.html</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	9
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	10	<BODY>
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	12	<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	13
13975 c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	14	This directory contains proofs in classical algebra. It is intended
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	15	as a base for any algebraic development in Isabelle. Emphasis is on
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	16	reusability. This is achieved by modelling algebraic structures
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	17	as first-class citizens of the logic (not axiomatic type classes, say).
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	18	The library is expected to grow in future releases of Isabelle.
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	19	Contributions are welcome.
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	20
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	21	<H2>GroupTheory, including Sylow's Theorem</H2>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	22
37435 ed79fa620012 added missing Umlaut blanchet parents: 35849 diff changeset	23	<P>These proofs are mainly by Florian Kammüller. (Later, Larry
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	24	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	25	the original motivation for locales.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	26
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	27	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	28	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	29	groups, commutative monoids, commutative groups, homomorphisms and the
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	30	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	31	(This theory was reimplemented by Clemens Ballarin).
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	32
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	33	<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	34	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	35	Clemens Ballarin).
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	36
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	37	<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	38	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	39	subgroup is a group.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	40
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	41	<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	42	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	43	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	44
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	45	<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	46	combinatorial argument underlying Sylow's first theorem.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	47
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	48	<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	49	contains a proof of the first Sylow theorem.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	50	</UL>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	51
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	52	<H2>Rings and Polynomials</H2>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	53
51516 237190475d79 Remove obsolete URLs in documentation of HOL-Algebra. ballarin parents: 51404 diff changeset	54	<UL><LI>Theory <A HREF="Ring.html"><CODE>CRing</CODE></A>
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	55	defines Abelian monoids and groups. The difference to commutative
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	56	structures is merely notational: the binary operation is
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	57	addition rather than multiplication. Commutative rings are
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	58	obtained by inheriting properties from Abelian groups and
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	59	commutative monoids. Further structures in the algebraic
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	60	hierarchy of rings: integral domain.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	61
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	62	<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	63	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	64	R is a ring.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	65
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	66	<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	67	constructs univariate polynomials over rings and integral domains.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	68	Degree function. Universal Property.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	69	</UL>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	70
51517 7957d26c3334 Discontinued theories src/HOL/Algebra/abstract and .../poly. ballarin parents: 51516 diff changeset	71	<H2>Development of Polynomials using Type Classes</H2>
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	72
51517 7957d26c3334 Discontinued theories src/HOL/Algebra/abstract and .../poly. ballarin parents: 51516 diff changeset	73	<P>A development of univariate polynomials for HOL's ring classes
7957d26c3334 Discontinued theories src/HOL/Algebra/abstract and .../poly. ballarin parents: 51516 diff changeset	74	is available at <CODE>HOL/Library/Polynomial</CODE>.
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	75
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	76	<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	77
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	78	<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
51516 237190475d79 Remove obsolete URLs in documentation of HOL-Algebra. ballarin parents: 51404 diff changeset	79	Author's PhD thesis, 1999. Also University of Cambridge, Computer Laboratory Technical Report number 473.
13944 9b34607cd83e new proofs about direct products, etc. paulson parents: 7998 diff changeset	80
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	81	<ADDRESS>
51516 237190475d79 Remove obsolete URLs in documentation of HOL-Algebra. ballarin parents: 51404 diff changeset	82	<P><A HREF="http://www21.in.tum.de/~ballarin">Clemens Ballarin</A>.
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	83	</ADDRESS>
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	84	</BODY>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	85	</HTML>

author	wenzelm
	Fri, 25 Apr 2014 23:29:54 +0200
changeset 56732	da3fefcb43c3
parent 51517	7957d26c3334
permissions	-rw-r--r--