src/HOL/Integ/int_factor_simprocs.ML
author wenzelm
Thu Dec 01 22:04:27 2005 +0100 (2005-12-01)
changeset 18328 841261f303a1
parent 17877 67d5ab1cb0d8
child 18442 b35d7312c64f
permissions -rw-r--r--
simprocs: static evaluation of simpset;
paulson@10536
     1
(*  Title:      HOL/int_factor_simprocs.ML
paulson@10536
     2
    ID:         $Id$
paulson@10536
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@10536
     4
    Copyright   2000  University of Cambridge
paulson@10536
     5
paulson@14390
     6
Factor cancellation simprocs for the integers (and for fields).
paulson@10536
     7
paulson@14378
     8
This file can't be combined with int_arith1 because it requires IntDiv.thy.
paulson@10536
     9
*)
paulson@10536
    10
paulson@14390
    11
paulson@14390
    12
(*To quote from Provers/Arith/cancel_numeral_factor.ML:
paulson@14390
    13
paulson@14390
    14
Cancels common coefficients in balanced expressions:
paulson@14390
    15
paulson@14390
    16
     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
paulson@14390
    17
paulson@14390
    18
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
paulson@14390
    19
and d = gcd(m,m') and n=m/d and n'=m'/d.
paulson@14390
    20
*)
paulson@14390
    21
paulson@14390
    22
val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq];
paulson@14390
    23
paulson@14390
    24
(** Factor cancellation theorems for integer division (div, not /) **)
paulson@10536
    25
paulson@11868
    26
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
wenzelm@13462
    27
by (stac zdiv_zmult_zmult1 1);
wenzelm@13462
    28
by Auto_tac;
paulson@10536
    29
qed "int_mult_div_cancel1";
paulson@10536
    30
paulson@10703
    31
(*For ExtractCommonTermFun, cancelling common factors*)
paulson@11868
    32
Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
wenzelm@13462
    33
by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
paulson@10703
    34
qed "int_mult_div_cancel_disj";
paulson@10703
    35
paulson@14378
    36
paulson@10536
    37
local
paulson@10536
    38
  open Int_Numeral_Simprocs
paulson@10536
    39
in
paulson@10536
    40
paulson@10536
    41
structure CancelNumeralFactorCommon =
paulson@10536
    42
  struct
wenzelm@13462
    43
  val mk_coeff          = mk_coeff
wenzelm@13462
    44
  val dest_coeff        = dest_coeff 1
wenzelm@16973
    45
  val trans_tac         = fn _ => trans_tac
wenzelm@18328
    46
wenzelm@18328
    47
  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
wenzelm@18328
    48
  val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps
wenzelm@18328
    49
  val norm_ss3 = HOL_ss addsimps mult_ac
wenzelm@16973
    50
  fun norm_tac ss =
wenzelm@18328
    51
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@18328
    52
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@18328
    53
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
wenzelm@18328
    54
wenzelm@18328
    55
  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps
wenzelm@18328
    56
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
wenzelm@16973
    57
  val simplify_meta_eq = 
paulson@14390
    58
	Int_Numeral_Simprocs.simplify_meta_eq
paulson@14390
    59
	     [add_0, add_0_right,
paulson@14390
    60
	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
paulson@10536
    61
  end
paulson@10536
    62
paulson@14390
    63
(*Version for integer division*)
paulson@10536
    64
structure DivCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    65
 (open CancelNumeralFactorCommon
wenzelm@13485
    66
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
    67
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
paulson@10536
    68
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
paulson@10536
    69
  val cancel = int_mult_div_cancel1 RS trans
paulson@10536
    70
  val neg_exchanges = false
paulson@10536
    71
)
paulson@10536
    72
paulson@14390
    73
(*Version for fields*)
paulson@14390
    74
structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
paulson@14390
    75
 (open CancelNumeralFactorCommon
paulson@14390
    76
  val prove_conv = Bin_Simprocs.prove_conv
paulson@14390
    77
  val mk_bal   = HOLogic.mk_binop "HOL.divide"
paulson@14390
    78
  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
paulson@14390
    79
  val cancel = mult_divide_cancel_left RS trans
paulson@14390
    80
  val neg_exchanges = false
paulson@14390
    81
)
paulson@14390
    82
paulson@14390
    83
(*Version for ordered rings: mult_cancel_left requires an ordering*)
paulson@10536
    84
structure EqCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    85
 (open CancelNumeralFactorCommon
wenzelm@13485
    86
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
    87
  val mk_bal   = HOLogic.mk_eq
paulson@14390
    88
  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
paulson@14378
    89
  val cancel = mult_cancel_left RS trans
paulson@10536
    90
  val neg_exchanges = false
paulson@10536
    91
)
paulson@10536
    92
paulson@14390
    93
(*Version for (unordered) fields*)
paulson@14390
    94
structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
paulson@14390
    95
 (open CancelNumeralFactorCommon
paulson@14390
    96
  val prove_conv = Bin_Simprocs.prove_conv
paulson@14390
    97
  val mk_bal   = HOLogic.mk_eq
paulson@14390
    98
  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
paulson@14390
    99
  val cancel = field_mult_cancel_left RS trans
paulson@14390
   100
  val neg_exchanges = false
paulson@14390
   101
)
paulson@14390
   102
paulson@10536
   103
structure LessCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   104
 (open CancelNumeralFactorCommon
wenzelm@13485
   105
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
   106
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@14390
   107
  val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
paulson@14378
   108
  val cancel = mult_less_cancel_left RS trans
paulson@10536
   109
  val neg_exchanges = true
paulson@10536
   110
)
paulson@10536
   111
paulson@10536
   112
structure LeCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   113
 (open CancelNumeralFactorCommon
wenzelm@13485
   114
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
   115
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@14390
   116
  val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
paulson@14378
   117
  val cancel = mult_le_cancel_left RS trans
paulson@10536
   118
  val neg_exchanges = true
paulson@10536
   119
)
paulson@10536
   120
paulson@14390
   121
val ring_cancel_numeral_factors =
paulson@11868
   122
  map Bin_Simprocs.prep_simproc
paulson@14390
   123
   [("ring_eq_cancel_numeral_factor",
obua@14738
   124
     ["(l::'a::{ordered_idom,number_ring}) * m = n",
obua@14738
   125
      "(l::'a::{ordered_idom,number_ring}) = m * n"],
paulson@10536
   126
     EqCancelNumeralFactor.proc),
paulson@14390
   127
    ("ring_less_cancel_numeral_factor",
obua@14738
   128
     ["(l::'a::{ordered_idom,number_ring}) * m < n",
obua@14738
   129
      "(l::'a::{ordered_idom,number_ring}) < m * n"],
paulson@10536
   130
     LessCancelNumeralFactor.proc),
paulson@14390
   131
    ("ring_le_cancel_numeral_factor",
obua@14738
   132
     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
obua@14738
   133
      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
paulson@10536
   134
     LeCancelNumeralFactor.proc),
paulson@14390
   135
    ("int_div_cancel_numeral_factors",
paulson@14390
   136
     ["((l::int) * m) div n", "(l::int) div (m * n)"],
paulson@10536
   137
     DivCancelNumeralFactor.proc)];
paulson@10536
   138
paulson@14390
   139
paulson@14390
   140
val field_cancel_numeral_factors =
paulson@14390
   141
  map Bin_Simprocs.prep_simproc
paulson@14390
   142
   [("field_eq_cancel_numeral_factor",
paulson@14390
   143
     ["(l::'a::{field,number_ring}) * m = n",
paulson@14390
   144
      "(l::'a::{field,number_ring}) = m * n"],
paulson@14390
   145
     FieldEqCancelNumeralFactor.proc),
paulson@14390
   146
    ("field_cancel_numeral_factor",
paulson@14426
   147
     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
paulson@14426
   148
      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
paulson@14426
   149
      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
paulson@14390
   150
     FieldDivCancelNumeralFactor.proc)]
paulson@14390
   151
paulson@10536
   152
end;
paulson@10536
   153
paulson@14390
   154
Addsimprocs ring_cancel_numeral_factors;
paulson@14390
   155
Addsimprocs field_cancel_numeral_factors;
paulson@10536
   156
paulson@10536
   157
(*examples:
paulson@10536
   158
print_depth 22;
paulson@10536
   159
set timing;
paulson@10536
   160
set trace_simp;
wenzelm@13462
   161
fun test s = (Goal s; by (Simp_tac 1));
paulson@10536
   162
wenzelm@11704
   163
test "9*x = 12 * (y::int)";
wenzelm@11704
   164
test "(9*x) div (12 * (y::int)) = z";
wenzelm@11704
   165
test "9*x < 12 * (y::int)";
wenzelm@11704
   166
test "9*x <= 12 * (y::int)";
paulson@10536
   167
wenzelm@11704
   168
test "-99*x = 132 * (y::int)";
wenzelm@11704
   169
test "(-99*x) div (132 * (y::int)) = z";
wenzelm@11704
   170
test "-99*x < 132 * (y::int)";
wenzelm@11704
   171
test "-99*x <= 132 * (y::int)";
paulson@10536
   172
wenzelm@11704
   173
test "999*x = -396 * (y::int)";
wenzelm@11704
   174
test "(999*x) div (-396 * (y::int)) = z";
wenzelm@11704
   175
test "999*x < -396 * (y::int)";
wenzelm@11704
   176
test "999*x <= -396 * (y::int)";
paulson@10536
   177
wenzelm@11704
   178
test "-99*x = -81 * (y::int)";
wenzelm@11704
   179
test "(-99*x) div (-81 * (y::int)) = z";
wenzelm@11704
   180
test "-99*x <= -81 * (y::int)";
wenzelm@11704
   181
test "-99*x < -81 * (y::int)";
paulson@10536
   182
wenzelm@11704
   183
test "-2 * x = -1 * (y::int)";
wenzelm@11704
   184
test "-2 * x = -(y::int)";
wenzelm@11704
   185
test "(-2 * x) div (-1 * (y::int)) = z";
wenzelm@11704
   186
test "-2 * x < -(y::int)";
wenzelm@11704
   187
test "-2 * x <= -1 * (y::int)";
wenzelm@11704
   188
test "-x < -23 * (y::int)";
wenzelm@11704
   189
test "-x <= -23 * (y::int)";
paulson@10536
   190
*)
paulson@10536
   191
paulson@14390
   192
(*And the same examples for fields such as rat or real:
paulson@14390
   193
test "0 <= (y::rat) * -2";
paulson@14390
   194
test "9*x = 12 * (y::rat)";
paulson@14390
   195
test "(9*x) / (12 * (y::rat)) = z";
paulson@14390
   196
test "9*x < 12 * (y::rat)";
paulson@14390
   197
test "9*x <= 12 * (y::rat)";
paulson@14390
   198
paulson@14390
   199
test "-99*x = 132 * (y::rat)";
paulson@14390
   200
test "(-99*x) / (132 * (y::rat)) = z";
paulson@14390
   201
test "-99*x < 132 * (y::rat)";
paulson@14390
   202
test "-99*x <= 132 * (y::rat)";
paulson@14390
   203
paulson@14390
   204
test "999*x = -396 * (y::rat)";
paulson@14390
   205
test "(999*x) / (-396 * (y::rat)) = z";
paulson@14390
   206
test "999*x < -396 * (y::rat)";
paulson@14390
   207
test "999*x <= -396 * (y::rat)";
paulson@14390
   208
paulson@14390
   209
test  "(- ((2::rat) * x) <= 2 * y)";
paulson@14390
   210
test "-99*x = -81 * (y::rat)";
paulson@14390
   211
test "(-99*x) / (-81 * (y::rat)) = z";
paulson@14390
   212
test "-99*x <= -81 * (y::rat)";
paulson@14390
   213
test "-99*x < -81 * (y::rat)";
paulson@14390
   214
paulson@14390
   215
test "-2 * x = -1 * (y::rat)";
paulson@14390
   216
test "-2 * x = -(y::rat)";
paulson@14390
   217
test "(-2 * x) / (-1 * (y::rat)) = z";
paulson@14390
   218
test "-2 * x < -(y::rat)";
paulson@14390
   219
test "-2 * x <= -1 * (y::rat)";
paulson@14390
   220
test "-x < -23 * (y::rat)";
paulson@14390
   221
test "-x <= -23 * (y::rat)";
paulson@14390
   222
*)
paulson@14390
   223
paulson@10703
   224
paulson@10703
   225
(** Declarations for ExtractCommonTerm **)
paulson@10703
   226
paulson@10703
   227
local
paulson@10703
   228
  open Int_Numeral_Simprocs
paulson@10703
   229
in
paulson@10703
   230
paulson@10703
   231
(*Find first term that matches u*)
wenzelm@13462
   232
fun find_first past u []         = raise TERM("find_first", [])
paulson@10703
   233
  | find_first past u (t::terms) =
wenzelm@13462
   234
        if u aconv t then (rev past @ terms)
paulson@10703
   235
        else find_first (t::past) u terms
wenzelm@13462
   236
        handle TERM _ => find_first (t::past) u terms;
paulson@10703
   237
paulson@15271
   238
(** Final simplification for the CancelFactor simprocs **)
paulson@15271
   239
val simplify_one = 
paulson@15271
   240
    Int_Numeral_Simprocs.simplify_meta_eq  
paulson@15271
   241
       [mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
paulson@15271
   242
wenzelm@16973
   243
fun cancel_simplify_meta_eq cancel_th ss th =
wenzelm@16973
   244
    simplify_one ss (([th, cancel_th]) MRS trans);
paulson@10703
   245
paulson@14426
   246
(*At present, long_mk_prod creates Numeral1, so this requires the axclass
paulson@14426
   247
  number_ring*)
paulson@10703
   248
structure CancelFactorCommon =
paulson@10703
   249
  struct
wenzelm@13462
   250
  val mk_sum            = long_mk_prod
wenzelm@13462
   251
  val dest_sum          = dest_prod
wenzelm@13462
   252
  val mk_coeff          = mk_coeff
wenzelm@13462
   253
  val dest_coeff        = dest_coeff
wenzelm@13462
   254
  val find_first        = find_first []
wenzelm@16973
   255
  val trans_tac         = fn _ => trans_tac
wenzelm@18328
   256
  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
wenzelm@18328
   257
  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
paulson@10703
   258
  end;
paulson@10703
   259
obua@14738
   260
(*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
paulson@14387
   261
  rat_arith.ML works for all fields.*)
paulson@10703
   262
structure EqCancelFactor = ExtractCommonTermFun
paulson@10703
   263
 (open CancelFactorCommon
wenzelm@13485
   264
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10703
   265
  val mk_bal   = HOLogic.mk_eq
paulson@10703
   266
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
paulson@14378
   267
  val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
paulson@10703
   268
);
paulson@10703
   269
paulson@14387
   270
(*int_mult_div_cancel_disj is for integer division (div). The version in
paulson@14387
   271
  rat_arith.ML works for all fields, using real division (/).*)
paulson@10703
   272
structure DivideCancelFactor = ExtractCommonTermFun
paulson@10703
   273
 (open CancelFactorCommon
wenzelm@13485
   274
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10703
   275
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
paulson@10703
   276
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
paulson@10703
   277
  val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
paulson@10703
   278
);
paulson@10703
   279
wenzelm@13462
   280
val int_cancel_factor =
paulson@11868
   281
  map Bin_Simprocs.prep_simproc
paulson@15271
   282
   [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
paulson@14390
   283
    EqCancelFactor.proc),
paulson@14390
   284
    ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
paulson@10703
   285
     DivideCancelFactor.proc)];
paulson@10703
   286
paulson@14390
   287
(** Versions for all fields, including unordered ones (type complex).*)
paulson@14390
   288
paulson@14390
   289
structure FieldEqCancelFactor = ExtractCommonTermFun
paulson@14390
   290
 (open CancelFactorCommon
paulson@14390
   291
  val prove_conv = Bin_Simprocs.prove_conv
paulson@14390
   292
  val mk_bal   = HOLogic.mk_eq
paulson@14390
   293
  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
paulson@14390
   294
  val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
paulson@14390
   295
);
paulson@14390
   296
paulson@14390
   297
structure FieldDivideCancelFactor = ExtractCommonTermFun
paulson@14390
   298
 (open CancelFactorCommon
paulson@14390
   299
  val prove_conv = Bin_Simprocs.prove_conv
paulson@14390
   300
  val mk_bal   = HOLogic.mk_binop "HOL.divide"
paulson@14390
   301
  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
paulson@14390
   302
  val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
paulson@14390
   303
);
paulson@14390
   304
paulson@15271
   305
(*The number_ring class is necessary because the simprocs refer to the
paulson@14426
   306
  binary number 1.  FIXME: probably they could use 1 instead.*)
paulson@14390
   307
val field_cancel_factor =
paulson@14390
   308
  map Bin_Simprocs.prep_simproc
paulson@14390
   309
   [("field_eq_cancel_factor",
paulson@14426
   310
     ["(l::'a::{field,number_ring}) * m = n",
paulson@15271
   311
      "(l::'a::{field,number_ring}) = m * n"],
paulson@14390
   312
     FieldEqCancelFactor.proc),
paulson@14390
   313
    ("field_divide_cancel_factor",
paulson@14426
   314
     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
paulson@14426
   315
      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
paulson@14390
   316
     FieldDivideCancelFactor.proc)];
paulson@14390
   317
paulson@10703
   318
end;
paulson@10703
   319
paulson@10703
   320
Addsimprocs int_cancel_factor;
paulson@14390
   321
Addsimprocs field_cancel_factor;
paulson@10703
   322
paulson@10703
   323
paulson@10703
   324
(*examples:
paulson@10703
   325
print_depth 22;
paulson@10703
   326
set timing;
paulson@10703
   327
set trace_simp;
wenzelm@13462
   328
fun test s = (Goal s; by (Asm_simp_tac 1));
paulson@10703
   329
paulson@10703
   330
test "x*k = k*(y::int)";
wenzelm@13462
   331
test "k = k*(y::int)";
paulson@10703
   332
test "a*(b*c) = (b::int)";
paulson@10703
   333
test "a*(b*c) = d*(b::int)*(x*a)";
paulson@10703
   334
paulson@10703
   335
test "(x*k) div (k*(y::int)) = (uu::int)";
wenzelm@13462
   336
test "(k) div (k*(y::int)) = (uu::int)";
paulson@10703
   337
test "(a*(b*c)) div ((b::int)) = (uu::int)";
paulson@10703
   338
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
paulson@10703
   339
*)
paulson@10703
   340
paulson@14390
   341
(*And the same examples for fields such as rat or real:
paulson@14390
   342
print_depth 22;
paulson@14390
   343
set timing;
paulson@14390
   344
set trace_simp;
paulson@14390
   345
fun test s = (Goal s; by (Asm_simp_tac 1));
paulson@14390
   346
paulson@14390
   347
test "x*k = k*(y::rat)";
paulson@14390
   348
test "k = k*(y::rat)";
paulson@14390
   349
test "a*(b*c) = (b::rat)";
paulson@14390
   350
test "a*(b*c) = d*(b::rat)*(x*a)";
paulson@14390
   351
paulson@14390
   352
paulson@14390
   353
test "(x*k) / (k*(y::rat)) = (uu::rat)";
paulson@14390
   354
test "(k) / (k*(y::rat)) = (uu::rat)";
paulson@14390
   355
test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
paulson@14390
   356
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
paulson@14390
   357
paulson@14390
   358
(*FIXME: what do we do about this?*)
paulson@14390
   359
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
paulson@14390
   360
*)