author paulson Fri Oct 29 15:16:31 2004 +0200 (2004-10-29) changeset 15271 3c32a26510c4 parent 15270 8b3f707a78a7 child 15272 79a7a4f20f50
fixed some awkward problems with nat/int simprocs
```     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
```