simproc bug fix: negative literals and large terms
authorpaulson
Thu Dec 21 10:11:10 2000 +0100 (2000-12-21)
changeset 1071369c9fc1d11f2
parent 10712 351ba950d4d9
child 10714 07f75bf77a33
simproc bug fix: negative literals and large terms
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_factor_simprocs.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Dec 20 12:15:52 2000 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 21 10:11:10 2000 +0100
     1.3 @@ -173,6 +173,18 @@
     1.4  (*To let us treat subtraction as addition*)
     1.5  val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
     1.6  
     1.7 +(*push the unary minus down: - x * y = x * - y *)
     1.8 +val int_minus_mult_eq_1_to_2 = 
     1.9 +    [zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard;
    1.10 +
    1.11 +(*to extract again any uncancelled minuses*)
    1.12 +val int_minus_from_mult_simps = 
    1.13 +    [zminus_zminus, zmult_zminus, zmult_zminus_right];
    1.14 +
    1.15 +(*combine unary minus with numeric literals, however nested within a product*)
    1.16 +val int_mult_minus_simps =
    1.17 +    [zmult_assoc, zmult_zminus RS sym, int_minus_mult_eq_1_to_2];
    1.18 +
    1.19  (*Apply the given rewrite (if present) just once*)
    1.20  fun trans_tac None      = all_tac
    1.21    | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
    1.22 @@ -207,11 +219,12 @@
    1.23    val dest_coeff	= dest_coeff 1
    1.24    val find_first_coeff	= find_first_coeff []
    1.25    val trans_tac         = trans_tac
    1.26 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    1.27 -                                                     zminus_simps@zadd_ac))
    1.28 -                 THEN ALLGOALS
    1.29 -                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    1.30 -                                               bin_simps@zadd_ac@zmult_ac))
    1.31 +  val norm_tac = 
    1.32 +     ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    1.33 +                                         zminus_simps@zadd_ac))
    1.34 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
    1.35 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
    1.36 +                                              zadd_ac@zmult_ac))
    1.37    val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    1.38    val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
    1.39    end;
    1.40 @@ -273,12 +286,12 @@
    1.41    val left_distrib	= left_zadd_zmult_distrib RS trans
    1.42    val prove_conv        = prove_conv_nohyps "int_combine_numerals"
    1.43    val trans_tac          = trans_tac
    1.44 -  val norm_tac = ALLGOALS
    1.45 -                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    1.46 -                                              zminus_simps@zadd_ac))
    1.47 -                 THEN ALLGOALS
    1.48 -                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    1.49 -                                               bin_simps@zadd_ac@zmult_ac))
    1.50 +  val norm_tac = 
    1.51 +     ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
    1.52 +                                         zminus_simps@zadd_ac))
    1.53 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
    1.54 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
    1.55 +                                              zadd_ac@zmult_ac))
    1.56    val numeral_simp_tac	= ALLGOALS 
    1.57                      (simp_tac (HOL_ss addsimps add_0s@bin_simps))
    1.58    val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
     2.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Wed Dec 20 12:15:52 2000 +0100
     2.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 21 10:11:10 2000 +0100
     2.3 @@ -43,10 +43,11 @@
     2.4    val mk_coeff		= mk_coeff
     2.5    val dest_coeff	= dest_coeff 1
     2.6    val trans_tac         = trans_tac
     2.7 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
     2.8 -                 THEN ALLGOALS
     2.9 -                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    2.10 -                                               bin_simps@zmult_ac))
    2.11 +  val norm_tac = 
    2.12 +     ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
    2.13 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
    2.14 +     THEN ALLGOALS
    2.15 +            (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@zmult_ac))
    2.16    val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    2.17    val simplify_meta_eq  = simplify_meta_eq mult_1s
    2.18    end