# HG changeset patch
# User paulson
# Date 930127019 -7200
# Node ID 941c4f70db91d63ac57147e991c2222fc42c282e
# Parent  1bd850260747635912575e0784b6da1e4e16f620
rewrite rules to distribute CONSTANT multiplication over sum and difference;
removed automatic rewriting of 2x to x+x

diff -r 1bd850260747 -r 941c4f70db91 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Thu Jun 17 10:43:05 1999 +0200
+++ b/src/HOL/Integ/Bin.ML	Wed Jun 23 10:36:59 1999 +0200
@@ -200,33 +200,41 @@
 
 Addsimps [zdiff0, zdiff0_right, zdiff_self];
 
+(** Distributive laws for constants only **)
+
+Addsimps (map (read_instantiate_sg (sign_of Bin.thy) [("w", "integ_of ?v")])
+	  [zadd_zmult_distrib, zadd_zmult_distrib2,
+	   zdiff_zmult_distrib, zdiff_zmult_distrib2]);
+
+(** Special-case simplification for small constants **)
+
 Goal "#0 * z = #0";
 by (Simp_tac 1);
 qed "zmult_0";
 
+Goal "z * #0 = #0";
+by (Simp_tac 1);
+qed "zmult_0_right";
+
 Goal "#1 * z = z";
 by (Simp_tac 1);
 qed "zmult_1";
 
+Goal "z * #1 = z";
+by (Simp_tac 1);
+qed "zmult_1_right";
+
+(*For specialist use*)
 Goal "#2 * z = z+z";
 by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
 qed "zmult_2";
 
-Goal "z * #0 = #0";
-by (Simp_tac 1);
-qed "zmult_0_right";
-
-Goal "z * #1 = z";
-by (Simp_tac 1);
-qed "zmult_1_right";
-
 Goal "z * #2 = z+z";
 by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
 qed "zmult_2_right";
 
 Addsimps [zmult_0, zmult_0_right, 
-	  zmult_1, zmult_1_right, 
-	  zmult_2, zmult_2_right];
+	  zmult_1, zmult_1_right];
 
 Goal "(w < z + #1) = (w<z | w=z)";
 by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
@@ -679,3 +687,6 @@
 	      simpset() addsimps [neg_eq_less_0, zle_def]));
 qed "nat_less_eq_zless";
 
+
+Addsimps zadd_ac;
+Addsimps zmult_ac;