[isabelle-dev] Checked "assume" command

[Tobias Nipkow]

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