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

[Lars Noschinski]

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>