On 11/03/2013, at 11:42 AM, Makarius <makar...@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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
