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

[Gerwin Klein]

On 11/03/2013, at 11:42 AM, Makarius <makarius at sketis.net> wrote:
> On Mon, 11 Mar 2013, David Greenaway wrote:
>
>> As a data point, inside the seL4 proof, a largish application of Isabelle, such a "solve-or-fail" mechanism would have been very helpful.
>
> So can you show the sources for that, to give an idea what is done there?


You know we'd be much happier if we could share these proof sources, but it's not under our control (General Dynamics is the owner, I can give you contact details, who knows maybe it actually helps if they start getting emails about this ;-)).

But we can show some things. 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.

I'm not sure the ! syntax is the best choice, but that's a separate discussion.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.