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