[isabelle-dev] Polynomial theory
Brian Huffman
brianh at cs.pdx.edu
Mon Jan 12 14:44:10 CET 2009
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
More information about the isabelle-dev
mailing list