Fixing a simproc bug

--- a/src/HOL/Integ/int_arith1.ML	Tue Jul 15 15:12:22 2003 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Tue Jul 15 15:20:54 2003 +0200
@@ -175,6 +175,11 @@
                  add_number_of_left, 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 \\ [add_number_of_left, number_of_add RS sym];
+
 (*To evaluate binary negations of coefficients*)
 val zminus_simps = NCons_simps @
                    [zminus_1_eq_m1, number_of_minus RS sym,
@@ -215,7 +220,7 @@
   val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@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 non_add_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))
@@ -282,7 +287,7 @@
   val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@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 non_add_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

--- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Jul 15 15:12:22 2003 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Jul 15 15:20:54 2003 +0200
@@ -46,8 +46,7 @@
   val norm_tac =
      ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
      THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
-     THEN ALLGOALS
-            (simp_tac (HOL_ss addsimps zmult_ac))
+     THEN ALLGOALS (simp_tac (HOL_ss addsimps zmult_ac))
   val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
   val simplify_meta_eq  = simplify_meta_eq mult_1s
   end

--- a/src/HOL/ex/BinEx.thy	Tue Jul 15 15:12:22 2003 +0200
+++ b/src/HOL/ex/BinEx.thy	Tue Jul 15 15:20:54 2003 +0200
@@ -8,6 +8,122 @@
 
 theory BinEx = Main:
 
+subsection {* Regression Testing for Cancellation Simprocs *}
+
+(*taken from HOL/Integ/int_arith1.ML *)
+
+
+lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
+apply simp  oops
+
+lemma "2*u = (u::int)"
+apply simp  oops
+
+lemma "(i + j + 12 + (k::int)) - 15 = y"
+apply simp  oops
+
+lemma "(i + j + 12 + (k::int)) - 5 = y"
+apply simp  oops
+
+lemma "y - b < (b::int)"
+apply simp  oops
+
+lemma "y - (3*b + c) < (b::int) - 2*c"
+apply simp  oops
+
+lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"
+apply simp  oops
+
+lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
+apply simp  oops
+
+lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
+apply simp  oops
+
+lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
+apply simp  oops
+
+lemma "(i + j + 12 + (k::int)) = u + 15 + y"
+apply simp  oops
+
+lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"
+apply simp  oops
+
+lemma "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"
+apply simp  oops
+
+lemma "a + -(b+c) + b = (d::int)"
+apply simp  oops
+
+lemma "a + -(b+c) - b = (d::int)"
+apply simp  oops
+
+(*negative numerals*)
+lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
+apply simp  oops
+
+lemma "(i + j + -3 + (k::int)) < u + 5 + y"
+apply simp  oops
+
+lemma "(i + j + 3 + (k::int)) < u + -6 + y"
+apply simp  oops
+
+lemma "(i + j + -12 + (k::int)) - 15 = y"
+apply simp  oops
+
+lemma "(i + j + 12 + (k::int)) - -15 = y"
+apply simp  oops
+
+lemma "(i + j + -12 + (k::int)) - -15 = y"
+apply simp  oops
+
+
+subsection {* Arithmetic Method Tests *}
+
+
+lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"
+by arith
+
+lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"
+by arith
+
+lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"
+by arith
+
+lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"
+by arith
+
+lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
+by arith
+
+lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
+by arith
+
+lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
+by arith
+
+lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
+      ==> a <= l"
+by arith
+
+lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
+      ==> a+a+a+a <= l+l+l+l"
+by arith
+
+lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
+      ==> a+a+a+a+a <= l+l+l+l+i"
+by arith
+
+lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
+      ==> a+a+a+a+a+a <= l+l+l+l+i+l"
+by arith
+
+lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
+      ==> 6*a <= 5*l+i"
+by arith
+
+
+
 subsection {* The Integers *}
 
 text {* Addition *}
@@ -349,7 +465,7 @@
   apply (rule normal.intros)
    apply assumption
   apply (simp add: normal_Pls_eq_0)
-  apply (simp only: number_of_minus zminus_0 iszero_def 
+  apply (simp only: number_of_minus zminus_0 iszero_def
                     zminus_equation [of _ "0"])
   apply (simp add: eq_commute)
   done