*To*: David Sanan <sananbad at scss.tcd.ie>*Subject*: Re: [isabelle] Ordinal of a datatype instantiated to enum*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 17 Jul 2013 13:43:52 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <6c92270f8c7fe0cd027617b8eb06d183@scss.tcd.ie>*References*: <6c92270f8c7fe0cd027617b8eb06d183@scss.tcd.ie>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

Hi David,

"ordinal x = (THE i. i < length (enum_class.enum :: 'a list) & enum_class.enum !! i = x)"

You still have to prove the assignment manually for your instantiation, i.e., "ordinal dat0 = 0" "ordinal dat1 = 1" "ordinal dat2 = 2" but this will be automatic with index. Hope this helps, Andreas On 16/07/13 18:49, David Sanan wrote:

Dear all, I am starting with Isabelle and I am trying something I consider a basic thing but I can't see how to do it. From a datatype which I have instantiated to enum, I want to get the ordinal of an element as defined in the Enum.enum list. So if I define datatype my_data = dat0| dat1| dat2 lemma user_my_data_induct: "P dat0 <--> P dat1 ==> P dat2 ==> P x" by (cases x) auto lemma UNIV_my_data [no_atp]: "UNIV = { dat0, dat1, dat2}" apply (safe) apply (case_tac x) apply (auto intro:user_my_data_induct) done instantiation my_data :: enum begin definition "enum_my_data= [dat0, dat1, dat2]" definition "enum_all_my_data P <--> P dat0 /\ P dat1 /\ P dat2" definition "enum_ex_my_data P <--> P dat0 \/ P dat1 \/ P dat2" instance proof qed (simp_all only: enum_my_data_def enum_all_my_data_def enum_ex_my_data_def UNIV_my_data, simp_all) end I want to map dat0 to 0, dat1 to 1 ... Is there define any function for that? I have looking but I could not find anything. I can always create it, of course but I would like to know whether there is something for this or not. Thanks and best regards, David.

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

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

- Previous by Date: Re: [isabelle] Can't abbreviate ==> like I want; something to do with prop
- Next by Date: Re: [isabelle] Can't abbreviate ==> like I want; something to do with prop
- Previous by Thread: [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