author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10123  9469c039ff57 
child 10700  b18f417d0b62 
permissions  rwrr 
9393  1 
(* Title: HOL/Hoare/Examples.ML 
1335  2 
ID: $Id$ 
5646  3 
Author: Norbert Galm & Tobias Nipkow 
4 
Copyright 1998 TUM 

1335  5 
*) 
6 

5646  7 
(*** ARITHMETIC ***) 
1335  8 

6802  9 
(** multiplication by successive addition **) 
1335  10 

9147  11 
Goal " VARS m s a b. \ 
12 
\ {a=A & b=B} \ 

13 
\ m := 0; s := 0; \ 

5646  14 
\ WHILE m~=a \ 
9147  15 
\ INV {s=m*b & a=A & b=B} \ 
5646  16 
\ DO s := s+b; m := m+1 OD \ 
9147  17 
\ {s = A*B}"; 
6162  18 
by (hoare_tac (Asm_full_simp_tac) 1); 
1335  19 
qed "multiply_by_add"; 
20 

6802  21 
(** Euclid's algorithm for GCD **) 
1335  22 

5646  23 
Goal " VARS a b. \ 
9147  24 
\ {0<A & 0<B} \ 
25 
\ a := A; b := B; \ 

5646  26 
\ WHILE a~=b \ 
27 
\ INV {0<a & 0<b & gcd A B = gcd a b} \ 

28 
\ DO IF a<b THEN b := ba ELSE a := ab FI OD \ 

1335  29 
\ {a = gcd A B}"; 
5646  30 
by (hoare_tac (K all_tac) 1); 
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset

31 
(*Now prove the verification conditions*) 
9147  32 
by Auto_tac; 
33 
by (etac gcd_nnn 4); 

34 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3); 

35 
by (force_tac (claset(), 

5646  36 
simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2); 
37 
by (asm_simp_tac (simpset() addsimps [gcd_diff_r,less_imp_le]) 1); 

1335  38 
qed "Euclid_GCD"; 
39 

10123  40 
(** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **) 
41 
(* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474), 

42 
where it is given without the invariant. Instead of defining scm 

43 
explicitly we have used the theorem scm x y = x*y/gcd x y and avoided 

44 
division by mupltiplying with gcd x y. 

45 
*) 

46 

47 
val distribs = 

48 
[diff_mult_distrib,diff_mult_distrib2,add_mult_distrib,add_mult_distrib2]; 

49 

50 
Goal " VARS a b x y. \ 

51 
\ {0<A & 0<B & a=A & b=B & x=B & y=A} \ 

52 
\ WHILE a ~= b \ 

53 
\ INV {0<a & 0<b & gcd A B = gcd a b & #2*A*B = a*x + b*y} \ 

54 
\ DO IF a<b THEN (b := ba; x := x+y) ELSE (a := ab; y := y+x) FI OD \ 

55 
\ {a = gcd A B & #2*A*B = a*(x+y)}"; 

56 
by (hoare_tac (K all_tac) 1); 

57 
by(Asm_simp_tac 1); 

58 
by(asm_simp_tac (simpset() addsimps 

59 
(distribs @ [gcd_diff_r,not_less_iff_le, gcd_diff_l])) 1); 

60 
by(arith_tac 1); 

61 
by(asm_full_simp_tac (simpset() addsimps (distribs @ [gcd_nnn])) 1); 

62 
qed "gcd_scm"; 

63 

6802  64 
(** Power by iterated squaring and multiplication **) 
1335  65 

5646  66 
Goal " VARS a b c. \ 
67 
\ {a=A & b=B} \ 

68 
\ c := 1; \ 

69 
\ WHILE b ~= 0 \ 

70 
\ INV {A^B = c * a^b} \ 

8791  71 
\ DO WHILE b mod #2 = 0 \ 
5646  72 
\ INV {A^B = c * a^b} \ 
8791  73 
\ DO a := a*a; b := b div #2 OD; \ 
5646  74 
\ c := c*a; b := b1 \ 
75 
\ OD \ 

4359  76 
\ {c = A^B}"; 
6162  77 
by (hoare_tac (Asm_full_simp_tac) 1); 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

78 
by (case_tac "b" 1); 
9147  79 
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1); 
8791  80 
by (Asm_simp_tac 1); 
1335  81 
qed "power_by_mult"; 
82 

6802  83 
(** Factorial **) 
84 

5646  85 
Goal " VARS a b. \ 
86 
\ {a=A} \ 

87 
\ b := 1; \ 

88 
\ WHILE a ~= 0 \ 

89 
\ INV {fac A = b * fac a} \ 

90 
\ DO b := b*a; a := a1 OD \ 

1335  91 
\ {b = fac A}"; 
5646  92 
by (hoare_tac Asm_full_simp_tac 1); 
5655
afd75136b236
Mods because of: Installed trans_tac in solver of simpset().
nipkow
parents:
5646
diff
changeset

93 
by (Clarify_tac 1); 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

94 
by (case_tac "a" 1); 
9147  95 
by (ALLGOALS (asm_simp_tac 
4089  96 
(simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc]))); 
9147  97 
qed "factorial"; 
1335  98 

6802  99 
(** Square root **) 
100 

6816  101 
(* the easy way: *) 
6802  102 

9147  103 
Goal " VARS r x. \ 
104 
\ {True} \ 

105 
\ x := X; r := 0; \ 

6802  106 
\ WHILE (r+1)*(r+1) <= x \ 
9147  107 
\ INV {r*r <= x & x=X} \ 
6802  108 
\ DO r := r+1 OD \ 
9147  109 
\ {r*r <= X & X < (r+1)*(r+1)}"; 
110 
by (hoare_tac (SELECT_GOAL Auto_tac) 1); 

6802  111 
qed "sqrt"; 
112 

113 
(* without multiplication *) 

114 

9147  115 
Goal " VARS u w r x. \ 
116 
\ {True} \ 

117 
\ x := X; u := 1; w := 1; r := 0; \ 

6802  118 
\ WHILE w <= x \ 
9147  119 
\ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} \ 
6802  120 
\ DO r := r+1; w := w+u+2; u := u+2 OD \ 
9147  121 
\ {r*r <= X & X < (r+1)*(r+1)}"; 
122 
by (hoare_tac (SELECT_GOAL Auto_tac) 1); 

6802  123 
qed "sqrt_without_multiplication"; 
124 

125 

5646  126 
(*** LISTS ***) 
127 

128 
Goal " VARS y x. \ 

129 
\ {x=X} \ 

130 
\ y:=[]; \ 

131 
\ WHILE x ~= [] \ 

132 
\ INV {rev(x)@y = rev(X)} \ 

133 
\ DO y := (hd x # y); x := tl x OD \ 

134 
\ {y=rev(X)}"; 

135 
by (hoare_tac Asm_full_simp_tac 1); 

9147  136 
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); 
137 
by Auto_tac; 

5646  138 
qed "imperative_reverse"; 
139 

140 
Goal 

141 
" VARS x y. \ 

142 
\ {x=X & y=Y} \ 

143 
\ x := rev(x); \ 

144 
\ WHILE x~=[] \ 

145 
\ INV {rev(x)@y = X@Y} \ 

146 
\ DO y := (hd x # y); \ 

147 
\ x := tl x \ 

148 
\ OD \ 

149 
\ {y = X@Y}"; 

150 
by (hoare_tac Asm_full_simp_tac 1); 

9147  151 
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); 
152 
by Auto_tac; 

5646  153 
qed "imperative_append"; 
154 

155 

156 
(*** ARRAYS ***) 

157 

158 
(* Search for 0 *) 

159 
Goal 

160 
" VARS A i. \ 

161 
\ {True} \ 

162 
\ i := 0; \ 

163 
\ WHILE i < length A & A!i ~= 0 \ 

164 
\ INV {!j. j<i > A!j ~= 0} \ 

165 
\ DO i := i+1 OD \ 

166 
\ {(i < length A > A!i = 0) & \ 

167 
\ (i = length A > (!j. j < length A > A!j ~= 0))}"; 

168 
by (hoare_tac Asm_full_simp_tac 1); 

6162  169 
by (blast_tac (claset() addSEs [less_SucE]) 1); 
5646  170 
qed "zero_search"; 
171 

172 
(* 

173 
The `partition' procedure for quicksort. 

174 
`A' is the array to be sorted (modelled as a list). 

175 
Elements of A must be of class order to infer at the end 

176 
that the elements between u and l are equal to pivot. 

177 

178 
Ambiguity warnings of parser are due to := being used 

179 
both for assignment and list update. 

180 
*) 

181 
Goal 

182 
"[ leq == %A i. !k. k<i > A!k <= pivot; \ 

183 
\ geq == %A i. !k. i<k & k<length A > pivot <= A!k ] ==> \ 

184 
\  VARS A u l.\ 

185 
\ {0 < length(A::('a::order)list)} \ 

186 
\ l := 0; u := length A  1; \ 

187 
\ WHILE l <= u \ 

188 
\ INV {leq A l & geq A u & u<length A & l<=length A} \ 

189 
\ DO WHILE l < length A & A!l <= pivot \ 

190 
\ INV {leq A l & geq A u & u<length A & l<=length A} \ 

191 
\ DO l := l+1 OD; \ 

192 
\ WHILE 0 < u & pivot <= A!u \ 

193 
\ INV {leq A l & geq A u & u<length A & l<=length A} \ 

194 
\ DO u := u1 OD; \ 

195 
\ IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI \ 

196 
\ OD \ 

197 
\ {leq A u & (!k. u<k & k<l > A!k = pivot) & geq A l}"; 

198 
(* expand and delete abbreviations first *) 

6162  199 
by (asm_simp_tac HOL_basic_ss 1); 
9147  200 
by (REPEAT (etac thin_rl 1)); 
5646  201 
by (hoare_tac Asm_full_simp_tac 1); 
9147  202 
by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [neq_Nil_conv])) 1); 
6162  203 
by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1); 
9147  204 
by (blast_tac (claset() addSEs [less_SucE] addIs [less_imp_diff_less] 
205 
addDs [pred_less_imp_le RS le_imp_less_Suc] ) 1); 

206 
by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [nth_list_update])) 1); 

207 
by (SELECT_GOAL (auto_tac (claset() addIs [order_antisym], simpset())) 1); 

5646  208 
qed "Partition"; 