isabelle: src/HOL/Algebra/README.html@ed97e877ff2d (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
15283 f21466450330 DOCTYPE declaration added webertj parents: 13975 diff changeset	23	<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	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
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	54	<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	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
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	71	<H2>Legacy Development of Rings using Axiomatic Type Classes</H2>
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	72
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	73	<P>This development of univariate polynomials is separated into an
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	74	abstract development of rings and the development of polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	75	itself. The formalisation is based on [Jacobson1985], and polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	76	have a sparse, mathematical representation. These theories were
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	77	developed as a base for the integration of a computer algebra system
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	78	to Isabelle [Ballarin1999], and was designed to match implementations
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	79	of these domains in some typed computer algebra systems. Summary:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	80
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	81	<P><EM>Rings:</EM>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	82	Classes of rings are represented by axiomatic type classes. The
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	83	following are available:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	84
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	85	<PRE>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	86	ring: Commutative rings with one (including a summation
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	87	operator, which is needed for the polynomials)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	88	domain: Integral domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	89	factorial: Factorial domains (divisor chain condition is missing)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	90	pid: Principal ideal domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	91	field: Fields
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	92	</PRE>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	93
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	94	Also, some facts about ring homomorphisms and ideals are mechanised.
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	<P><EM>Polynomials:</EM>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	97	Polynomials have a natural, mathematical representation. Facts about
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	98	the following topics are provided:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	99
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	100	<MENU>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	101	<LI>Degree function
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	102	<LI> Universal Property, evaluation homomorphism
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	103	<LI>Long division (existence and uniqueness)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	104	<LI>Polynomials over a ring form a ring
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	105	<LI>Polynomials over an integral domain form an integral domain
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	106	</MENU>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	107
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	108	<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
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>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	111	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	112
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	113	<HR>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	114	<P>Last modified on $Date$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	115
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	116	<ADDRESS>
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	117	<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	118	</ADDRESS>
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	119	</BODY>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	120	</HTML>

author	wenzelm
	Tue, 11 May 2010 23:36:06 +0200
changeset 36817	ed97e877ff2d
parent 35849	b5522b51cb1e
child 37435	ed79fa620012
permissions	-rw-r--r--