Fixing a simproc bug
authorpaulson
Tue Jul 15 15:20:54 2003 +0200 (2003-07-15)
changeset 141137b3513ba0f86
parent 14112 95d51043d2a3
child 14114 e97ca1034caa
Fixing a simproc bug
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/ex/BinEx.thy
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Tue Jul 15 15:12:22 2003 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Jul 15 15:20:54 2003 +0200
     1.3 @@ -175,6 +175,11 @@
     1.4                   add_number_of_left, mult_number_of_left] @
     1.5                  bin_arith_simps @ bin_rel_simps;
     1.6  
     1.7 +(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
     1.8 +  during re-arrangement*)
     1.9 +val non_add_bin_simps = 
    1.10 +    bin_simps \\ [add_number_of_left, number_of_add RS sym];
    1.11 +
    1.12  (*To evaluate binary negations of coefficients*)
    1.13  val zminus_simps = NCons_simps @
    1.14                     [zminus_1_eq_m1, number_of_minus RS sym,
    1.15 @@ -215,7 +220,7 @@
    1.16    val norm_tac =
    1.17       ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
    1.18                                           diff_simps@zminus_simps@zadd_ac))
    1.19 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
    1.20 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@int_mult_minus_simps))
    1.21       THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
    1.22                                                zadd_ac@zmult_ac))
    1.23    val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    1.24 @@ -282,7 +287,7 @@
    1.25    val norm_tac =
    1.26       ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
    1.27                                           diff_simps@zminus_simps@zadd_ac))
    1.28 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
    1.29 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@int_mult_minus_simps))
    1.30       THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
    1.31                                                zadd_ac@zmult_ac))
    1.32    val numeral_simp_tac  = ALLGOALS
     2.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Jul 15 15:12:22 2003 +0200
     2.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Jul 15 15:20:54 2003 +0200
     2.3 @@ -46,8 +46,7 @@
     2.4    val norm_tac =
     2.5       ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
     2.6       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
     2.7 -     THEN ALLGOALS
     2.8 -            (simp_tac (HOL_ss addsimps zmult_ac))
     2.9 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps zmult_ac))
    2.10    val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    2.11    val simplify_meta_eq  = simplify_meta_eq mult_1s
    2.12    end
     3.1 --- a/src/HOL/ex/BinEx.thy	Tue Jul 15 15:12:22 2003 +0200
     3.2 +++ b/src/HOL/ex/BinEx.thy	Tue Jul 15 15:20:54 2003 +0200
     3.3 @@ -8,6 +8,122 @@
     3.4  
     3.5  theory BinEx = Main:
     3.6  
     3.7 +subsection {* Regression Testing for Cancellation Simprocs *}
     3.8 +
     3.9 +(*taken from HOL/Integ/int_arith1.ML *)
    3.10 +
    3.11 +
    3.12 +lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
    3.13 +apply simp  oops
    3.14 +
    3.15 +lemma "2*u = (u::int)"
    3.16 +apply simp  oops
    3.17 +
    3.18 +lemma "(i + j + 12 + (k::int)) - 15 = y"
    3.19 +apply simp  oops
    3.20 +
    3.21 +lemma "(i + j + 12 + (k::int)) - 5 = y"
    3.22 +apply simp  oops
    3.23 +
    3.24 +lemma "y - b < (b::int)"
    3.25 +apply simp  oops
    3.26 +
    3.27 +lemma "y - (3*b + c) < (b::int) - 2*c"
    3.28 +apply simp  oops
    3.29 +
    3.30 +lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"
    3.31 +apply simp  oops
    3.32 +
    3.33 +lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
    3.34 +apply simp  oops
    3.35 +
    3.36 +lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
    3.37 +apply simp  oops
    3.38 +
    3.39 +lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
    3.40 +apply simp  oops
    3.41 +
    3.42 +lemma "(i + j + 12 + (k::int)) = u + 15 + y"
    3.43 +apply simp  oops
    3.44 +
    3.45 +lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"
    3.46 +apply simp  oops
    3.47 +
    3.48 +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)"
    3.49 +apply simp  oops
    3.50 +
    3.51 +lemma "a + -(b+c) + b = (d::int)"
    3.52 +apply simp  oops
    3.53 +
    3.54 +lemma "a + -(b+c) - b = (d::int)"
    3.55 +apply simp  oops
    3.56 +
    3.57 +(*negative numerals*)
    3.58 +lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
    3.59 +apply simp  oops
    3.60 +
    3.61 +lemma "(i + j + -3 + (k::int)) < u + 5 + y"
    3.62 +apply simp  oops
    3.63 +
    3.64 +lemma "(i + j + 3 + (k::int)) < u + -6 + y"
    3.65 +apply simp  oops
    3.66 +
    3.67 +lemma "(i + j + -12 + (k::int)) - 15 = y"
    3.68 +apply simp  oops
    3.69 +
    3.70 +lemma "(i + j + 12 + (k::int)) - -15 = y"
    3.71 +apply simp  oops
    3.72 +
    3.73 +lemma "(i + j + -12 + (k::int)) - -15 = y"
    3.74 +apply simp  oops
    3.75 +
    3.76 +
    3.77 +subsection {* Arithmetic Method Tests *}
    3.78 +
    3.79 +
    3.80 +lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"
    3.81 +by arith
    3.82 +
    3.83 +lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"
    3.84 +by arith
    3.85 +
    3.86 +lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"
    3.87 +by arith
    3.88 +
    3.89 +lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"
    3.90 +by arith
    3.91 +
    3.92 +lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
    3.93 +by arith
    3.94 +
    3.95 +lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
    3.96 +by arith
    3.97 +
    3.98 +lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
    3.99 +by arith
   3.100 +
   3.101 +lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   3.102 +      ==> a <= l"
   3.103 +by arith
   3.104 +
   3.105 +lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   3.106 +      ==> a+a+a+a <= l+l+l+l"
   3.107 +by arith
   3.108 +
   3.109 +lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   3.110 +      ==> a+a+a+a+a <= l+l+l+l+i"
   3.111 +by arith
   3.112 +
   3.113 +lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   3.114 +      ==> a+a+a+a+a+a <= l+l+l+l+i+l"
   3.115 +by arith
   3.116 +
   3.117 +lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   3.118 +      ==> 6*a <= 5*l+i"
   3.119 +by arith
   3.120 +
   3.121 +
   3.122 +
   3.123  subsection {* The Integers *}
   3.124  
   3.125  text {* Addition *}
   3.126 @@ -349,7 +465,7 @@
   3.127    apply (rule normal.intros)
   3.128     apply assumption
   3.129    apply (simp add: normal_Pls_eq_0)
   3.130 -  apply (simp only: number_of_minus zminus_0 iszero_def 
   3.131 +  apply (simp only: number_of_minus zminus_0 iszero_def
   3.132                      zminus_equation [of _ "0"])
   3.133    apply (simp add: eq_commute)
   3.134    done