src/HOL/Hoare/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@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
nipkow@13856
     9
theory ExamplesAbort = HoareAbort:
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