# HG changeset patch
# User paulson
# Date 931509909 -7200
# Node ID f52c70a449fba35fe592d0710c22c25db1b75dc8
# Parent  ee6640456cbb6a944cf640099fa7d396790bc1dc
products of signs as equivalences

diff -r ee6640456cbb -r f52c70a449fb src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Thu Jul 08 18:40:43 1999 +0200
+++ b/src/HOL/Integ/Bin.ML	Fri Jul 09 10:45:09 1999 +0200
@@ -157,6 +157,15 @@
 qed "number_of_mult";
 
 
+(*The correctness of shifting.  But it doesn't seem to give a measurable
+  speed-up.*)
+Goal "(#2::int) * number_of w = number_of (w BIT False)";
+by (induct_tac "w" 1);
+by (ALLGOALS (asm_simp_tac
+    (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));
+qed "double_number_of_BIT";
+
+
 (** Simplification rules with integer constants **)
 
 Goal "#0 + z = (z::int)";
@@ -281,29 +290,6 @@
 AddIffs [zero_zle_int];
 
 
-(** Products of signs  **)
-
-Goal "[| (m::int) < #0;  n < #0 |] ==> #0 < m*n";
-by (dtac zmult_zless_mono1_neg 1);
-by Auto_tac;
-qed "neg_times_neg_is_pos";
-
-Goal "[| (m::int) < #0;  #0 < n |] ==> m*n < #0";
-by (dtac zmult_zless_mono1 1);
-by Auto_tac;
-qed "neg_times_pos_is_neg";
-
-Goal "[| #0 < (m::int);  n < #0 |] ==> m*n < #0";
-by (dtac zmult_zless_mono1_neg 1);
-by Auto_tac;
-qed "pos_times_neg_is_neg";
-
-Goal "[| #0 < (m::int);  #0 < n |] ==> #0 < m*n";
-by (dtac zmult_zless_mono1 1);
-by Auto_tac;
-qed "pos_times_pos_is_pos";
-
-
 (** Needed because (int 0) rewrites to #0.
     Can these be generalized without evaluating large numbers?**)
 
@@ -720,3 +706,43 @@
 Addsimps zadd_ac;
 Addsimps zmult_ac;
 Addsimps [zmult_zminus, zmult_zminus_right];
+
+
+
+(** Products of signs **)
+
+Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)";
+by Auto_tac;
+by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
+by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
+by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
+by (force_tac (claset() addDs [zmult_zless_mono1_neg], 
+	       simpset() addsimps [order_le_less]) 1);
+qed "neg_imp_zmult_pos_iff";
+
+Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)";
+by Auto_tac;
+by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
+by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
+by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
+by (force_tac (claset() addDs [zmult_zless_mono1_neg], 
+	       simpset() addsimps [order_le_less]) 1);
+qed "neg_imp_zmult_neg_iff";
+
+Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)";
+by Auto_tac;
+by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
+by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
+by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
+by (force_tac (claset() addDs [zmult_zless_mono1], 
+	       simpset() addsimps [order_le_less]) 1);
+qed "pos_imp_zmult_neg_iff";
+
+Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)";
+by Auto_tac;
+by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
+by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
+by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
+by (force_tac (claset() addDs [zmult_zless_mono1], 
+	       simpset() addsimps [order_le_less]) 1);
+qed "pos_imp_zmult_pos_iff";