[isabelle-dev] Polynomial theory

Amine Chaieb ac638 at cam.ac.uk
Mon Jan 12 16:56:22 CET 2009

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...


More information about the isabelle-dev mailing list