Re: [isabelle] lift_definition + constructor



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.