src/HOL/Hoare/ExamplesAbort.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 13875 12997e3ddd8d
child 16733 236dfafbeb63
permissions -rw-r--r--
migrated theory headers to new format
nipkow@13857
     1
(*  Title:      HOL/Hoare/ExamplesAbort.thy
nipkow@13857
     2
    ID:         $Id$
nipkow@13857
     3
    Author:     Tobias Nipkow
nipkow@13857
     4
    Copyright   1998 TUM
nipkow@13857
     5
nipkow@13857
     6
Some small examples for programs that may abort.
nipkow@13857
     7
*)
nipkow@13857
     8
haftmann@16417
     9
theory ExamplesAbort imports HoareAbort begin
nipkow@13856
    10
nipkow@13856
    11
lemma "VARS x y z::nat
nipkow@13856
    12
 {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
nipkow@13856
    13
by vcg_simp
nipkow@13856
    14
nipkow@13875
    15
lemma
nipkow@13875
    16
 "VARS a i j
nipkow@13875
    17
 {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
nipkow@13875
    18
apply vcg_simp
nipkow@13875
    19
apply arith
nipkow@13875
    20
done
nipkow@13875
    21
nipkow@13856
    22
lemma "VARS (a::int list) i
nipkow@13856
    23
 {True}
nipkow@13856
    24
 i := 0;
nipkow@13856
    25
 WHILE i < length a
nipkow@13856
    26
 INV {i <= length a}
nipkow@13875
    27
 DO a[i] := 7; i := i+1 OD
nipkow@13856
    28
 {True}"
nipkow@13856
    29
apply vcg_simp
nipkow@13856
    30
apply arith
nipkow@13856
    31
done
nipkow@13856
    32
nipkow@13856
    33
end