src/HOL/Hoare/Examples.thy
changeset 13789 d37f66755f47
parent 13737 e564c3d2d174
child 13857 11d7c5a8dbb7
     1.1 --- a/src/HOL/Hoare/Examples.thy	Tue Jan 28 07:39:29 2003 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Tue Jan 28 22:53:39 2003 +0100
     1.3 @@ -21,6 +21,24 @@
     1.4    {s = A*B}"
     1.5  by vcg_simp
     1.6  
     1.7 +lemma "VARS M N P :: int
     1.8 + {m=M & n=N}
     1.9 + IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
    1.10 + P := 0;
    1.11 + WHILE 0 < M
    1.12 + INV {0 <= M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)}
    1.13 + DO P := P+N; M := M - 1 OD
    1.14 + {P = m*n}"
    1.15 +apply vcg_simp
    1.16 + apply (simp add:int_distrib)
    1.17 +apply clarsimp
    1.18 +apply(subgoal_tac "M=0")
    1.19 + prefer 2 apply simp
    1.20 +apply clarsimp
    1.21 +apply(rule conjI)
    1.22 + apply clarsimp
    1.23 +apply clarsimp
    1.24 +done
    1.25  
    1.26  (** Euclid's algorithm for GCD **)
    1.27