Re: [isabelle] lift_definition + constructor
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. You haven't mentioned code generation, but if you are interested,
I'd be happy to explain the details.
On 13/12/13 15:17, Walther Neuper wrote:
thanks for your hints !
In the course of general considerations  we come back to this specific question:
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 polynomial representation
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 "pCons"?
I.e. a constructor like
datatype 'a pcons = Zero | pCons 'a "'a pcons"
could be somehow associated with lift_definition ? Or is this possible with
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 idea ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and