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