src/HOL/Integ/int_factor_simprocs.ML
author paulson
Tue Feb 10 12:02:11 2004 +0100 (2004-02-10)
changeset 14378 69c4d5997669
parent 14113 7b3513ba0f86
child 14387 e96d5c42c4b0
permissions -rw-r--r--
generic of_nat and of_int functions, and generalization of iszero
and neg
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@10536
     6
Factor cancellation simprocs for the integers.
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@10536
    11
(** Factor cancellation theorems for "int" **)
paulson@10536
    12
paulson@11868
    13
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
wenzelm@13462
    14
by (stac zdiv_zmult_zmult1 1);
wenzelm@13462
    15
by Auto_tac;
paulson@10536
    16
qed "int_mult_div_cancel1";
paulson@10536
    17
paulson@10703
    18
(*For ExtractCommonTermFun, cancelling common factors*)
paulson@11868
    19
Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
wenzelm@13462
    20
by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
paulson@10703
    21
qed "int_mult_div_cancel_disj";
paulson@10703
    22
paulson@14378
    23
paulson@10536
    24
local
paulson@10536
    25
  open Int_Numeral_Simprocs
paulson@10536
    26
in
paulson@10536
    27
paulson@10536
    28
structure CancelNumeralFactorCommon =
paulson@10536
    29
  struct
wenzelm@13462
    30
  val mk_coeff          = mk_coeff
wenzelm@13462
    31
  val dest_coeff        = dest_coeff 1
paulson@10536
    32
  val trans_tac         = trans_tac
wenzelm@13462
    33
  val norm_tac =
paulson@12018
    34
     ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
paulson@10713
    35
     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
paulson@14113
    36
     THEN ALLGOALS (simp_tac (HOL_ss addsimps zmult_ac))
wenzelm@13462
    37
  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
paulson@10536
    38
  val simplify_meta_eq  = simplify_meta_eq mult_1s
paulson@10536
    39
  end
paulson@10536
    40
paulson@10536
    41
structure DivCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    42
 (open CancelNumeralFactorCommon
wenzelm@13485
    43
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
    44
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
paulson@10536
    45
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
paulson@10536
    46
  val cancel = int_mult_div_cancel1 RS trans
paulson@10536
    47
  val neg_exchanges = false
paulson@10536
    48
)
paulson@10536
    49
paulson@10536
    50
structure EqCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    51
 (open CancelNumeralFactorCommon
wenzelm@13485
    52
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
    53
  val mk_bal   = HOLogic.mk_eq
paulson@10536
    54
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
paulson@14378
    55
  val cancel = mult_cancel_left RS trans
paulson@10536
    56
  val neg_exchanges = false
paulson@10536
    57
)
paulson@10536
    58
paulson@10536
    59
structure LessCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    60
 (open CancelNumeralFactorCommon
wenzelm@13485
    61
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
    62
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@10536
    63
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
paulson@14378
    64
  val cancel = mult_less_cancel_left RS trans
paulson@10536
    65
  val neg_exchanges = true
paulson@10536
    66
)
paulson@10536
    67
paulson@10536
    68
structure LeCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    69
 (open CancelNumeralFactorCommon
wenzelm@13485
    70
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
    71
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@10536
    72
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
paulson@14378
    73
  val cancel = mult_le_cancel_left RS trans
paulson@10536
    74
  val neg_exchanges = true
paulson@10536
    75
)
paulson@10536
    76
wenzelm@13462
    77
val int_cancel_numeral_factors =
paulson@11868
    78
  map Bin_Simprocs.prep_simproc
wenzelm@13462
    79
   [("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"],
paulson@10536
    80
     EqCancelNumeralFactor.proc),
wenzelm@13462
    81
    ("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"],
paulson@10536
    82
     LessCancelNumeralFactor.proc),
wenzelm@13462
    83
    ("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"],
paulson@10536
    84
     LeCancelNumeralFactor.proc),
wenzelm@13462
    85
    ("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"],
paulson@10536
    86
     DivCancelNumeralFactor.proc)];
paulson@10536
    87
paulson@10536
    88
end;
paulson@10536
    89
paulson@10536
    90
Addsimprocs int_cancel_numeral_factors;
paulson@10536
    91
paulson@10536
    92
paulson@10536
    93
(*examples:
paulson@10536
    94
print_depth 22;
paulson@10536
    95
set timing;
paulson@10536
    96
set trace_simp;
wenzelm@13462
    97
fun test s = (Goal s; by (Simp_tac 1));
paulson@10536
    98
wenzelm@11704
    99
test "9*x = 12 * (y::int)";
wenzelm@11704
   100
test "(9*x) div (12 * (y::int)) = z";
wenzelm@11704
   101
test "9*x < 12 * (y::int)";
wenzelm@11704
   102
test "9*x <= 12 * (y::int)";
paulson@10536
   103
wenzelm@11704
   104
test "-99*x = 132 * (y::int)";
wenzelm@11704
   105
test "(-99*x) div (132 * (y::int)) = z";
wenzelm@11704
   106
test "-99*x < 132 * (y::int)";
wenzelm@11704
   107
test "-99*x <= 132 * (y::int)";
paulson@10536
   108
wenzelm@11704
   109
test "999*x = -396 * (y::int)";
wenzelm@11704
   110
test "(999*x) div (-396 * (y::int)) = z";
wenzelm@11704
   111
test "999*x < -396 * (y::int)";
wenzelm@11704
   112
test "999*x <= -396 * (y::int)";
paulson@10536
   113
wenzelm@11704
   114
test "-99*x = -81 * (y::int)";
wenzelm@11704
   115
test "(-99*x) div (-81 * (y::int)) = z";
wenzelm@11704
   116
test "-99*x <= -81 * (y::int)";
wenzelm@11704
   117
test "-99*x < -81 * (y::int)";
paulson@10536
   118
wenzelm@11704
   119
test "-2 * x = -1 * (y::int)";
wenzelm@11704
   120
test "-2 * x = -(y::int)";
wenzelm@11704
   121
test "(-2 * x) div (-1 * (y::int)) = z";
wenzelm@11704
   122
test "-2 * x < -(y::int)";
wenzelm@11704
   123
test "-2 * x <= -1 * (y::int)";
wenzelm@11704
   124
test "-x < -23 * (y::int)";
wenzelm@11704
   125
test "-x <= -23 * (y::int)";
paulson@10536
   126
*)
paulson@10536
   127
paulson@10703
   128
paulson@10703
   129
(** Declarations for ExtractCommonTerm **)
paulson@10703
   130
paulson@10703
   131
local
paulson@10703
   132
  open Int_Numeral_Simprocs
paulson@10703
   133
in
paulson@10703
   134
paulson@10703
   135
paulson@10703
   136
(*this version ALWAYS includes a trailing one*)
paulson@10703
   137
fun long_mk_prod []        = one
paulson@10703
   138
  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
paulson@10703
   139
paulson@10703
   140
(*Find first term that matches u*)
wenzelm@13462
   141
fun find_first past u []         = raise TERM("find_first", [])
paulson@10703
   142
  | find_first past u (t::terms) =
wenzelm@13462
   143
        if u aconv t then (rev past @ terms)
paulson@10703
   144
        else find_first (t::past) u terms
wenzelm@13462
   145
        handle TERM _ => find_first (t::past) u terms;
paulson@10703
   146
paulson@10703
   147
(*Final simplification: cancel + and *  *)
wenzelm@13462
   148
fun cancel_simplify_meta_eq cancel_th th =
wenzelm@13462
   149
    Int_Numeral_Simprocs.simplify_meta_eq
wenzelm@13462
   150
        [zmult_1, zmult_1_right]
paulson@10703
   151
        (([th, cancel_th]) MRS trans);
paulson@10703
   152
paulson@10703
   153
structure CancelFactorCommon =
paulson@10703
   154
  struct
wenzelm@13462
   155
  val mk_sum            = long_mk_prod
wenzelm@13462
   156
  val dest_sum          = dest_prod
wenzelm@13462
   157
  val mk_coeff          = mk_coeff
wenzelm@13462
   158
  val dest_coeff        = dest_coeff
wenzelm@13462
   159
  val find_first        = find_first []
paulson@10703
   160
  val trans_tac         = trans_tac
paulson@10703
   161
  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))
paulson@10703
   162
  end;
paulson@10703
   163
paulson@10703
   164
structure EqCancelFactor = ExtractCommonTermFun
paulson@10703
   165
 (open CancelFactorCommon
wenzelm@13485
   166
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10703
   167
  val mk_bal   = HOLogic.mk_eq
paulson@10703
   168
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
paulson@14378
   169
  val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
paulson@10703
   170
);
paulson@10703
   171
paulson@10703
   172
structure DivideCancelFactor = ExtractCommonTermFun
paulson@10703
   173
 (open CancelFactorCommon
wenzelm@13485
   174
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10703
   175
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
paulson@10703
   176
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
paulson@10703
   177
  val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
paulson@10703
   178
);
paulson@10703
   179
wenzelm@13462
   180
val int_cancel_factor =
paulson@11868
   181
  map Bin_Simprocs.prep_simproc
wenzelm@13462
   182
   [("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc),
wenzelm@13462
   183
    ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"],
paulson@10703
   184
     DivideCancelFactor.proc)];
paulson@10703
   185
paulson@10703
   186
end;
paulson@10703
   187
paulson@10703
   188
Addsimprocs int_cancel_factor;
paulson@10703
   189
paulson@10703
   190
paulson@10703
   191
(*examples:
paulson@10703
   192
print_depth 22;
paulson@10703
   193
set timing;
paulson@10703
   194
set trace_simp;
wenzelm@13462
   195
fun test s = (Goal s; by (Asm_simp_tac 1));
paulson@10703
   196
paulson@10703
   197
test "x*k = k*(y::int)";
wenzelm@13462
   198
test "k = k*(y::int)";
paulson@10703
   199
test "a*(b*c) = (b::int)";
paulson@10703
   200
test "a*(b*c) = d*(b::int)*(x*a)";
paulson@10703
   201
paulson@10703
   202
test "(x*k) div (k*(y::int)) = (uu::int)";
wenzelm@13462
   203
test "(k) div (k*(y::int)) = (uu::int)";
paulson@10703
   204
test "(a*(b*c)) div ((b::int)) = (uu::int)";
paulson@10703
   205
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
paulson@10703
   206
*)
paulson@10703
   207