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

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	<!-- $Id$ -->
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	4	<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	5
13975 c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	6	This directory contains proofs in classical algebra. It is intended
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	7	as a base for any algebraic development in Isabelle. Emphasis is on
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	8	reusability. This is achieved by modelling algebraic structures
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	9	as first-class citizens of the logic (not axiomatic type classes, say).
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	10	The library is expected to grow in future releases of Isabelle.
c8e9a89883ce Small changes for release Isabelle 2003. ballarin parents: 13949 diff changeset	11	Contributions are welcome.
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	12
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	13	<H2>GroupTheory, including Sylow's Theorem</H2>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	14
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	15	<P>These proofs are mainly by Florian Kamm�ller. (Later, Larry
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	16	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	17	the original motivation for locales.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	18
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	19	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	20	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	21	groups, commutative monoids, commutative groups, homomorphisms and the
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	22	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	23	(This theory was reimplemented by Clemens Ballarin).
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	24
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	25	<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	26	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	27	Clemens Ballarin).
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	<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	30	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	31	subgroup is a group.
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="Bij.html"><CODE>Bij</CODE></A>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	34	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	35	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	36
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	37	<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	38	combinatorial argument underlying Sylow's first theorem.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	39
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	40	<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	41	contains a proof of the first Sylow theorem.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	42	</UL>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	43
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	44	<H2>Rings and Polynomials</H2>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	45
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	46	<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	47	defines Abelian monoids and groups. The difference to commutative
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	48	structures is merely notational: the binary operation is
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	49	addition rather than multiplication. Commutative rings are
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	50	obtained by inheriting properties from Abelian groups and
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	51	commutative monoids. Further structures in the algebraic
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	52	hierarchy of rings: integral domain.
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	<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	55	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	56	R is a ring.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	57
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	58	<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	59	constructs univariate polynomials over rings and integral domains.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	60	Degree function. Universal Property.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	61	</UL>
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	62
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	63	<H2>Legacy Development of Rings using Axiomatic Type Classes</H2>
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	64
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	65	<P>This development of univariate polynomials is separated into an
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	66	abstract development of rings and the development of polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	67	itself. The formalisation is based on [Jacobson1985], and polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	68	have a sparse, mathematical representation. These theories were
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	69	developed as a base for the integration of a computer algebra system
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	70	to Isabelle [Ballarin1999], and was designed to match implementations
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	71	of these domains in some typed computer algebra systems. Summary:
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><EM>Rings:</EM>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	74	Classes of rings are represented by axiomatic type classes. The
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	75	following are available:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	76
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	77	<PRE>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	78	ring: Commutative rings with one (including a summation
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	79	operator, which is needed for the polynomials)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	80	domain: Integral domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	81	factorial: Factorial domains (divisor chain condition is missing)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	82	pid: Principal ideal domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	83	field: Fields
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	84	</PRE>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	85
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	86	Also, some facts about ring homomorphisms and ideals are mechanised.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	87
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	88	<P><EM>Polynomials:</EM>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	89	Polynomials have a natural, mathematical representation. Facts about
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	90	the following topics are provided:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	91
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	92	<MENU>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	93	<LI>Degree function
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	94	<LI> Universal Property, evaluation homomorphism
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	95	<LI>Long division (existence and uniqueness)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	96	<LI>Polynomials over a ring form a ring
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	97	<LI>Polynomials over an integral domain form an integral domain
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	98	</MENU>
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	<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
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	<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	103	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	104
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	105	<HR>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	106	<P>Last modified on $Date$
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	<ADDRESS>
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13944 diff changeset	109	<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	110	</ADDRESS>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	111	</BODY></HTML>

author	ballarin
	Wed, 07 May 2003 22:07:33 +0200
changeset 13975	c8e9a89883ce
parent 13949	0ce528cd6f19
child 15283	f21466450330
permissions	-rw-r--r--