[isabelle-dev] Checked "assume" command

[Lars Noschinski]

On 05.09.2012 13:24, Makarius wrote:
> On Tue, 4 Sep 2012, Lars Noschinski wrote:
>
>> As an user, an easy method to test whether the current set of
>> assumptions still fit one of the pending goals is "fix P show P
>> sorry". As I don't know any scenario where wrong assumptions would
>> have an useful effect, I propose to embed this check into the assume
>> command.
[...]
> Generally, any changes to the core of the Isar proof engine (proof.ML)
> are restricted to exactly one person: myself. This policy stems from the
> experience over the years, and people trying to tinker with its very
> delicate balance of how things work.

This is the reason I not just committed the patch but sent it here as a 
basis for discussion.

> BTW, it is part of the classic Isar principles that assumptions alone
> cannot be "wrong", and there is a-priori no goal focus for results.

Note that this change does not focus on any specific goal (and the 
choice of an hard error was made rather arbitrarily).

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.

> In recent years some side conditions of Isar have changed anyway: with
> the advent of the Prover IDE, system feedback is no longer restricted to
> the peepwhole view of a single command with its associated proof state.
> There can be additional feedback with knowledge of the partial proof
> document and its structure that is already in the editor buffer.
>
> I have already started some very small beginnings there, to make the
> editing experience of Isar proofs fit into the PIDE mode, mainly about
> the ending of proofs so far.

I like this goal; but, as you said, this is a long term process and a 
solution to this particular issue does not need more then a `peepwhole 
view`. We also don't deviate much from existing practice, as "show" does 
a similar trick already.

> This will require much more work. What helps most are observations from
> practice what works smoothly and what not, without any specific
> proposals how the Isar machinery should be changed.

What does not work smoothly: In a structured proof where I need to 
manually state the assumptions, Isabelle/Isar does not notify me if I 
"assume" things so that I'm not able to discharge any of the pending 
goals anymore.

   -- Lars