isabelle: src/HOL/Algebra/README.html@3d03190d2864 (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
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>

author	wenzelm
	Fri, 06 Mar 2009 22:32:27 +0100
changeset 30318	3d03190d2864
parent 15582	7219facb3fd0
child 35849	b5522b51cb1e
permissions	-rw-r--r--