Re: [isabelle] lift_definition + constructor



Walther,

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.

Andreas

On 13/12/13 15:17, Walther Neuper wrote:
Brian,

thanks for your hints !
In the course of general considerations [1] 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 [2], could be lifted as well (establishing respective morphisms) by something like

    lift_definition dCons :: "..."
    is "..."


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
datatype_new ?
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 ?

Walther

[1] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00262.html
[2] http://afp.sourceforge.net/entries/Polynomials.shtml






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