--- a/src/ZF/ex/Bin.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/ex/Bin.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/ex/Bin.ML
+(* Title: ZF/ex/Bin.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
For Bin.thy. Arithmetic on binary integers.
@@ -11,8 +11,8 @@
(*Perform induction on l, then prove the major premise using prems. *)
fun bin_ind_tac a prems i =
EVERY [res_inst_tac [("x",a)] bin.induct i,
- rename_last_tac a ["1"] (i+3),
- ares_tac prems i];
+ rename_last_tac a ["1"] (i+3),
+ ares_tac prems i];
(** bin_rec -- by Vset recursion **)
@@ -44,7 +44,7 @@
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]))));
+ bin_rec_Bcons]))));
qed "bin_rec_type";
(** Versions for use with definitions **)
@@ -68,7 +68,7 @@
qed "def_bin_rec_Bcons";
fun bin_recs def = map standard
- ([def] RL [def_bin_rec_Plus, def_bin_rec_Minus, def_bin_rec_Bcons]);
+ ([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);
@@ -92,8 +92,8 @@
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];
+ norm_Bcons_Minus_0, norm_Bcons_Minus_1,
+ norm_Bcons_Bcons];
(** Type checking **)
@@ -102,7 +102,7 @@
goalw Bin.thy [integ_of_bin_def]
"!!w. w: bin ==> integ_of_bin(w) : integ";
by (typechk_tac (bin_typechecks0@integ_typechecks@
- nat_typechecks@[bool_into_nat]));
+ nat_typechecks@[bool_into_nat]));
qed "integ_of_bin_type";
goalw Bin.thy [norm_Bcons_def]
@@ -130,13 +130,13 @@
goalw Bin.thy [bin_add_def]
"!!v w. [| v: bin; w: bin |] ==> bin_add(v,w) : bin";
by (typechk_tac ([norm_Bcons_type, bin_succ_type, bin_pred_type]@
- bin_typechecks0@ bool_typechecks@ZF_typechecks));
+ 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 ([norm_Bcons_type, bin_minus_type, bin_add_type]@
- bin_typechecks0@ bool_typechecks));
+ bin_typechecks0@ bool_typechecks));
qed "bin_mult_type";
val bin_typechecks = bin_typechecks0 @
@@ -145,8 +145,8 @@
val bin_ss = integ_ss
addsimps([bool_1I, bool_0I,
- bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @
- bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks);
+ bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @
+ bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks);
val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
[bool_subset_nat RS subsetD];
@@ -178,7 +178,7 @@
(*norm_Bcons preserves the integer value of its argument*)
goal Bin.thy
- "!!w. [| w: bin; b: bool |] ==> \
+ "!!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);
@@ -213,7 +213,7 @@
val bin_minus_ss =
bin_ss addsimps (bin_recs bin_minus_def @
- [integ_of_bin_succ, integ_of_bin_pred]);
+ [integ_of_bin_succ, integ_of_bin_pred]);
goal Bin.thy
"!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
@@ -252,9 +252,9 @@
qed "bin_add_Bcons_Bcons";
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];
+ 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_simps);
@@ -283,11 +283,11 @@
val bin_mult_ss =
bin_ss addsimps (bin_recs bin_mult_def @
- [integ_of_bin_minus, integ_of_bin_add,
- integ_of_bin_norm_Bcons]);
+ [integ_of_bin_minus, integ_of_bin_add,
+ integ_of_bin_norm_Bcons]);
val major::prems = goal Bin.thy
- "[| v: bin; w: bin |] ==> \
+ "[| v: bin; w: bin |] ==> \
\ integ_of_bin(bin_mult(v,w)) = \
\ integ_of_bin(v) $* integ_of_bin(w)";
by (cut_facts_tac prems 1);
@@ -373,19 +373,19 @@
val bin_comp_ss = integ_ss
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] @
+ 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));
@@ -395,63 +395,63 @@
(*All runtimes below are on a SPARCserver 10*)
goal Bin.thy "#13 $+ #19 = #32";
-by (simp_tac bin_comp_ss 1); (*0.4 secs*)
+by (simp_tac bin_comp_ss 1); (*0.4 secs*)
result();
bin_add(binary_of_int 13, binary_of_int 19);
goal Bin.thy "#1234 $+ #5678 = #6912";
-by (simp_tac bin_comp_ss 1); (*1.3 secs*)
+by (simp_tac bin_comp_ss 1); (*1.3 secs*)
result();
bin_add(binary_of_int 1234, binary_of_int 5678);
goal Bin.thy "#1359 $+ #~2468 = #~1109";
-by (simp_tac bin_comp_ss 1); (*1.2 secs*)
+by (simp_tac bin_comp_ss 1); (*1.2 secs*)
result();
bin_add(binary_of_int 1359, binary_of_int ~2468);
goal Bin.thy "#93746 $+ #~46375 = #47371";
-by (simp_tac bin_comp_ss 1); (*1.9 secs*)
+by (simp_tac bin_comp_ss 1); (*1.9 secs*)
result();
bin_add(binary_of_int 93746, binary_of_int ~46375);
goal Bin.thy "$~ #65745 = #~65745";
-by (simp_tac bin_comp_ss 1); (*0.4 secs*)
+by (simp_tac bin_comp_ss 1); (*0.4 secs*)
result();
bin_minus(binary_of_int 65745);
(* negation of ~54321 *)
goal Bin.thy "$~ #~54321 = #54321";
-by (simp_tac bin_comp_ss 1); (*0.5 secs*)
+by (simp_tac bin_comp_ss 1); (*0.5 secs*)
result();
bin_minus(binary_of_int ~54321);
goal Bin.thy "#13 $* #19 = #247";
-by (simp_tac bin_comp_ss 1); (*0.7 secs*)
+by (simp_tac bin_comp_ss 1); (*0.7 secs*)
result();
bin_mult(binary_of_int 13, binary_of_int 19);
goal Bin.thy "#~84 $* #51 = #~4284";
-by (simp_tac bin_comp_ss 1); (*1.3 secs*)
+by (simp_tac bin_comp_ss 1); (*1.3 secs*)
result();
bin_mult(binary_of_int ~84, binary_of_int 51);
(*The worst case for 8-bit operands *)
goal Bin.thy "#255 $* #255 = #65025";
-by (simp_tac bin_comp_ss 1); (*4.3 secs*)
+by (simp_tac bin_comp_ss 1); (*4.3 secs*)
result();
bin_mult(binary_of_int 255, binary_of_int 255);
goal Bin.thy "#1359 $* #~2468 = #~3354012";
-by (simp_tac bin_comp_ss 1); (*6.1 secs*)
+by (simp_tac bin_comp_ss 1); (*6.1 secs*)
result();
bin_mult(binary_of_int 1359, binary_of_int ~2468);