Re: [isabelle] Ordinal of a datatype instantiated to enum



Hi David,

From what you write, I guess that you want to have an operation ordinal :: 'a :: enum => nat such that "ordinal x" returns the position of x in the enumeration list enum_class.enum.

I am not aware of any pre-defined setup for this use case in the Isabelle/HOL library. You can of course define

"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.

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.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.