src/HOL/Hoare/Pointer_ExamplesAbort.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 38353 d98baa2cf589
child 44890 22f665a2e91c
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     1 (*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
     2     Author:     Tobias Nipkow
     3     Copyright   2002 TUM
     4 
     5 Examples of verifications of pointer programs
     6 *)
     7 
     8 theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
     9 
    10 section "Verifications"
    11 
    12 subsection "List reversal"
    13 
    14 text "Interestingly, this proof is the same as for the unguarded program:"
    15 
    16 lemma "VARS tl p q r
    17   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
    18   WHILE p \<noteq> Null
    19   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
    20                  rev ps @ qs = rev Ps @ Qs}
    21   DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
    22   {List tl q (rev Ps @ Qs)}"
    23 apply vcg_simp
    24   apply fastsimp
    25  apply(fastsimp intro:notin_List_update[THEN iffD2])
    26 apply fastsimp
    27 done
    28 
    29 end