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



I reply to myself, 
Just defining the class and with the assumption "ordinal = index enum_class.enum" datatype instantiations are straightforward using definitions.

Thanks and best regards,
David.

On 22 Jul 2013, at 13:24, David Sanán <sananbad at scss.tcd.ie> wrote:

> Dear Andreas and Florian,
> 
> Thanks for your valuables comment. I will follow your suggestions. 
> 
> Code generation is not an actual concern. However combining the use of Tobia's index and Florian suggestion 
> 
> assumes "n < length (Enum.enum :: 'a list) ==> (Enum.enum ! ordinal x) = x"
> 
> would release the needed to prove manually the instantiation "ordinal dat0 = 0" "ordinal dat1 = 1" "ordinal dat2 = 2" ...  am I right?
> 
> Before reading your last posts I had already tried to prove "n < length (Enum.enum :: 'a list) ==> (Enum.enum ! ordinal x) = x" in a general function (not within an instantiation), but I could not (I need more experience!). I will try with instantiations then. 
> 
> Thanks again and best regards,
> David.
> 
> On 18 Jul 2013, at 11:38, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
> 
>> 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.
>> 
>> Best,
>> Andreas
>> 
>> 
>> 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 (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
>>> 
>> 
> 





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