[isabelle-dev] Checked "assume" command

[Makarius]

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.

I did not know the "fix P show P sorry" trick yet, but this is something 
for isabelle-users.

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.  It takes myself often years of 
rethinking and reforming some of its fundamental details that emerged so 
well in the pionerring years of 1999-2001.

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.


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.

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.


 	Makarius