[isabelle-dev] Feature suggestion: apply (meth[1!])
Lars Noschinski
noschinl at in.tum.de
Mon Mar 11 14:44:50 CET 2013
On 11.03.2013 14:10, Gerwin Klein wrote:
> 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.
Indeed and I'm in happy situation that I'm able to share my sources.
Unfortunately, due to necessary background theory, this example is quite
large and depends on autocorres[1] and hence Isabelle 2012.
See for example the proof of validNF_is_subgraph in the theory
Kuratowski_Noalloc in the attachment (the other proofs of C functinos
might also be interesting and can easily be found by looking for
applications of the "wp" method):
lemma validNF_is_subgraph:
notes validNF_in_verts'[where iG=iG and g=g, wp, THEN validNF_valid, wp]
and validNF_in_verts'[where iG=iH and g=h, wp, THEN validNF_valid, wp]
and validNF_in_edges'[where iG=iH and g=h, wp, THEN validNF_valid, wp]
shows "⦃ λs. P (if subgraph (mk_graph iG) (mk_graph iH) ∧ IGraph_inv
iG then 1 else 0) s ∧ graph s iG g ∧ graph s iH h⦄
is_subgraph' g h
⦃ P ⦄!"
apply (clarsimp simp: is_subgraph'_def split del: split_if)
apply (subst whileLoopE_add_inv[where
M="λ(n,m) s. unat (m - n)" and
I="λ(n,m) s. P (if subgraph (mk_graph iG) (mk_graph iH) ∧
IGraph_inv iG then 1 else 0) s ∧ is_subgraph_verts_inv iG iH (unat n) ∧
n ≤ m ∧ length (ig_verts iG) = unat m ∧ graph s iG g ∧ graph s iH h"])
apply (subst whileLoopE_add_inv[where
M="λ(n,m) s. unat (m - n)" and
I="λ(n,m) s. P (if subgraph (mk_graph iG) (mk_graph iH) ∧
IGraph_inv iG then 1 else 0) s ∧ is_subgraph_edges_inv iG iH (unat n)
∧ is_subgraph_verts_inv iG iH (length (ig_verts iG))
∧ n ≤ m ∧ length (ig_edges iG) = unat m ∧ graph s iG g ∧ graph
s iH h"])
apply wp
apply (clarsimp simp: edge_t_C_in_pte edge_cnt'_spc edge'_spc
less_is_non_zero_p1 unatSuc2 inc_le word_le_nat_alt
word_less_nat_alt)
apply safe
apply ((auto elim!: is_subgraph_false split: prod.splits
split_if_asm)+)[]
apply ((auto elim!: is_subgraph_false split: prod.splits
split_if_asm)+)[]
apply (subst is_subgraph_edges_step, (fastforce simp:
pte_etc_conv)+)[]
apply ((auto elim!: is_subgraph_false split: prod.splits
split_if_asm)+)[]
apply (metis (lifting) imageI pair_collapse)
apply ((auto elim!: is_subgraph_false split: prod.splits
split_if_asm)+)[]
apply ((auto elim!: is_subgraph_false split: prod.splits
split_if_asm)+)[]
apply (subst is_subgraph_edges_step,auto)[]
apply (wp validE_whenE)
apply (simp add: edge_cnt'_spc)
apply (elim conjE)
apply (simp add: edge_cnt'_spc)
apply (clarsimp simp: edge_cnt'_spc edge'_spc unat_less_helper,
fastforce simp: unat_sub_if' unatSuc2 less_is_non_zero_p1
word_less_nat_alt )
apply (fastforce simp: is_subgraph_verts_edges_last IGraph_inv_conv')
apply wp
apply (fastforce simp: set_mp vert'_spc vert_cnt'_spc
mkg_simps is_subgraph_verts_step
unat_sub_if' unatSuc2 less_is_non_zero_p1 inc_le word_less_nat_alt
split: split_if_asm)
apply (wp validE_whenE)
apply (clarsimp simp: vert_cnt'_spc vert'_spc unat_less_helper,
fastforce simp: unat_sub_if' unatSuc2 less_is_non_zero_p1
word_less_nat_alt )
apply (fastforce simp: edge_cnt'_spc is_subgraph_edges_0)
apply wp
apply (fastforce simp: vert_cnt'_spc is_subgraph_verts_0)
done
The heavy lifting is done outside of this proof (i.e., all the lemmas
referring to "subgraph"). The method "wp" generates the verification
conditions. What is left is mostly for associating the concrete
datastructures from the C program (32 word, an own "tuple"
datastructure) with the more abstract types from Isabelle (nat, pairs).
This proof is one of the uglier ones I got (see validNF_is_K33' for a
nicer example). Usually, I manage to use fastforce almost exclusively
(which has a builtin solve-or-fail behaviour), maybe with the occasional
clarsimp, but here I found no easy way to replace auto and simp.
As Gerwin mentioned, I used indentation to make clear which goals should
be solved. Moreover, I tried to use only methods with a fairly
predictable behaviour as methods which generate new goals and refrained
from using auto's attack-all-goals functionality.
[1] http://ssrg.nicta.com.au/projects/TS/autocorres/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ex.tar.gz
Type: application/x-gzip
Size: 90232 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130311/a6fa47e0/attachment-0002.bin>
More information about the isabelle-dev
mailing list