src/HOL/Tools/int_factor_simprocs.ML
author haftmann
Fri May 08 08:01:09 2009 +0200 (2009-05-08)
changeset 31067 fd7ec31f850c
parent 30931 86ca651da03e
permissions -rw-r--r--
generalized simproc for mod
wenzelm@23164
     1
(*  Title:      HOL/int_factor_simprocs.ML
wenzelm@23164
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@23164
     3
    Copyright   2000  University of Cambridge
wenzelm@23164
     4
wenzelm@23164
     5
Factor cancellation simprocs for the integers (and for fields).
wenzelm@23164
     6
wenzelm@23164
     7
This file can't be combined with int_arith1 because it requires IntDiv.thy.
wenzelm@23164
     8
*)
wenzelm@23164
     9
wenzelm@23164
    10
wenzelm@23164
    11
(*To quote from Provers/Arith/cancel_numeral_factor.ML:
wenzelm@23164
    12
wenzelm@23164
    13
Cancels common coefficients in balanced expressions:
wenzelm@23164
    14
wenzelm@23164
    15
     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
wenzelm@23164
    16
wenzelm@23164
    17
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
wenzelm@23164
    18
and d = gcd(m,m') and n=m/d and n'=m'/d.
wenzelm@23164
    19
*)
wenzelm@23164
    20
huffman@29038
    21
val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}];
wenzelm@23164
    22
wenzelm@23164
    23
local
wenzelm@23164
    24
  open Int_Numeral_Simprocs
wenzelm@23164
    25
in
wenzelm@23164
    26
wenzelm@23164
    27
structure CancelNumeralFactorCommon =
wenzelm@23164
    28
  struct
wenzelm@23164
    29
  val mk_coeff          = mk_coeff
wenzelm@23164
    30
  val dest_coeff        = dest_coeff 1
haftmann@30518
    31
  val trans_tac         = K Arith_Data.trans_tac
wenzelm@23164
    32
wenzelm@23164
    33
  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
wenzelm@23164
    34
  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
haftmann@23881
    35
  val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
wenzelm@23164
    36
  fun norm_tac ss =
wenzelm@23164
    37
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@23164
    38
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@23164
    39
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
wenzelm@23164
    40
wenzelm@23164
    41
  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
wenzelm@23164
    42
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
haftmann@30518
    43
  val simplify_meta_eq = Arith_Data.simplify_meta_eq
wenzelm@23164
    44
    [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
huffman@26086
    45
      @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
wenzelm@23164
    46
  end
wenzelm@23164
    47
haftmann@30931
    48
(*Version for semiring_div*)
haftmann@30931
    49
structure DivCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
    50
 (open CancelNumeralFactorCommon
haftmann@30496
    51
  val prove_conv = Arith_Data.prove_conv
wenzelm@23164
    52
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
haftmann@30931
    53
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
haftmann@30931
    54
  val cancel = @{thm div_mult_mult1} RS trans
wenzelm@23164
    55
  val neg_exchanges = false
wenzelm@23164
    56
)
wenzelm@23164
    57
wenzelm@23164
    58
(*Version for fields*)
wenzelm@23164
    59
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
    60
 (open CancelNumeralFactorCommon
haftmann@30496
    61
  val prove_conv = Arith_Data.prove_conv
wenzelm@23164
    62
  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
wenzelm@23164
    63
  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
nipkow@23413
    64
  val cancel = @{thm mult_divide_mult_cancel_left} RS trans
wenzelm@23164
    65
  val neg_exchanges = false
wenzelm@23164
    66
)
wenzelm@23164
    67
wenzelm@23164
    68
structure EqCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
    69
 (open CancelNumeralFactorCommon
haftmann@30496
    70
  val prove_conv = Arith_Data.prove_conv
wenzelm@23164
    71
  val mk_bal   = HOLogic.mk_eq
wenzelm@23164
    72
  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
wenzelm@23164
    73
  val cancel = @{thm mult_cancel_left} RS trans
wenzelm@23164
    74
  val neg_exchanges = false
wenzelm@23164
    75
)
wenzelm@23164
    76
wenzelm@23164
    77
structure LessCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
    78
 (open CancelNumeralFactorCommon
haftmann@30496
    79
  val prove_conv = Arith_Data.prove_conv
haftmann@23881
    80
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
haftmann@23881
    81
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
wenzelm@23164
    82
  val cancel = @{thm mult_less_cancel_left} RS trans
wenzelm@23164
    83
  val neg_exchanges = true
wenzelm@23164
    84
)
wenzelm@23164
    85
wenzelm@23164
    86
structure LeCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
    87
 (open CancelNumeralFactorCommon
haftmann@30496
    88
  val prove_conv = Arith_Data.prove_conv
haftmann@23881
    89
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
haftmann@23881
    90
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
wenzelm@23164
    91
  val cancel = @{thm mult_le_cancel_left} RS trans
wenzelm@23164
    92
  val neg_exchanges = true
wenzelm@23164
    93
)
wenzelm@23164
    94
wenzelm@23164
    95
val cancel_numeral_factors =
haftmann@30496
    96
  map Arith_Data.prep_simproc
wenzelm@23164
    97
   [("ring_eq_cancel_numeral_factor",
wenzelm@23164
    98
     ["(l::'a::{idom,number_ring}) * m = n",
wenzelm@23164
    99
      "(l::'a::{idom,number_ring}) = m * n"],
wenzelm@23164
   100
     K EqCancelNumeralFactor.proc),
wenzelm@23164
   101
    ("ring_less_cancel_numeral_factor",
wenzelm@23164
   102
     ["(l::'a::{ordered_idom,number_ring}) * m < n",
wenzelm@23164
   103
      "(l::'a::{ordered_idom,number_ring}) < m * n"],
wenzelm@23164
   104
     K LessCancelNumeralFactor.proc),
wenzelm@23164
   105
    ("ring_le_cancel_numeral_factor",
wenzelm@23164
   106
     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
wenzelm@23164
   107
      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
wenzelm@23164
   108
     K LeCancelNumeralFactor.proc),
wenzelm@23164
   109
    ("int_div_cancel_numeral_factors",
haftmann@30931
   110
     ["((l::'a::{semiring_div,number_ring}) * m) div n",
haftmann@30931
   111
      "(l::'a::{semiring_div,number_ring}) div (m * n)"],
haftmann@30931
   112
     K DivCancelNumeralFactor.proc),
wenzelm@23164
   113
    ("divide_cancel_numeral_factor",
wenzelm@23164
   114
     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
wenzelm@23164
   115
      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
wenzelm@23164
   116
      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
wenzelm@23164
   117
     K DivideCancelNumeralFactor.proc)];
wenzelm@23164
   118
wenzelm@23164
   119
(* referenced by rat_arith.ML *)
wenzelm@23164
   120
val field_cancel_numeral_factors =
haftmann@30496
   121
  map Arith_Data.prep_simproc
wenzelm@23164
   122
   [("field_eq_cancel_numeral_factor",
wenzelm@23164
   123
     ["(l::'a::{field,number_ring}) * m = n",
wenzelm@23164
   124
      "(l::'a::{field,number_ring}) = m * n"],
wenzelm@23164
   125
     K EqCancelNumeralFactor.proc),
wenzelm@23164
   126
    ("field_cancel_numeral_factor",
wenzelm@23164
   127
     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
wenzelm@23164
   128
      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
wenzelm@23164
   129
      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
wenzelm@23164
   130
     K DivideCancelNumeralFactor.proc)]
wenzelm@23164
   131
wenzelm@23164
   132
end;
wenzelm@23164
   133
wenzelm@23164
   134
Addsimprocs cancel_numeral_factors;
wenzelm@23164
   135
wenzelm@23164
   136
(*examples:
wenzelm@23164
   137
print_depth 22;
wenzelm@23164
   138
set timing;
wenzelm@23164
   139
set trace_simp;
wenzelm@23164
   140
fun test s = (Goal s; by (Simp_tac 1));
wenzelm@23164
   141
wenzelm@23164
   142
test "9*x = 12 * (y::int)";
wenzelm@23164
   143
test "(9*x) div (12 * (y::int)) = z";
wenzelm@23164
   144
test "9*x < 12 * (y::int)";
wenzelm@23164
   145
test "9*x <= 12 * (y::int)";
wenzelm@23164
   146
wenzelm@23164
   147
test "-99*x = 132 * (y::int)";
wenzelm@23164
   148
test "(-99*x) div (132 * (y::int)) = z";
wenzelm@23164
   149
test "-99*x < 132 * (y::int)";
wenzelm@23164
   150
test "-99*x <= 132 * (y::int)";
wenzelm@23164
   151
wenzelm@23164
   152
test "999*x = -396 * (y::int)";
wenzelm@23164
   153
test "(999*x) div (-396 * (y::int)) = z";
wenzelm@23164
   154
test "999*x < -396 * (y::int)";
wenzelm@23164
   155
test "999*x <= -396 * (y::int)";
wenzelm@23164
   156
wenzelm@23164
   157
test "-99*x = -81 * (y::int)";
wenzelm@23164
   158
test "(-99*x) div (-81 * (y::int)) = z";
wenzelm@23164
   159
test "-99*x <= -81 * (y::int)";
wenzelm@23164
   160
test "-99*x < -81 * (y::int)";
wenzelm@23164
   161
wenzelm@23164
   162
test "-2 * x = -1 * (y::int)";
wenzelm@23164
   163
test "-2 * x = -(y::int)";
wenzelm@23164
   164
test "(-2 * x) div (-1 * (y::int)) = z";
wenzelm@23164
   165
test "-2 * x < -(y::int)";
wenzelm@23164
   166
test "-2 * x <= -1 * (y::int)";
wenzelm@23164
   167
test "-x < -23 * (y::int)";
wenzelm@23164
   168
test "-x <= -23 * (y::int)";
wenzelm@23164
   169
*)
wenzelm@23164
   170
wenzelm@23164
   171
(*And the same examples for fields such as rat or real:
wenzelm@23164
   172
test "0 <= (y::rat) * -2";
wenzelm@23164
   173
test "9*x = 12 * (y::rat)";
wenzelm@23164
   174
test "(9*x) / (12 * (y::rat)) = z";
wenzelm@23164
   175
test "9*x < 12 * (y::rat)";
wenzelm@23164
   176
test "9*x <= 12 * (y::rat)";
wenzelm@23164
   177
wenzelm@23164
   178
test "-99*x = 132 * (y::rat)";
wenzelm@23164
   179
test "(-99*x) / (132 * (y::rat)) = z";
wenzelm@23164
   180
test "-99*x < 132 * (y::rat)";
wenzelm@23164
   181
test "-99*x <= 132 * (y::rat)";
wenzelm@23164
   182
wenzelm@23164
   183
test "999*x = -396 * (y::rat)";
wenzelm@23164
   184
test "(999*x) / (-396 * (y::rat)) = z";
wenzelm@23164
   185
test "999*x < -396 * (y::rat)";
wenzelm@23164
   186
test "999*x <= -396 * (y::rat)";
wenzelm@23164
   187
wenzelm@23164
   188
test  "(- ((2::rat) * x) <= 2 * y)";
wenzelm@23164
   189
test "-99*x = -81 * (y::rat)";
wenzelm@23164
   190
test "(-99*x) / (-81 * (y::rat)) = z";
wenzelm@23164
   191
test "-99*x <= -81 * (y::rat)";
wenzelm@23164
   192
test "-99*x < -81 * (y::rat)";
wenzelm@23164
   193
wenzelm@23164
   194
test "-2 * x = -1 * (y::rat)";
wenzelm@23164
   195
test "-2 * x = -(y::rat)";
wenzelm@23164
   196
test "(-2 * x) / (-1 * (y::rat)) = z";
wenzelm@23164
   197
test "-2 * x < -(y::rat)";
wenzelm@23164
   198
test "-2 * x <= -1 * (y::rat)";
wenzelm@23164
   199
test "-x < -23 * (y::rat)";
wenzelm@23164
   200
test "-x <= -23 * (y::rat)";
wenzelm@23164
   201
*)
wenzelm@23164
   202
wenzelm@23164
   203
wenzelm@23164
   204
(** Declarations for ExtractCommonTerm **)
wenzelm@23164
   205
wenzelm@23164
   206
local
wenzelm@23164
   207
  open Int_Numeral_Simprocs
wenzelm@23164
   208
in
wenzelm@23164
   209
wenzelm@23164
   210
(*Find first term that matches u*)
wenzelm@23164
   211
fun find_first_t past u []         = raise TERM ("find_first_t", [])
wenzelm@23164
   212
  | find_first_t past u (t::terms) =
wenzelm@23164
   213
        if u aconv t then (rev past @ terms)
wenzelm@23164
   214
        else find_first_t (t::past) u terms
wenzelm@23164
   215
        handle TERM _ => find_first_t (t::past) u terms;
wenzelm@23164
   216
wenzelm@23164
   217
(** Final simplification for the CancelFactor simprocs **)
haftmann@30518
   218
val simplify_one = Arith_Data.simplify_meta_eq  
nipkow@30031
   219
  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
wenzelm@23164
   220
nipkow@30649
   221
fun cancel_simplify_meta_eq ss cancel_th th =
wenzelm@23164
   222
    simplify_one ss (([th, cancel_th]) MRS trans);
wenzelm@23164
   223
nipkow@30649
   224
local
haftmann@31067
   225
  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop)
nipkow@30649
   226
  fun Eq_True_elim Eq = 
nipkow@30649
   227
    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
nipkow@30649
   228
in
nipkow@30649
   229
fun sign_conv pos_th neg_th ss t =
nipkow@30649
   230
  let val T = fastype_of t;
nipkow@30649
   231
      val zero = Const(@{const_name HOL.zero}, T);
nipkow@30649
   232
      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
nipkow@30649
   233
      val pos = less $ zero $ t and neg = less $ t $ zero
nipkow@30649
   234
      fun prove p =
haftmann@30685
   235
        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
nipkow@30649
   236
        handle THM _ => NONE
nipkow@30649
   237
    in case prove pos of
nipkow@30649
   238
         SOME th => SOME(th RS pos_th)
nipkow@30649
   239
       | NONE => (case prove neg of
nipkow@30649
   240
                    SOME th => SOME(th RS neg_th)
nipkow@30649
   241
                  | NONE => NONE)
nipkow@30649
   242
    end;
nipkow@30649
   243
end
nipkow@30649
   244
wenzelm@23164
   245
structure CancelFactorCommon =
wenzelm@23164
   246
  struct
wenzelm@23164
   247
  val mk_sum            = long_mk_prod
wenzelm@23164
   248
  val dest_sum          = dest_prod
wenzelm@23164
   249
  val mk_coeff          = mk_coeff
wenzelm@23164
   250
  val dest_coeff        = dest_coeff
wenzelm@23164
   251
  val find_first        = find_first_t []
haftmann@30518
   252
  val trans_tac         = K Arith_Data.trans_tac
haftmann@23881
   253
  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
wenzelm@23164
   254
  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
nipkow@30649
   255
  val simplify_meta_eq  = cancel_simplify_meta_eq 
wenzelm@23164
   256
  end;
wenzelm@23164
   257
wenzelm@23164
   258
(*mult_cancel_left requires a ring with no zero divisors.*)
wenzelm@23164
   259
structure EqCancelFactor = ExtractCommonTermFun
wenzelm@23164
   260
 (open CancelFactorCommon
haftmann@30496
   261
  val prove_conv = Arith_Data.prove_conv
wenzelm@23164
   262
  val mk_bal   = HOLogic.mk_eq
wenzelm@23164
   263
  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
nipkow@30649
   264
  val simp_conv = K (K (SOME @{thm mult_cancel_left}))
nipkow@30649
   265
);
nipkow@30649
   266
nipkow@30649
   267
(*for ordered rings*)
nipkow@30649
   268
structure LeCancelFactor = ExtractCommonTermFun
nipkow@30649
   269
 (open CancelFactorCommon
nipkow@30649
   270
  val prove_conv = Arith_Data.prove_conv
nipkow@30649
   271
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
nipkow@30649
   272
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
nipkow@30649
   273
  val simp_conv = sign_conv
nipkow@30649
   274
    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
nipkow@30649
   275
);
nipkow@30649
   276
nipkow@30649
   277
(*for ordered rings*)
nipkow@30649
   278
structure LessCancelFactor = ExtractCommonTermFun
nipkow@30649
   279
 (open CancelFactorCommon
nipkow@30649
   280
  val prove_conv = Arith_Data.prove_conv
nipkow@30649
   281
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
nipkow@30649
   282
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
nipkow@30649
   283
  val simp_conv = sign_conv
nipkow@30649
   284
    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
wenzelm@23164
   285
);
wenzelm@23164
   286
haftmann@30931
   287
(*for semirings with division*)
haftmann@30931
   288
structure DivCancelFactor = ExtractCommonTermFun
wenzelm@23164
   289
 (open CancelFactorCommon
haftmann@30496
   290
  val prove_conv = Arith_Data.prove_conv
wenzelm@23164
   291
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
haftmann@30931
   292
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
haftmann@30931
   293
  val simp_conv = K (K (SOME @{thm div_mult_mult1_if}))
wenzelm@23164
   294
);
wenzelm@23164
   295
haftmann@30931
   296
structure ModCancelFactor = ExtractCommonTermFun
nipkow@24395
   297
 (open CancelFactorCommon
haftmann@30496
   298
  val prove_conv = Arith_Data.prove_conv
nipkow@24395
   299
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
haftmann@31067
   300
  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
haftmann@30931
   301
  val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
nipkow@24395
   302
);
nipkow@24395
   303
haftmann@30931
   304
(*for idoms*)
haftmann@30931
   305
structure DvdCancelFactor = ExtractCommonTermFun
nipkow@23969
   306
 (open CancelFactorCommon
haftmann@30496
   307
  val prove_conv = Arith_Data.prove_conv
haftmann@27651
   308
  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
huffman@29981
   309
  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
nipkow@30649
   310
  val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
nipkow@23969
   311
);
nipkow@23969
   312
wenzelm@23164
   313
(*Version for all fields, including unordered ones (type complex).*)
wenzelm@23164
   314
structure DivideCancelFactor = ExtractCommonTermFun
wenzelm@23164
   315
 (open CancelFactorCommon
haftmann@30496
   316
  val prove_conv = Arith_Data.prove_conv
wenzelm@23164
   317
  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
wenzelm@23164
   318
  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
nipkow@30649
   319
  val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
wenzelm@23164
   320
);
wenzelm@23164
   321
wenzelm@23164
   322
val cancel_factors =
haftmann@30496
   323
  map Arith_Data.prep_simproc
wenzelm@23164
   324
   [("ring_eq_cancel_factor",
haftmann@30931
   325
     ["(l::'a::idom) * m = n",
haftmann@30931
   326
      "(l::'a::idom) = m * n"],
nipkow@30649
   327
     K EqCancelFactor.proc),
nipkow@30649
   328
    ("ordered_ring_le_cancel_factor",
nipkow@30649
   329
     ["(l::'a::ordered_ring) * m <= n",
nipkow@30649
   330
      "(l::'a::ordered_ring) <= m * n"],
nipkow@30649
   331
     K LeCancelFactor.proc),
nipkow@30649
   332
    ("ordered_ring_less_cancel_factor",
nipkow@30649
   333
     ["(l::'a::ordered_ring) * m < n",
nipkow@30649
   334
      "(l::'a::ordered_ring) < m * n"],
nipkow@30649
   335
     K LessCancelFactor.proc),
wenzelm@23164
   336
    ("int_div_cancel_factor",
haftmann@30931
   337
     ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],
haftmann@30931
   338
     K DivCancelFactor.proc),
nipkow@24395
   339
    ("int_mod_cancel_factor",
haftmann@30931
   340
     ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"],
haftmann@30931
   341
     K ModCancelFactor.proc),
huffman@29981
   342
    ("dvd_cancel_factor",
huffman@29981
   343
     ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
haftmann@30931
   344
     K DvdCancelFactor.proc),
wenzelm@23164
   345
    ("divide_cancel_factor",
nipkow@23400
   346
     ["((l::'a::{division_by_zero,field}) * m) / n",
nipkow@23400
   347
      "(l::'a::{division_by_zero,field}) / (m * n)"],
wenzelm@23164
   348
     K DivideCancelFactor.proc)];
wenzelm@23164
   349
wenzelm@23164
   350
end;
wenzelm@23164
   351
wenzelm@23164
   352
Addsimprocs cancel_factors;
wenzelm@23164
   353
wenzelm@23164
   354
wenzelm@23164
   355
(*examples:
wenzelm@23164
   356
print_depth 22;
wenzelm@23164
   357
set timing;
wenzelm@23164
   358
set trace_simp;
wenzelm@23164
   359
fun test s = (Goal s; by (Asm_simp_tac 1));
wenzelm@23164
   360
wenzelm@23164
   361
test "x*k = k*(y::int)";
wenzelm@23164
   362
test "k = k*(y::int)";
wenzelm@23164
   363
test "a*(b*c) = (b::int)";
wenzelm@23164
   364
test "a*(b*c) = d*(b::int)*(x*a)";
wenzelm@23164
   365
wenzelm@23164
   366
test "(x*k) div (k*(y::int)) = (uu::int)";
wenzelm@23164
   367
test "(k) div (k*(y::int)) = (uu::int)";
wenzelm@23164
   368
test "(a*(b*c)) div ((b::int)) = (uu::int)";
wenzelm@23164
   369
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
wenzelm@23164
   370
*)
wenzelm@23164
   371
wenzelm@23164
   372
(*And the same examples for fields such as rat or real:
wenzelm@23164
   373
print_depth 22;
wenzelm@23164
   374
set timing;
wenzelm@23164
   375
set trace_simp;
wenzelm@23164
   376
fun test s = (Goal s; by (Asm_simp_tac 1));
wenzelm@23164
   377
wenzelm@23164
   378
test "x*k = k*(y::rat)";
wenzelm@23164
   379
test "k = k*(y::rat)";
wenzelm@23164
   380
test "a*(b*c) = (b::rat)";
wenzelm@23164
   381
test "a*(b*c) = d*(b::rat)*(x*a)";
wenzelm@23164
   382
wenzelm@23164
   383
wenzelm@23164
   384
test "(x*k) / (k*(y::rat)) = (uu::rat)";
wenzelm@23164
   385
test "(k) / (k*(y::rat)) = (uu::rat)";
wenzelm@23164
   386
test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
wenzelm@23164
   387
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
wenzelm@23164
   388
wenzelm@23164
   389
(*FIXME: what do we do about this?*)
wenzelm@23164
   390
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
wenzelm@23164
   391
*)