[isabelle] HOL/../Polynomial + afp/../Polynomial
In the Isabelle2013-1 distribution there is a new type of multi-variate
polynomial , which is the basis for proving the Fundamental Theorem
of Algebra etc. In addition to providing algebraic structure, the
executable version of  corresponds to a _recursive_ representation.
In the AFP is another type of executable multi-variate polynomial  in
_distributive_ representation. This specific representation is required
for specific algorithms, for instance, the Groebner Bases algorithm.
After promising trials with both,  and , 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 ) with new properties added
(b) given several executable representations for polynomials, at least
recursive (like "pCons" in ) and distributive (like "monom list" in
) 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and