[isabelle] HOL/../Polynomial + afp/../Polynomial

In the Isabelle2013-1 distribution there is a new type of multi-variate polynomial [1], which is the basis for proving the Fundamental Theorem of Algebra etc. In addition to providing algebraic structure, the executable version of [1] corresponds to a _recursive_ representation.

In the AFP is another type of executable multi-variate polynomial [2] in _distributive_ representation. This specific representation is required for specific algorithms, for instance, the Groebner Bases algorithm.

After promising trials with both, [1] and [2], we envisage to develop theories for algebraic geometry including efficient polynomial algorithms --- and we have many, many questions. The first question is, what we consider the most principal one:

(a) given a type of multi-variate polynomial providing algebraic structure (like [1]) with new properties added (b) given several executable representations for polynomials, at least recursive (like "pCons" in [1]) and distributive (like "monom list" in [2]) with respective conversions ? What is the most succinct way to share the properties from (a) with several representations (b) in Isabelle (such that generated code "inherits" properties from (a)) ?

We are grateful for any input and prepared for not-so-easy suggestions,

[1] http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Polynomial.html
[2] http://afp.sourceforge.net/entries/Polynomials.shtml
[3] http://isabelle.in.tum.de/dist/library/HOL/HOL-Decision_Procs/Reflected_Multivariate_Polynomial.html

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.