206 |
234 |
207 goalw Bin.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)"; |
235 goalw Bin.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)"; |
208 by (asm_simp_tac bin_ss 1); |
236 by (asm_simp_tac bin_ss 1); |
209 qed "bin_add_Minus"; |
237 qed "bin_add_Minus"; |
210 |
238 |
211 goalw Bin.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x"; |
239 goalw Bin.thy [bin_add_def] "bin_add(Bcons(v,x),Plus) = Bcons(v,x)"; |
212 by (simp_tac bin_ss 1); |
240 by (simp_tac bin_ss 1); |
213 qed "bin_add_Bcons_Plus"; |
241 qed "bin_add_Bcons_Plus"; |
214 |
242 |
215 goalw Bin.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)"; |
243 goalw Bin.thy [bin_add_def] "bin_add(Bcons(v,x),Minus) = bin_pred(Bcons(v,x))"; |
216 by (simp_tac bin_ss 1); |
244 by (simp_tac bin_ss 1); |
217 qed "bin_add_Bcons_Minus"; |
245 qed "bin_add_Bcons_Minus"; |
218 |
246 |
219 goalw Bin.thy [bin_add_def] |
247 goalw Bin.thy [bin_add_def] |
220 "!!w y. [| w: bin; y: bool |] ==> \ |
248 "!!w y. [| w: bin; y: bool |] ==> \ |
221 \ bin_add(v$$x, w$$y) = \ |
249 \ bin_add(Bcons(v,x), Bcons(w,y)) = \ |
222 \ bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)"; |
250 \ norm_Bcons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"; |
223 by (asm_simp_tac bin_ss 1); |
251 by (asm_simp_tac bin_ss 1); |
224 qed "bin_add_Bcons_Bcons"; |
252 qed "bin_add_Bcons_Bcons"; |
225 |
253 |
226 val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, |
254 val bin_add_simps = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, |
227 bin_add_Bcons_Minus, bin_add_Bcons_Bcons, |
255 bin_add_Bcons_Minus, bin_add_Bcons_Bcons, |
228 integ_of_bin_succ, integ_of_bin_pred]; |
256 integ_of_bin_succ, integ_of_bin_pred, |
229 |
257 integ_of_bin_norm_Bcons]; |
230 val bin_add_ss = bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_rews); |
258 |
|
259 val bin_add_ss = |
|
260 bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_simps); |
231 |
261 |
232 goal Bin.thy |
262 goal Bin.thy |
233 "!!v. v: bin ==> \ |
263 "!!v. v: bin ==> \ |
234 \ ALL w: bin. integ_of_bin(bin_add(v,w)) = \ |
264 \ ALL w: bin. integ_of_bin(bin_add(v,w)) = \ |
235 \ integ_of_bin(v) $+ integ_of_bin(w)"; |
265 \ integ_of_bin(v) $+ integ_of_bin(w)"; |
236 by (etac bin.induct 1); |
266 by (etac bin.induct 1); |
237 by (simp_tac bin_add_ss 1); |
267 by (simp_tac bin_add_ss 1); |
238 by (simp_tac bin_add_ss 1); |
268 by (simp_tac bin_add_ss 1); |
239 by (rtac ballI 1); |
269 by (rtac ballI 1); |
240 by (bin_ind_tac "wa" [] 1); |
270 by (bin_ind_tac "wa" [] 1); |
241 by (asm_simp_tac (bin_add_ss addsimps [zadd_0_right]) 1); |
|
242 by (asm_simp_tac bin_add_ss 1); |
271 by (asm_simp_tac bin_add_ss 1); |
243 by (REPEAT (ares_tac (zadd_commute::typechecks) 1)); |
272 by (asm_simp_tac (bin_add_ss addsimps zadd_ac) 1); |
244 by (etac boolE 1); |
273 by (etac boolE 1); |
245 by (asm_simp_tac (bin_add_ss addsimps [zadd_assoc, zadd_swap_pairs]) 2); |
274 by (asm_simp_tac (bin_add_ss addsimps zadd_ac) 2); |
246 by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2)); |
275 by (etac boolE 1); |
247 by (etac boolE 1); |
276 by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps zadd_ac))); |
248 by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs]))); |
277 val integ_of_bin_add_lemma = result(); |
249 by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@ |
278 |
250 typechecks) 1)); |
279 bind_thm("integ_of_bin_add", integ_of_bin_add_lemma RS bspec); |
251 qed "integ_of_bin_add_lemma"; |
|
252 |
|
253 val integ_of_bin_add = integ_of_bin_add_lemma RS bspec; |
|
254 |
280 |
255 |
281 |
256 (*** bin_add: binary multiplication ***) |
282 (*** bin_add: binary multiplication ***) |
257 |
283 |
258 val bin_mult_ss = |
284 val bin_mult_ss = |
259 bin_ss addsimps (bin_recs bin_mult_def @ |
285 bin_ss addsimps (bin_recs bin_mult_def @ |
260 [integ_of_bin_minus, integ_of_bin_add]); |
286 [integ_of_bin_minus, integ_of_bin_add, |
261 |
287 integ_of_bin_norm_Bcons]); |
262 |
288 |
263 val major::prems = goal Bin.thy |
289 val major::prems = goal Bin.thy |
264 "[| v: bin; w: bin |] ==> \ |
290 "[| v: bin; w: bin |] ==> \ |
265 \ integ_of_bin(bin_mult(v,w)) = \ |
291 \ integ_of_bin(bin_mult(v,w)) = \ |
266 \ integ_of_bin(v) $* integ_of_bin(w)"; |
292 \ integ_of_bin(v) $* integ_of_bin(w)"; |
267 by (cut_facts_tac prems 1); |
293 by (cut_facts_tac prems 1); |
268 by (bin_ind_tac "v" [major] 1); |
294 by (bin_ind_tac "v" [major] 1); |
269 by (asm_simp_tac (bin_mult_ss addsimps [zmult_0]) 1); |
295 by (asm_simp_tac bin_mult_ss 1); |
270 by (asm_simp_tac (bin_mult_ss addsimps [zmult_1,zmult_zminus]) 1); |
296 by (asm_simp_tac bin_mult_ss 1); |
271 by (etac boolE 1); |
297 by (etac boolE 1); |
272 by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2); |
298 by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2); |
273 by (asm_simp_tac |
299 by (asm_simp_tac |
274 (bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1); |
300 (bin_mult_ss addsimps ([zadd_zmult_distrib, zmult_1] @ zadd_ac)) 1); |
275 by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@ |
|
276 typechecks) 1)); |
|
277 qed "integ_of_bin_mult"; |
301 qed "integ_of_bin_mult"; |
278 |
302 |
279 (**** Computations ****) |
303 (**** Computations ****) |
280 |
304 |
281 (** extra rules for bin_succ, bin_pred **) |
305 (** extra rules for bin_succ, bin_pred **) |
282 |
306 |
283 val [bin_succ_Plus, bin_succ_Minus, _] = bin_recs bin_succ_def; |
307 val [bin_succ_Plus, bin_succ_Minus, _] = bin_recs bin_succ_def; |
284 val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def; |
308 val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def; |
285 |
309 |
286 goal Bin.thy "bin_succ(w$$1) = bin_succ(w) $$ 0"; |
310 goal Bin.thy "bin_succ(Bcons(w,1)) = Bcons(bin_succ(w), 0)"; |
287 by (simp_tac carry_ss 1); |
311 by (simp_tac carry_ss 1); |
288 qed "bin_succ_Bcons1"; |
312 qed "bin_succ_Bcons1"; |
289 |
313 |
290 goal Bin.thy "bin_succ(w$$0) = w$$1"; |
314 goal Bin.thy "bin_succ(Bcons(w,0)) = norm_Bcons(w,1)"; |
291 by (simp_tac carry_ss 1); |
315 by (simp_tac carry_ss 1); |
292 qed "bin_succ_Bcons0"; |
316 qed "bin_succ_Bcons0"; |
293 |
317 |
294 goal Bin.thy "bin_pred(w$$1) = w$$0"; |
318 goal Bin.thy "bin_pred(Bcons(w,1)) = norm_Bcons(w,0)"; |
295 by (simp_tac carry_ss 1); |
319 by (simp_tac carry_ss 1); |
296 qed "bin_pred_Bcons1"; |
320 qed "bin_pred_Bcons1"; |
297 |
321 |
298 goal Bin.thy "bin_pred(w$$0) = bin_pred(w) $$ 1"; |
322 goal Bin.thy "bin_pred(Bcons(w,0)) = Bcons(bin_pred(w), 1)"; |
299 by (simp_tac carry_ss 1); |
323 by (simp_tac carry_ss 1); |
300 qed "bin_pred_Bcons0"; |
324 qed "bin_pred_Bcons0"; |
301 |
325 |
302 (** extra rules for bin_minus **) |
326 (** extra rules for bin_minus **) |
303 |
327 |
304 val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def; |
328 val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def; |
305 |
329 |
306 goal Bin.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)"; |
330 goal Bin.thy "bin_minus(Bcons(w,1)) = bin_pred(Bcons(bin_minus(w), 0))"; |
307 by (simp_tac bin_minus_ss 1); |
331 by (simp_tac bin_minus_ss 1); |
308 qed "bin_minus_Bcons1"; |
332 qed "bin_minus_Bcons1"; |
309 |
333 |
310 goal Bin.thy "bin_minus(w$$0) = bin_minus(w) $$ 0"; |
334 goal Bin.thy "bin_minus(Bcons(w,0)) = Bcons(bin_minus(w), 0)"; |
311 by (simp_tac bin_minus_ss 1); |
335 by (simp_tac bin_minus_ss 1); |
312 qed "bin_minus_Bcons0"; |
336 qed "bin_minus_Bcons0"; |
313 |
337 |
314 (** extra rules for bin_add **) |
338 (** extra rules for bin_add **) |
315 |
339 |
316 goal Bin.thy |
340 goal Bin.thy |
317 "!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0"; |
341 "!!w. w: bin ==> bin_add(Bcons(v,1), Bcons(w,1)) = \ |
|
342 \ norm_Bcons(bin_add(v, bin_succ(w)), 0)"; |
318 by (asm_simp_tac bin_add_ss 1); |
343 by (asm_simp_tac bin_add_ss 1); |
319 qed "bin_add_Bcons_Bcons11"; |
344 qed "bin_add_Bcons_Bcons11"; |
320 |
345 |
321 goal Bin.thy |
346 goal Bin.thy |
322 "!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1"; |
347 "!!w. w: bin ==> bin_add(Bcons(v,1), Bcons(w,0)) = \ |
|
348 \ norm_Bcons(bin_add(v,w), 1)"; |
323 by (asm_simp_tac bin_add_ss 1); |
349 by (asm_simp_tac bin_add_ss 1); |
324 qed "bin_add_Bcons_Bcons10"; |
350 qed "bin_add_Bcons_Bcons10"; |
325 |
351 |
326 goal Bin.thy |
352 goal Bin.thy |
327 "!!w y.[| w: bin; y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y"; |
353 "!!w y. [| w: bin; y: bool |] ==> \ |
|
354 \ bin_add(Bcons(v,0), Bcons(w,y)) = norm_Bcons(bin_add(v,w), y)"; |
328 by (asm_simp_tac bin_add_ss 1); |
355 by (asm_simp_tac bin_add_ss 1); |
329 qed "bin_add_Bcons_Bcons0"; |
356 qed "bin_add_Bcons_Bcons0"; |
330 |
357 |
331 (** extra rules for bin_mult **) |
358 (** extra rules for bin_mult **) |
332 |
359 |
333 val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def; |
360 val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def; |
334 |
361 |
335 goal Bin.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)"; |
362 goal Bin.thy |
|
363 "bin_mult(Bcons(v,1), w) = bin_add(norm_Bcons(bin_mult(v,w),0), w)"; |
336 by (simp_tac bin_mult_ss 1); |
364 by (simp_tac bin_mult_ss 1); |
337 qed "bin_mult_Bcons1"; |
365 qed "bin_mult_Bcons1"; |
338 |
366 |
339 goal Bin.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0"; |
367 goal Bin.thy "bin_mult(Bcons(v,0), w) = norm_Bcons(bin_mult(v,w),0)"; |
340 by (simp_tac bin_mult_ss 1); |
368 by (simp_tac bin_mult_ss 1); |
341 qed "bin_mult_Bcons0"; |
369 qed "bin_mult_Bcons0"; |
342 |
370 |
343 |
371 |
344 (*** The computation simpset ***) |
372 (*** The computation simpset ***) |
345 |
373 |
346 val bin_comp_ss = integ_ss |
374 val bin_comp_ss = integ_ss |
347 addsimps [bin_succ_Plus, bin_succ_Minus, |
375 addsimps [integ_of_bin_add RS sym, (*invoke bin_add*) |
348 bin_succ_Bcons1, bin_succ_Bcons0, |
376 integ_of_bin_minus RS sym, (*invoke bin_minus*) |
349 bin_pred_Plus, bin_pred_Minus, |
377 integ_of_bin_mult RS sym, (*invoke bin_mult*) |
350 bin_pred_Bcons1, bin_pred_Bcons0, |
378 bin_succ_Plus, bin_succ_Minus, |
351 bin_minus_Plus, bin_minus_Minus, |
379 bin_succ_Bcons1, bin_succ_Bcons0, |
352 bin_minus_Bcons1, bin_minus_Bcons0, |
380 bin_pred_Plus, bin_pred_Minus, |
353 bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, |
381 bin_pred_Bcons1, bin_pred_Bcons0, |
354 bin_add_Bcons_Minus, bin_add_Bcons_Bcons0, |
382 bin_minus_Plus, bin_minus_Minus, |
355 bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11, |
383 bin_minus_Bcons1, bin_minus_Bcons0, |
356 bin_mult_Plus, bin_mult_Minus, |
384 bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, |
357 bin_mult_Bcons1, bin_mult_Bcons0] |
385 bin_add_Bcons_Minus, bin_add_Bcons_Bcons0, |
|
386 bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11, |
|
387 bin_mult_Plus, bin_mult_Minus, |
|
388 bin_mult_Bcons1, bin_mult_Bcons0] @ |
|
389 norm_Bcons_simps |
358 setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0)); |
390 setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0)); |
359 |
391 |
360 (*** Examples of performing binary arithmetic by simplification ***) |
392 (*** Examples of performing binary arithmetic by simplification ***) |
361 |
393 |
362 proof_timing := true; |
394 proof_timing := true; |
363 (*All runtimes below are on a SPARCserver 10*) |
395 (*All runtimes below are on a SPARCserver 10*) |
364 |
396 |
365 (* 13+19 = 32 *) |
397 goal Bin.thy "#13 $+ #19 = #32"; |
366 goal Bin.thy |
398 by (simp_tac bin_comp_ss 1); (*0.4 secs*) |
367 "bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0"; |
|
368 by (simp_tac bin_comp_ss 1); (*0.6 secs*) |
|
369 result(); |
399 result(); |
370 |
400 |
371 bin_add(binary_of_int 13, binary_of_int 19); |
401 bin_add(binary_of_int 13, binary_of_int 19); |
372 |
402 |
373 (* 1234+5678 = 6912 *) |
403 goal Bin.thy "#1234 $+ #5678 = #6912"; |
374 goal Bin.thy |
404 by (simp_tac bin_comp_ss 1); (*1.3 secs*) |
375 "bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \ |
|
376 \ Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \ |
|
377 \ Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0"; |
|
378 by (simp_tac bin_comp_ss 1); (*2.6 secs*) |
|
379 result(); |
405 result(); |
380 |
406 |
381 bin_add(binary_of_int 1234, binary_of_int 5678); |
407 bin_add(binary_of_int 1234, binary_of_int 5678); |
382 |
408 |
383 (* 1359-2468 = ~1109 *) |
409 goal Bin.thy "#1359 $+ #~2468 = #~1109"; |
384 goal Bin.thy |
410 by (simp_tac bin_comp_ss 1); (*1.2 secs*) |
385 "bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \ |
|
386 \ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \ |
|
387 \ Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1"; |
|
388 by (simp_tac bin_comp_ss 1); (*2.3 secs*) |
|
389 result(); |
411 result(); |
390 |
412 |
391 bin_add(binary_of_int 1359, binary_of_int ~2468); |
413 bin_add(binary_of_int 1359, binary_of_int ~2468); |
392 |
414 |
393 (* 93746-46375 = 47371 *) |
415 goal Bin.thy "#93746 $+ #~46375 = #47371"; |
394 goal Bin.thy |
416 by (simp_tac bin_comp_ss 1); (*1.9 secs*) |
395 "bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \ |
|
396 \ Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \ |
|
397 \ Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1"; |
|
398 by (simp_tac bin_comp_ss 1); (*3.9 secs*) |
|
399 result(); |
417 result(); |
400 |
418 |
401 bin_add(binary_of_int 93746, binary_of_int ~46375); |
419 bin_add(binary_of_int 93746, binary_of_int ~46375); |
402 |
420 |
403 (* negation of 65745 *) |
421 goal Bin.thy "$~ #65745 = #~65745"; |
404 goal Bin.thy |
422 by (simp_tac bin_comp_ss 1); (*0.4 secs*) |
405 "bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \ |
|
406 \ Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1"; |
|
407 by (simp_tac bin_comp_ss 1); (*0.6 secs*) |
|
408 result(); |
423 result(); |
409 |
424 |
410 bin_minus(binary_of_int 65745); |
425 bin_minus(binary_of_int 65745); |
411 |
426 |
412 (* negation of ~54321 *) |
427 (* negation of ~54321 *) |
413 goal Bin.thy |
428 goal Bin.thy "$~ #~54321 = #54321"; |
414 "bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \ |
429 by (simp_tac bin_comp_ss 1); (*0.5 secs*) |
415 \ Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1"; |
430 result(); |
|
431 |
|
432 bin_minus(binary_of_int ~54321); |
|
433 |
|
434 goal Bin.thy "#13 $* #19 = #247"; |
416 by (simp_tac bin_comp_ss 1); (*0.7 secs*) |
435 by (simp_tac bin_comp_ss 1); (*0.7 secs*) |
417 result(); |
436 result(); |
418 |
437 |
419 bin_minus(binary_of_int ~54321); |
|
420 |
|
421 (* 13*19 = 247 *) |
|
422 goal Bin.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \ |
|
423 \ Plus$$1$$1$$1$$1$$0$$1$$1$$1"; |
|
424 by (simp_tac bin_comp_ss 1); (*1.5 secs*) |
|
425 result(); |
|
426 |
|
427 bin_mult(binary_of_int 13, binary_of_int 19); |
438 bin_mult(binary_of_int 13, binary_of_int 19); |
428 |
439 |
429 (* ~84 * 51 = ~4284 *) |
440 goal Bin.thy "#~84 $* #51 = #~4284"; |
430 goal Bin.thy |
441 by (simp_tac bin_comp_ss 1); (*1.3 secs*) |
431 "bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \ |
|
432 \ Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0"; |
|
433 by (simp_tac bin_comp_ss 1); (*2.6 secs*) |
|
434 result(); |
442 result(); |
435 |
443 |
436 bin_mult(binary_of_int ~84, binary_of_int 51); |
444 bin_mult(binary_of_int ~84, binary_of_int 51); |
437 |
445 |
438 (* 255*255 = 65025; the worst case for 8-bit operands *) |
446 (*The worst case for 8-bit operands *) |
439 goal Bin.thy |
447 goal Bin.thy "#255 $* #255 = #65025"; |
440 "bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \ |
448 by (simp_tac bin_comp_ss 1); (*4.3 secs*) |
441 \ Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \ |
|
442 \ Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1"; |
|
443 by (simp_tac bin_comp_ss 1); (*9.8 secs*) |
|
444 result(); |
449 result(); |
445 |
450 |
446 bin_mult(binary_of_int 255, binary_of_int 255); |
451 bin_mult(binary_of_int 255, binary_of_int 255); |
447 |
452 |
448 (* 1359 * ~2468 = ~3354012 *) |
453 goal Bin.thy "#1359 $* #~2468 = #~3354012"; |
449 goal Bin.thy |
454 by (simp_tac bin_comp_ss 1); (*6.1 secs*) |
450 "bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \ |
|
451 \ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \ |
|
452 \ Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0"; |
|
453 by (simp_tac bin_comp_ss 1); (*13.7 secs*) |
|
454 result(); |
455 result(); |
455 |
456 |
456 bin_mult(binary_of_int 1359, binary_of_int ~2468); |
457 bin_mult(binary_of_int 1359, binary_of_int ~2468); |