On Mon, 11 Mar 2013, Gerwin Klein wrote:
A very typical situation in those proofs are scripts that look like
this:
lemma "some statement"
apply wp
apply simp
apply fastforce
apply (auto simp: some_rule intro!: other_rule)[1]
apply clarsimp
apply (simp add: other_things)
apply simp
done
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
uninteresting.
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
use.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
