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 >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
