src/HOL/Integ/int_factor_simprocs.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15271 3c32a26510c4
child 16973 b2a894562b8f
permissions -rw-r--r--
Constant "If" is now local
     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 (and for fields).
     7 
     8 This file can't be combined with int_arith1 because it requires IntDiv.thy.
     9 *)
    10 
    11 
    12 (*To quote from Provers/Arith/cancel_numeral_factor.ML:
    13 
    14 Cancels common coefficients in balanced expressions:
    15 
    16      u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
    17 
    18 where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
    19 and d = gcd(m,m') and n=m/d and n'=m'/d.
    20 *)
    21 
    22 val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq];
    23 
    24 (** Factor cancellation theorems for integer division (div, not /) **)
    25 
    26 Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
    27 by (stac zdiv_zmult_zmult1 1);
    28 by Auto_tac;
    29 qed "int_mult_div_cancel1";
    30 
    31 (*For ExtractCommonTermFun, cancelling common factors*)
    32 Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
    33 by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
    34 qed "int_mult_div_cancel_disj";
    35 
    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 minus_from_mult_simps @ mult_1s))
    48      THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
    49      THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
    50   val numeral_simp_tac  =
    51          ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
    52   val simplify_meta_eq  = 
    53 	Int_Numeral_Simprocs.simplify_meta_eq
    54 	     [add_0, add_0_right,
    55 	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
    56   end
    57 
    58 (*Version for integer division*)
    59 structure DivCancelNumeralFactor = CancelNumeralFactorFun
    60  (open CancelNumeralFactorCommon
    61   val prove_conv = Bin_Simprocs.prove_conv
    62   val mk_bal   = HOLogic.mk_binop "Divides.op div"
    63   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    64   val cancel = int_mult_div_cancel1 RS trans
    65   val neg_exchanges = false
    66 )
    67 
    68 (*Version for fields*)
    69 structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
    70  (open CancelNumeralFactorCommon
    71   val prove_conv = Bin_Simprocs.prove_conv
    72   val mk_bal   = HOLogic.mk_binop "HOL.divide"
    73   val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
    74   val cancel = mult_divide_cancel_left RS trans
    75   val neg_exchanges = false
    76 )
    77 
    78 (*Version for ordered rings: mult_cancel_left requires an ordering*)
    79 structure EqCancelNumeralFactor = CancelNumeralFactorFun
    80  (open CancelNumeralFactorCommon
    81   val prove_conv = Bin_Simprocs.prove_conv
    82   val mk_bal   = HOLogic.mk_eq
    83   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    84   val cancel = mult_cancel_left RS trans
    85   val neg_exchanges = false
    86 )
    87 
    88 (*Version for (unordered) fields*)
    89 structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
    90  (open CancelNumeralFactorCommon
    91   val prove_conv = Bin_Simprocs.prove_conv
    92   val mk_bal   = HOLogic.mk_eq
    93   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    94   val cancel = field_mult_cancel_left RS trans
    95   val neg_exchanges = false
    96 )
    97 
    98 structure LessCancelNumeralFactor = CancelNumeralFactorFun
    99  (open CancelNumeralFactorCommon
   100   val prove_conv = Bin_Simprocs.prove_conv
   101   val mk_bal   = HOLogic.mk_binrel "op <"
   102   val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
   103   val cancel = mult_less_cancel_left RS trans
   104   val neg_exchanges = true
   105 )
   106 
   107 structure LeCancelNumeralFactor = CancelNumeralFactorFun
   108  (open CancelNumeralFactorCommon
   109   val prove_conv = Bin_Simprocs.prove_conv
   110   val mk_bal   = HOLogic.mk_binrel "op <="
   111   val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
   112   val cancel = mult_le_cancel_left RS trans
   113   val neg_exchanges = true
   114 )
   115 
   116 val ring_cancel_numeral_factors =
   117   map Bin_Simprocs.prep_simproc
   118    [("ring_eq_cancel_numeral_factor",
   119      ["(l::'a::{ordered_idom,number_ring}) * m = n",
   120       "(l::'a::{ordered_idom,number_ring}) = m * n"],
   121      EqCancelNumeralFactor.proc),
   122     ("ring_less_cancel_numeral_factor",
   123      ["(l::'a::{ordered_idom,number_ring}) * m < n",
   124       "(l::'a::{ordered_idom,number_ring}) < m * n"],
   125      LessCancelNumeralFactor.proc),
   126     ("ring_le_cancel_numeral_factor",
   127      ["(l::'a::{ordered_idom,number_ring}) * m <= n",
   128       "(l::'a::{ordered_idom,number_ring}) <= m * n"],
   129      LeCancelNumeralFactor.proc),
   130     ("int_div_cancel_numeral_factors",
   131      ["((l::int) * m) div n", "(l::int) div (m * n)"],
   132      DivCancelNumeralFactor.proc)];
   133 
   134 
   135 val field_cancel_numeral_factors =
   136   map Bin_Simprocs.prep_simproc
   137    [("field_eq_cancel_numeral_factor",
   138      ["(l::'a::{field,number_ring}) * m = n",
   139       "(l::'a::{field,number_ring}) = m * n"],
   140      FieldEqCancelNumeralFactor.proc),
   141     ("field_cancel_numeral_factor",
   142      ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   143       "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   144       "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   145      FieldDivCancelNumeralFactor.proc)]
   146 
   147 end;
   148 
   149 Addsimprocs ring_cancel_numeral_factors;
   150 Addsimprocs field_cancel_numeral_factors;
   151 
   152 (*examples:
   153 print_depth 22;
   154 set timing;
   155 set trace_simp;
   156 fun test s = (Goal s; by (Simp_tac 1));
   157 
   158 test "9*x = 12 * (y::int)";
   159 test "(9*x) div (12 * (y::int)) = z";
   160 test "9*x < 12 * (y::int)";
   161 test "9*x <= 12 * (y::int)";
   162 
   163 test "-99*x = 132 * (y::int)";
   164 test "(-99*x) div (132 * (y::int)) = z";
   165 test "-99*x < 132 * (y::int)";
   166 test "-99*x <= 132 * (y::int)";
   167 
   168 test "999*x = -396 * (y::int)";
   169 test "(999*x) div (-396 * (y::int)) = z";
   170 test "999*x < -396 * (y::int)";
   171 test "999*x <= -396 * (y::int)";
   172 
   173 test "-99*x = -81 * (y::int)";
   174 test "(-99*x) div (-81 * (y::int)) = z";
   175 test "-99*x <= -81 * (y::int)";
   176 test "-99*x < -81 * (y::int)";
   177 
   178 test "-2 * x = -1 * (y::int)";
   179 test "-2 * x = -(y::int)";
   180 test "(-2 * x) div (-1 * (y::int)) = z";
   181 test "-2 * x < -(y::int)";
   182 test "-2 * x <= -1 * (y::int)";
   183 test "-x < -23 * (y::int)";
   184 test "-x <= -23 * (y::int)";
   185 *)
   186 
   187 (*And the same examples for fields such as rat or real:
   188 test "0 <= (y::rat) * -2";
   189 test "9*x = 12 * (y::rat)";
   190 test "(9*x) / (12 * (y::rat)) = z";
   191 test "9*x < 12 * (y::rat)";
   192 test "9*x <= 12 * (y::rat)";
   193 
   194 test "-99*x = 132 * (y::rat)";
   195 test "(-99*x) / (132 * (y::rat)) = z";
   196 test "-99*x < 132 * (y::rat)";
   197 test "-99*x <= 132 * (y::rat)";
   198 
   199 test "999*x = -396 * (y::rat)";
   200 test "(999*x) / (-396 * (y::rat)) = z";
   201 test "999*x < -396 * (y::rat)";
   202 test "999*x <= -396 * (y::rat)";
   203 
   204 test  "(- ((2::rat) * x) <= 2 * y)";
   205 test "-99*x = -81 * (y::rat)";
   206 test "(-99*x) / (-81 * (y::rat)) = z";
   207 test "-99*x <= -81 * (y::rat)";
   208 test "-99*x < -81 * (y::rat)";
   209 
   210 test "-2 * x = -1 * (y::rat)";
   211 test "-2 * x = -(y::rat)";
   212 test "(-2 * x) / (-1 * (y::rat)) = z";
   213 test "-2 * x < -(y::rat)";
   214 test "-2 * x <= -1 * (y::rat)";
   215 test "-x < -23 * (y::rat)";
   216 test "-x <= -23 * (y::rat)";
   217 *)
   218 
   219 
   220 (** Declarations for ExtractCommonTerm **)
   221 
   222 local
   223   open Int_Numeral_Simprocs
   224 in
   225 
   226 (*Find first term that matches u*)
   227 fun find_first past u []         = raise TERM("find_first", [])
   228   | find_first past u (t::terms) =
   229         if u aconv t then (rev past @ terms)
   230         else find_first (t::past) u terms
   231         handle TERM _ => find_first (t::past) u terms;
   232 
   233 (** Final simplification for the CancelFactor simprocs **)
   234 val simplify_one = 
   235     Int_Numeral_Simprocs.simplify_meta_eq  
   236        [mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
   237 
   238 fun cancel_simplify_meta_eq cancel_th th =
   239     simplify_one (([th, cancel_th]) MRS trans);
   240 
   241 (*At present, long_mk_prod creates Numeral1, so this requires the axclass
   242   number_ring*)
   243 structure CancelFactorCommon =
   244   struct
   245   val mk_sum            = long_mk_prod
   246   val dest_sum          = dest_prod
   247   val mk_coeff          = mk_coeff
   248   val dest_coeff        = dest_coeff
   249   val find_first        = find_first []
   250   val trans_tac         = trans_tac
   251   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
   252   end;
   253 
   254 (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
   255   rat_arith.ML works for all fields.*)
   256 structure EqCancelFactor = ExtractCommonTermFun
   257  (open CancelFactorCommon
   258   val prove_conv = Bin_Simprocs.prove_conv
   259   val mk_bal   = HOLogic.mk_eq
   260   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   261   val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
   262 );
   263 
   264 (*int_mult_div_cancel_disj is for integer division (div). The version in
   265   rat_arith.ML works for all fields, using real division (/).*)
   266 structure DivideCancelFactor = ExtractCommonTermFun
   267  (open CancelFactorCommon
   268   val prove_conv = Bin_Simprocs.prove_conv
   269   val mk_bal   = HOLogic.mk_binop "Divides.op div"
   270   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
   271   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
   272 );
   273 
   274 val int_cancel_factor =
   275   map Bin_Simprocs.prep_simproc
   276    [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
   277     EqCancelFactor.proc),
   278     ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
   279      DivideCancelFactor.proc)];
   280 
   281 (** Versions for all fields, including unordered ones (type complex).*)
   282 
   283 structure FieldEqCancelFactor = ExtractCommonTermFun
   284  (open CancelFactorCommon
   285   val prove_conv = Bin_Simprocs.prove_conv
   286   val mk_bal   = HOLogic.mk_eq
   287   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   288   val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
   289 );
   290 
   291 structure FieldDivideCancelFactor = ExtractCommonTermFun
   292  (open CancelFactorCommon
   293   val prove_conv = Bin_Simprocs.prove_conv
   294   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   295   val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   296   val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
   297 );
   298 
   299 (*The number_ring class is necessary because the simprocs refer to the
   300   binary number 1.  FIXME: probably they could use 1 instead.*)
   301 val field_cancel_factor =
   302   map Bin_Simprocs.prep_simproc
   303    [("field_eq_cancel_factor",
   304      ["(l::'a::{field,number_ring}) * m = n",
   305       "(l::'a::{field,number_ring}) = m * n"],
   306      FieldEqCancelFactor.proc),
   307     ("field_divide_cancel_factor",
   308      ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   309       "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
   310      FieldDivideCancelFactor.proc)];
   311 
   312 end;
   313 
   314 Addsimprocs int_cancel_factor;
   315 Addsimprocs field_cancel_factor;
   316 
   317 
   318 (*examples:
   319 print_depth 22;
   320 set timing;
   321 set trace_simp;
   322 fun test s = (Goal s; by (Asm_simp_tac 1));
   323 
   324 test "x*k = k*(y::int)";
   325 test "k = k*(y::int)";
   326 test "a*(b*c) = (b::int)";
   327 test "a*(b*c) = d*(b::int)*(x*a)";
   328 
   329 test "(x*k) div (k*(y::int)) = (uu::int)";
   330 test "(k) div (k*(y::int)) = (uu::int)";
   331 test "(a*(b*c)) div ((b::int)) = (uu::int)";
   332 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   333 *)
   334 
   335 (*And the same examples for fields such as rat or real:
   336 print_depth 22;
   337 set timing;
   338 set trace_simp;
   339 fun test s = (Goal s; by (Asm_simp_tac 1));
   340 
   341 test "x*k = k*(y::rat)";
   342 test "k = k*(y::rat)";
   343 test "a*(b*c) = (b::rat)";
   344 test "a*(b*c) = d*(b::rat)*(x*a)";
   345 
   346 
   347 test "(x*k) / (k*(y::rat)) = (uu::rat)";
   348 test "(k) / (k*(y::rat)) = (uu::rat)";
   349 test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   350 test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   351 
   352 (*FIXME: what do we do about this?*)
   353 test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   354 *)