Re: [isabelle] lift_definition + constructor
thanks for your kind offer ...
[...] You haven't mentioned code generation, but if you are
interested, I'd be happy to explain the details.
... because code generation is in our focus: we want to generate
algorithms from theories in algebraic geometry, while different
algorithms require different representations of polynomials for
efficiency reasons. So we are happy to hear ...
if you need pattern-matching only for code generation (e.g., to pick
an efficient implementation), then that's still possible (to some
extent) even if polynomials are not defined as a datatype.
... and in your paper  to find a quick guide to the following code
snippets derived from :
datatype ('a, 'b) phantom = phantom 'b
datatype poly_impl = Poly_IMPL
definition poly_Recursive :: poly_impl where "poly_Recursive = Poly_IMPL"
definition poly_Distrib_Sparse :: poly_impl where
"poly_Distrib_Sparse = Poly_IMPL"
definition poly_Distrib_Sense :: poly_impl where "poly_Distrib_Sense
class poly_impl =
fixes poly_impl :: "('a, poly_impl) phantom"
code_datatype poly_Recursive poly_Distrib_Sparse poly_Distrib_Sense
From now on we probably have to go another way: we need to choose
different representations not specific with respect to types, but
specific with respect to algorithms.
We are looking forward with great interest, how we can ...
* flexibly switch between representations of polynomials (probably even
within one single, but complex algorithm)
* derive properties for algorithms uniformly from a "logically unique
representation for polynomials" like 
... and are going to study your approach in detail. Any hints are
On 12/16/2013 08:46 AM, Andreas Lochbihler wrote:
Let me comment a bit, even though I am not an expert on polynomials in
Isabelle. The definition in HOL/Library/Polynomials gives you a
logically unique representation for polynomials, i.e., if two
polynomials evaluate to the same at all points, then they are equal
(in the sense of op =). Your construction with the datatype does not
give you this identity, i.e., you get a different type with different
properties. Of course, you can do so on your own, but in my experience
redundancy in a type usually makes proving harder. Although you can
interpret a polynomial in one representation or in the other, the
logic does not distinguish them and neither can you in your proofs.
However, if you need pattern-matching only for code generation (e.g.,
to pick an efficient implementation), then that's still possible (to
some extent) even if polynomials are not defined as a datatype.
On 13/12/13 15:17, Walther Neuper wrote:
thanks for your hints !
In the course of general considerations  we come back to this
On 11/19/2013 08:24 PM, Brian Huffman wrote:
On Tue, Nov 19, 2013 at 9:57 AM, Walther Neuper
<wneuper at ist.tugraz.at> wrote:
In Isabelle2013-1 in HOL/Library/Polynomial there is
lift_definition pCons :: "'a::zero => 'a poly => 'a poly"
is "λa p. nat_case a (coeff p)"
Other kinds of representations, for instance sparse distributive
like , could be lifted as well (establishing respective morphisms)
by something like
lift_definition dCons :: "..."
and then there is the question, how to distinguish between "pCons"
and "dCons": pattern
matching, for instance by ...
case p of
pCons _ => ...
| dCons _ => ...
... on constructors "pCons" and "dCons" was an idea ...
Is there a way to have a constructor "pCons" instead of function
I.e. a constructor like
datatype 'a pcons = Zero | pCons 'a "'a pcons"
could be somehow associated with lift_definition ? Or is this
What exactly do you mean by "constructor"? HOL doesn't have any
built-in logical distinction between constructors and other functions.
The signatures of pCons, dCons, etc are under question, also the
location with respect to
the lift_definition --- do you find anything realisable about this
This archive was generated by a fusion of
Pipermail (Mailman edition) and