[isabelle-dev] Checked "assume" command
christian.urban at kcl.ac.uk
Wed Sep 5 13:47:55 CEST 2012
On Wednesday, September 5, 2012 at 13:24:27 (+0200), 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.
> 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.
... or in the words of another famous Frenchman:
"L'état, c'est moi"
Sorry, could not resist this spam email ;o)
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev