Am 07/09/2012 16:51, schrieb Makarius: > On Thu, 6 Sep 2012, Tobias Nipkow wrote: > >> Am 05/09/2012 15:46, schrieb Makarius: >>> On Wed, 5 Sep 2012, Lars Noschinski wrote: >>> >>>> As far as I can see, the only way to issue a successful "show" after a >>>> wrong >>>> assumption (or, if you prefer, an "assumption which does not fit any of the >>>> pending goals") is discarding everything with "next". So, I don't see >>>> anything useful which can be achived without the check, but cannot with >>>> this >>>> check. If I just want to experiment, I can open another block. >>>> >>>> Also, this change gives an fail-early property, which is useful when >>>> maintaining proofs. >>> >>> Formally, I can just put this on my stack of things to be revisited >>> eventually. >>> >>> What I need is to watch over the shoulders of more people trying to write >>> Isar proofs in the current Prover IDE. In May this year I had 15 people and >>> 2 days to get some impressions where to continue next. >> >> I don't understand this empirical approach and the IDE angle. > > As Larry has rightly pointed out, fresh users are particularly helpful in > getting to the actual problems quickly, because they just try to use the > system > without any prejudice how it should behave.
A frequent experience from user-land: novices are quite surprised that one can assume propositions that are not in any context. Telling them that this is how Isar works is not a convincing answer. Power users are surprised no more. > Power users are much more > challanging, because they already have fixed models in their head how things > should work. So in the second case one needs to spend extra efforts to get to > the actual issues behind the surface, when someone says how he thinks the > system > should work. > > >> You don't dispute that the proofs that Lars' check rejects cannot be >> completed >> without modifying the assumption in question? So what is the potential gain >> of >> not telling the user about it? Over the past decade I have frequently been in >> this situation and have always regarded the absence of such a check as an >> annoyance. > > I did not get as far as dissecting the proposal, because it was formally > invalid. It was in conflict with the published, documented and implemented > Isar/VM semantics, which is two levels more sophisticated than it seems: one > to > make it work, and another to make it look simple. > > Already many years ago, I had to shut down any attempt to modify the workings > of > the Isar proof engine by users. A sophisticated language cannot be designed > and > maintained like that. If I had followed only half of the suggestions over the > past few years, not much the the language would be left now. > > So in order to avoid wasting energy by everybody involved, any proposals to > change the Isar proof language (especially Isar/proof.ML) are syntactically > malformed by definition. This is the ultimate cop out. Moreover, you may note that I was not asking you to change Isar, I was asking (search for "?") if my understanding of Isar is correct and what the rational is. Tobias > > This does not mean that there couldn't be exchange of experience on > isabelle-users, about how Isar proofs work and how things can be accomplished > elegantly with it, or which traps need to be avoided. > > > Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
