src/HOL/Hoare/Examples.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 35316 870dfea4f9c0 child 42154 478bdcea240a permissions -rw-r--r--
1 (*  Title:      HOL/Hoare/Examples.thy
2     Author:     Norbert Galm
5 Various examples.
6 *)
8 theory Examples imports Hoare_Logic Arith2 begin
10 (*** ARITHMETIC ***)
12 (** multiplication by successive addition **)
14 lemma multiply_by_add: "VARS m s a b
15   {a=A & b=B}
16   m := 0; s := 0;
17   WHILE m~=a
18   INV {s=m*b & a=A & b=B}
19   DO s := s+b; m := m+(1::nat) OD
20   {s = A*B}"
21 by vcg_simp
23 lemma "VARS M N P :: int
24  {m=M & n=N}
25  IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
26  P := 0;
27  WHILE 0 < M
28  INV {0 <= M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)}
29  DO P := P+N; M := M - 1 OD
30  {P = m*n}"
31 apply vcg_simp
33 apply clarsimp
34 apply(rule conjI)
35  apply clarsimp
36 apply clarsimp
37 done
39 (** Euclid's algorithm for GCD **)
41 lemma Euclid_GCD: "VARS a b
42  {0<A & 0<B}
43  a := A; b := B;
44  WHILE  a \<noteq> b
45  INV {0<a & 0<b & gcd A B = gcd a b}
46  DO IF a<b THEN b := b-a ELSE a := a-b FI OD
47  {a = gcd A B}"
48 apply vcg
49 (*Now prove the verification conditions*)
50   apply auto
53 apply(erule gcd_nnn)
54 done
56 (** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
57 (* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
58    where it is given without the invariant. Instead of defining scm
59    explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
60    division by mupltiplying with gcd x y.
61 *)
63 lemmas distribs =
66 lemma gcd_scm: "VARS a b x y
67  {0<A & 0<B & a=A & b=B & x=B & y=A}
68  WHILE  a ~= b
69  INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
70  DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
71  {a = gcd A B & 2*A*B = a*(x+y)}"
72 apply vcg
73   apply simp
74  apply(simp add: distribs gcd_diff_r linorder_not_less gcd_diff_l)
76 done
78 (** Power by iterated squaring and multiplication **)
80 lemma power_by_mult: "VARS a b c
81  {a=A & b=B}
82  c := (1::nat);
83  WHILE b ~= 0
84  INV {A^B = c * a^b}
85  DO  WHILE b mod 2 = 0
86      INV {A^B = c * a^b}
87      DO  a := a*a; b := b div 2 OD;
88      c := c*a; b := b - 1
89  OD
90  {c = A^B}"
91 apply vcg_simp
92 apply(case_tac "b")
94 apply simp
95 done
97 (** Factorial **)
99 lemma factorial: "VARS a b
100  {a=A}
101  b := 1;
102  WHILE a ~= 0
103  INV {fac A = b * fac a}
104  DO b := b*a; a := a - 1 OD
105  {b = fac A}"
106 apply vcg_simp
107 apply(clarsimp split: nat_diff_split)
108 done
110 lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
111 by(induct i, simp_all)
113 lemma "VARS i f
114  {True}
115  i := (1::nat); f := 1;
116  WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
117  DO f := f*i; i := i+1 OD
118  {f = fac n}"
119 apply vcg_simp
120 apply(subgoal_tac "i = Suc n")
121 apply simp
122 apply arith
123 done
125 (** Square root **)
127 (* the easy way: *)
129 lemma sqrt: "VARS r x
130  {True}
131  x := X; r := (0::nat);
132  WHILE (r+1)*(r+1) <= x
133  INV {r*r <= x & x=X}
134  DO r := r+1 OD
135  {r*r <= X & X < (r+1)*(r+1)}"
136 apply vcg_simp
137 done
139 (* without multiplication *)
141 lemma sqrt_without_multiplication: "VARS u w r x
142  {True}
143  x := X; u := 1; w := 1; r := (0::nat);
144  WHILE w <= x
145  INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
146  DO r := r + 1; w := w + u + 2; u := u + 2 OD
147  {r*r <= X & X < (r+1)*(r+1)}"
148 apply vcg_simp
149 done
152 (*** LISTS ***)
154 lemma imperative_reverse: "VARS y x
155  {x=X}
156  y:=[];
157  WHILE x ~= []
158  INV {rev(x)@y = rev(X)}
159  DO y := (hd x # y); x := tl x OD
160  {y=rev(X)}"
161 apply vcg_simp
163  apply auto
164 done
166 lemma imperative_append: "VARS x y
167  {x=X & y=Y}
168  x := rev(x);
169  WHILE x~=[]
170  INV {rev(x)@y = X@Y}
171  DO y := (hd x # y);
172     x := tl x
173  OD
174  {y = X@Y}"
175 apply vcg_simp
177 apply auto
178 done
181 (*** ARRAYS ***)
183 (* Search for a key *)
184 lemma zero_search: "VARS A i
185  {True}
186  i := 0;
187  WHILE i < length A & A!i ~= key
188  INV {!j. j<i --> A!j ~= key}
189  DO i := i+1 OD
190  {(i < length A --> A!i = key) &
191   (i = length A --> (!j. j < length A --> A!j ~= key))}"
192 apply vcg_simp
193 apply(blast elim!: less_SucE)
194 done
196 (*
197 The `partition' procedure for quicksort.
198 `A' is the array to be sorted (modelled as a list).
199 Elements of A must be of class order to infer at the end
200 that the elements between u and l are equal to pivot.
202 Ambiguity warnings of parser are due to := being used
203 both for assignment and list update.
204 *)
205 lemma lem: "m - Suc 0 < n ==> m < Suc n"
206 by arith
209 lemma Partition:
210 "[| leq == %A i. !k. k<i --> A!k <= pivot;
211     geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
212  VARS A u l
213  {0 < length(A::('a::order)list)}
214  l := 0; u := length A - Suc 0;
215  WHILE l <= u
216   INV {leq A l & geq A u & u<length A & l<=length A}
217   DO WHILE l < length A & A!l <= pivot
218      INV {leq A l & geq A u & u<length A & l<=length A}
219      DO l := l+1 OD;
220      WHILE 0 < u & pivot <= A!u
221      INV {leq A l & geq A u  & u<length A & l<=length A}
222      DO u := u - 1 OD;
223      IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
224   OD
225  {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
226 (* expand and delete abbreviations first *)
227 apply (simp);
228 apply (erule thin_rl)+
229 apply vcg_simp
230    apply (force simp: neq_Nil_conv)
231   apply (blast elim!: less_SucE intro: Suc_leI)
232  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
233 apply (force simp: nth_list_update)
234 done
236 end