[isabelle-dev] Polynomial theory

[Brian Huffman]

Quoting Amine Chaieb <ac638 at cam.ac.uk>:
>> 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?

I just meant using a typedef, something like

typedef 'a poly = "{f :: 'a fps. finite_fps f}"

Then the operations like addition, multiplication, etc. could be  
defined in terms of the underlying fps operations like this

definition
   "p * q = Abs_poly (Rep_poly p * Rep_poly q)"

Then the transfer of theorems from fps (like, say, associativity of  
multiplication) would not be automatic, but they would be really easy  
proofs.

- Brian