webertj@15283

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

webertj@15283

2 

webertj@15582

3 
<HTML>

webertj@15582

4 

webertj@15582

5 
<HEAD>

webertj@15582

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

webertj@15582

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

webertj@15582

8 
</HEAD>

webertj@15582

9 

webertj@15582

10 
<BODY>

paulson@7998

11 

ballarin@13949

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

ballarin@13949

13 

ballarin@13975

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

ballarin@13975

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

ballarin@13975

16 
reusability. This is achieved by modelling algebraic structures

ballarin@13975

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

ballarin@13975

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

ballarin@13975

19 
Contributions are welcome.

ballarin@13949

20 

ballarin@13949

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

ballarin@13949

22 

blanchet@37435

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

ballarin@13949

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

ballarin@13949

25 
the original motivation for locales.

ballarin@13949

26 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

29 
groups, commutative monoids, commutative groups, homomorphisms and the

ballarin@13949

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

ballarin@13949

31 
(This theory was reimplemented by Clemens Ballarin).

ballarin@13949

32 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

35 
Clemens Ballarin).

ballarin@13949

36 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

39 
subgroup is a group.

ballarin@13949

40 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

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

ballarin@13949

44 

ballarin@13949

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

ballarin@13949

46 
combinatorial argument underlying Sylow's first theorem.

ballarin@13949

47 

ballarin@13949

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

ballarin@13949

49 
contains a proof of the first Sylow theorem.

ballarin@13949

50 
</UL>

ballarin@13949

51 

ballarin@13949

52 
<H2>Rings and Polynomials</H2>

ballarin@13949

53 

ballarin@51516

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

ballarin@13949

55 
defines Abelian monoids and groups. The difference to commutative

ballarin@13949

56 
structures is merely notational: the binary operation is

ballarin@13949

57 
addition rather than multiplication. Commutative rings are

ballarin@13949

58 
obtained by inheriting properties from Abelian groups and

ballarin@13949

59 
commutative monoids. Further structures in the algebraic

ballarin@13949

60 
hierarchy of rings: integral domain.

ballarin@13949

61 

ballarin@13949

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

ballarin@13949

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

ballarin@13949

64 
R is a ring.

ballarin@13949

65 

ballarin@13949

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

ballarin@13949

67 
constructs univariate polynomials over rings and integral domains.

ballarin@13949

68 
Degree function. Universal Property.

ballarin@13949

69 
</UL>

ballarin@13949

70 

ballarin@13949

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

paulson@7998

72 

paulson@7998

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

paulson@7998

74 
abstract development of rings and the development of polynomials

paulson@7998

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

paulson@7998

76 
have a sparse, mathematical representation. These theories were

paulson@7998

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

paulson@7998

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

paulson@7998

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

paulson@7998

80 

paulson@7998

81 
<P><EM>Rings:</EM>

paulson@7998

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

paulson@7998

83 
following are available:

paulson@7998

84 

paulson@7998

85 
<PRE>

paulson@7998

86 
ring: Commutative rings with one (including a summation

paulson@7998

87 
operator, which is needed for the polynomials)

paulson@7998

88 
domain: Integral domains

paulson@7998

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

paulson@7998

90 
pid: Principal ideal domains

paulson@7998

91 
field: Fields

paulson@7998

92 
</PRE>

paulson@7998

93 

paulson@7998

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

paulson@7998

95 

paulson@7998

96 
<P><EM>Polynomials:</EM>

paulson@7998

97 
Polynomials have a natural, mathematical representation. Facts about

paulson@7998

98 
the following topics are provided:

paulson@7998

99 

paulson@7998

100 
<MENU>

paulson@7998

101 
<LI>Degree function

paulson@7998

102 
<LI> Universal Property, evaluation homomorphism

paulson@7998

103 
<LI>Long division (existence and uniqueness)

paulson@7998

104 
<LI>Polynomials over a ring form a ring

paulson@7998

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

paulson@7998

106 
</MENU>

paulson@7998

107 

paulson@7998

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

paulson@7998

109 

paulson@7998

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

ballarin@51516

111 
Author's PhD thesis, 1999. Also University of Cambridge, Computer Laboratory Technical Report number 473.

paulson@13944

112 

paulson@7998

113 
<ADDRESS>

ballarin@51516

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

paulson@7998

115 
</ADDRESS>

webertj@15582

116 
</BODY>

webertj@15582

117 
</HTML>
