author | paulson |
Fri, 14 Jun 1996 12:25:02 +0200 | |
changeset 1798 | c055505f36d1 |
parent 1465 | 5d7a7e439cec |
child 1875 | 54c0462f8fb2 |
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}"; |
|
17 |
by(hoare_tac 1); |
|
18 |
by(ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac))); |
|
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); |
|
38 |
||
39 |
by (safe_tac HOL_cs); |
|
40 |
||
1465 | 41 |
by (etac less_imp_diff_positive 1); |
42 |
by (etac gcd_diff_r 1); |
|
1335 | 43 |
|
44 |
by (cut_facts_tac [less_linear] 1); |
|
45 |
by (cut_facts_tac [less_linear] 2); |
|
1465 | 46 |
by (rtac less_imp_diff_positive 1); |
47 |
by (rtac gcd_diff_l 2); |
|
1335 | 48 |
|
1465 | 49 |
by (dtac gcd_nnn 3); |
1335 | 50 |
|
51 |
by (ALLGOALS (fast_tac HOL_cs)); |
|
52 |
||
53 |
qed "Euclid_GCD"; |
|
54 |
||
55 |
||
56 |
(*** Power by interated squaring and multiplication ***) |
|
57 |
||
58 |
goal thy |
|
59 |
" {a=A & b=B} \ |
|
60 |
\ c:=1; \ |
|
61 |
\ WHILE b~=0 \ |
|
62 |
\ DO {A pow B = c * a pow b} \ |
|
63 |
\ WHILE b mod 2=0 \ |
|
64 |
\ DO {A pow B = c * a pow b} \ |
|
65 |
\ a:=a*a; \ |
|
66 |
\ b:=b div 2 \ |
|
67 |
\ END; \ |
|
68 |
\ c:=c*a; \ |
|
69 |
\ b:=b-1 \ |
|
70 |
\ END \ |
|
71 |
\ {c = A pow B}"; |
|
72 |
||
73 |
by (hoare_tac 1); |
|
74 |
||
75 |
by (simp_tac ((simpset_of "Arith") addsimps [pow_0]) 3); |
|
76 |
||
77 |
by (safe_tac HOL_cs); |
|
78 |
||
79 |
by (subgoal_tac "a*a=a pow 2" 1); |
|
80 |
by (Asm_simp_tac 1); |
|
1465 | 81 |
by (rtac (pow_pow_reduce RS ssubst) 1); |
1335 | 82 |
|
83 |
by (subgoal_tac "(b div 2)*2=b" 1); |
|
84 |
by (subgoal_tac "0<2" 2); |
|
85 |
by (dres_inst_tac [("m","b")] mod_div_equality 2); |
|
86 |
||
87 |
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc]))); |
|
88 |
||
89 |
by (subgoal_tac "b~=0" 1); |
|
90 |
by (res_inst_tac [("n","b")] natE 1); |
|
91 |
by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3); |
|
1465 | 92 |
by (assume_tac 4); |
1335 | 93 |
|
94 |
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc]))); |
|
1465 | 95 |
by (rtac mod_less 1); |
1335 | 96 |
by (Simp_tac 1); |
97 |
||
98 |
qed "power_by_mult"; |
|
99 |
||
100 |
(*** factorial ***) |
|
101 |
||
102 |
goal thy |
|
103 |
" {a=A} \ |
|
104 |
\ b:=1; \ |
|
105 |
\ WHILE a~=0 \ |
|
106 |
\ DO {fac A = b*fac a} \ |
|
107 |
\ b:=b*a; \ |
|
108 |
\ a:=a-1 \ |
|
109 |
\ END \ |
|
110 |
\ {b = fac A}"; |
|
111 |
||
112 |
by (hoare_tac 1); |
|
113 |
by (safe_tac HOL_cs); |
|
114 |
by (res_inst_tac [("n","a")] natE 1); |
|
1798
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset
|
115 |
by (ALLGOALS |
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset
|
116 |
(asm_simp_tac |
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset
|
117 |
(!simpset addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc]))); |
1335 | 118 |
by (fast_tac HOL_cs 1); |
119 |
||
120 |
qed"factorial"; |