author | wenzelm |
Fri, 10 Oct 1997 19:02:28 +0200 | |
changeset 3842 | b55686a7b22c |
parent 3372 | 6e472c8f0011 |
child 4089 | 96fba19bcbe2 |
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); |
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*) |
1875 | 39 |
by (safe_tac (!claset)); |
1465 | 40 |
by (etac less_imp_diff_positive 1); |
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset
|
41 |
by (asm_simp_tac (!simpset addsimps [less_imp_le, gcd_diff_r]) 1); |
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset
|
42 |
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, gcd_diff_l]) 2); |
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset
|
43 |
by (etac gcd_nnn 2); |
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset
|
44 |
by (full_simp_tac (!simpset addsimps [not_less_iff_le, le_eq_less_or_eq]) 1); |
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset
|
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 \ |
|
55 |
\ DO {A pow B = c * a pow b} \ |
|
56 |
\ WHILE b mod 2=0 \ |
|
57 |
\ DO {A pow B = c * a pow b} \ |
|
58 |
\ a:=a*a; \ |
|
59 |
\ b:=b div 2 \ |
|
60 |
\ END; \ |
|
61 |
\ c:=c*a; \ |
|
62 |
\ b:=b-1 \ |
|
63 |
\ END \ |
|
64 |
\ {c = A pow B}"; |
|
65 |
||
66 |
by (hoare_tac 1); |
|
67 |
||
68 |
by (simp_tac ((simpset_of "Arith") addsimps [pow_0]) 3); |
|
69 |
||
1875 | 70 |
by (safe_tac (!claset)); |
1335 | 71 |
|
72 |
by (subgoal_tac "a*a=a pow 2" 1); |
|
73 |
by (Asm_simp_tac 1); |
|
2031 | 74 |
by (stac pow_pow_reduce 1); |
1335 | 75 |
|
76 |
by (subgoal_tac "(b div 2)*2=b" 1); |
|
77 |
by (subgoal_tac "0<2" 2); |
|
78 |
by (dres_inst_tac [("m","b")] mod_div_equality 2); |
|
79 |
||
80 |
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc]))); |
|
81 |
||
82 |
by (subgoal_tac "b~=0" 1); |
|
83 |
by (res_inst_tac [("n","b")] natE 1); |
|
84 |
by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3); |
|
1465 | 85 |
by (assume_tac 4); |
1335 | 86 |
|
87 |
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc]))); |
|
1465 | 88 |
by (rtac mod_less 1); |
1335 | 89 |
by (Simp_tac 1); |
90 |
||
91 |
qed "power_by_mult"; |
|
92 |
||
93 |
(*** factorial ***) |
|
94 |
||
95 |
goal thy |
|
96 |
" {a=A} \ |
|
97 |
\ b:=1; \ |
|
98 |
\ WHILE a~=0 \ |
|
99 |
\ DO {fac A = b*fac a} \ |
|
100 |
\ b:=b*a; \ |
|
101 |
\ a:=a-1 \ |
|
102 |
\ END \ |
|
103 |
\ {b = fac A}"; |
|
104 |
||
105 |
by (hoare_tac 1); |
|
1875 | 106 |
by (safe_tac (!claset)); |
1335 | 107 |
by (res_inst_tac [("n","a")] natE 1); |
1798
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset
|
108 |
by (ALLGOALS |
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset
|
109 |
(asm_simp_tac |
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset
|
110 |
(!simpset addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc]))); |
1875 | 111 |
by (Fast_tac 1); |
1335 | 112 |
|
113 |
qed"factorial"; |