[isabelle] Ordinal of a datatype instantiated to enum




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.