src/HOL/Integ/int_arith1.ML
changeset 14113 7b3513ba0f86
parent 13499 f95f5818f24f
child 14271 8ed6989228bb
     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