--- a/src/HOL/Integ/int_factor_simprocs.ML Tue Mar 02 11:05:55 2004 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML Tue Mar 02 11:06:37 2004 +0100
@@ -139,9 +139,9 @@
"(l::'a::{field,number_ring}) = m * n"],
FieldEqCancelNumeralFactor.proc),
("field_cancel_numeral_factor",
- ["((l::'a::{field,number_ring}) * m) / n",
- "(l::'a::{field,number_ring}) / (m * n)",
- "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
+ ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+ "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
+ "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
FieldDivCancelNumeralFactor.proc)]
end;
@@ -236,6 +236,8 @@
[mult_1, mult_1_right]
(([th, cancel_th]) MRS trans);
+(*At present, long_mk_prod creates Numeral1, so this requires the axclass
+ number_ring*)
structure CancelFactorCommon =
struct
val mk_sum = long_mk_prod
@@ -292,13 +294,17 @@
val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
);
+(*The number_ring class is necessary because the simprocs refer to the
+ binary number 1. FIXME: probably they could use 1 instead.*)
val field_cancel_factor =
map Bin_Simprocs.prep_simproc
[("field_eq_cancel_factor",
- ["(l::'a::field) * m = n", "(l::'a::field) = m * n"],
+ ["(l::'a::{field,number_ring}) * m = n",
+ "(l::'a::{field,number_ring}) = m * n"],
FieldEqCancelFactor.proc),
("field_divide_cancel_factor",
- ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
+ ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+ "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
FieldDivideCancelFactor.proc)];
end;