author  nipkow 
Wed, 14 Oct 1998 15:26:31 +0200  
changeset 5646  7c2ddbaf8b8c 
parent 5591  fbb4e1ac234d 
child 5655  afd75136b236 
permissions  rwrr 
1465  1 
(* Title: HOL/Hoare/Examples.thy 
1335  2 
ID: $Id$ 
5646  3 
Author: Norbert Galm & Tobias Nipkow 
4 
Copyright 1998 TUM 

1335  5 
*) 
6 

5646  7 
(*** ARITHMETIC ***) 
1335  8 

9 
(*** multiplication by successive addition ***) 

10 

5646  11 
Goal " VARS m s. \ 
12 
\ {m=0 & s=0} \ 

13 
\ WHILE m~=a \ 

14 
\ INV {s=m*b} \ 

15 
\ DO s := s+b; m := m+1 OD \ 

16 
\ {s = a*b}"; 

17 
by(hoare_tac (Asm_full_simp_tac) 1); 

1335  18 
qed "multiply_by_add"; 
19 

20 
(*** Euclid's algorithm for GCD ***) 

21 

5646  22 
Goal " VARS a b. \ 
23 
\ {0<A & 0<B & a=A & b=B} \ 

24 
\ WHILE a~=b \ 

25 
\ INV {0<a & 0<b & gcd A B = gcd a b} \ 

26 
\ DO IF a<b THEN b := ba ELSE a := ab FI OD \ 

1335  27 
\ {a = gcd A B}"; 
5646  28 
by (hoare_tac (K all_tac) 1); 
1335  29 

3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
2031
diff
changeset

30 
(*Now prove the verification conditions*) 
5338  31 
by Auto_tac; 
32 
by (etac gcd_nnn 4); 

33 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3); 

34 
by (force_tac (claset(), 

5646  35 
simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2); 
36 
by (asm_simp_tac (simpset() addsimps [gcd_diff_r,less_imp_le]) 1); 

1335  37 
qed "Euclid_GCD"; 
38 

5646  39 
(*** Power by iterated squaring and multiplication ***) 
1335  40 

5646  41 
Goal " VARS a b c. \ 
42 
\ {a=A & b=B} \ 

43 
\ c := 1; \ 

44 
\ WHILE b ~= 0 \ 

45 
\ INV {A^B = c * a^b} \ 

46 
\ DO WHILE b mod 2 = 0 \ 

47 
\ INV {A^B = c * a^b} \ 

48 
\ DO a := a*a; b := b div 2 OD; \ 

49 
\ c := c*a; b := b1 \ 

50 
\ OD \ 

4359  51 
\ {c = A^B}"; 
5646  52 
by(hoare_tac (Asm_full_simp_tac) 1); 
5183  53 
by (exhaust_tac "b" 1); 
4356  54 
by (hyp_subst_tac 1); 
55 
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1); 

4359  56 
by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1); 
1335  57 
qed "power_by_mult"; 
58 

5646  59 
Goal " VARS a b. \ 
60 
\ {a=A} \ 

61 
\ b := 1; \ 

62 
\ WHILE a ~= 0 \ 

63 
\ INV {fac A = b * fac a} \ 

64 
\ DO b := b*a; a := a1 OD \ 

1335  65 
\ {b = fac A}"; 
5646  66 
by (hoare_tac Asm_full_simp_tac 1); 
4153  67 
by Safe_tac; 
5183  68 
by (exhaust_tac "a" 1); 
1798
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset

69 
by (ALLGOALS 
c055505f36d1
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1465
diff
changeset

70 
(asm_simp_tac 
4089  71 
(simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc]))); 
1875  72 
by (Fast_tac 1); 
5646  73 
qed"factorial"; 
1335  74 

5646  75 
(*** LISTS ***) 
76 

77 
Goal " VARS y x. \ 

78 
\ {x=X} \ 

79 
\ y:=[]; \ 

80 
\ WHILE x ~= [] \ 

81 
\ INV {rev(x)@y = rev(X)} \ 

82 
\ DO y := (hd x # y); x := tl x OD \ 

83 
\ {y=rev(X)}"; 

84 
by (hoare_tac Asm_full_simp_tac 1); 

85 
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); 

86 
by Safe_tac; 

87 
by (ALLGOALS(Asm_full_simp_tac )); 

88 
qed "imperative_reverse"; 

89 

90 
Goal 

91 
" VARS x y. \ 

92 
\ {x=X & y=Y} \ 

93 
\ x := rev(x); \ 

94 
\ WHILE x~=[] \ 

95 
\ INV {rev(x)@y = X@Y} \ 

96 
\ DO y := (hd x # y); \ 

97 
\ x := tl x \ 

98 
\ OD \ 

99 
\ {y = X@Y}"; 

100 
by (hoare_tac Asm_full_simp_tac 1); 

101 
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); 

102 
by Safe_tac; 

103 
by (ALLGOALS(Asm_full_simp_tac)); 

104 
qed "imperative_append"; 

105 

106 

107 
(*** ARRAYS ***) 

108 

109 
(* Search for 0 *) 

110 
Goal 

111 
" VARS A i. \ 

112 
\ {True} \ 

113 
\ i := 0; \ 

114 
\ WHILE i < length A & A!i ~= 0 \ 

115 
\ INV {!j. j<i > A!j ~= 0} \ 

116 
\ DO i := i+1 OD \ 

117 
\ {(i < length A > A!i = 0) & \ 

118 
\ (i = length A > (!j. j < length A > A!j ~= 0))}"; 

119 
by (hoare_tac Asm_full_simp_tac 1); 

120 
by(blast_tac (claset() addSEs [less_SucE]) 1); 

121 
qed "zero_search"; 

122 

123 
(* 

124 
The `partition' procedure for quicksort. 

125 
`A' is the array to be sorted (modelled as a list). 

126 
Elements of A must be of class order to infer at the end 

127 
that the elements between u and l are equal to pivot. 

128 

129 
Ambiguity warnings of parser are due to := being used 

130 
both for assignment and list update. 

131 
*) 

132 
Goal 

133 
"[ leq == %A i. !k. k<i > A!k <= pivot; \ 

134 
\ geq == %A i. !k. i<k & k<length A > pivot <= A!k ] ==> \ 

135 
\  VARS A u l.\ 

136 
\ {0 < length(A::('a::order)list)} \ 

137 
\ l := 0; u := length A  1; \ 

138 
\ WHILE l <= u \ 

139 
\ INV {leq A l & geq A u & u<length A & l<=length A} \ 

140 
\ DO WHILE l < length A & A!l <= pivot \ 

141 
\ INV {leq A l & geq A u & u<length A & l<=length A} \ 

142 
\ DO l := l+1 OD; \ 

143 
\ WHILE 0 < u & pivot <= A!u \ 

144 
\ INV {leq A l & geq A u & u<length A & l<=length A} \ 

145 
\ DO u := u1 OD; \ 

146 
\ IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI \ 

147 
\ OD \ 

148 
\ {leq A u & (!k. u<k & k<l > A!k = pivot) & geq A l}"; 

149 
(* expand and delete abbreviations first *) 

150 
by(asm_simp_tac HOL_basic_ss 1); 

151 
by(REPEAT(etac thin_rl 1)); 

152 
by (hoare_tac Asm_full_simp_tac 1); 

153 
by(asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1); 

154 
by(Clarify_tac 1); 

155 
by(asm_full_simp_tac (simpset() addsimps [nth_list_update] 

156 
addSolver cut_trans_tac) 1); 

157 
by(blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1); 

158 
br conjI 1; 

159 
by(Clarify_tac 1); 

160 
bd (pred_less_imp_le RS le_imp_less_Suc) 1; 

161 
by(blast_tac (claset() addSEs [less_SucE]) 1); 

162 
br less_imp_diff_less 1; 

163 
by(Blast_tac 1); 

164 
by(Clarify_tac 1); 

165 
by(asm_simp_tac (simpset() addsimps [nth_list_update] 

166 
addSolver cut_trans_tac) 1); 

167 
by(Clarify_tac 1); 

168 
by(trans_tac 1); 

169 
by(Clarify_tac 1); 

170 
by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1); 

171 
br conjI 1; 

172 
by(Clarify_tac 1); 

173 
br order_antisym 1; 

174 
by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1); 

175 
by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1); 

176 
by(Clarify_tac 1); 

177 
by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1); 

178 
qed "Partition"; 