summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/README.html

author | paulson |

Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) | |

changeset 16587 | b34c8aa657a5 |

parent 15582 | 7219facb3fd0 |

child 35849 | b5522b51cb1e |

permissions | -rw-r--r-- |

Constant "If" is now local

1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

3 <!-- $Id$ -->

5 <HTML>

7 <HEAD>

8 <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">

9 <TITLE>HOL/Algebra/README.html</TITLE>

10 </HEAD>

12 <BODY>

14 <H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>

16 This directory contains proofs in classical algebra. It is intended

17 as a base for any algebraic development in Isabelle. Emphasis is on

18 reusability. This is achieved by modelling algebraic structures

19 as first-class citizens of the logic (not axiomatic type classes, say).

20 The library is expected to grow in future releases of Isabelle.

21 Contributions are welcome.

23 <H2>GroupTheory, including Sylow's Theorem</H2>

25 <P>These proofs are mainly by Florian Kammller. (Later, Larry

26 Paulson simplified some of the proofs.) These theories were indeed

27 the original motivation for locales.

29 Here is an outline of the directory's contents: <UL> <LI>Theory <A

30 HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,

31 groups, commutative monoids, commutative groups, homomorphisms and the

32 subgroup relation. It also defines the product of two groups

33 (This theory was reimplemented by Clemens Ballarin).

35 <LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends

36 commutative groups by a product operator for finite sets (provided by

37 Clemens Ballarin).

39 <LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> defines

40 the factorization of a group and shows that the factorization a normal

41 subgroup is a group.

43 <LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>

44 defines bijections over sets and operations on them and shows that they

45 are a group. It shows that automorphisms form a group.

47 <LI>Theory <A HREF="Exponent.html"><CODE>Exponent</CODE></A> the

48 combinatorial argument underlying Sylow's first theorem.

50 <LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>

51 contains a proof of the first Sylow theorem.

52 </UL>

54 <H2>Rings and Polynomials</H2>

56 <UL><LI>Theory <A HREF="CRing.html"><CODE>CRing</CODE></A>

57 defines Abelian monoids and groups. The difference to commutative

58 structures is merely notational: the binary operation is

59 addition rather than multiplication. Commutative rings are

60 obtained by inheriting properties from Abelian groups and

61 commutative monoids. Further structures in the algebraic

62 hierarchy of rings: integral domain.

64 <LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>

65 introduces the notion of a R-left-module over an Abelian group, where

66 R is a ring.

68 <LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>

69 constructs univariate polynomials over rings and integral domains.

70 Degree function. Universal Property.

71 </UL>

73 <H2>Legacy Development of Rings using Axiomatic Type Classes</H2>

75 <P>This development of univariate polynomials is separated into an

76 abstract development of rings and the development of polynomials

77 itself. The formalisation is based on [Jacobson1985], and polynomials

78 have a sparse, mathematical representation. These theories were

79 developed as a base for the integration of a computer algebra system

80 to Isabelle [Ballarin1999], and was designed to match implementations

81 of these domains in some typed computer algebra systems. Summary:

83 <P><EM>Rings:</EM>

84 Classes of rings are represented by axiomatic type classes. The

85 following are available:

87 <PRE>

88 ring: Commutative rings with one (including a summation

89 operator, which is needed for the polynomials)

90 domain: Integral domains

91 factorial: Factorial domains (divisor chain condition is missing)

92 pid: Principal ideal domains

93 field: Fields

94 </PRE>

96 Also, some facts about ring homomorphisms and ideals are mechanised.

98 <P><EM>Polynomials:</EM>

99 Polynomials have a natural, mathematical representation. Facts about

100 the following topics are provided:

102 <MENU>

103 <LI>Degree function

104 <LI> Universal Property, evaluation homomorphism

105 <LI>Long division (existence and uniqueness)

106 <LI>Polynomials over a ring form a ring

107 <LI>Polynomials over an integral domain form an integral domain

108 </MENU>

110 <P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.

112 <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,

113 Author's <A HREF="http://www4.in.tum.de/~ballarin/publications.html">PhD thesis</A>, 1999.

115 <HR>

116 <P>Last modified on $Date$

118 <ADDRESS>

119 <P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.

120 </ADDRESS>

121 </BODY>

122 </HTML>