[isabelle-dev] Checked "assume" command

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