src/HOL/Hoare/Pointer_ExamplesAbort.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 13875 12997e3ddd8d
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
nipkow@13875
     1
(*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
nipkow@13875
     2
    ID:         $Id$
nipkow@13875
     3
    Author:     Tobias Nipkow
nipkow@13875
     4
    Copyright   2002 TUM
nipkow@13875
     5
nipkow@13875
     6
Examples of verifications of pointer programs
nipkow@13875
     7
*)
nipkow@13875
     8
nipkow@13875
     9
theory Pointer_ExamplesAbort = HeapSyntaxAbort:
nipkow@13875
    10
nipkow@13875
    11
section "Verifications"
nipkow@13875
    12
nipkow@13875
    13
subsection "List reversal"
nipkow@13875
    14
nipkow@13875
    15
text "Interestingly, this proof is the same as for the unguarded program:"
nipkow@13875
    16
nipkow@13875
    17
lemma "VARS tl p q r
nipkow@13875
    18
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
nipkow@13875
    19
  WHILE p \<noteq> Null
nipkow@13875
    20
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13875
    21
                 rev ps @ qs = rev Ps @ Qs}
nipkow@13875
    22
  DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
nipkow@13875
    23
  {List tl q (rev Ps @ Qs)}"
nipkow@13875
    24
apply vcg_simp
nipkow@13875
    25
  apply fastsimp
nipkow@13875
    26
 apply(fastsimp intro:notin_List_update[THEN iffD2])
nipkow@13875
    27
apply fastsimp
nipkow@13875
    28
done
nipkow@13875
    29
nipkow@13875
    30
end