*To*: Walther Neuper <wneuper at ist.tugraz.at>, Brian Huffman <huffman.brian.c at gmail.com>*Subject*: Re: [isabelle] lift_definition + constructor*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 16 Dec 2013 08:46:33 +0100*Cc*: Wolfgang Schreiner <Wolfgang.Schreiner at risc.uni-linz.ac.at>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <52AB170B.30206@ist.tugraz.at>*References*: <528BA694.1080607@ist.tugraz.at> <CAAMXsib76KFwk-WkaZb++yQp9oF6FJrT5qOCHVRr=Q-6rJpQiQ@mail.gmail.com> <52AB170B.30206@ist.tugraz.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.1

Walther,

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

**Follow-Ups**:**Re: [isabelle] lift_definition + constructor***From:*Walther Neuper

**References**:**Re: [isabelle] lift_definition + constructor***From:*Walther Neuper

- Previous by Date: Re: [isabelle] Announcing Isabelle2013-2
- Next by Date: Re: [isabelle] Announcing Isabelle2013-2
- Previous by Thread: Re: [isabelle] lift_definition + constructor
- Next by Thread: Re: [isabelle] lift_definition + constructor
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list