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

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.


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 (,
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.


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