src/HOL/Hoare/Examples.ML

tuned;

(*  Title:      HOL/Hoare/Examples.thy
    ID:         $Id$
    Author:     Norbert Galm
    Copyright   1995 TUM

Various arithmetic examples.
*)

open Examples;

(*** multiplication by successive addition ***)

goal thy
 "{m=0 & s=0} \
\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\
\ {s = a*b}";
by (hoare_tac 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
qed "multiply_by_add";


(*** Euclid's algorithm for GCD ***)

goal thy
" {0<A & 0<B & a=A & b=B}   \
\ WHILE a ~= b  \
\ DO  {0<a & 0<b & gcd A B = gcd a b} \
\      IF a<b   \
\      THEN   \
\           b:=b-a   \
\      ELSE   \
\           a:=a-b   \
\      END   \
\ END   \
\ {a = gcd A B}";

by (hoare_tac 1);
(*Now prove the verification conditions*)
by Safe_tac;
by (etac less_imp_diff_positive 1);
by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2);
by (etac gcd_nnn 2);
by (full_simp_tac (simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 1);
by (blast_tac (claset() addIs [less_imp_diff_positive]) 1);
qed "Euclid_GCD";


(*** Power by interated squaring and multiplication ***)

goal thy
" {a=A & b=B}   \
\ c:=1;   \
\ WHILE b~=0   \
\ DO {A^B = c * a^b}   \
\      WHILE b mod 2=0   \
\      DO  {A^B = c * a^b}  \
\           a:=a*a;   \
\           b:=b div 2   \
\      END;   \
\      c:=c*a;   \
\      b:= b - 1 \
\ END   \
\ {c = A^B}";

by (hoare_tac 1);

by (res_inst_tac [("n","b")] natE 1);
by (hyp_subst_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);

qed "power_by_mult";

(*** factorial ***)

goal thy
" {a=A}   \
\ b:=1;   \
\ WHILE a~=0    \
\ DO  {fac A = b*fac a} \
\      b:=b*a;   \
\      a:=a-1   \
\ END   \
\ {b = fac A}";

by (hoare_tac 1);
by Safe_tac;
by (res_inst_tac [("n","a")] natE 1);
by (ALLGOALS
    (asm_simp_tac
     (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
by (Fast_tac 1);

qed"factorial";