90 "norm_Bcons(Bcons(w,x),b) = Bcons(Bcons(w,x),b)"; |
90 "norm_Bcons(Bcons(w,x),b) = Bcons(Bcons(w,x),b)"; |
91 by (asm_simp_tac (ZF_ss addsimps bin.case_eqns) 1); |
91 by (asm_simp_tac (ZF_ss addsimps bin.case_eqns) 1); |
92 qed "norm_Bcons_Bcons"; |
92 qed "norm_Bcons_Bcons"; |
93 |
93 |
94 val norm_Bcons_simps = [norm_Bcons_Plus_0, norm_Bcons_Plus_1, |
94 val norm_Bcons_simps = [norm_Bcons_Plus_0, norm_Bcons_Plus_1, |
95 norm_Bcons_Minus_0, norm_Bcons_Minus_1, |
95 norm_Bcons_Minus_0, norm_Bcons_Minus_1, |
96 norm_Bcons_Bcons]; |
96 norm_Bcons_Bcons]; |
97 |
97 |
98 (** Type checking **) |
98 (** Type checking **) |
99 |
99 |
100 val bin_typechecks0 = bin_rec_type :: bin.intrs; |
100 val bin_typechecks0 = bin_rec_type :: bin.intrs; |
101 |
101 |
102 goalw Bin.thy [integ_of_bin_def] |
102 goalw Bin.thy [integ_of_bin_def] |
103 "!!w. w: bin ==> integ_of_bin(w) : integ"; |
103 "!!w. w: bin ==> integ_of_bin(w) : integ"; |
104 by (typechk_tac (bin_typechecks0@integ_typechecks@ |
104 by (typechk_tac (bin_typechecks0@integ_typechecks@ |
105 nat_typechecks@[bool_into_nat])); |
105 nat_typechecks@[bool_into_nat])); |
106 qed "integ_of_bin_type"; |
106 qed "integ_of_bin_type"; |
107 |
107 |
108 goalw Bin.thy [norm_Bcons_def] |
108 goalw Bin.thy [norm_Bcons_def] |
109 "!!w. [| w: bin; b: bool |] ==> norm_Bcons(w,b) : bin"; |
109 "!!w. [| w: bin; b: bool |] ==> norm_Bcons(w,b) : bin"; |
110 by (etac bin.elim 1); |
110 by (etac bin.elim 1); |
128 qed "bin_minus_type"; |
128 qed "bin_minus_type"; |
129 |
129 |
130 goalw Bin.thy [bin_add_def] |
130 goalw Bin.thy [bin_add_def] |
131 "!!v w. [| v: bin; w: bin |] ==> bin_add(v,w) : bin"; |
131 "!!v w. [| v: bin; w: bin |] ==> bin_add(v,w) : bin"; |
132 by (typechk_tac ([norm_Bcons_type, bin_succ_type, bin_pred_type]@ |
132 by (typechk_tac ([norm_Bcons_type, bin_succ_type, bin_pred_type]@ |
133 bin_typechecks0@ bool_typechecks@ZF_typechecks)); |
133 bin_typechecks0@ bool_typechecks@ZF_typechecks)); |
134 qed "bin_add_type"; |
134 qed "bin_add_type"; |
135 |
135 |
136 goalw Bin.thy [bin_mult_def] |
136 goalw Bin.thy [bin_mult_def] |
137 "!!v w. [| v: bin; w: bin |] ==> bin_mult(v,w) : bin"; |
137 "!!v w. [| v: bin; w: bin |] ==> bin_mult(v,w) : bin"; |
138 by (typechk_tac ([norm_Bcons_type, bin_minus_type, bin_add_type]@ |
138 by (typechk_tac ([norm_Bcons_type, bin_minus_type, bin_add_type]@ |
139 bin_typechecks0@ bool_typechecks)); |
139 bin_typechecks0@ bool_typechecks)); |
140 qed "bin_mult_type"; |
140 qed "bin_mult_type"; |
141 |
141 |
142 val bin_typechecks = bin_typechecks0 @ |
142 val bin_typechecks = bin_typechecks0 @ |
143 [integ_of_bin_type, norm_Bcons_type, bin_succ_type, bin_pred_type, |
143 [integ_of_bin_type, norm_Bcons_type, bin_succ_type, bin_pred_type, |
144 bin_minus_type, bin_add_type, bin_mult_type]; |
144 bin_minus_type, bin_add_type, bin_mult_type]; |
145 |
145 |
146 val bin_ss = integ_ss |
146 val bin_ss = integ_ss |
147 addsimps([bool_1I, bool_0I, |
147 addsimps([bool_1I, bool_0I, |
148 bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ |
148 bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ |
149 bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks); |
149 bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks); |
150 |
150 |
151 val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @ |
151 val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @ |
152 [bool_subset_nat RS subsetD]; |
152 [bool_subset_nat RS subsetD]; |
153 |
153 |
154 (**** The carry/borrow functions, bin_succ and bin_pred ****) |
154 (**** The carry/borrow functions, bin_succ and bin_pred ****) |
371 |
371 |
372 (*** The computation simpset ***) |
372 (*** The computation simpset ***) |
373 |
373 |
374 val bin_comp_ss = integ_ss |
374 val bin_comp_ss = integ_ss |
375 addsimps [integ_of_bin_add RS sym, (*invoke bin_add*) |
375 addsimps [integ_of_bin_add RS sym, (*invoke bin_add*) |
376 integ_of_bin_minus RS sym, (*invoke bin_minus*) |
376 integ_of_bin_minus RS sym, (*invoke bin_minus*) |
377 integ_of_bin_mult RS sym, (*invoke bin_mult*) |
377 integ_of_bin_mult RS sym, (*invoke bin_mult*) |
378 bin_succ_Plus, bin_succ_Minus, |
378 bin_succ_Plus, bin_succ_Minus, |
379 bin_succ_Bcons1, bin_succ_Bcons0, |
379 bin_succ_Bcons1, bin_succ_Bcons0, |
380 bin_pred_Plus, bin_pred_Minus, |
380 bin_pred_Plus, bin_pred_Minus, |
381 bin_pred_Bcons1, bin_pred_Bcons0, |
381 bin_pred_Bcons1, bin_pred_Bcons0, |
382 bin_minus_Plus, bin_minus_Minus, |
382 bin_minus_Plus, bin_minus_Minus, |
383 bin_minus_Bcons1, bin_minus_Bcons0, |
383 bin_minus_Bcons1, bin_minus_Bcons0, |
384 bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, |
384 bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, |
385 bin_add_Bcons_Minus, bin_add_Bcons_Bcons0, |
385 bin_add_Bcons_Minus, bin_add_Bcons_Bcons0, |
386 bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11, |
386 bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11, |
387 bin_mult_Plus, bin_mult_Minus, |
387 bin_mult_Plus, bin_mult_Minus, |
388 bin_mult_Bcons1, bin_mult_Bcons0] @ |
388 bin_mult_Bcons1, bin_mult_Bcons0] @ |
389 norm_Bcons_simps |
389 norm_Bcons_simps |
390 setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0)); |
390 setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0)); |
391 |
391 |
392 (*** Examples of performing binary arithmetic by simplification ***) |
392 (*** Examples of performing binary arithmetic by simplification ***) |
393 |
393 |
394 proof_timing := true; |
394 proof_timing := true; |
395 (*All runtimes below are on a SPARCserver 10*) |
395 (*All runtimes below are on a SPARCserver 10*) |
396 |
396 |
397 goal Bin.thy "#13 $+ #19 = #32"; |
397 goal Bin.thy "#13 $+ #19 = #32"; |
398 by (simp_tac bin_comp_ss 1); (*0.4 secs*) |
398 by (simp_tac bin_comp_ss 1); (*0.4 secs*) |
399 result(); |
399 result(); |
400 |
400 |
401 bin_add(binary_of_int 13, binary_of_int 19); |
401 bin_add(binary_of_int 13, binary_of_int 19); |
402 |
402 |
403 goal Bin.thy "#1234 $+ #5678 = #6912"; |
403 goal Bin.thy "#1234 $+ #5678 = #6912"; |
404 by (simp_tac bin_comp_ss 1); (*1.3 secs*) |
404 by (simp_tac bin_comp_ss 1); (*1.3 secs*) |
405 result(); |
405 result(); |
406 |
406 |
407 bin_add(binary_of_int 1234, binary_of_int 5678); |
407 bin_add(binary_of_int 1234, binary_of_int 5678); |
408 |
408 |
409 goal Bin.thy "#1359 $+ #~2468 = #~1109"; |
409 goal Bin.thy "#1359 $+ #~2468 = #~1109"; |
410 by (simp_tac bin_comp_ss 1); (*1.2 secs*) |
410 by (simp_tac bin_comp_ss 1); (*1.2 secs*) |
411 result(); |
411 result(); |
412 |
412 |
413 bin_add(binary_of_int 1359, binary_of_int ~2468); |
413 bin_add(binary_of_int 1359, binary_of_int ~2468); |
414 |
414 |
415 goal Bin.thy "#93746 $+ #~46375 = #47371"; |
415 goal Bin.thy "#93746 $+ #~46375 = #47371"; |
416 by (simp_tac bin_comp_ss 1); (*1.9 secs*) |
416 by (simp_tac bin_comp_ss 1); (*1.9 secs*) |
417 result(); |
417 result(); |
418 |
418 |
419 bin_add(binary_of_int 93746, binary_of_int ~46375); |
419 bin_add(binary_of_int 93746, binary_of_int ~46375); |
420 |
420 |
421 goal Bin.thy "$~ #65745 = #~65745"; |
421 goal Bin.thy "$~ #65745 = #~65745"; |
422 by (simp_tac bin_comp_ss 1); (*0.4 secs*) |
422 by (simp_tac bin_comp_ss 1); (*0.4 secs*) |
423 result(); |
423 result(); |
424 |
424 |
425 bin_minus(binary_of_int 65745); |
425 bin_minus(binary_of_int 65745); |
426 |
426 |
427 (* negation of ~54321 *) |
427 (* negation of ~54321 *) |
428 goal Bin.thy "$~ #~54321 = #54321"; |
428 goal Bin.thy "$~ #~54321 = #54321"; |
429 by (simp_tac bin_comp_ss 1); (*0.5 secs*) |
429 by (simp_tac bin_comp_ss 1); (*0.5 secs*) |
430 result(); |
430 result(); |
431 |
431 |
432 bin_minus(binary_of_int ~54321); |
432 bin_minus(binary_of_int ~54321); |
433 |
433 |
434 goal Bin.thy "#13 $* #19 = #247"; |
434 goal Bin.thy "#13 $* #19 = #247"; |
435 by (simp_tac bin_comp_ss 1); (*0.7 secs*) |
435 by (simp_tac bin_comp_ss 1); (*0.7 secs*) |
436 result(); |
436 result(); |
437 |
437 |
438 bin_mult(binary_of_int 13, binary_of_int 19); |
438 bin_mult(binary_of_int 13, binary_of_int 19); |
439 |
439 |
440 goal Bin.thy "#~84 $* #51 = #~4284"; |
440 goal Bin.thy "#~84 $* #51 = #~4284"; |
441 by (simp_tac bin_comp_ss 1); (*1.3 secs*) |
441 by (simp_tac bin_comp_ss 1); (*1.3 secs*) |
442 result(); |
442 result(); |
443 |
443 |
444 bin_mult(binary_of_int ~84, binary_of_int 51); |
444 bin_mult(binary_of_int ~84, binary_of_int 51); |
445 |
445 |
446 (*The worst case for 8-bit operands *) |
446 (*The worst case for 8-bit operands *) |
447 goal Bin.thy "#255 $* #255 = #65025"; |
447 goal Bin.thy "#255 $* #255 = #65025"; |
448 by (simp_tac bin_comp_ss 1); (*4.3 secs*) |
448 by (simp_tac bin_comp_ss 1); (*4.3 secs*) |
449 result(); |
449 result(); |
450 |
450 |
451 bin_mult(binary_of_int 255, binary_of_int 255); |
451 bin_mult(binary_of_int 255, binary_of_int 255); |
452 |
452 |
453 goal Bin.thy "#1359 $* #~2468 = #~3354012"; |
453 goal Bin.thy "#1359 $* #~2468 = #~3354012"; |
454 by (simp_tac bin_comp_ss 1); (*6.1 secs*) |
454 by (simp_tac bin_comp_ss 1); (*6.1 secs*) |
455 result(); |
455 result(); |
456 |
456 |
457 bin_mult(binary_of_int 1359, binary_of_int ~2468); |
457 bin_mult(binary_of_int 1359, binary_of_int ~2468); |