--- a/src/HOL/Hoare/Examples.thy Tue Jan 28 07:39:29 2003 +0100
+++ b/src/HOL/Hoare/Examples.thy Tue Jan 28 22:53:39 2003 +0100
@@ -21,6 +21,24 @@
{s = A*B}"
by vcg_simp
+lemma "VARS M N P :: int
+ {m=M & n=N}
+ IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
+ P := 0;
+ WHILE 0 < M
+ INV {0 <= M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)}
+ DO P := P+N; M := M - 1 OD
+ {P = m*n}"
+apply vcg_simp
+ apply (simp add:int_distrib)
+apply clarsimp
+apply(subgoal_tac "M=0")
+ prefer 2 apply simp
+apply clarsimp
+apply(rule conjI)
+ apply clarsimp
+apply clarsimp
+done
(** Euclid's algorithm for GCD **)