# HG changeset patch # User lcp # Date 793901485 -3600 # Node ID 6cd9c397f36ad5e395b0d57046d9278abfdeb86d # Parent 80b581036036253cca65204315243041a3c0064f Redefined arithmetic to suppress redundant leading 0s and 1s renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix. diff -r 80b581036036 -r 6cd9c397f36a src/ZF/ex/Bin.ML --- a/src/ZF/ex/Bin.ML Mon Feb 27 17:08:51 1995 +0100 +++ b/src/ZF/ex/Bin.ML Mon Feb 27 17:11:25 1995 +0100 @@ -29,7 +29,7 @@ by (simp_tac rank_ss 1); qed "bin_rec_Minus"; -goal Bin.thy "bin_rec(w$$x,a,b,h) = h(w, x, bin_rec(w,a,b,h))"; +goal Bin.thy "bin_rec(Bcons(w,x),a,b,h) = h(w, x, bin_rec(w,a,b,h))"; by (rtac (bin_rec_def RS def_Vrec RS trans) 1); by (rewrite_goals_tac bin.con_defs); by (simp_tac rank_ss 1); @@ -39,12 +39,12 @@ val prems = goal Bin.thy "[| w: bin; \ \ a: C(Plus); b: C(Minus); \ -\ !!w x r. [| w: bin; x: bool; r: C(w) |] ==> h(w,x,r): C(w$$x) \ +\ !!w x r. [| w: bin; x: bool; r: C(w) |] ==> h(w,x,r): C(Bcons(w,x)) \ \ |] ==> bin_rec(w,a,b,h) : C(w)"; by (bin_ind_tac "w" prems 1); by (ALLGOALS - (asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus,bin_rec_Minus, - bin_rec_Bcons])))); + (asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus, bin_rec_Minus, + bin_rec_Bcons])))); qed "bin_rec_type"; (** Versions for use with definitions **) @@ -62,7 +62,7 @@ qed "def_bin_rec_Minus"; val [rew] = goal Bin.thy - "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(w$$x) = h(w,x,j(w))"; + "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Bcons(w,x)) = h(w,x,j(w))"; by (rewtac rew); by (rtac bin_rec_Bcons 1); qed "def_bin_rec_Bcons"; @@ -70,6 +70,31 @@ fun bin_recs def = map standard ([def] RL [def_bin_rec_Plus, def_bin_rec_Minus, def_bin_rec_Bcons]); +goalw Bin.thy [norm_Bcons_def] "norm_Bcons(Plus,0) = Plus"; +by (asm_simp_tac (ZF_ss addsimps (bin.case_eqns @ bool_simps)) 1); +qed "norm_Bcons_Plus_0"; + +goalw Bin.thy [norm_Bcons_def] "norm_Bcons(Plus,1) = Bcons(Plus,1)"; +by (asm_simp_tac (ZF_ss addsimps (bin.case_eqns @ bool_simps)) 1); +qed "norm_Bcons_Plus_1"; + +goalw Bin.thy [norm_Bcons_def] "norm_Bcons(Minus,0) = Bcons(Minus,0)"; +by (asm_simp_tac (ZF_ss addsimps (bin.case_eqns @ bool_simps)) 1); +qed "norm_Bcons_Minus_0"; + +goalw Bin.thy [norm_Bcons_def] "norm_Bcons(Minus,1) = Minus"; +by (asm_simp_tac (ZF_ss addsimps (bin.case_eqns @ bool_simps)) 1); +qed "norm_Bcons_Minus_1"; + +goalw Bin.thy [norm_Bcons_def] + "norm_Bcons(Bcons(w,x),b) = Bcons(Bcons(w,x),b)"; +by (asm_simp_tac (ZF_ss addsimps bin.case_eqns) 1); +qed "norm_Bcons_Bcons"; + +val norm_Bcons_simps = [norm_Bcons_Plus_0, norm_Bcons_Plus_1, + norm_Bcons_Minus_0, norm_Bcons_Minus_1, + norm_Bcons_Bcons]; + (** Type checking **) val bin_typechecks0 = bin_rec_type :: bin.intrs; @@ -80,14 +105,21 @@ nat_typechecks@[bool_into_nat])); qed "integ_of_bin_type"; +goalw Bin.thy [norm_Bcons_def] + "!!w. [| w: bin; b: bool |] ==> norm_Bcons(w,b) : bin"; +by (etac bin.elim 1); +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps bin.case_eqns))); +by (typechk_tac (bin_typechecks0@bool_typechecks)); +qed "norm_Bcons_type"; + goalw Bin.thy [bin_succ_def] "!!w. w: bin ==> bin_succ(w) : bin"; -by (typechk_tac (bin_typechecks0@bool_typechecks)); +by (typechk_tac ([norm_Bcons_type]@bin_typechecks0@bool_typechecks)); qed "bin_succ_type"; goalw Bin.thy [bin_pred_def] "!!w. w: bin ==> bin_pred(w) : bin"; -by (typechk_tac (bin_typechecks0@bool_typechecks)); +by (typechk_tac ([norm_Bcons_type]@bin_typechecks0@bool_typechecks)); qed "bin_pred_type"; goalw Bin.thy [bin_minus_def] @@ -97,18 +129,18 @@ goalw Bin.thy [bin_add_def] "!!v w. [| v: bin; w: bin |] ==> bin_add(v,w) : bin"; -by (typechk_tac ([bin_succ_type,bin_pred_type]@bin_typechecks0@ - bool_typechecks@ZF_typechecks)); +by (typechk_tac ([norm_Bcons_type, bin_succ_type, bin_pred_type]@ + bin_typechecks0@ bool_typechecks@ZF_typechecks)); qed "bin_add_type"; goalw Bin.thy [bin_mult_def] "!!v w. [| v: bin; w: bin |] ==> bin_mult(v,w) : bin"; -by (typechk_tac ([bin_minus_type,bin_add_type]@bin_typechecks0@ - bool_typechecks)); +by (typechk_tac ([norm_Bcons_type, bin_minus_type, bin_add_type]@ + bin_typechecks0@ bool_typechecks)); qed "bin_mult_type"; val bin_typechecks = bin_typechecks0 @ - [integ_of_bin_type, bin_succ_type, bin_pred_type, + [integ_of_bin_type, norm_Bcons_type, bin_succ_type, bin_pred_type, bin_minus_type, bin_add_type, bin_mult_type]; val bin_ss = integ_ss @@ -136,46 +168,42 @@ by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1)); qed "zadd_assoc_swap"; -val zadd_cong = - read_instantiate_sg (sign_of Integ.thy) [("t","op $+")] subst_context2; - -val zadd_kill = (refl RS zadd_cong); -val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans); - (*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*) bind_thm ("zadd_assoc_znat", (znat_type RS zadd_assoc_swap)); -goal Integ.thy - "!!z w. [| z: integ; w: integ |] \ -\ ==> w $+ (z $+ (w $+ z)) = w $+ (w $+ (z $+ z))"; -by (REPEAT (ares_tac [zadd_kill, zadd_assoc_swap] 1)); -qed "zadd_swap_pairs"; - val carry_ss = bin_ss addsimps (bin_recs bin_succ_def @ bin_recs bin_pred_def); + +(*norm_Bcons preserves the integer value of its argument*) +goal Bin.thy + "!!w. [| w: bin; b: bool |] ==> \ +\ integ_of_bin(norm_Bcons(w,b)) = integ_of_bin(Bcons(w,b))"; +by (etac bin.elim 1); +by (asm_simp_tac (ZF_ss addsimps norm_Bcons_simps) 3); +by (ALLGOALS (etac boolE)); +by (ALLGOALS (asm_simp_tac (bin_ss addsimps (norm_Bcons_simps)))); +qed "integ_of_bin_norm_Bcons"; + goal Bin.thy "!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)"; by (etac bin.induct 1); -by (simp_tac (carry_ss addsimps [zadd_0_right]) 1); -by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1); +by (simp_tac carry_ss 1); +by (simp_tac carry_ss 1); by (etac boolE 1); -by (ALLGOALS (asm_simp_tac (carry_ss addsimps [zadd_assoc]))); -by (REPEAT (ares_tac (zadd_swap_pairs::typechecks) 1)); +by (ALLGOALS + (asm_simp_tac (carry_ss addsimps integ_of_bin_norm_Bcons::zadd_ac))); qed "integ_of_bin_succ"; goal Bin.thy "!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)"; by (etac bin.induct 1); -by (simp_tac (carry_ss addsimps [zadd_0_right]) 1); -by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1); +by (simp_tac carry_ss 1); +by (simp_tac carry_ss 1); by (etac boolE 1); -by (ALLGOALS - (asm_simp_tac - (carry_ss addsimps [zadd_assoc RS sym, - zadd_zminus_inverse, zadd_zminus_inverse2]))); -by (REPEAT (ares_tac ([zadd_commute, zadd_cong, refl]@typechecks) 1)); +by (ALLGOALS + (asm_simp_tac (carry_ss addsimps integ_of_bin_norm_Bcons::zadd_ac))); qed "integ_of_bin_pred"; (*These two results replace the definitions of bin_succ and bin_pred*) @@ -190,8 +218,8 @@ goal Bin.thy "!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)"; by (etac bin.induct 1); -by (simp_tac (bin_minus_ss addsimps [zminus_0]) 1); -by (simp_tac (bin_minus_ss addsimps [zadd_0_right]) 1); +by (simp_tac bin_minus_ss 1); +by (simp_tac bin_minus_ss 1); by (etac boolE 1); by (ALLGOALS (asm_simp_tac (bin_minus_ss addsimps [zminus_zadd_distrib, zadd_assoc]))); @@ -208,26 +236,28 @@ by (asm_simp_tac bin_ss 1); qed "bin_add_Minus"; -goalw Bin.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x"; +goalw Bin.thy [bin_add_def] "bin_add(Bcons(v,x),Plus) = Bcons(v,x)"; by (simp_tac bin_ss 1); qed "bin_add_Bcons_Plus"; -goalw Bin.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)"; +goalw Bin.thy [bin_add_def] "bin_add(Bcons(v,x),Minus) = bin_pred(Bcons(v,x))"; by (simp_tac bin_ss 1); qed "bin_add_Bcons_Minus"; goalw Bin.thy [bin_add_def] "!!w y. [| w: bin; y: bool |] ==> \ -\ bin_add(v$$x, w$$y) = \ -\ bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)"; +\ bin_add(Bcons(v,x), Bcons(w,y)) = \ +\ norm_Bcons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"; by (asm_simp_tac bin_ss 1); qed "bin_add_Bcons_Bcons"; -val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, - bin_add_Bcons_Minus, bin_add_Bcons_Bcons, - integ_of_bin_succ, integ_of_bin_pred]; +val bin_add_simps = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, + bin_add_Bcons_Minus, bin_add_Bcons_Bcons, + integ_of_bin_succ, integ_of_bin_pred, + integ_of_bin_norm_Bcons]; -val bin_add_ss = bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_rews); +val bin_add_ss = + bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_simps); goal Bin.thy "!!v. v: bin ==> \ @@ -238,27 +268,23 @@ by (simp_tac bin_add_ss 1); by (rtac ballI 1); by (bin_ind_tac "wa" [] 1); -by (asm_simp_tac (bin_add_ss addsimps [zadd_0_right]) 1); by (asm_simp_tac bin_add_ss 1); -by (REPEAT (ares_tac (zadd_commute::typechecks) 1)); +by (asm_simp_tac (bin_add_ss addsimps zadd_ac) 1); by (etac boolE 1); -by (asm_simp_tac (bin_add_ss addsimps [zadd_assoc, zadd_swap_pairs]) 2); -by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2)); +by (asm_simp_tac (bin_add_ss addsimps zadd_ac) 2); by (etac boolE 1); -by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs]))); -by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@ - typechecks) 1)); -qed "integ_of_bin_add_lemma"; +by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps zadd_ac))); +val integ_of_bin_add_lemma = result(); -val integ_of_bin_add = integ_of_bin_add_lemma RS bspec; +bind_thm("integ_of_bin_add", integ_of_bin_add_lemma RS bspec); (*** bin_add: binary multiplication ***) val bin_mult_ss = bin_ss addsimps (bin_recs bin_mult_def @ - [integ_of_bin_minus, integ_of_bin_add]); - + [integ_of_bin_minus, integ_of_bin_add, + integ_of_bin_norm_Bcons]); val major::prems = goal Bin.thy "[| v: bin; w: bin |] ==> \ @@ -266,14 +292,12 @@ \ integ_of_bin(v) $* integ_of_bin(w)"; by (cut_facts_tac prems 1); by (bin_ind_tac "v" [major] 1); -by (asm_simp_tac (bin_mult_ss addsimps [zmult_0]) 1); -by (asm_simp_tac (bin_mult_ss addsimps [zmult_1,zmult_zminus]) 1); +by (asm_simp_tac bin_mult_ss 1); +by (asm_simp_tac bin_mult_ss 1); by (etac boolE 1); by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2); by (asm_simp_tac - (bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1); -by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@ - typechecks) 1)); + (bin_mult_ss addsimps ([zadd_zmult_distrib, zmult_1] @ zadd_ac)) 1); qed "integ_of_bin_mult"; (**** Computations ****) @@ -283,19 +307,19 @@ val [bin_succ_Plus, bin_succ_Minus, _] = bin_recs bin_succ_def; val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def; -goal Bin.thy "bin_succ(w$$1) = bin_succ(w) $$ 0"; +goal Bin.thy "bin_succ(Bcons(w,1)) = Bcons(bin_succ(w), 0)"; by (simp_tac carry_ss 1); qed "bin_succ_Bcons1"; -goal Bin.thy "bin_succ(w$$0) = w$$1"; +goal Bin.thy "bin_succ(Bcons(w,0)) = norm_Bcons(w,1)"; by (simp_tac carry_ss 1); qed "bin_succ_Bcons0"; -goal Bin.thy "bin_pred(w$$1) = w$$0"; +goal Bin.thy "bin_pred(Bcons(w,1)) = norm_Bcons(w,0)"; by (simp_tac carry_ss 1); qed "bin_pred_Bcons1"; -goal Bin.thy "bin_pred(w$$0) = bin_pred(w) $$ 1"; +goal Bin.thy "bin_pred(Bcons(w,0)) = Bcons(bin_pred(w), 1)"; by (simp_tac carry_ss 1); qed "bin_pred_Bcons0"; @@ -303,28 +327,31 @@ val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def; -goal Bin.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)"; +goal Bin.thy "bin_minus(Bcons(w,1)) = bin_pred(Bcons(bin_minus(w), 0))"; by (simp_tac bin_minus_ss 1); qed "bin_minus_Bcons1"; -goal Bin.thy "bin_minus(w$$0) = bin_minus(w) $$ 0"; +goal Bin.thy "bin_minus(Bcons(w,0)) = Bcons(bin_minus(w), 0)"; by (simp_tac bin_minus_ss 1); qed "bin_minus_Bcons0"; (** extra rules for bin_add **) goal Bin.thy - "!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0"; + "!!w. w: bin ==> bin_add(Bcons(v,1), Bcons(w,1)) = \ +\ norm_Bcons(bin_add(v, bin_succ(w)), 0)"; by (asm_simp_tac bin_add_ss 1); qed "bin_add_Bcons_Bcons11"; goal Bin.thy - "!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1"; + "!!w. w: bin ==> bin_add(Bcons(v,1), Bcons(w,0)) = \ +\ norm_Bcons(bin_add(v,w), 1)"; by (asm_simp_tac bin_add_ss 1); qed "bin_add_Bcons_Bcons10"; goal Bin.thy - "!!w y.[| w: bin; y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y"; + "!!w y. [| w: bin; y: bool |] ==> \ +\ bin_add(Bcons(v,0), Bcons(w,y)) = norm_Bcons(bin_add(v,w), y)"; by (asm_simp_tac bin_add_ss 1); qed "bin_add_Bcons_Bcons0"; @@ -332,11 +359,12 @@ val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def; -goal Bin.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)"; +goal Bin.thy + "bin_mult(Bcons(v,1), w) = bin_add(norm_Bcons(bin_mult(v,w),0), w)"; by (simp_tac bin_mult_ss 1); qed "bin_mult_Bcons1"; -goal Bin.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0"; +goal Bin.thy "bin_mult(Bcons(v,0), w) = norm_Bcons(bin_mult(v,w),0)"; by (simp_tac bin_mult_ss 1); qed "bin_mult_Bcons0"; @@ -344,17 +372,21 @@ (*** The computation simpset ***) val bin_comp_ss = integ_ss - addsimps [bin_succ_Plus, bin_succ_Minus, - bin_succ_Bcons1, bin_succ_Bcons0, - bin_pred_Plus, bin_pred_Minus, - bin_pred_Bcons1, bin_pred_Bcons0, - bin_minus_Plus, bin_minus_Minus, - bin_minus_Bcons1, bin_minus_Bcons0, - bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, - bin_add_Bcons_Minus, bin_add_Bcons_Bcons0, - bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11, - bin_mult_Plus, bin_mult_Minus, - bin_mult_Bcons1, bin_mult_Bcons0] + addsimps [integ_of_bin_add RS sym, (*invoke bin_add*) + integ_of_bin_minus RS sym, (*invoke bin_minus*) + integ_of_bin_mult RS sym, (*invoke bin_mult*) + bin_succ_Plus, bin_succ_Minus, + bin_succ_Bcons1, bin_succ_Bcons0, + bin_pred_Plus, bin_pred_Minus, + bin_pred_Bcons1, bin_pred_Bcons0, + bin_minus_Plus, bin_minus_Minus, + bin_minus_Bcons1, bin_minus_Bcons0, + bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, + bin_add_Bcons_Minus, bin_add_Bcons_Bcons0, + bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11, + bin_mult_Plus, bin_mult_Minus, + bin_mult_Bcons1, bin_mult_Bcons0] @ + norm_Bcons_simps setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0)); (*** Examples of performing binary arithmetic by simplification ***) @@ -362,95 +394,64 @@ proof_timing := true; (*All runtimes below are on a SPARCserver 10*) -(* 13+19 = 32 *) -goal Bin.thy - "bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0"; -by (simp_tac bin_comp_ss 1); (*0.6 secs*) +goal Bin.thy "#13 $+ #19 = #32"; +by (simp_tac bin_comp_ss 1); (*0.4 secs*) result(); bin_add(binary_of_int 13, binary_of_int 19); -(* 1234+5678 = 6912 *) -goal Bin.thy - "bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \ -\ Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \ -\ Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0"; -by (simp_tac bin_comp_ss 1); (*2.6 secs*) +goal Bin.thy "#1234 $+ #5678 = #6912"; +by (simp_tac bin_comp_ss 1); (*1.3 secs*) result(); bin_add(binary_of_int 1234, binary_of_int 5678); -(* 1359-2468 = ~1109 *) -goal Bin.thy - "bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \ -\ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \ -\ Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1"; -by (simp_tac bin_comp_ss 1); (*2.3 secs*) +goal Bin.thy "#1359 $+ #~2468 = #~1109"; +by (simp_tac bin_comp_ss 1); (*1.2 secs*) result(); bin_add(binary_of_int 1359, binary_of_int ~2468); -(* 93746-46375 = 47371 *) -goal Bin.thy - "bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \ -\ Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \ -\ Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1"; -by (simp_tac bin_comp_ss 1); (*3.9 secs*) +goal Bin.thy "#93746 $+ #~46375 = #47371"; +by (simp_tac bin_comp_ss 1); (*1.9 secs*) result(); bin_add(binary_of_int 93746, binary_of_int ~46375); -(* negation of 65745 *) -goal Bin.thy - "bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \ -\ Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1"; -by (simp_tac bin_comp_ss 1); (*0.6 secs*) +goal Bin.thy "$~ #65745 = #~65745"; +by (simp_tac bin_comp_ss 1); (*0.4 secs*) result(); bin_minus(binary_of_int 65745); (* negation of ~54321 *) -goal Bin.thy - "bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \ -\ Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1"; -by (simp_tac bin_comp_ss 1); (*0.7 secs*) +goal Bin.thy "$~ #~54321 = #54321"; +by (simp_tac bin_comp_ss 1); (*0.5 secs*) result(); bin_minus(binary_of_int ~54321); -(* 13*19 = 247 *) -goal Bin.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \ -\ Plus$$1$$1$$1$$1$$0$$1$$1$$1"; -by (simp_tac bin_comp_ss 1); (*1.5 secs*) +goal Bin.thy "#13 $* #19 = #247"; +by (simp_tac bin_comp_ss 1); (*0.7 secs*) result(); bin_mult(binary_of_int 13, binary_of_int 19); -(* ~84 * 51 = ~4284 *) -goal Bin.thy - "bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \ -\ Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0"; -by (simp_tac bin_comp_ss 1); (*2.6 secs*) +goal Bin.thy "#~84 $* #51 = #~4284"; +by (simp_tac bin_comp_ss 1); (*1.3 secs*) result(); bin_mult(binary_of_int ~84, binary_of_int 51); -(* 255*255 = 65025; the worst case for 8-bit operands *) -goal Bin.thy - "bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \ -\ Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \ -\ Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1"; -by (simp_tac bin_comp_ss 1); (*9.8 secs*) +(*The worst case for 8-bit operands *) +goal Bin.thy "#255 $* #255 = #65025"; +by (simp_tac bin_comp_ss 1); (*4.3 secs*) result(); bin_mult(binary_of_int 255, binary_of_int 255); -(* 1359 * ~2468 = ~3354012 *) -goal Bin.thy - "bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \ -\ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \ -\ Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0"; -by (simp_tac bin_comp_ss 1); (*13.7 secs*) +goal Bin.thy "#1359 $* #~2468 = #~3354012"; +by (simp_tac bin_comp_ss 1); (*6.1 secs*) result(); bin_mult(binary_of_int 1359, binary_of_int ~2468);