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 ***
     1 theory ExamplesAbort = HoareAbort:
     2 
     3 syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("_ \<rightarrow> _" 60)
     4 translations "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
     5 
     6 lemma "VARS x y z::nat
     7  {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
     8 by vcg_simp
     9 
    10 lemma "VARS (a::int list) i
    11  {True}
    12  i := 0;
    13  WHILE i < length a
    14  INV {i <= length a}
    15  DO i < length a \<rightarrow> a := a[i := 7];
    16     i := i+1
    17  OD
    18  {True}"
    19 apply vcg_simp
    20 apply arith
    21 done
    22 
    23 end