1335

1 
(* Title: HOL/Hoare/Examples.thy


2 
ID: $Id$


3 
Author: Norbert Galm


4 
Copyright 1995 TUM


5 


6 
Various arithmetic examples.


7 
*)


8 


9 
open Examples;


10 


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


12 


13 
goal thy


14 
"{m=0 & s=0} \


15 
\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\


16 
\ {s = a*b}";


17 
by(hoare_tac 1);


18 
by(ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac)));


19 
qed "multiply_by_add";


20 


21 


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


23 


24 
goal thy


25 
" {0<A & 0<B & a=A & b=B} \


26 
\ WHILE a ~= b \


27 
\ DO {0<a & 0<b & gcd A B = gcd a b} \


28 
\ IF a<b \


29 
\ THEN \


30 
\ b:=ba \


31 
\ ELSE \


32 
\ a:=ab \


33 
\ END \


34 
\ END \


35 
\ {a = gcd A B}";


36 


37 
by (hoare_tac 1);


38 


39 
by (safe_tac HOL_cs);


40 


41 
be less_imp_diff_positive 1;


42 
be gcd_diff_r 1;


43 


44 
by (cut_facts_tac [less_linear] 1);


45 
by (cut_facts_tac [less_linear] 2);


46 
br less_imp_diff_positive 1;


47 
br gcd_diff_l 2;


48 


49 
bd gcd_nnn 3;


50 


51 
by (ALLGOALS (fast_tac HOL_cs));


52 


53 
qed "Euclid_GCD";


54 


55 


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


57 


58 
goal thy


59 
" {a=A & b=B} \


60 
\ c:=1; \


61 
\ WHILE b~=0 \


62 
\ DO {A pow B = c * a pow b} \


63 
\ WHILE b mod 2=0 \


64 
\ DO {A pow B = c * a pow b} \


65 
\ a:=a*a; \


66 
\ b:=b div 2 \


67 
\ END; \


68 
\ c:=c*a; \


69 
\ b:=b1 \


70 
\ END \


71 
\ {c = A pow B}";


72 


73 
by (hoare_tac 1);


74 


75 
by (simp_tac ((simpset_of "Arith") addsimps [pow_0]) 3);


76 


77 
by (safe_tac HOL_cs);


78 


79 
by (subgoal_tac "a*a=a pow 2" 1);


80 
by (Asm_simp_tac 1);


81 
br (pow_pow_reduce RS ssubst) 1;


82 


83 
by (subgoal_tac "(b div 2)*2=b" 1);


84 
by (subgoal_tac "0<2" 2);


85 
by (dres_inst_tac [("m","b")] mod_div_equality 2);


86 


87 
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc])));


88 


89 
by (subgoal_tac "b~=0" 1);


90 
by (res_inst_tac [("n","b")] natE 1);


91 
by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3);


92 
ba 4;


93 


94 
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc])));


95 
br mod_less 1;


96 
by (Simp_tac 1);


97 


98 
qed "power_by_mult";


99 


100 
(*** factorial ***)


101 


102 
goal thy


103 
" {a=A} \


104 
\ b:=1; \


105 
\ WHILE a~=0 \


106 
\ DO {fac A = b*fac a} \


107 
\ b:=b*a; \


108 
\ a:=a1 \


109 
\ END \


110 
\ {b = fac A}";


111 


112 
by (hoare_tac 1);


113 


114 
by (safe_tac HOL_cs);


115 


116 
by (res_inst_tac [("n","a")] natE 1);


117 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mult_assoc])));


118 
by (fast_tac HOL_cs 1);


119 


120 
qed"factorial";
