author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9000  c20d58286a51 
permissions  rwrr 
5545  1 
(* Title: HOL/ex/BinEx.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5199  5 

5545  6 
Examples of performing binary arithmetic by simplification 
7 

8 
Also a proof that binary arithmetic on normalized operands 

9 
yields normalized results. 

10 
*) 

11 

7037  12 
(**** The Integers ****) 
13 

6920  14 
(*** Addition ***) 
5491  15 

6909  16 
Goal "(#13::int) + #19 = #32"; 
5199  17 
by (Simp_tac 1); 
18 
result(); 

19 

6909  20 
Goal "(#1234::int) + #5678 = #6912"; 
5199  21 
by (Simp_tac 1); 
22 
result(); 

23 

6909  24 
Goal "(#1359::int) + #2468 = #1109"; 
5199  25 
by (Simp_tac 1); 
26 
result(); 

27 

6909  28 
Goal "(#93746::int) + #46375 = #47371"; 
5199  29 
by (Simp_tac 1); 
30 
result(); 

31 

6920  32 
(*** Negation ***) 
5491  33 

6909  34 
Goal " (#65745::int) = #65745"; 
5199  35 
by (Simp_tac 1); 
36 
result(); 

37 

6909  38 
Goal " (#54321::int) = #54321"; 
5199  39 
by (Simp_tac 1); 
40 
result(); 

41 

5491  42 

6920  43 
(*** Multiplication ***) 
5491  44 

6909  45 
Goal "(#13::int) * #19 = #247"; 
5199  46 
by (Simp_tac 1); 
47 
result(); 

48 

6909  49 
Goal "(#84::int) * #51 = #4284"; 
5199  50 
by (Simp_tac 1); 
51 
result(); 

52 

6909  53 
Goal "(#255::int) * #255 = #65025"; 
5199  54 
by (Simp_tac 1); 
55 
result(); 

56 

6909  57 
Goal "(#1359::int) * #2468 = #3354012"; 
5199  58 
by (Simp_tac 1); 
59 
result(); 

60 

6909  61 
Goal "(#89::int) * #10 ~= #889"; 
5199  62 
by (Simp_tac 1); 
63 
result(); 

64 

6909  65 
Goal "(#13::int) < #18  #4"; 
5199  66 
by (Simp_tac 1); 
67 
result(); 

68 

6909  69 
Goal "(#345::int) < #242 + #100"; 
5199  70 
by (Simp_tac 1); 
71 
result(); 

72 

6909  73 
Goal "(#13557456::int) < #18678654"; 
5199  74 
by (Simp_tac 1); 
75 
result(); 

76 

6909  77 
Goal "(#999999::int) <= (#1000001 + #1)#2"; 
5199  78 
by (Simp_tac 1); 
79 
result(); 

80 

6909  81 
Goal "(#1234567::int) <= #1234567"; 
5199  82 
by (Simp_tac 1); 
83 
result(); 

5545  84 

85 

7037  86 
(*** Quotient and Remainder ***) 
6920  87 

88 
Goal "(#10::int) div #3 = #3"; 

89 
by (Simp_tac 1); 

90 
result(); 

91 

92 
Goal "(#10::int) mod #3 = #1"; 

93 
by (Simp_tac 1); 

94 
result(); 

95 

96 
(** A negative divisor **) 

97 

98 
Goal "(#10::int) div #3 = #4"; 

99 
by (Simp_tac 1); 

100 
result(); 

101 

102 
Goal "(#10::int) mod #3 = #2"; 

103 
by (Simp_tac 1); 

104 
result(); 

105 

106 
(** A negative dividend 

107 
[ The definition agrees with mathematical convention but not with 

108 
the hardware of most computers ] 

109 
**) 

110 

111 
Goal "(#10::int) div #3 = #4"; 

112 
by (Simp_tac 1); 

113 
result(); 

114 

115 
Goal "(#10::int) mod #3 = #2"; 

116 
by (Simp_tac 1); 

117 
result(); 

118 

119 
(** A negative dividend AND divisor **) 

120 

121 
Goal "(#10::int) div #3 = #3"; 

122 
by (Simp_tac 1); 

123 
result(); 

124 

125 
Goal "(#10::int) mod #3 = #1"; 

126 
by (Simp_tac 1); 

127 
result(); 

128 

129 
(** A few bigger examples **) 

130 

131 
Goal "(#8452::int) mod #3 = #1"; 

132 
by (Simp_tac 1); 

133 
result(); 

134 

135 
Goal "(#59485::int) div #434 = #137"; 

136 
by (Simp_tac 1); 

137 
result(); 

138 

139 
Goal "(#1000006::int) mod #10 = #6"; 

140 
by (Simp_tac 1); 

141 
result(); 

142 

143 

7037  144 
(** division by shifting **) 
145 

146 
Goal "#10000000 div #2 = (#5000000::int)"; 

147 
by (Simp_tac 1); 

148 
result(); 

149 

150 
Goal "#10000001 mod #2 = (#1::int)"; 

151 
by (Simp_tac 1); 

152 
result(); 

153 

154 
Goal "#10000055 div #32 = (#312501::int)"; 

155 
by (Simp_tac 1); 

156 

157 
Goal "#10000055 mod #32 = (#23::int)"; 

158 
by (Simp_tac 1); 

159 

160 
Goal "#100094 div #144 = (#695::int)"; 

161 
by (Simp_tac 1); 

162 
result(); 

163 

164 
Goal "#100094 mod #144 = (#14::int)"; 

165 
by (Simp_tac 1); 

166 
result(); 

167 

168 

169 

170 
(**** The Natural Numbers ****) 

171 

172 
(** Successor **) 

173 

174 
Goal "Suc #99999 = #100000"; 

175 
by (asm_simp_tac (simpset() addsimps [Suc_nat_number_of]) 1); 

176 
(*not a default rewrite since sometimes we want to have Suc(#nnn)*) 

177 
result(); 

178 

179 

180 
(** Addition **) 

181 

182 
Goal "(#13::nat) + #19 = #32"; 

183 
by (Simp_tac 1); 

184 
result(); 

185 

186 
Goal "(#1234::nat) + #5678 = #6912"; 

187 
by (Simp_tac 1); 

188 
result(); 

189 

190 
Goal "(#973646::nat) + #6475 = #980121"; 

191 
by (Simp_tac 1); 

192 
result(); 

193 

194 

195 
(** Subtraction **) 

196 

197 
Goal "(#32::nat)  #14 = #18"; 

198 
by (Simp_tac 1); 

199 
result(); 

200 

201 
Goal "(#14::nat)  #15 = #0"; 

202 
by (Simp_tac 1); 

203 
result(); 

204 

205 
Goal "(#14::nat)  #1576644 = #0"; 

206 
by (Simp_tac 1); 

207 
result(); 

208 

209 
Goal "(#48273776::nat)  #3873737 = #44400039"; 

210 
by (Simp_tac 1); 

211 
result(); 

212 

213 

214 
(** Multiplication **) 

215 

216 
Goal "(#12::nat) * #11 = #132"; 

217 
by (Simp_tac 1); 

218 
result(); 

219 

220 
Goal "(#647::nat) * #3643 = #2357021"; 

221 
by (Simp_tac 1); 

222 
result(); 

223 

224 

225 
(** Quotient and Remainder **) 

226 

227 
Goal "(#10::nat) div #3 = #3"; 

228 
by (Simp_tac 1); 

229 
result(); 

230 

231 
Goal "(#10::nat) mod #3 = #1"; 

232 
by (Simp_tac 1); 

233 
result(); 

234 

235 
Goal "(#10000::nat) div #9 = #1111"; 

236 
by (Simp_tac 1); 

237 
result(); 

238 

239 
Goal "(#10000::nat) mod #9 = #1"; 

240 
by (Simp_tac 1); 

241 
result(); 

242 

243 
Goal "(#10000::nat) div #16 = #625"; 

244 
by (Simp_tac 1); 

245 
result(); 

246 

247 
Goal "(#10000::nat) mod #16 = #0"; 

248 
by (Simp_tac 1); 

249 
result(); 

250 

251 

6920  252 
(*** Testing the cancellation of complementary terms ***) 
5601  253 

6909  254 
Goal "y + (x + x) = (#0::int) + y"; 
5601  255 
by (Simp_tac 1); 
256 
result(); 

257 

6909  258 
Goal "y + (x + ( y + x)) = (#0::int)"; 
5601  259 
by (Simp_tac 1); 
260 
result(); 

261 

6909  262 
Goal "x + (y + ( y + x)) = (#0::int)"; 
5601  263 
by (Simp_tac 1); 
264 
result(); 

265 

6909  266 
Goal "x + (x + ( x + ( x + ( y +  z)))) = (#0::int)  y  z"; 
5601  267 
by (Simp_tac 1); 
268 
result(); 

269 

6909  270 
Goal "x + x  x  x  y  z = (#0::int)  y  z"; 
5601  271 
by (Simp_tac 1); 
272 
result(); 

273 

6909  274 
Goal "x + y + z  (x + z) = y  (#0::int)"; 
5601  275 
by (Simp_tac 1); 
276 
result(); 

277 

6909  278 
Goal "x+(y+(y+(y+ (x + x)))) = (#0::int) + y  x + y + y"; 
5601  279 
by (Simp_tac 1); 
280 
result(); 

281 

6909  282 
Goal "x+(y+(y+(y+ (y + x)))) = y + (#0::int) + y"; 
5601  283 
by (Simp_tac 1); 
284 
result(); 

285 

6909  286 
Goal "x + y  x + z  x  y  z + x < (#1::int)"; 
5601  287 
by (Simp_tac 1); 
288 
result(); 

289 

290 

5545  291 
Addsimps normal.intrs; 
292 

293 
Goal "(w BIT b): normal ==> (w BIT b BIT c): normal"; 

294 
by (case_tac "c" 1); 

295 
by Auto_tac; 

296 
qed "normal_BIT_I"; 

297 

298 
Addsimps [normal_BIT_I]; 

299 

300 
Goal "w BIT b: normal ==> w: normal"; 

301 
by (etac normal.elim 1); 

302 
by Auto_tac; 

303 
qed "normal_BIT_D"; 

304 

305 
Goal "w : normal > NCons w b : normal"; 

306 
by (induct_tac "w" 1); 

307 
by (auto_tac (claset(), simpset() addsimps [NCons_Pls, NCons_Min])); 

308 
qed_spec_mp "NCons_normal"; 

309 

310 
Addsimps [NCons_normal]; 

311 

312 
Goal "NCons w True ~= Pls"; 

313 
by (induct_tac "w" 1); 

314 
by Auto_tac; 

315 
qed "NCons_True"; 

316 

317 
Goal "NCons w False ~= Min"; 

318 
by (induct_tac "w" 1); 

319 
by Auto_tac; 

320 
qed "NCons_False"; 

321 

322 
Goal "w: normal ==> bin_succ w : normal"; 

323 
by (etac normal.induct 1); 

8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

324 
by (case_tac "w" 4); 
5545  325 
by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT])); 
326 
qed "bin_succ_normal"; 

327 

328 
Goal "w: normal ==> bin_pred w : normal"; 

329 
by (etac normal.induct 1); 

8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

330 
by (case_tac "w" 3); 
5545  331 
by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT])); 
332 
qed "bin_pred_normal"; 

333 

334 
Addsimps [bin_succ_normal, bin_pred_normal]; 

335 

336 
Goal "w : normal > (ALL z. z: normal > bin_add w z : normal)"; 

337 
by (induct_tac "w" 1); 

338 
by (Simp_tac 1); 

339 
by (Simp_tac 1); 

340 
by (rtac impI 1); 

341 
by (rtac allI 1); 

342 
by (induct_tac "z" 1); 

343 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT]))); 

344 
by (safe_tac (claset() addSDs [normal_BIT_D])); 

345 
by (ALLGOALS Asm_simp_tac); 

346 
qed_spec_mp "bin_add_normal"; 

347 

6909  348 
Goal "w: normal ==> (w = Pls) = (number_of w = (#0::int))"; 
5545  349 
by (etac normal.induct 1); 
350 
by Auto_tac; 

351 
qed "normal_Pls_eq_0"; 

352 

353 
Goal "w : normal ==> bin_minus w : normal"; 

354 
by (etac normal.induct 1); 

355 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT]))); 

356 
by (resolve_tac normal.intrs 1); 

357 
by (assume_tac 1); 

358 
by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1); 

359 
by (asm_full_simp_tac 

6920  360 
(simpset_of Int.thy 
361 
addsimps [number_of_minus, iszero_def, 

362 
read_instantiate [("y","int 0")] zminus_equation]) 1); 

363 
by (etac not_sym 1); 

5545  364 
qed "bin_minus_normal"; 
365 

366 
Goal "w : normal ==> z: normal > bin_mult w z : normal"; 

367 
by (etac normal.induct 1); 

5569
8c7e1190e789
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5545
diff
changeset

368 
by (ALLGOALS 
8c7e1190e789
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5545
diff
changeset

369 
(asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT]))); 
5545  370 
by (safe_tac (claset() addSDs [normal_BIT_D])); 
371 
by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1); 

372 
qed_spec_mp "bin_mult_normal"; 