*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Ordinal of a datatype instantiated to enum*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 18 Jul 2013 12:38:22 +0200*Cc*: sananbad at scss.tcd.ie, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51E7BB27.4060603@informatik.tu-muenchen.de>*References*: <6c92270f8c7fe0cd027617b8eb06d183@scss.tcd.ie> <51E68378.4000605@inf.ethz.ch> <51E7BB27.4060603@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

Hi Florian and David,

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"

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

- Previous by Date: Re: [isabelle] Scala code generator: how to write code generated from Isabelle library dependencies to a shared package?
- Next by Date: [isabelle] Unable to prove easy existential "directly"
- 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