src/HOL/Hoare/ExamplesAbort.thy
author nipkow
Tue Mar 11 15:04:24 2003 +0100 (2003-03-11)
changeset 13856 f5d08c341216
child 13857 11d7c5a8dbb7
permissions -rw-r--r--
*** empty log message ***
nipkow@13856
     1
theory ExamplesAbort = HoareAbort:
nipkow@13856
     2
nipkow@13856
     3
syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("_ \<rightarrow> _" 60)
nipkow@13856
     4
translations "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
nipkow@13856
     5
nipkow@13856
     6
lemma "VARS x y z::nat
nipkow@13856
     7
 {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
nipkow@13856
     8
by vcg_simp
nipkow@13856
     9
nipkow@13856
    10
lemma "VARS (a::int list) i
nipkow@13856
    11
 {True}
nipkow@13856
    12
 i := 0;
nipkow@13856
    13
 WHILE i < length a
nipkow@13856
    14
 INV {i <= length a}
nipkow@13856
    15
 DO i < length a \<rightarrow> a := a[i := 7];
nipkow@13856
    16
    i := i+1
nipkow@13856
    17
 OD
nipkow@13856
    18
 {True}"
nipkow@13856
    19
apply vcg_simp
nipkow@13856
    20
apply arith
nipkow@13856
    21
done
nipkow@13856
    22
nipkow@13856
    23
end