src/HOL/Integ/int_factor_simprocs.ML
 changeset 14426 de890c247b38 parent 14390 55fe71faadda child 14738 83f1a514dcb4
```     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Mar 02 11:05:55 2004 +0100
1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Mar 02 11:06:37 2004 +0100
1.3 @@ -139,9 +139,9 @@
1.4        "(l::'a::{field,number_ring}) = m * n"],
1.5       FieldEqCancelNumeralFactor.proc),
1.6      ("field_cancel_numeral_factor",
1.7 -     ["((l::'a::{field,number_ring}) * m) / n",
1.8 -      "(l::'a::{field,number_ring}) / (m * n)",
1.9 -      "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
1.10 +     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
1.11 +      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
1.12 +      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
1.13       FieldDivCancelNumeralFactor.proc)]
1.14
1.15  end;
1.16 @@ -236,6 +236,8 @@
1.17          [mult_1, mult_1_right]
1.18          (([th, cancel_th]) MRS trans);
1.19
1.20 +(*At present, long_mk_prod creates Numeral1, so this requires the axclass
1.21 +  number_ring*)
1.22  structure CancelFactorCommon =
1.23    struct
1.24    val mk_sum            = long_mk_prod
1.25 @@ -292,13 +294,17 @@
1.26    val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
1.27  );
1.28
1.29 +(*The number_ring class is necessary because the simprocs refer to the
1.30 +  binary number 1.  FIXME: probably they could use 1 instead.*)
1.31  val field_cancel_factor =
1.32    map Bin_Simprocs.prep_simproc
1.33     [("field_eq_cancel_factor",
1.34 -     ["(l::'a::field) * m = n", "(l::'a::field) = m * n"],
1.35 +     ["(l::'a::{field,number_ring}) * m = n",
1.36 +      "(l::'a::{field,number_ring}) = m * n"],
1.37       FieldEqCancelFactor.proc),
1.38      ("field_divide_cancel_factor",
1.39 -     ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
1.40 +     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
1.41 +      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
1.42       FieldDivideCancelFactor.proc)];
1.43
1.44  end;
```