--- a/src/ZF/Integ/Bin.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/Integ/Bin.ML Mon Aug 07 10:29:54 2000 +0200
@@ -105,7 +105,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
qed "integ_of_succ";
-Goal "w: bin ==> integ_of(bin_pred(w)) = $~ ($#1) $+ integ_of(w)";
+Goal "w: bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
@@ -118,7 +118,7 @@
(*** bin_minus: (unary!) negation of binary integers ***)
-Goal "w: bin ==> integ_of(bin_minus(w)) = $~ integ_of(w)";
+Goal "w: bin ==> integ_of(bin_minus(w)) = $- integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
@@ -238,6 +238,41 @@
qed "bin_mult_BIT0";
+(** Simplification rules with integer constants **)
+
+Goal "#0 $+ z = intify(z)";
+by (Simp_tac 1);
+qed "zadd_0_intify";
+
+Goal "z $+ #0 = intify(z)";
+by (Simp_tac 1);
+qed "zadd_0_right_intify";
+
+Addsimps [zadd_0_intify, zadd_0_right_intify];
+
+Goal "#1 $* z = intify(z)";
+by (Simp_tac 1);
+qed "zmult_1_intify";
+
+Goal "z $* #1 = intify(z)";
+by (stac zmult_commute 1);
+by (Simp_tac 1);
+qed "zmult_1_right_intify";
+
+Addsimps [zmult_1_intify, zmult_1_right_intify];
+
+Goal "#0 $* z = #0";
+by (Simp_tac 1);
+qed "zmult_0";
+
+Goal "z $* #0 = #0";
+by (stac zmult_commute 1);
+by (Simp_tac 1);
+qed "zmult_0_right";
+
+Addsimps [zmult_0, zmult_0_right];
+
+
(*Delete the original rewrites, with their clumsy conditional expressions*)
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT,
NCons_Pls, NCons_Min, bin_adder_BIT, bin_mult_BIT];