src/HOL/Hoare/Pointer_ExamplesAbort.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 44890 22f665a2e91c
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
nipkow@13875
     1
(*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
nipkow@13875
     2
    Author:     Tobias Nipkow
nipkow@13875
     3
    Copyright   2002 TUM
nipkow@13875
     4
nipkow@13875
     5
Examples of verifications of pointer programs
nipkow@13875
     6
*)
nipkow@13875
     7
haftmann@16417
     8
theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
nipkow@13875
     9
nipkow@13875
    10
section "Verifications"
nipkow@13875
    11
nipkow@13875
    12
subsection "List reversal"
nipkow@13875
    13
nipkow@13875
    14
text "Interestingly, this proof is the same as for the unguarded program:"
nipkow@13875
    15
nipkow@13875
    16
lemma "VARS tl p q r
nipkow@13875
    17
  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
nipkow@13875
    18
  WHILE p \<noteq> Null
nipkow@13875
    19
  INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
nipkow@13875
    20
                 rev ps @ qs = rev Ps @ Qs}
nipkow@13875
    21
  DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
nipkow@13875
    22
  {List tl q (rev Ps @ Qs)}"
nipkow@13875
    23
apply vcg_simp
nipkow@44890
    24
  apply fastforce
nipkow@44890
    25
 apply(fastforce intro:notin_List_update[THEN iffD2])
nipkow@44890
    26
apply fastforce
nipkow@13875
    27
done
nipkow@13875
    28
nipkow@13875
    29
end