author | wenzelm |
Tue, 25 Jul 2000 00:06:46 +0200 | |
changeset 9436 | 62bb04ab4b01 |
parent 9000 | c20d58286a51 |
permissions | -rw-r--r-- |
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"; |