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



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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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