src/HOL/Hoare/ExamplesAbort.thy
changeset 13856 f5d08c341216
child 13857 11d7c5a8dbb7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 11 15:04:24 2003 +0100
     1.3 @@ -0,0 +1,23 @@
     1.4 +theory ExamplesAbort = HoareAbort:
     1.5 +
     1.6 +syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("_ \<rightarrow> _" 60)
     1.7 +translations "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
     1.8 +
     1.9 +lemma "VARS x y z::nat
    1.10 + {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
    1.11 +by vcg_simp
    1.12 +
    1.13 +lemma "VARS (a::int list) i
    1.14 + {True}
    1.15 + i := 0;
    1.16 + WHILE i < length a
    1.17 + INV {i <= length a}
    1.18 + DO i < length a \<rightarrow> a := a[i := 7];
    1.19 +    i := i+1
    1.20 + OD
    1.21 + {True}"
    1.22 +apply vcg_simp
    1.23 +apply arith
    1.24 +done
    1.25 +
    1.26 +end