[isabelle-dev] Polynomial theory

[Tobias Nipkow]

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

Brian Huffman schrieb:
> Hi all,
> 
> Recently I was inspired by Mark Janney's comments on the Isabelle users
> list to finish up the polynomial theory that started working on a while
> ago. Basically, it is a heavily-reworked version of Clemens Ballarin's
> theories from HOL/Abstract/poly in the distribution. It includes most of
> the same operations: coefficients, monomials, degree, scalar
> multiplication, and all the ring operations. It also includes
> definitions for div and mod, and is fully integrated with the HOL
> algebraic type class hierarchy.
> 
> If there are no objections, I would like to add this theory to the main
> Isabelle/HOL source directory. Since the main HOL image already includes
> a list-based formalization of polynomials (Univ_Poly.thy), I think that
> a formalization using a real type constructor would be an improvement;
> it probably wouldn't be too hard to adapt the other theories to use the
> new polynomial type instead.
> 
> The source file is attached (it will probably only work with the
> development snapshot).
> 
> - Brian
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev