[isabelle-dev] Checked "assume" command

[Tobias Nipkow]

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

Tobias