Re: [Isarmathlib-devel] Re: Polynomial ring

[Slawomir Kolodynski]

After some thinking I have a clear idea on what the right approach to defining 
the polynomials is. The best way is to first write a small theory on finitely 
supported functions.

Support of a (monoid valued) function f: X -> G is the set 

definition
"Supp(f,G,A) = { x\<in> domain(f). f`(x) \<noteq> TheNeutralElement(G,A)"

Finitely supported functions are those functions (valued in a monoid) whose 
support is finite.

definition
"FinSuppFuncs(X,M.A) = {f\<in> X -> G. Supp(f,G,A) \<in> FinPow(X)}

Polynomials are a special case of finitely supprted functions.
"PolynomialsOver(R,A) = FinSuppFuncs(nat,R,A)

Finitely supported functions show up in the IsarMathLib's construction of real 
numbers. Namely (for an abelian group (G,A)) we say that f: G -> G is an almost 
homomorphism if the map (n,m) \mapsto f(n+m) - f(n) - f(m) is finitely 
supported. Almost homomorphisms form a group with the lifted (pointwise 
addition) operation and the set of finitely supported functions is a subgroup 
of this group. The (additive group of) real numbers is really constructed as 
the quotient group: (almost homomorphism)/(finitely supported functions), where 
the group G we start with is the group of integers.
This shows that the notion of finitely supported functions is useful and worth 
to have. 

On a different note I got some bounce notification from the Mailman site 
administrator. That means that some messages may not have reached some list 
members. Nabble.com provides a nice interface to isarmathlib-devel at 
http://www.nabble.com/isarmathlib-devel-f7722.html . This is good for checking 
if you got all messages.