*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Ordinal of a datatype instantiated to enum*From*: David Sanán <sananbad at scss.tcd.ie>*Date*: Mon, 22 Jul 2013 13:24:37 +0100*Cc*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51E7C59E.50607@inf.ethz.ch>*References*: <6c92270f8c7fe0cd027617b8eb06d183@scss.tcd.ie> <51E68378.4000605@inf.ethz.ch> <51E7BB27.4060603@informatik.tu-muenchen.de> <51E7C59E.50607@inf.ethz.ch>

Dear Andreas and Florian, Thanks for your valuables comment. I will follow your suggestions. Code generation is not an actual concern. However combining the use of Tobia's index and Florian suggestion assumes "n < length (Enum.enum :: 'a list) ==> (Enum.enum ! ordinal x) = x" would release the needed to prove manually the instantiation "ordinal dat0 = 0" "ordinal dat1 = 1" "ordinal dat2 = 2" ... am I right? Before reading your last posts I had already tried to prove "n < length (Enum.enum :: 'a list) ==> (Enum.enum ! ordinal x) = x" in a general function (not within an instantiation), but I could not (I need more experience!). I will try with instantiations then. Thanks again and best regards, David. On 18 Jul 2013, at 11:38, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: > Hi Florian and David, > > If code generation is a concern, Florian is right: a separate type class with the index operation is preferable, because then, you can tailor the code equations for ordinal to every datatype you are using. If you use large datatypes, I expect that this will improve the run-time considerably. However, I did not see from the original post that code generation was intended (although the enum class mainly serves for code generation). > > However, even then, I suggest to build on Tobias' AFP entry as follows: > > class index = enum + > fixes ordinal :: "'a => nat" > assumes ordinal_conv_index: "ordinal = index enum_class.enum" > > As ordinal is fully specified, the assumption of the type class can directly be definitional. (You can even start working with "index enum_class.enum" directly and later on introduce such a type class for code generation, but that leads too far here. > > Best, > Andreas > > > On 18/07/13 11:53, Florian Haftmann wrote: >>> "ordinal x = >>> (THE i. i < length (enum_class.enum :: 'a list) & enum_class.enum !! i >>> = x)" >> >>> but that won't be fun to work with. The entry List_Index in the Archive >>> of Formal Proofs (http://afp.sourceforge.net/entries/List-Index.shtml), >>> however, defines a function index such that "ordinal = index >>> enum_class.enum". That should fit your purpose. >> >> An alternative could be: >> >> class index = enum + >> fixes ordinal :: "'a => nat" >> assumes "n < length (Enum.enum :: 'a list) ==> ordinal >> (Enum.enum ! n :: 'a) = n" >> assumes "n < length (Enum.enum :: 'a list) ==> (Enum.enum ! >> ordinal x) = x" -- {* disclaimer: not checked in Isabelle yet *} >> >> I.e. the THE-definition of ordinal is absorbed into a constructive type >> class. This leaves you still to provided reasonable instance >> definitions for ordinal for each instance type, but this might turn out >> simple if you have a look at the corresponding Enum.enum instances. >> >> Practice shows which approach is more appropriate. >> >> Cheers, >> Florian >> >

**Follow-Ups**:**Re: [isabelle] Ordinal of a datatype instantiated to enum***From:*David Sanán

**References**:**[isabelle] Ordinal of a datatype instantiated to enum***From:*David Sanan

**Re: [isabelle] Ordinal of a datatype instantiated to enum***From:*Andreas Lochbihler

**Re: [isabelle] Ordinal of a datatype instantiated to enum***From:*Florian Haftmann

**Re: [isabelle] Ordinal of a datatype instantiated to enum***From:*Andreas Lochbihler

- Previous by Date: [isabelle] set length of Output buffer
- Next by Date: Re: [isabelle] Ordinal of a datatype instantiated to enum
- Previous by Thread: Re: [isabelle] Ordinal of a datatype instantiated to enum
- Next by Thread: Re: [isabelle] Ordinal of a datatype instantiated to enum
- Cl-isabelle-users July 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