author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 15582  7219facb3fd0 
child 35849  b5522b51cb1e 
permissions  rwrr 
15283  1 
<!DOCTYPE HTML PUBLIC "//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> 
2 

7998  3 
<! $Id$ > 
15582  4 

5 
<HTML> 

6 

7 
<HEAD> 

8 
<meta httpequiv="contenttype" content="text/html;charset=iso88591"> 

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

10 
</HEAD> 

11 

12 
<BODY> 

7998  13 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

14 
<H1>Algebra  Classical Algebra, using Explicit Structures and Locales</H1> 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

15 

13975  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 firstclass 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. 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

22 

0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

23 
<H2>GroupTheory, including Sylow's Theorem</H2> 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

24 

15283  25 
<P>These proofs are mainly by Florian Kammller. (Later, Larry 
13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

26 
Paulson simplified some of the proofs.) These theories were indeed 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

27 
the original motivation for locales. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

28 

0ce528cd6f19
HOLAlgebra 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
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

30 
HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids, 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

31 
groups, commutative monoids, commutative groups, homomorphisms and the 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

32 
subgroup relation. It also defines the product of two groups 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

33 
(This theory was reimplemented by Clemens Ballarin). 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

34 

0ce528cd6f19
HOLAlgebra 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
HOLAlgebra 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
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

37 
Clemens Ballarin). 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

38 

0ce528cd6f19
HOLAlgebra 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
HOLAlgebra 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
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

41 
subgroup is a group. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

42 

0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

43 
<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A> 
0ce528cd6f19
HOLAlgebra 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
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

45 
are a group. It shows that automorphisms form a group. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

46 

0ce528cd6f19
HOLAlgebra 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
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

48 
combinatorial argument underlying Sylow's first theorem. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

49 

0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

50 
<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A> 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

51 
contains a proof of the first Sylow theorem. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

52 
</UL> 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

53 

0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

54 
<H2>Rings and Polynomials</H2> 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

55 

0ce528cd6f19
HOLAlgebra 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
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

57 
defines Abelian monoids and groups. The difference to commutative 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

58 
structures is merely notational: the binary operation is 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

59 
addition rather than multiplication. Commutative rings are 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

60 
obtained by inheriting properties from Abelian groups and 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

61 
commutative monoids. Further structures in the algebraic 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

62 
hierarchy of rings: integral domain. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

63 

0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

64 
<LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A> 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

65 
introduces the notion of a Rleftmodule over an Abelian group, where 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

66 
R is a ring. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

67 

0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

68 
<LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A> 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

69 
constructs univariate polynomials over rings and integral domains. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

70 
Degree function. Universal Property. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

71 
</UL> 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

72 

0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

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

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: 

82 

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

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

85 
following are available: 

86 

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> 

95 

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

97 

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

99 
Polynomials have a natural, mathematical representation. Facts about 

100 
the following topics are provided: 

101 

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> 

109 

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

111 

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

13949
0ce528cd6f19
HOLAlgebra 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  114 

7998  115 
<HR> 
116 
<P>Last modified on $Date$ 

117 

118 
<ADDRESS> 

13949
0ce528cd6f19
HOLAlgebra 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  120 
</ADDRESS> 
15582  121 
</BODY> 
122 
</HTML> 