Re: [Isarmathlib-devel] Re: Polynomial ring

[Slawomir Kolodynski]

Seo,

Couple of remarks on your first version:

I would use TheNeutralElement(R,A) instead of Z in
your definition of the set of of polynomials over R. 
Something like:

definition
"PolynomialsOver(R,A) \<equiv> 
{x \<in> nat -> R . HasAmaximum(Le, {n \<in> nat. x(n)
\<noteq> TheNeutralElement(R,A)}"

This is not very important, but it is a little closer
to what we think polynomials are.

I suggest you consider defining polynomial addition as
a restriction of the lift of the addition to the set
of polynomials. The lift of the addition to a function
space over nat is the pointwise addition of infinite
sequences, then you restrict it to the subset of
polynomials. Something like

definition
"PolynomialAddition(R,A) \<equiv>
restrict(A {lifted to function space over} nat,
PolynomialsOver(R,A)\<times>PolynomialsOver(R,A))"

This should make it easier to show that polynomials
form a group.

See func_ZF.thy for about lifting and restricting of
associative and commutative operations.
More remarks later.

Slawek 

This will make it easier to show that polynomials form
a group.



http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)