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



I partially answer myself...

The proof was not already done (or was it?)although it said there was not any subgoals left and there was no error in the end of the instance proof... Instead of using "by" I have used "apply" and now the proof steps look clearer to me. 

Finally I have solved it just adding another definition to the simplification method and the final proof is:

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: data_my_data_def ordinal_my_data_def enum_UNIV)  
 qed
end

However, shouldn't the whole instance proof be marked as incomplete (that is the end of the proof should not be clear) in my first attempt?

Also If I remove the definition "data_my_data_def" from the simplification I have:

Successful attempt to solve goal by exported rule:
  data (ordinal ?m2) = Some ?m2 
Failed to finish proof:
goal (1 subgoal):
data (ordinal m) = Some m
 1. data (index enum_class.enum m) = Some m 
proof (state): step 6

this:
  data (ordinal m) = Some m

goal:
No subgoals!

Does it means that the proof is done??? It seems so to me, but when I try to build the model I have:

Failed to finish proof (line 210 of "List-Index/List_Index.thy"):
*** goal (1 subgoal):
*** data (ordinal m) = Some m
***  1. data (index enum_class.enum m) = Some m
*** At command "by" (line 210 of "List-Index/List_Index.thy")


Thanks and regards,
David.

On 27 Aug 2013, at 15:08, David Sanán <sananbad at scss.tcd.ie> wrote:

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