author | wenzelm |
Fri, 29 May 1998 13:50:21 +0200 | |
changeset 4987 | 257aeccdefc3 |
parent 4710 | 05e57f1879ee |
child 5069 | 3ea049f7979d |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Hoare/Examples.thy |
1335 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Norbert Galm |
1335 | 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}"; |
|
2031 | 17 |
by (hoare_tac 1); |
4089 | 18 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac))); |
1335 | 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); |
|
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset
|
38 |
(*Now prove the verification conditions*) |
4153 | 39 |
by Safe_tac; |
1465 | 40 |
by (etac less_imp_diff_positive 1); |
4089 | 41 |
by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1); |
42 |
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2); |
|
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset
|
43 |
by (etac gcd_nnn 2); |
4089 | 44 |
by (full_simp_tac (simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 1); |
45 |
by (blast_tac (claset() addIs [less_imp_diff_positive]) 1); |
|
1335 | 46 |
qed "Euclid_GCD"; |
47 |
||
48 |
||
49 |
(*** Power by interated squaring and multiplication ***) |
|
50 |
||
51 |
goal thy |
|
52 |
" {a=A & b=B} \ |
|
53 |
\ c:=1; \ |
|
54 |
\ WHILE b~=0 \ |
|
4359 | 55 |
\ DO {A^B = c * a^b} \ |
1335 | 56 |
\ WHILE b mod 2=0 \ |
4359 | 57 |
\ DO {A^B = c * a^b} \ |
1335 | 58 |
\ a:=a*a; \ |
59 |
\ b:=b div 2 \ |
|
60 |
\ END; \ |
|
61 |
\ c:=c*a; \ |
|
4710 | 62 |
\ b:= b - 1 \ |
1335 | 63 |
\ END \ |
4359 | 64 |
\ {c = A^B}"; |
1335 | 65 |
|
66 |
by (hoare_tac 1); |
|
67 |
||
68 |
by (res_inst_tac [("n","b")] natE 1); |
|
4356 | 69 |
by (hyp_subst_tac 1); |
70 |
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1); |
|
4359 | 71 |
by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1); |
1335 | 72 |
|
73 |
qed "power_by_mult"; |
|
74 |
||
75 |
(*** factorial ***) |
|
76 |
||
77 |
goal thy |
|
78 |
" {a=A} \ |
|
79 |
\ b:=1; \ |
|
80 |
\ WHILE a~=0 \ |
|
81 |
\ DO {fac A = b*fac a} \ |
|
82 |
\ b:=b*a; \ |
|
83 |
\ a:=a-1 \ |
|
84 |
\ END \ |
|
85 |
\ {b = fac A}"; |
|
86 |
||
87 |
by (hoare_tac 1); |
|
4153 | 88 |
by Safe_tac; |
1335 | 89 |
by (res_inst_tac [("n","a")] natE 1); |
1798
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset
|
90 |
by (ALLGOALS |
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset
|
91 |
(asm_simp_tac |
4089 | 92 |
(simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc]))); |
1875 | 93 |
by (Fast_tac 1); |
1335 | 94 |
|
95 |
qed"factorial"; |