# HG changeset patch
# User nipkow
# Date 1043790819 -3600
# Node ID d37f66755f477e490fa86c8652e2289fc3a2069b
# Parent  fd03c4ab89d4e504abb8e8b2e9199536464d2417
New example

diff -r fd03c4ab89d4 -r d37f66755f47 src/HOL/Hoare/Examples.thy
--- 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 **)