7998

1 
<! $Id$ >


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


3 


4 
<H2>Algebra: Theories of Rings and Polynomials</H2>


5 


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


7 
abstract development of rings and the development of polynomials


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


9 
have a sparse, mathematical representation. These theories were


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


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


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


13 


14 
<P><EM>Rings:</EM>


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


16 
following are available:


17 


18 
<PRE>


19 
ringS: Syntactic class


20 
ring: Commutative rings with one (including a summation


21 
operator, which is needed for the polynomials)


22 
domain: Integral domains


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


24 
pid: Principal ideal domains


25 
field: Fields


26 
</PRE>


27 


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


29 


30 
<P><EM>Polynomials:</EM>


31 
Polynomials have a natural, mathematical representation. Facts about


32 
the following topics are provided:


33 


34 
<MENU>


35 
<LI>Degree function


36 
<LI> Universal Property, evaluation homomorphism


37 
<LI>Long division (existence and uniqueness)


38 
<LI>Polynomials over a ring form a ring


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


40 
</MENU>


41 


42 
<P>Still missing are


43 
Polynomials over a factorial domain form a factorial domain


44 
(difficult), and polynomials over a field form a pid.


45 


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


47 


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


49 
Author's <A HREF="http://iakswww.ira.uka.de/iakscalmet/ballarin/publications.html">PhD thesis</A>, 1999.


50 

13944

51 
<H2>GroupTheory  Group Theory using Locales, including Sylow's Theorem</H2>


52 


53 
<P>This directory presents proofs about group theory, by


54 
Florian Kammüller. (Later, Larry Paulson simplified some of the proofs.)


55 
These theories use locales and were indeed the original motivation for


56 
locales. However, this treatment of groups must still be regarded as


57 
experimental. We can expect to see refinements in the future.


58 


59 
Here is an outline of the directory's contents:


60 


61 
<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines


62 
semigroups, groups, homomorphisms and the subgroup relation. It also defines


63 
the product of two groups. It defines the factorization of a group and shows


64 
that the factorization a normal subgroup is a group.


65 


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


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


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


69 


70 
<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves


71 
a few basic theorems. Ring automorphisms are shown to form a group.


72 


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


74 
contains a proof of the first Sylow theorem.


75 


76 
<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends


77 
abelian groups by a summation operator for finite sets (provided by


78 
Clemens Ballarin).


79 
</UL>


80 

7998

81 
<HR>


82 
<P>Last modified on $Date$


83 


84 
<ADDRESS>


85 
<P><A HREF="http://iakswww.ira.uka.de/iakscalmet/ballarin">Clemens Ballarin</A>. Karlsruhe, October 1999


86 


87 
<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>


88 
</ADDRESS>


89 
</BODY></HTML>
