[isabelle-dev] Polynomial theory

[Amine Chaieb]

Brian Huffman wrote:

> For multivariate polynomials, one way to get these would be to simply
> iterate the univariate polynomial type constructor. For example, you
> can think of the type 'a poly poly as representing polynomials over
> two variables with coefficients in 'a.
>
Yes that's what I did with the list representation, but every thing is
outside the logic as soon as you want to reason about the different
variables etc...

> If you want something more general (maybe you want to reason about
> polynomials with an arbitrary number of variables) then maybe a monoid
> ring (http://en.wikipedia.org/wiki/Monoid_ring) would be a good
> generalization to use. This could be a type constructor with two
> parameters, one for the ring of coefficients, and one for the monoid
> of exponents. Then ('a, nat) monoid_ring would represent univariate
> polynomials, and ('a, 'b multiset) monoid_ring could represent
> multivariate polynomials, where 'b is a finite type indexing all of
> the indeterminate variables. I'm not sure why a Vectors theory would
> be necessary.

Not necessary, but they can be useful. One way to formalize multivariate
polynomials is to consider the (finite) vectors nat^'n, these formalize
the monomials (the elements of the vector are the powers of each
variable), a formalization of 'a['n] is then the set of all functions
p:: nat^'n => 'a such that ALL x. (ALL i: dimension of 'n. x_i > N) -->
p x = 0 for some N. The function p associates with each monomial a
coefficient.
Immediately we obtain 'a poly isomorphic to 'a[1].

> I have thought about formal power series as well, and I had noticed
> that many proofs about addition and multiplication are the same as
> with polynomials. I think it would be simple to define one in terms of
> the other. If you don't do it already, we would want to define 'a fps
> using a typedef, rather than as a type synonym. Then we could define
> addition, multiplication, etc. on 'a fps, and give instances for
> group, ring, and idom classes. 

All that and much more is done.

> Then we could define 'a poly as the subset of "finite" elements of 'a
> fps. We just need to prove that operations like addition and
> multiplication preserve the "finite" property, and we could inherit
> all of the other properties of those operations from 'a fps.
I am interested in what you say here. Do you think it is possible to
"define" (as you say above) without  construction a new type? or using
classes?

Best wishes,
Amine.