[isabelle-dev] Polynomial theory

[Brian Huffman]

Quoting Tobias Nipkow <nipkow at in.tum.de>:

> The theory is certainly welcome. Ideally both concrete and abstract
> polynomials should be in the same place and should reference each other,
> to facilitate choice between the theories.
>
> What is the main advantage of abstract polynomials? That "=" is what you
> want it to be? And the main drawback? Non-executability?
>
> Thanks a lot!
> Tobias

Actually, I had executability in mind when creating this theory. A new  
feature, which is not present in the original HOL/Abstract/poly  
development, is the constructor function pCons :: 'a => 'a poly => 'a  
poly. It basically means the same thing as Cons in the list-based  
theory. For example, the polynomial x^2 + 2*x + 5 could be written as  
(pCons 5 (pCons 2 (pCons 1 0))). (It would also be easy to add some  
list-style syntax for pCons.)

Anyway, I think it would be easy to do code generation for these  
polynomials, using 0 and pCons as the constructors. All of the  
operations defined in the theory would be executable on this  
representation, including div and mod.

Here are some of the advantages of an abstract polynomial type:
   - "=" means what you want it to
   - "+", "-", "*", "0", "1", "dvd", "div", "mod", etc. mean what you  
want them to
   - no need to define a bunch of new operators (+++,***,--, divides,  
etc) and prove properties about them
   - type class instances give us lots of useful theorems automatically
   - proof automation via existing ring simprocs (e.g. cancellation)
   - can be made executable

The only disadvantage I can think of right now, compared to list-based  
polynomials, is that "length" is easier to reason about than "degree".  
However, this is probably just a matter of finding a good set of  
lemmas about "degree".

- Brian