src/HOL/Integ/int_factor_simprocs.ML
author paulson
Wed Nov 29 10:21:43 2000 +0100 (2000-11-29)
changeset 10536 8f34ecae1446
child 10703 ba98f00cec4f
permissions -rw-r--r--
invoking CancelNumeralFactorFun
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@10536
     8
This file can't be combined with int_arith1,2 because it requires IntDiv.thy.
paulson@10536
     9
*)
paulson@10536
    10
paulson@10536
    11
(** Factor cancellation theorems for "int" **)
paulson@10536
    12
paulson@10536
    13
Goal "!!k::int. (k*m <= k*n) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))";
paulson@10536
    14
by (stac zmult_zle_cancel1 1);
paulson@10536
    15
by Auto_tac;  
paulson@10536
    16
qed "int_mult_le_cancel1";
paulson@10536
    17
paulson@10536
    18
Goal "!!k::int. (k*m < k*n) = ((#0 < k & m<n) | (k < #0 & n<m))";
paulson@10536
    19
by (stac zmult_zless_cancel1 1);
paulson@10536
    20
by Auto_tac;  
paulson@10536
    21
qed "int_mult_less_cancel1";
paulson@10536
    22
paulson@10536
    23
Goal "!!k::int. (k*m = k*n) = (k = #0 | m=n)";
paulson@10536
    24
by Auto_tac;  
paulson@10536
    25
qed "int_mult_eq_cancel1";
paulson@10536
    26
paulson@10536
    27
Goal "!!k::int. k~=#0 ==> (k*m) div (k*n) = (m div n)";
paulson@10536
    28
by (stac zdiv_zmult_zmult1 1); 
paulson@10536
    29
by Auto_tac;  
paulson@10536
    30
qed "int_mult_div_cancel1";
paulson@10536
    31
paulson@10536
    32
local
paulson@10536
    33
  open Int_Numeral_Simprocs
paulson@10536
    34
in
paulson@10536
    35
paulson@10536
    36
structure CancelNumeralFactorCommon =
paulson@10536
    37
  struct
paulson@10536
    38
  val mk_coeff		= mk_coeff
paulson@10536
    39
  val dest_coeff	= dest_coeff 1
paulson@10536
    40
  val trans_tac         = trans_tac
paulson@10536
    41
  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
paulson@10536
    42
                 THEN ALLGOALS
paulson@10536
    43
                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
paulson@10536
    44
                                               bin_simps@zmult_ac))
paulson@10536
    45
  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
paulson@10536
    46
  val simplify_meta_eq  = simplify_meta_eq mult_1s
paulson@10536
    47
  end
paulson@10536
    48
paulson@10536
    49
structure DivCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    50
 (open CancelNumeralFactorCommon
paulson@10536
    51
  val prove_conv = prove_conv "intdiv_cancel_numeral_factor"
paulson@10536
    52
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
paulson@10536
    53
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
paulson@10536
    54
  val cancel = int_mult_div_cancel1 RS trans
paulson@10536
    55
  val neg_exchanges = false
paulson@10536
    56
)
paulson@10536
    57
paulson@10536
    58
structure EqCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    59
 (open CancelNumeralFactorCommon
paulson@10536
    60
  val prove_conv = prove_conv "inteq_cancel_numeral_factor"
paulson@10536
    61
  val mk_bal   = HOLogic.mk_eq
paulson@10536
    62
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
paulson@10536
    63
  val cancel = int_mult_eq_cancel1 RS trans
paulson@10536
    64
  val neg_exchanges = false
paulson@10536
    65
)
paulson@10536
    66
paulson@10536
    67
structure LessCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    68
 (open CancelNumeralFactorCommon
paulson@10536
    69
  val prove_conv = prove_conv "intless_cancel_numeral_factor"
paulson@10536
    70
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@10536
    71
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
paulson@10536
    72
  val cancel = int_mult_less_cancel1 RS trans
paulson@10536
    73
  val neg_exchanges = true
paulson@10536
    74
)
paulson@10536
    75
paulson@10536
    76
structure LeCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
    77
 (open CancelNumeralFactorCommon
paulson@10536
    78
  val prove_conv = prove_conv "intle_cancel_numeral_factor"
paulson@10536
    79
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@10536
    80
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
paulson@10536
    81
  val cancel = int_mult_le_cancel1 RS trans
paulson@10536
    82
  val neg_exchanges = true
paulson@10536
    83
)
paulson@10536
    84
paulson@10536
    85
val int_cancel_numeral_factors = 
paulson@10536
    86
  map prep_simproc
paulson@10536
    87
   [("inteq_cancel_numeral_factors",
paulson@10536
    88
     prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
paulson@10536
    89
     EqCancelNumeralFactor.proc),
paulson@10536
    90
    ("intless_cancel_numeral_factors", 
paulson@10536
    91
     prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
paulson@10536
    92
     LessCancelNumeralFactor.proc),
paulson@10536
    93
    ("intle_cancel_numeral_factors", 
paulson@10536
    94
     prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
paulson@10536
    95
     LeCancelNumeralFactor.proc),
paulson@10536
    96
    ("intdiv_cancel_numeral_factors", 
paulson@10536
    97
     prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
paulson@10536
    98
     DivCancelNumeralFactor.proc)];
paulson@10536
    99
paulson@10536
   100
end;
paulson@10536
   101
paulson@10536
   102
Addsimprocs int_cancel_numeral_factors;
paulson@10536
   103
paulson@10536
   104
paulson@10536
   105
(*examples:
paulson@10536
   106
print_depth 22;
paulson@10536
   107
set timing;
paulson@10536
   108
set trace_simp;
paulson@10536
   109
fun test s = (Goal s; by (Simp_tac 1)); 
paulson@10536
   110
paulson@10536
   111
test "#9*x = #12 * (y::int)";
paulson@10536
   112
test "(#9*x) div (#12 * (y::int)) = z";
paulson@10536
   113
test "#9*x < #12 * (y::int)";
paulson@10536
   114
test "#9*x <= #12 * (y::int)";
paulson@10536
   115
paulson@10536
   116
test "#-99*x = #132 * (y::int)";
paulson@10536
   117
test "(#-99*x) div (#132 * (y::int)) = z";
paulson@10536
   118
test "#-99*x < #132 * (y::int)";
paulson@10536
   119
test "#-99*x <= #132 * (y::int)";
paulson@10536
   120
paulson@10536
   121
test "#999*x = #-396 * (y::int)";
paulson@10536
   122
test "(#999*x) div (#-396 * (y::int)) = z";
paulson@10536
   123
test "#999*x < #-396 * (y::int)";
paulson@10536
   124
test "#999*x <= #-396 * (y::int)";
paulson@10536
   125
paulson@10536
   126
test "#-99*x = #-81 * (y::int)";
paulson@10536
   127
test "(#-99*x) div (#-81 * (y::int)) = z";
paulson@10536
   128
test "#-99*x <= #-81 * (y::int)";
paulson@10536
   129
test "#-99*x < #-81 * (y::int)";
paulson@10536
   130
paulson@10536
   131
test "#-2 * x = #-1 * (y::int)";
paulson@10536
   132
test "#-2 * x = -(y::int)";
paulson@10536
   133
test "(#-2 * x) div (#-1 * (y::int)) = z";
paulson@10536
   134
test "#-2 * x < -(y::int)";
paulson@10536
   135
test "#-2 * x <= #-1 * (y::int)";
paulson@10536
   136
test "-x < #-23 * (y::int)";
paulson@10536
   137
test "-x <= #-23 * (y::int)";
paulson@10536
   138
*)
paulson@10536
   139