Theory Pointer_ExamplesAbort

theory Pointer_ExamplesAbort
imports HeapSyntaxAbort
(*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
    Author:     Tobias Nipkow
    Copyright   2002 TUM

Examples of verifications of pointer programs
*)

theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin

section "Verifications"

subsection "List reversal"

text "Interestingly, this proof is the same as for the unguarded program:"

lemma "VARS tl p q r
  {List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {}}
  WHILE p ≠ Null
  INV {∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧
                 rev ps @ qs = rev Ps @ Qs}
  DO r := p; (p ≠ Null -> p := p^.tl); r^.tl := q; q := r OD
  {List tl q (rev Ps @ Qs)}"
apply vcg_simp
  apply fastforce
 apply(fastforce intro:notin_List_update[THEN iffD2])
apply fastforce
done

end