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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
