author | wenzelm |
Sat, 06 Oct 2001 00:02:46 +0200 | |
changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 12486 | 0ed8bdd883e0 |
permissions | -rw-r--r-- |
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} \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
16 |
\ DO s := s+b; m := m+(1::nat) 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 := b-a ELSE a := a-b 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 \ |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
53 |
\ INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y} \ |
10123 | 54 |
\ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD \ |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
55 |
\ {a = gcd A B & 2*A*B = a*(x+y)}"; |
10123 | 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} \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
68 |
\ c := (1::nat); \ |
5646 | 69 |
\ WHILE b ~= 0 \ |
70 |
\ INV {A^B = c * a^b} \ |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
71 |
\ DO WHILE b mod 2 = 0 \ |
5646 | 72 |
\ INV {A^B = c * a^b} \ |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
73 |
\ DO a := a*a; b := b div 2 OD; \ |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
74 |
\ c := c*a; b := b - 1 \ |
5646 | 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} \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
90 |
\ DO b := b*a; a := a - 1 OD \ |
1335 | 91 |
\ {b = fac A}"; |
10700 | 92 |
by (hoare_tac (asm_full_simp_tac (simpset() addsplits [nat_diff_split])) 1); |
93 |
by Auto_tac; |
|
9147 | 94 |
qed "factorial"; |
1335 | 95 |
|
6802 | 96 |
(** Square root **) |
97 |
||
6816 | 98 |
(* the easy way: *) |
6802 | 99 |
|
9147 | 100 |
Goal "|- VARS r x. \ |
101 |
\ {True} \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
102 |
\ x := X; r := (0::nat); \ |
6802 | 103 |
\ WHILE (r+1)*(r+1) <= x \ |
9147 | 104 |
\ INV {r*r <= x & x=X} \ |
6802 | 105 |
\ DO r := r+1 OD \ |
9147 | 106 |
\ {r*r <= X & X < (r+1)*(r+1)}"; |
107 |
by (hoare_tac (SELECT_GOAL Auto_tac) 1); |
|
6802 | 108 |
qed "sqrt"; |
109 |
||
110 |
(* without multiplication *) |
|
111 |
||
9147 | 112 |
Goal "|- VARS u w r x. \ |
113 |
\ {True} \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
114 |
\ x := X; u := 1; w := 1; r := (0::nat); \ |
6802 | 115 |
\ WHILE w <= x \ |
9147 | 116 |
\ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} \ |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
117 |
\ DO r := r + 1; w := w + u + 2; u := u + 2 OD \ |
9147 | 118 |
\ {r*r <= X & X < (r+1)*(r+1)}"; |
119 |
by (hoare_tac (SELECT_GOAL Auto_tac) 1); |
|
6802 | 120 |
qed "sqrt_without_multiplication"; |
121 |
||
122 |
||
5646 | 123 |
(*** LISTS ***) |
124 |
||
125 |
Goal "|- VARS y x. \ |
|
126 |
\ {x=X} \ |
|
127 |
\ y:=[]; \ |
|
128 |
\ WHILE x ~= [] \ |
|
129 |
\ INV {rev(x)@y = rev(X)} \ |
|
130 |
\ DO y := (hd x # y); x := tl x OD \ |
|
131 |
\ {y=rev(X)}"; |
|
132 |
by (hoare_tac Asm_full_simp_tac 1); |
|
9147 | 133 |
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); |
134 |
by Auto_tac; |
|
5646 | 135 |
qed "imperative_reverse"; |
136 |
||
137 |
Goal |
|
138 |
"|- VARS x y. \ |
|
139 |
\ {x=X & y=Y} \ |
|
140 |
\ x := rev(x); \ |
|
141 |
\ WHILE x~=[] \ |
|
142 |
\ INV {rev(x)@y = X@Y} \ |
|
143 |
\ DO y := (hd x # y); \ |
|
144 |
\ x := tl x \ |
|
145 |
\ OD \ |
|
146 |
\ {y = X@Y}"; |
|
147 |
by (hoare_tac Asm_full_simp_tac 1); |
|
9147 | 148 |
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); |
149 |
by Auto_tac; |
|
5646 | 150 |
qed "imperative_append"; |
151 |
||
152 |
||
153 |
(*** ARRAYS ***) |
|
154 |
||
155 |
(* Search for 0 *) |
|
156 |
Goal |
|
157 |
"|- VARS A i. \ |
|
158 |
\ {True} \ |
|
159 |
\ i := 0; \ |
|
160 |
\ WHILE i < length A & A!i ~= 0 \ |
|
161 |
\ INV {!j. j<i --> A!j ~= 0} \ |
|
162 |
\ DO i := i+1 OD \ |
|
163 |
\ {(i < length A --> A!i = 0) & \ |
|
164 |
\ (i = length A --> (!j. j < length A --> A!j ~= 0))}"; |
|
165 |
by (hoare_tac Asm_full_simp_tac 1); |
|
6162 | 166 |
by (blast_tac (claset() addSEs [less_SucE]) 1); |
5646 | 167 |
qed "zero_search"; |
168 |
||
169 |
(* |
|
170 |
The `partition' procedure for quicksort. |
|
171 |
`A' is the array to be sorted (modelled as a list). |
|
172 |
Elements of A must be of class order to infer at the end |
|
173 |
that the elements between u and l are equal to pivot. |
|
174 |
||
175 |
Ambiguity warnings of parser are due to := being used |
|
176 |
both for assignment and list update. |
|
177 |
*) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
178 |
Goal "m - Suc 0 < n ==> m < Suc n"; |
10962 | 179 |
by (arith_tac 1); |
180 |
qed "lemma"; |
|
181 |
||
5646 | 182 |
Goal |
183 |
"[| leq == %A i. !k. k<i --> A!k <= pivot; \ |
|
184 |
\ geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==> \ |
|
185 |
\ |- VARS A u l.\ |
|
186 |
\ {0 < length(A::('a::order)list)} \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
187 |
\ l := 0; u := length A - Suc 0; \ |
5646 | 188 |
\ WHILE l <= u \ |
189 |
\ INV {leq A l & geq A u & u<length A & l<=length A} \ |
|
190 |
\ DO WHILE l < length A & A!l <= pivot \ |
|
191 |
\ INV {leq A l & geq A u & u<length A & l<=length A} \ |
|
192 |
\ DO l := l+1 OD; \ |
|
193 |
\ WHILE 0 < u & pivot <= A!u \ |
|
194 |
\ INV {leq A l & geq A u & u<length A & l<=length A} \ |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
195 |
\ DO u := u - 1 OD; \ |
5646 | 196 |
\ IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI \ |
197 |
\ OD \ |
|
198 |
\ {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"; |
|
199 |
(* expand and delete abbreviations first *) |
|
6162 | 200 |
by (asm_simp_tac HOL_basic_ss 1); |
9147 | 201 |
by (REPEAT (etac thin_rl 1)); |
5646 | 202 |
by (hoare_tac Asm_full_simp_tac 1); |
10700 | 203 |
by (force_tac (claset(), simpset() addsimps [neq_Nil_conv]) 1); |
6162 | 204 |
by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1); |
10962 | 205 |
by (blast_tac (claset() addSEs [less_SucE] |
206 |
addIs [less_imp_diff_less] addDs [lemma]) 1); |
|
10700 | 207 |
by (force_tac (claset(), simpset() addsimps [nth_list_update]) 1); |
208 |
by (auto_tac (claset() addIs [order_antisym], simpset())); |
|
5646 | 209 |
qed "Partition"; |