# HG changeset patch
# User paulson
# Date 977389870 -3600
# Node ID 69c9fc1d11f256df324f90b547255ff2867afe1f
# Parent  351ba950d4d9b42bc37edcf65714ecfddeca40c9
simproc bug fix: negative literals and large terms

diff -r 351ba950d4d9 -r 69c9fc1d11f2 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Wed Dec 20 12:15:52 2000 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 21 10:11:10 2000 +0100
@@ -173,6 +173,18 @@
 (*To let us treat subtraction as addition*)
 val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
 
+(*push the unary minus down: - x * y = x * - y *)
+val int_minus_mult_eq_1_to_2 = 
+    [zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard;
+
+(*to extract again any uncancelled minuses*)
+val int_minus_from_mult_simps = 
+    [zminus_zminus, zmult_zminus, zmult_zminus_right];
+
+(*combine unary minus with numeric literals, however nested within a product*)
+val int_mult_minus_simps =
+    [zmult_assoc, zmult_zminus RS sym, int_minus_mult_eq_1_to_2];
+
 (*Apply the given rewrite (if present) just once*)
 fun trans_tac None      = all_tac
   | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
@@ -207,11 +219,12 @@
   val dest_coeff	= dest_coeff 1
   val find_first_coeff	= find_first_coeff []
   val trans_tac         = trans_tac
-  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
-                                                     zminus_simps@zadd_ac))
-                 THEN ALLGOALS
-                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
-                                               bin_simps@zadd_ac@zmult_ac))
+  val norm_tac = 
+     ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
+                                         zminus_simps@zadd_ac))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
+                                              zadd_ac@zmult_ac))
   val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   end;
@@ -273,12 +286,12 @@
   val left_distrib	= left_zadd_zmult_distrib RS trans
   val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   val trans_tac          = trans_tac
-  val norm_tac = ALLGOALS
-                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
-                                              zminus_simps@zadd_ac))
-                 THEN ALLGOALS
-                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
-                                               bin_simps@zadd_ac@zmult_ac))
+  val norm_tac = 
+     ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
+                                         zminus_simps@zadd_ac))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
+                                              zadd_ac@zmult_ac))
   val numeral_simp_tac	= ALLGOALS 
                     (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
diff -r 351ba950d4d9 -r 69c9fc1d11f2 src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Wed Dec 20 12:15:52 2000 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 21 10:11:10 2000 +0100
@@ -43,10 +43,11 @@
   val mk_coeff		= mk_coeff
   val dest_coeff	= dest_coeff 1
   val trans_tac         = trans_tac
-  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
-                 THEN ALLGOALS
-                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
-                                               bin_simps@zmult_ac))
+  val norm_tac = 
+     ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
+     THEN ALLGOALS
+            (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@zmult_ac))
   val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
   val simplify_meta_eq  = simplify_meta_eq mult_1s
   end