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