src/HOL/Integ/int_factor_simprocs.ML
author paulson
Tue Jul 15 15:20:54 2003 +0200 (2003-07-15)
changeset 14113 7b3513ba0f86
parent 13485 acf39e924091
child 14378 69c4d5997669
permissions -rw-r--r--
Fixing a simproc bug
     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 (simp_tac (HOL_ss addsimps zmult_ac))
    50   val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    51   val simplify_meta_eq  = simplify_meta_eq mult_1s
    52   end
    53 
    54 structure DivCancelNumeralFactor = CancelNumeralFactorFun
    55  (open CancelNumeralFactorCommon
    56   val prove_conv = Bin_Simprocs.prove_conv
    57   val mk_bal   = HOLogic.mk_binop "Divides.op div"
    58   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    59   val cancel = int_mult_div_cancel1 RS trans
    60   val neg_exchanges = false
    61 )
    62 
    63 structure EqCancelNumeralFactor = CancelNumeralFactorFun
    64  (open CancelNumeralFactorCommon
    65   val prove_conv = Bin_Simprocs.prove_conv
    66   val mk_bal   = HOLogic.mk_eq
    67   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    68   val cancel = int_mult_eq_cancel1 RS trans
    69   val neg_exchanges = false
    70 )
    71 
    72 structure LessCancelNumeralFactor = CancelNumeralFactorFun
    73  (open CancelNumeralFactorCommon
    74   val prove_conv = Bin_Simprocs.prove_conv
    75   val mk_bal   = HOLogic.mk_binrel "op <"
    76   val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    77   val cancel = int_mult_less_cancel1 RS trans
    78   val neg_exchanges = true
    79 )
    80 
    81 structure LeCancelNumeralFactor = CancelNumeralFactorFun
    82  (open CancelNumeralFactorCommon
    83   val prove_conv = Bin_Simprocs.prove_conv
    84   val mk_bal   = HOLogic.mk_binrel "op <="
    85   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    86   val cancel = int_mult_le_cancel1 RS trans
    87   val neg_exchanges = true
    88 )
    89 
    90 val int_cancel_numeral_factors =
    91   map Bin_Simprocs.prep_simproc
    92    [("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"],
    93      EqCancelNumeralFactor.proc),
    94     ("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"],
    95      LessCancelNumeralFactor.proc),
    96     ("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"],
    97      LeCancelNumeralFactor.proc),
    98     ("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"],
    99      DivCancelNumeralFactor.proc)];
   100 
   101 end;
   102 
   103 Addsimprocs int_cancel_numeral_factors;
   104 
   105 
   106 (*examples:
   107 print_depth 22;
   108 set timing;
   109 set trace_simp;
   110 fun test s = (Goal s; by (Simp_tac 1));
   111 
   112 test "9*x = 12 * (y::int)";
   113 test "(9*x) div (12 * (y::int)) = z";
   114 test "9*x < 12 * (y::int)";
   115 test "9*x <= 12 * (y::int)";
   116 
   117 test "-99*x = 132 * (y::int)";
   118 test "(-99*x) div (132 * (y::int)) = z";
   119 test "-99*x < 132 * (y::int)";
   120 test "-99*x <= 132 * (y::int)";
   121 
   122 test "999*x = -396 * (y::int)";
   123 test "(999*x) div (-396 * (y::int)) = z";
   124 test "999*x < -396 * (y::int)";
   125 test "999*x <= -396 * (y::int)";
   126 
   127 test "-99*x = -81 * (y::int)";
   128 test "(-99*x) div (-81 * (y::int)) = z";
   129 test "-99*x <= -81 * (y::int)";
   130 test "-99*x < -81 * (y::int)";
   131 
   132 test "-2 * x = -1 * (y::int)";
   133 test "-2 * x = -(y::int)";
   134 test "(-2 * x) div (-1 * (y::int)) = z";
   135 test "-2 * x < -(y::int)";
   136 test "-2 * x <= -1 * (y::int)";
   137 test "-x < -23 * (y::int)";
   138 test "-x <= -23 * (y::int)";
   139 *)
   140 
   141 
   142 (** Declarations for ExtractCommonTerm **)
   143 
   144 local
   145   open Int_Numeral_Simprocs
   146 in
   147 
   148 
   149 (*this version ALWAYS includes a trailing one*)
   150 fun long_mk_prod []        = one
   151   | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
   152 
   153 (*Find first term that matches u*)
   154 fun find_first past u []         = raise TERM("find_first", [])
   155   | find_first past u (t::terms) =
   156         if u aconv t then (rev past @ terms)
   157         else find_first (t::past) u terms
   158         handle TERM _ => find_first (t::past) u terms;
   159 
   160 (*Final simplification: cancel + and *  *)
   161 fun cancel_simplify_meta_eq cancel_th th =
   162     Int_Numeral_Simprocs.simplify_meta_eq
   163         [zmult_1, zmult_1_right]
   164         (([th, cancel_th]) MRS trans);
   165 
   166 structure CancelFactorCommon =
   167   struct
   168   val mk_sum            = long_mk_prod
   169   val dest_sum          = dest_prod
   170   val mk_coeff          = mk_coeff
   171   val dest_coeff        = dest_coeff
   172   val find_first        = find_first []
   173   val trans_tac         = trans_tac
   174   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))
   175   end;
   176 
   177 structure EqCancelFactor = ExtractCommonTermFun
   178  (open CancelFactorCommon
   179   val prove_conv = Bin_Simprocs.prove_conv
   180   val mk_bal   = HOLogic.mk_eq
   181   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   182   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1
   183 );
   184 
   185 structure DivideCancelFactor = ExtractCommonTermFun
   186  (open CancelFactorCommon
   187   val prove_conv = Bin_Simprocs.prove_conv
   188   val mk_bal   = HOLogic.mk_binop "Divides.op div"
   189   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
   190   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
   191 );
   192 
   193 val int_cancel_factor =
   194   map Bin_Simprocs.prep_simproc
   195    [("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc),
   196     ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"],
   197      DivideCancelFactor.proc)];
   198 
   199 end;
   200 
   201 Addsimprocs int_cancel_factor;
   202 
   203 
   204 (*examples:
   205 print_depth 22;
   206 set timing;
   207 set trace_simp;
   208 fun test s = (Goal s; by (Asm_simp_tac 1));
   209 
   210 test "x*k = k*(y::int)";
   211 test "k = k*(y::int)";
   212 test "a*(b*c) = (b::int)";
   213 test "a*(b*c) = d*(b::int)*(x*a)";
   214 
   215 test "(x*k) div (k*(y::int)) = (uu::int)";
   216 test "(k) div (k*(y::int)) = (uu::int)";
   217 test "(a*(b*c)) div ((b::int)) = (uu::int)";
   218 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   219 *)
   220