# HG changeset patch
# User paulson
# Date 1058864622 -7200
# Node ID b300efca4ae079f6f3d188420ec68e3c4867c9c7
# Parent  433f9a4145378ebbbcf43ac9cfc9368545e9abb5
fixed simprocs

diff -r 433f9a414537 -r b300efca4ae0 src/HOL/Complex/ComplexBin.ML
--- a/src/HOL/Complex/ComplexBin.ML	Mon Jul 21 17:27:23 2003 +0200
+++ b/src/HOL/Complex/ComplexBin.ML	Tue Jul 22 11:03:42 2003 +0200
@@ -264,6 +264,11 @@
      minus_complex_number_of, diff_complex_number_of, mult_complex_number_of, 
      complex_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
 
+(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
+  during re-arrangement*)
+val non_add_bin_simps = 
+    bin_simps \\ [complex_add_number_of_left, add_complex_number_of];
+
 (*To evaluate binary negations of coefficients*)
 val complex_minus_simps = NCons_simps @
                    [complex_minus_1_eq_m1,minus_complex_number_of, 
@@ -309,7 +314,7 @@
   val norm_tac = 
      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
                                          complex_minus_simps@complex_add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@complex_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@complex_mult_minus_simps))
      THEN ALLGOALS
               (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps@
                                          complex_add_ac@complex_mult_ac))
@@ -349,7 +354,7 @@
   val norm_tac = 
      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
                                          complex_minus_simps@complex_add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@complex_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@complex_mult_minus_simps))
      THEN ALLGOALS (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps@
                                               complex_add_ac@complex_mult_ac))
   val numeral_simp_tac	= ALLGOALS 
diff -r 433f9a414537 -r b300efca4ae0 src/HOL/Complex/NSComplexBin.ML
--- a/src/HOL/Complex/NSComplexBin.ML	Mon Jul 21 17:27:23 2003 +0200
+++ b/src/HOL/Complex/NSComplexBin.ML	Tue Jul 22 11:03:42 2003 +0200
@@ -296,6 +296,11 @@
      minus_hcomplex_number_of, diff_hcomplex_number_of, mult_hcomplex_number_of, 
      hcomplex_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
 
+(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
+  during re-arrangement*)
+val non_add_bin_simps = 
+    bin_simps \\ [hcomplex_add_number_of_left, add_hcomplex_number_of];
+
 (*To evaluate binary negations of coefficients*)
 val hcomplex_minus_simps = NCons_simps @
                    [hcomplex_minus_1_eq_m1,minus_hcomplex_number_of, 
@@ -342,7 +347,7 @@
   val norm_tac = 
      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
                                          hcomplex_minus_simps@hcomplex_add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps))
      THEN ALLGOALS
               (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@
                                          hcomplex_add_ac@hcomplex_mult_ac))
@@ -382,7 +387,7 @@
   val norm_tac = 
      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
                                          hcomplex_minus_simps@hcomplex_add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps))
      THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@
                                               hcomplex_add_ac@hcomplex_mult_ac))
   val numeral_simp_tac	= ALLGOALS 
diff -r 433f9a414537 -r b300efca4ae0 src/HOL/Hyperreal/HyperBin.ML
--- a/src/HOL/Hyperreal/HyperBin.ML	Mon Jul 21 17:27:23 2003 +0200
+++ b/src/HOL/Hyperreal/HyperBin.ML	Tue Jul 22 11:03:42 2003 +0200
@@ -328,6 +328,11 @@
      diff_hypreal_number_of, mult_hypreal_number_of,
      hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
 
+(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
+  during re-arrangement*)
+val non_add_bin_simps = 
+    bin_simps \\ [hypreal_add_number_of_left, add_hypreal_number_of];
+
 (*To evaluate binary negations of coefficients*)
 val hypreal_minus_simps = NCons_simps @
                    [hypreal_minus_1_eq_m1, minus_hypreal_number_of,
@@ -372,7 +377,7 @@
   val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
                                          hypreal_minus_simps@hypreal_add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps))
      THEN ALLGOALS
               (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@
                                          hypreal_add_ac@hypreal_mult_ac))
@@ -440,7 +445,7 @@
   val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
                                          hypreal_minus_simps@hypreal_add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps))
      THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@
                                               hypreal_add_ac@hypreal_mult_ac))
   val numeral_simp_tac  = ALLGOALS
diff -r 433f9a414537 -r b300efca4ae0 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Mon Jul 21 17:27:23 2003 +0200
+++ b/src/HOL/Real/RealBin.ML	Tue Jul 22 11:03:42 2003 +0200
@@ -349,6 +349,11 @@
      diff_real_number_of, mult_real_number_of, real_mult_number_of_left] @
     bin_arith_simps @ bin_rel_simps;
 
+(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
+  during re-arrangement*)
+val non_add_bin_simps = 
+    bin_simps \\ [real_add_number_of_left, add_real_number_of];
+
 (*To evaluate binary negations of coefficients*)
 val real_minus_simps = NCons_simps @
                    [real_minus_1_eq_m1, minus_real_number_of,
@@ -396,7 +401,7 @@
   val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
                                          real_minus_simps@real_add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@real_mult_minus_simps))
      THEN ALLGOALS
               (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
                                          real_add_ac@real_mult_ac))
@@ -464,7 +469,7 @@
   val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
                                    diff_simps@real_minus_simps@real_add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@real_mult_minus_simps))
      THEN ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
                                               real_add_ac@real_mult_ac))
   val numeral_simp_tac  = ALLGOALS