fixed some awkward problems with nat/int simprocs
authorpaulson
Fri Oct 29 15:16:31 2004 +0200 (2004-10-29)
changeset 152713c32a26510c4
parent 15270 8b3f707a78a7
child 15272 79a7a4f20f50
fixed some awkward problems with nat/int simprocs
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Fri Oct 29 15:16:02 2004 +0200
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Fri Oct 29 15:16:31 2004 +0200
     1.3 @@ -230,11 +230,13 @@
     1.4          else find_first (t::past) u terms
     1.5          handle TERM _ => find_first (t::past) u terms;
     1.6  
     1.7 -(*Final simplification: cancel + and *  *)
     1.8 +(** Final simplification for the CancelFactor simprocs **)
     1.9 +val simplify_one = 
    1.10 +    Int_Numeral_Simprocs.simplify_meta_eq  
    1.11 +       [mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
    1.12 +
    1.13  fun cancel_simplify_meta_eq cancel_th th =
    1.14 -    Int_Numeral_Simprocs.simplify_meta_eq
    1.15 -        [mult_1, mult_1_right]
    1.16 -        (([th, cancel_th]) MRS trans);
    1.17 +    simplify_one (([th, cancel_th]) MRS trans);
    1.18  
    1.19  (*At present, long_mk_prod creates Numeral1, so this requires the axclass
    1.20    number_ring*)
    1.21 @@ -271,7 +273,7 @@
    1.22  
    1.23  val int_cancel_factor =
    1.24    map Bin_Simprocs.prep_simproc
    1.25 -   [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], 
    1.26 +   [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
    1.27      EqCancelFactor.proc),
    1.28      ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
    1.29       DivideCancelFactor.proc)];
    1.30 @@ -294,13 +296,13 @@
    1.31    val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
    1.32  );
    1.33  
    1.34 -(*The number_ring class is necessary because the simprocs refer to the 
    1.35 +(*The number_ring class is necessary because the simprocs refer to the
    1.36    binary number 1.  FIXME: probably they could use 1 instead.*)
    1.37  val field_cancel_factor =
    1.38    map Bin_Simprocs.prep_simproc
    1.39     [("field_eq_cancel_factor",
    1.40       ["(l::'a::{field,number_ring}) * m = n",
    1.41 -      "(l::'a::{field,number_ring}) = m * n"], 
    1.42 +      "(l::'a::{field,number_ring}) = m * n"],
    1.43       FieldEqCancelFactor.proc),
    1.44      ("field_divide_cancel_factor",
    1.45       ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
     2.1 --- a/src/HOL/Integ/nat_simprocs.ML	Fri Oct 29 15:16:02 2004 +0200
     2.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Fri Oct 29 15:16:31 2004 +0200
     2.3 @@ -351,10 +351,13 @@
     2.4          else find_first (t::past) u terms
     2.5          handle TERM _ => find_first (t::past) u terms;
     2.6  
     2.7 -(*Final simplification: cancel + and *  *)
     2.8 +(** Final simplification for the CancelFactor simprocs **)
     2.9 +val simplify_one = 
    2.10 +    Int_Numeral_Simprocs.simplify_meta_eq  
    2.11 +       [mult_1_left, mult_1_right, div_1, numeral_1_eq_Suc_0];
    2.12 +
    2.13  fun cancel_simplify_meta_eq cancel_th th =
    2.14 -    Int_Numeral_Simprocs.simplify_meta_eq  [zmult_1, zmult_1_right]
    2.15 -        (([th, cancel_th]) MRS trans);
    2.16 +    simplify_one (([th, cancel_th]) MRS trans);
    2.17  
    2.18  structure CancelFactorCommon =
    2.19    struct