Brian Huffman wrote:
> 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.
OK, that sound reasonable. I was thinking of that + a very simple tactic
to transfer the important theorems after a basic set of theorems about
conserving "finiteness". I will try that in my theory as soon as I can.
I was hoping that there is a way not to introduce a new type, and that
for once HOL behaves as nice as set-theory. But I should give up the
latter anyway...
Amine.
