[isabelle-dev] Towards the next release

[Tobias Nipkow]

Am 12/04/2012 14:06, schrieb Lawrence Paulson:
> There is something I'd like to mention, not a big deal, but worth considering.
> 
> I've been doing some proofs lately after a long gap, making myself a combination of a novice and expert. And I've got confused by things that would probably confuse true novices even more.
> 
> Here are two instantiations, both of which simply do overloading but justify no properties. Such instantiations always succeed, because there is nothing to prove. But I discovered that you have to be very careful to introduce overloading correctly. If it's wrong, the instantiation effectively does nothing; when that happens, a warning ought to appear.
> 
> The overloading rules are quite tricky. I don't understand why the first instantiation requires a definition of sup_hf (including the type in the constant name), while the second one simply requires a definition of minus. Perhaps because there is an explicit type in the first instantiation and not on the second one? In any event, if the user gets wrong, a warning would be appropriate. And I hope that wouldn't be difficult to implement.
> 
> instantiation hf :: sup
> begin
> 
> definition sup_hf :: "hf \<Rightarrow> hf \<Rightarrow> hf"
>   where "sup_hf a b = ..."
> 
> instantiation hf :: minus
> begin
> definition minus_hf where
>   "minus A B = ...
> instance proof 
> 

Probably most users of locales have experienced this situation. I don't know if
it is easy to explain the rules or to improve the situation. I think that the
fully qualified name f_type always works (?) and one can then try to see if the
suffix can be dropped. I would be happy with that but one problem remains: if
you drop the suffix, I don't know how to tell if it "worked" except that your
instance proof fails for no clear reason if it did not work. That is my main
source of confusion.

Tobias

> Larry
> 
> On 12 Apr 2012, at 10:02, Makarius wrote:
> 
>> Dear all,
>>
>> we need to get to a more concrete release schedule.  Presently I would like to aim for late May, which means we need to start consolidating and converging about now.
>>
>> Are there any further big things in the pipeline?
>>
>> This is also a good point to populate NEWS, CONTRIBUTORS, and update manuals to cover new things.  (I am speaking to myself here as well.)
>>
>>
>> 	Makarius
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev