[isabelle-dev] Towards the next release
nipkow at in.tum.de
Sun Apr 15 17:59:35 CEST 2012
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
> definition sup_hf :: "hf \<Rightarrow> hf \<Rightarrow> hf"
> where "sup_hf a b = ..."
> instantiation hf :: minus
> 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.
> 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.)
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev