paulson@7998

1 
<! $Id$ >

paulson@7998

2 
<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>

paulson@7998

3 

ballarin@13949

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

ballarin@13949

5 

ballarin@13975

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

ballarin@13975

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

ballarin@13975

8 
reusability. This is achieved by modelling algebraic structures

ballarin@13975

9 
as firstclass citizens of the logic (not axiomatic type classes, say).

ballarin@13975

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

ballarin@13975

11 
Contributions are welcome.

ballarin@13949

12 

ballarin@13949

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

ballarin@13949

14 

ballarin@13949

15 
<P>These proofs are mainly by Florian Kammüller. (Later, Larry

ballarin@13949

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

ballarin@13949

17 
the original motivation for locales.

ballarin@13949

18 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

21 
groups, commutative monoids, commutative groups, homomorphisms and the

ballarin@13949

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

ballarin@13949

23 
(This theory was reimplemented by Clemens Ballarin).

ballarin@13949

24 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

27 
Clemens Ballarin).

ballarin@13949

28 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

31 
subgroup is a group.

ballarin@13949

32 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

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

ballarin@13949

36 

ballarin@13949

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

ballarin@13949

38 
combinatorial argument underlying Sylow's first theorem.

ballarin@13949

39 

ballarin@13949

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

ballarin@13949

41 
contains a proof of the first Sylow theorem.

ballarin@13949

42 
</UL>

ballarin@13949

43 

ballarin@13949

44 
<H2>Rings and Polynomials</H2>

ballarin@13949

45 

ballarin@13949

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

ballarin@13949

47 
defines Abelian monoids and groups. The difference to commutative

ballarin@13949

48 
structures is merely notational: the binary operation is

ballarin@13949

49 
addition rather than multiplication. Commutative rings are

ballarin@13949

50 
obtained by inheriting properties from Abelian groups and

ballarin@13949

51 
commutative monoids. Further structures in the algebraic

ballarin@13949

52 
hierarchy of rings: integral domain.

ballarin@13949

53 

ballarin@13949

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

ballarin@13949

55 
introduces the notion of a Rleftmodule over an Abelian group, where

ballarin@13949

56 
R is a ring.

ballarin@13949

57 

ballarin@13949

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

ballarin@13949

59 
constructs univariate polynomials over rings and integral domains.

ballarin@13949

60 
Degree function. Universal Property.

ballarin@13949

61 
</UL>

ballarin@13949

62 

ballarin@13949

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

paulson@7998

64 

paulson@7998

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

paulson@7998

66 
abstract development of rings and the development of polynomials

paulson@7998

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

paulson@7998

68 
have a sparse, mathematical representation. These theories were

paulson@7998

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

paulson@7998

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

paulson@7998

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

paulson@7998

72 

paulson@7998

73 
<P><EM>Rings:</EM>

paulson@7998

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

paulson@7998

75 
following are available:

paulson@7998

76 

paulson@7998

77 
<PRE>

paulson@7998

78 
ring: Commutative rings with one (including a summation

paulson@7998

79 
operator, which is needed for the polynomials)

paulson@7998

80 
domain: Integral domains

paulson@7998

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

paulson@7998

82 
pid: Principal ideal domains

paulson@7998

83 
field: Fields

paulson@7998

84 
</PRE>

paulson@7998

85 

paulson@7998

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

paulson@7998

87 

paulson@7998

88 
<P><EM>Polynomials:</EM>

paulson@7998

89 
Polynomials have a natural, mathematical representation. Facts about

paulson@7998

90 
the following topics are provided:

paulson@7998

91 

paulson@7998

92 
<MENU>

paulson@7998

93 
<LI>Degree function

paulson@7998

94 
<LI> Universal Property, evaluation homomorphism

paulson@7998

95 
<LI>Long division (existence and uniqueness)

paulson@7998

96 
<LI>Polynomials over a ring form a ring

paulson@7998

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

paulson@7998

98 
</MENU>

paulson@7998

99 

paulson@7998

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

paulson@7998

101 

paulson@7998

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

ballarin@13949

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

paulson@13944

104 

paulson@7998

105 
<HR>

paulson@7998

106 
<P>Last modified on $Date$

paulson@7998

107 

paulson@7998

108 
<ADDRESS>

ballarin@13949

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

paulson@7998

110 
</ADDRESS>

paulson@7998

111 
</BODY></HTML>
