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

Andreas, thanks for your kind offer ...

[...] You haven't mentioned code generation, but if you areinterested, I'd be happy to explain the details.

if you need pattern-matching only for code generation (e.g., to pickan efficient implementation), then that's still possible (to someextent) even if polynomials are not defined as a datatype.

datatype ('a, 'b) phantom = phantom 'b datatype poly_impl = Poly_IMPL definition poly_Recursive :: poly_impl where "poly_Recursive = Poly_IMPL"

class poly_impl = fixes poly_impl :: "('a, poly_impl) phantom" code_datatype poly_Recursive poly_Distrib_Sparse poly_Distrib_Sense

We are looking forward with great interest, how we can ...

Walther

[2] http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Polynomial.html [3] http://afp.sourceforge.net/entries/Collections.shtml On 12/16/2013 08:46 AM, Andreas Lochbihler wrote:

Walther,Let me comment a bit, even though I am not an expert on polynomials inIsabelle. The definition in HOL/Library/Polynomials gives you alogically unique representation for polynomials, i.e., if twopolynomials evaluate to the same at all points, then they are equal(in the sense of op =). Your construction with the datatype does notgive you this identity, i.e., you get a different type with differentproperties. Of course, you can do so on your own, but in my experienceredundancy in a type usually makes proving harder. Although you caninterpret a polynomial in one representation or in the other, thelogic 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 (tosome extent) even if polynomials are not defined as a datatype.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 thisspecific 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 distributivepolynomial representationlike [2], could be lifted as well (establishing respective morphisms)by something likelift_definition dCons :: "..." is "..."and then there is the question, how to distinguish between "pCons"and "dCons": patternmatching, 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 thispossible withdatatype_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 thelocation with respect tothe lift_definition --- do you find anything realisable about thisidea ?Walther[1]https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00262.html[2] http://afp.sourceforge.net/entries/Polynomials.shtml

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

**Re: [isabelle] lift_definition + constructor***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Missing transfer rules in quotient type
- Next by Date: Re: [isabelle] Missing transfer rules in quotient type
- Previous by Thread: Re: [isabelle] lift_definition + constructor
- Next by Thread: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE
- 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