[isabelle-dev] Polynomial theory
brianh at cs.pdx.edu
Sun Jan 11 17:40:34 CET 2009
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!
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".
More information about the isabelle-dev