|
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://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999. |
|
50 |
|
51 <HR> |
|
52 <P>Last modified on $Date$ |
|
53 |
|
54 <ADDRESS> |
|
55 <P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>. Karlsruhe, October 1999 |
|
56 |
|
57 <A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A> |
|
58 </ADDRESS> |
|
59 </BODY></HTML> |