# 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 **)