|
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:=b-a \ |
|
31 \ ELSE \ |
|
32 \ a:=a-b \ |
|
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:=b-1 \ |
|
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:=a-1 \ |
|
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"; |