[isabelle-dev] Feature suggestion: apply (meth[1!])
makarius at sketis.net
Mon Mar 11 17:51:04 CET 2013
On Mon, 11 Mar 2013, Gerwin Klein wrote:
> A very typical situation in those proofs are scripts that look like
> lemma "some statement"
> apply wp
> apply simp
> apply fastforce
> apply (auto simp: some_rule intro!: other_rule)
> apply clarsimp
> apply (simp add: other_things)
> apply simp
> Lars' will probably look very similar. This is not that specific to our
> proofs, it's an issue with any larger apply-style development, esp with
> anything that solves verification conditions which aren't that nice to
> write down in structured proofs, because they tend to be large and
> It's clear from indentation what is supposed to solve a goal, but it
> would be much easier for maintenance if proofs failed early. There
> should be plenty of examples in the AFP, maybe also some in the
> distribution that would benefit.
This looks just like making the meaning of indentation a bit more formal.
Lets say as a mode of checking in the Prover IDE: fail if something is
wrong in that respect, or paint things in funny colors.
Markup.proof_state is there for a long time already, to turn it into some
More information about the isabelle-dev