src/HOL/Integ/int_factor_simprocs.ML
author paulson
Tue Feb 17 10:41:59 2004 +0100 (2004-02-17)
changeset 14390 55fe71faadda
parent 14387 e96d5c42c4b0
child 14426 de890c247b38
permissions -rw-r--r--
further tweaks to the numeric theories
     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_ring,number_ring}) * m = n",
   120       "(l::'a::{ordered_ring,number_ring}) = m * n"],
   121      EqCancelNumeralFactor.proc),
   122     ("ring_less_cancel_numeral_factor",
   123      ["(l::'a::{ordered_ring,number_ring}) * m < n",
   124       "(l::'a::{ordered_ring,number_ring}) < m * n"],
   125      LessCancelNumeralFactor.proc),
   126     ("ring_le_cancel_numeral_factor",
   127      ["(l::'a::{ordered_ring,number_ring}) * m <= n",
   128       "(l::'a::{ordered_ring,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::{field,number_ring}) * m) / n",
   143       "(l::'a::{field,number_ring}) / (m * n)",
   144       "((number_of v)::'a::{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: cancel + and *  *)
   234 fun cancel_simplify_meta_eq cancel_th th =
   235     Int_Numeral_Simprocs.simplify_meta_eq
   236         [mult_1, mult_1_right]
   237         (([th, cancel_th]) MRS trans);
   238 
   239 structure CancelFactorCommon =
   240   struct
   241   val mk_sum            = long_mk_prod
   242   val dest_sum          = dest_prod
   243   val mk_coeff          = mk_coeff
   244   val dest_coeff        = dest_coeff
   245   val find_first        = find_first []
   246   val trans_tac         = trans_tac
   247   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
   248   end;
   249 
   250 (*mult_cancel_left requires an ordered ring, such as int. The version in
   251   rat_arith.ML works for all fields.*)
   252 structure EqCancelFactor = ExtractCommonTermFun
   253  (open CancelFactorCommon
   254   val prove_conv = Bin_Simprocs.prove_conv
   255   val mk_bal   = HOLogic.mk_eq
   256   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   257   val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
   258 );
   259 
   260 (*int_mult_div_cancel_disj is for integer division (div). The version in
   261   rat_arith.ML works for all fields, using real division (/).*)
   262 structure DivideCancelFactor = ExtractCommonTermFun
   263  (open CancelFactorCommon
   264   val prove_conv = Bin_Simprocs.prove_conv
   265   val mk_bal   = HOLogic.mk_binop "Divides.op div"
   266   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
   267   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
   268 );
   269 
   270 val int_cancel_factor =
   271   map Bin_Simprocs.prep_simproc
   272    [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], 
   273     EqCancelFactor.proc),
   274     ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
   275      DivideCancelFactor.proc)];
   276 
   277 (** Versions for all fields, including unordered ones (type complex).*)
   278 
   279 structure FieldEqCancelFactor = ExtractCommonTermFun
   280  (open CancelFactorCommon
   281   val prove_conv = Bin_Simprocs.prove_conv
   282   val mk_bal   = HOLogic.mk_eq
   283   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   284   val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
   285 );
   286 
   287 structure FieldDivideCancelFactor = ExtractCommonTermFun
   288  (open CancelFactorCommon
   289   val prove_conv = Bin_Simprocs.prove_conv
   290   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   291   val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   292   val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
   293 );
   294 
   295 val field_cancel_factor =
   296   map Bin_Simprocs.prep_simproc
   297    [("field_eq_cancel_factor",
   298      ["(l::'a::field) * m = n", "(l::'a::field) = m * n"], 
   299      FieldEqCancelFactor.proc),
   300     ("field_divide_cancel_factor",
   301      ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
   302      FieldDivideCancelFactor.proc)];
   303 
   304 end;
   305 
   306 Addsimprocs int_cancel_factor;
   307 Addsimprocs field_cancel_factor;
   308 
   309 
   310 (*examples:
   311 print_depth 22;
   312 set timing;
   313 set trace_simp;
   314 fun test s = (Goal s; by (Asm_simp_tac 1));
   315 
   316 test "x*k = k*(y::int)";
   317 test "k = k*(y::int)";
   318 test "a*(b*c) = (b::int)";
   319 test "a*(b*c) = d*(b::int)*(x*a)";
   320 
   321 test "(x*k) div (k*(y::int)) = (uu::int)";
   322 test "(k) div (k*(y::int)) = (uu::int)";
   323 test "(a*(b*c)) div ((b::int)) = (uu::int)";
   324 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   325 *)
   326 
   327 (*And the same examples for fields such as rat or real:
   328 print_depth 22;
   329 set timing;
   330 set trace_simp;
   331 fun test s = (Goal s; by (Asm_simp_tac 1));
   332 
   333 test "x*k = k*(y::rat)";
   334 test "k = k*(y::rat)";
   335 test "a*(b*c) = (b::rat)";
   336 test "a*(b*c) = d*(b::rat)*(x*a)";
   337 
   338 
   339 test "(x*k) / (k*(y::rat)) = (uu::rat)";
   340 test "(k) / (k*(y::rat)) = (uu::rat)";
   341 test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   342 test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   343 
   344 (*FIXME: what do we do about this?*)
   345 test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   346 *)