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