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



Hi Again,

After successfully includes an "ordinal" operation for datatypes instantiating enum, I have included the reverse operation "data", which gives a datatype from an natural in case the given natural is within the datatype range. So I have extended the index class adding the new data operation fixes data :: "nat ⇒ 'a option" and the following assumption type_conv_ordinal: "data (ordinal (x)) = Some x".  

The problem comes when I am instantiating some datatype to index. When proving the assumption, which apparently can be done well "by auto", well using "by (simp_all add: ordinal_conv_index data_my_data_def  enum_UNIV)". For this instantiation

instantiation my_data:: index
begin
definition
"index_class.ordinal (a::my_data) ≡  index enum_class.enum a"

definition
"index_class.data (n::nat) ≡  
                                if n < size (enum_class.enum::(my_data list)) 
                                    then Some (nth  enum_class.enum  n)::(my_data option)
                                    else None::(my_data option)"

instance proof
  fix m::my_data
  show "index_class.ordinal m = index enum_class.enum m"  by (simp_all add: ordinal_my_data_def)
  show "data (ordinal (m)) = Some m" by (simp_all add: ordinal_conv_index data_my_data_def  enum_UNIV)
  qed
end

Although the proof finishes well, the second "show" is marked with a forbid symbol and "by (simp_all add: ordinal_conv_index data_my_data_def  enum_UNIV)" is red highlighted and the output shows the following:

show data (ordinal m) = Some m 
Successful attempt to solve goal by exported rule:
  data (ordinal ?m2) = Some ?m2 
proof (state): step 6

this:
  data (ordinal m) = Some m

goal:
No subgoals! 
Failed to finish proof:
goal (1 subgoal):
data (ordinal m) = Some m
 1. (ordinal m < length enum_class.enum ⟶ enum_class.enum ! ordinal m = m) ∧ ordinal m < length enum_class.enum

why is this happening? 

The whole index class and the instantiation are below. 

Thanks and best regards,
David.

class index = enum +
fixes ordinal :: "'a ⇒ nat"
fixes data :: "nat ⇒ 'a option"
assumes ordinal_conv_index: "ordinal m = index enum_class.enum m"
and type_conv_ordinal: "data (ordinal (x)) = Some x"
end

datatype my_data = dat0
                  |dat1
                  |dat2

lemma 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: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

instantiation my_data:: index
begin
definition
"index_class.ordinal (a::my_data) ≡  index enum_class.enum a"

definition
"index_class.data (n::nat) ≡  
                                if n < size (enum_class.enum::(my_data list)) 
                                    then Some (nth  enum_class.enum  n)::(my_data option)
                                    else None::(my_data option)"

instance proof
  fix m::my_data
  show "index_class.ordinal m = index enum_class.enum m"  by (simp_all add: ordinal_my_data_def)
  show "data (ordinal (m)) = Some m" by auto
  qed
end


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

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