--- a/src/ZF/Integ/Bin.ML Fri Sep 25 12:12:07 1998 +0200
+++ b/src/ZF/Integ/Bin.ML Fri Sep 25 13:18:07 1998 +0200
@@ -99,8 +99,8 @@
val bin_typechecks0 = bin_rec_type :: bin.intrs;
-Goalw [integ_of_def] "w: bin ==> integ_of(w) : integ";
-by (typechk_tac (bin_typechecks0@integ_typechecks@
+Goalw [integ_of_def] "w: bin ==> integ_of(w) : int";
+by (typechk_tac (bin_typechecks0@int_typechecks@
nat_typechecks@[bool_into_nat]));
qed "integ_of_type";
@@ -143,33 +143,13 @@
bin_rec_Pls, bin_rec_Min, bin_rec_Cons] @
bin_recs integ_of_def @ bin_typechecks);
-val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
+val typechecks = bin_typechecks @ int_typechecks @ nat_typechecks @
[bool_subset_nat RS subsetD];
(**** The carry/borrow functions, bin_succ and bin_pred ****)
-(** Lemmas **)
-
-goal Integ.thy
- "!!z v. [| z $+ v = z' $+ v'; \
-\ z: integ; z': integ; v: integ; v': integ; w: integ |] \
-\ ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
-qed "zadd_assoc_cong";
-
-goal Integ.thy
- "!!z v w. [| z: integ; v: integ; w: integ |] \
-\ ==> z $+ (v $+ w) = v $+ (z $+ w)";
-by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
-qed "zadd_assoc_swap";
-
-(*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*)
-bind_thm ("zadd_assoc_znat", (znat_type RS zadd_assoc_swap));
-
-
Addsimps (bin_recs bin_succ_def @ bin_recs bin_pred_def);
-
(*NCons preserves the integer value of its argument*)
Goal "[| w: bin; b: bool |] ==> \
\ integ_of(NCons(w,b)) = integ_of(Cons(w,b))";
@@ -346,7 +326,7 @@
(*** The computation simpset ***)
(*Adding the typechecking rules as rewrites is much slower, unfortunately...*)
-val bin_comp_ss = simpset_of Integ.thy
+val bin_comp_ss = simpset_of Int.thy
addsimps [integ_of_add RS sym, (*invoke bin_add*)
integ_of_minus RS sym, (*invoke bin_minus*)
integ_of_mult RS sym, (*invoke bin_mult*)