[isabelle-dev] Feature suggestion: apply (meth[1!])

[Makarius]

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