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