paulson@7998

1 
<! $Id$ >

paulson@7998

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

paulson@7998

3 

paulson@7998

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

paulson@7998

5 

paulson@7998

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

paulson@7998

7 
abstract development of rings and the development of polynomials

paulson@7998

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

paulson@7998

9 
have a sparse, mathematical representation. These theories were

paulson@7998

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

paulson@7998

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

paulson@7998

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

paulson@7998

13 

paulson@7998

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

paulson@7998

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

paulson@7998

16 
following are available:

paulson@7998

17 

paulson@7998

18 
<PRE>

paulson@7998

19 
ringS: Syntactic class

paulson@7998

20 
ring: Commutative rings with one (including a summation

paulson@7998

21 
operator, which is needed for the polynomials)

paulson@7998

22 
domain: Integral domains

paulson@7998

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

paulson@7998

24 
pid: Principal ideal domains

paulson@7998

25 
field: Fields

paulson@7998

26 
</PRE>

paulson@7998

27 

paulson@7998

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

paulson@7998

29 

paulson@7998

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

paulson@7998

31 
Polynomials have a natural, mathematical representation. Facts about

paulson@7998

32 
the following topics are provided:

paulson@7998

33 

paulson@7998

34 
<MENU>

paulson@7998

35 
<LI>Degree function

paulson@7998

36 
<LI> Universal Property, evaluation homomorphism

paulson@7998

37 
<LI>Long division (existence and uniqueness)

paulson@7998

38 
<LI>Polynomials over a ring form a ring

paulson@7998

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

paulson@7998

40 
</MENU>

paulson@7998

41 

paulson@7998

42 
<P>Still missing are

paulson@7998

43 
Polynomials over a factorial domain form a factorial domain

paulson@7998

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

paulson@7998

45 

paulson@7998

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

paulson@7998

47 

paulson@7998

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

paulson@7998

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

paulson@7998

50 

paulson@7998

51 
<HR>

paulson@7998

52 
<P>Last modified on $Date$

paulson@7998

53 

paulson@7998

54 
<ADDRESS>

paulson@7998

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

paulson@7998

56 

paulson@7998

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

paulson@7998

58 
</ADDRESS>

paulson@7998

59 
</BODY></HTML>
