src/HOL/Tools/int_factor_simprocs.ML
author nipkow
Sun Mar 22 19:36:04 2009 +0100 (2009-03-22)
changeset 30649 57753e0ec1d4
parent 30518 07b45c1aa788
child 30685 dd5fe091ff04
permissions -rw-r--r--
1. New cancellation simprocs for common factors in inequations
2. Updated the documentation
     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 = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}];
    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         = K Arith_Data.trans_tac
    33 
    34   val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
    35   val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
    36   val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
    37   fun norm_tac ss =
    38     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    39     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    40     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
    41 
    42   val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
    43   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    44   val simplify_meta_eq = Arith_Data.simplify_meta_eq
    45     [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
    46       @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
    47   end
    48 
    49 (*Version for integer division*)
    50 structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
    51  (open CancelNumeralFactorCommon
    52   val prove_conv = Arith_Data.prove_conv
    53   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
    54   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
    55   val cancel = @{thm zdiv_zmult_zmult1} RS trans
    56   val neg_exchanges = false
    57 )
    58 
    59 (*Version for fields*)
    60 structure DivideCancelNumeralFactor = CancelNumeralFactorFun
    61  (open CancelNumeralFactorCommon
    62   val prove_conv = Arith_Data.prove_conv
    63   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
    64   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
    65   val cancel = @{thm mult_divide_mult_cancel_left} RS trans
    66   val neg_exchanges = false
    67 )
    68 
    69 structure EqCancelNumeralFactor = CancelNumeralFactorFun
    70  (open CancelNumeralFactorCommon
    71   val prove_conv = Arith_Data.prove_conv
    72   val mk_bal   = HOLogic.mk_eq
    73   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    74   val cancel = @{thm mult_cancel_left} RS trans
    75   val neg_exchanges = false
    76 )
    77 
    78 structure LessCancelNumeralFactor = CancelNumeralFactorFun
    79  (open CancelNumeralFactorCommon
    80   val prove_conv = Arith_Data.prove_conv
    81   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
    82   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
    83   val cancel = @{thm mult_less_cancel_left} RS trans
    84   val neg_exchanges = true
    85 )
    86 
    87 structure LeCancelNumeralFactor = CancelNumeralFactorFun
    88  (open CancelNumeralFactorCommon
    89   val prove_conv = Arith_Data.prove_conv
    90   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
    91   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
    92   val cancel = @{thm mult_le_cancel_left} RS trans
    93   val neg_exchanges = true
    94 )
    95 
    96 val cancel_numeral_factors =
    97   map Arith_Data.prep_simproc
    98    [("ring_eq_cancel_numeral_factor",
    99      ["(l::'a::{idom,number_ring}) * m = n",
   100       "(l::'a::{idom,number_ring}) = m * n"],
   101      K EqCancelNumeralFactor.proc),
   102     ("ring_less_cancel_numeral_factor",
   103      ["(l::'a::{ordered_idom,number_ring}) * m < n",
   104       "(l::'a::{ordered_idom,number_ring}) < m * n"],
   105      K LessCancelNumeralFactor.proc),
   106     ("ring_le_cancel_numeral_factor",
   107      ["(l::'a::{ordered_idom,number_ring}) * m <= n",
   108       "(l::'a::{ordered_idom,number_ring}) <= m * n"],
   109      K LeCancelNumeralFactor.proc),
   110     ("int_div_cancel_numeral_factors",
   111      ["((l::int) * m) div n", "(l::int) div (m * n)"],
   112      K IntDivCancelNumeralFactor.proc),
   113     ("divide_cancel_numeral_factor",
   114      ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   115       "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   116       "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   117      K DivideCancelNumeralFactor.proc)];
   118 
   119 (* referenced by rat_arith.ML *)
   120 val field_cancel_numeral_factors =
   121   map Arith_Data.prep_simproc
   122    [("field_eq_cancel_numeral_factor",
   123      ["(l::'a::{field,number_ring}) * m = n",
   124       "(l::'a::{field,number_ring}) = m * n"],
   125      K EqCancelNumeralFactor.proc),
   126     ("field_cancel_numeral_factor",
   127      ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   128       "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   129       "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   130      K DivideCancelNumeralFactor.proc)]
   131 
   132 end;
   133 
   134 Addsimprocs cancel_numeral_factors;
   135 
   136 (*examples:
   137 print_depth 22;
   138 set timing;
   139 set trace_simp;
   140 fun test s = (Goal s; by (Simp_tac 1));
   141 
   142 test "9*x = 12 * (y::int)";
   143 test "(9*x) div (12 * (y::int)) = z";
   144 test "9*x < 12 * (y::int)";
   145 test "9*x <= 12 * (y::int)";
   146 
   147 test "-99*x = 132 * (y::int)";
   148 test "(-99*x) div (132 * (y::int)) = z";
   149 test "-99*x < 132 * (y::int)";
   150 test "-99*x <= 132 * (y::int)";
   151 
   152 test "999*x = -396 * (y::int)";
   153 test "(999*x) div (-396 * (y::int)) = z";
   154 test "999*x < -396 * (y::int)";
   155 test "999*x <= -396 * (y::int)";
   156 
   157 test "-99*x = -81 * (y::int)";
   158 test "(-99*x) div (-81 * (y::int)) = z";
   159 test "-99*x <= -81 * (y::int)";
   160 test "-99*x < -81 * (y::int)";
   161 
   162 test "-2 * x = -1 * (y::int)";
   163 test "-2 * x = -(y::int)";
   164 test "(-2 * x) div (-1 * (y::int)) = z";
   165 test "-2 * x < -(y::int)";
   166 test "-2 * x <= -1 * (y::int)";
   167 test "-x < -23 * (y::int)";
   168 test "-x <= -23 * (y::int)";
   169 *)
   170 
   171 (*And the same examples for fields such as rat or real:
   172 test "0 <= (y::rat) * -2";
   173 test "9*x = 12 * (y::rat)";
   174 test "(9*x) / (12 * (y::rat)) = z";
   175 test "9*x < 12 * (y::rat)";
   176 test "9*x <= 12 * (y::rat)";
   177 
   178 test "-99*x = 132 * (y::rat)";
   179 test "(-99*x) / (132 * (y::rat)) = z";
   180 test "-99*x < 132 * (y::rat)";
   181 test "-99*x <= 132 * (y::rat)";
   182 
   183 test "999*x = -396 * (y::rat)";
   184 test "(999*x) / (-396 * (y::rat)) = z";
   185 test "999*x < -396 * (y::rat)";
   186 test "999*x <= -396 * (y::rat)";
   187 
   188 test  "(- ((2::rat) * x) <= 2 * y)";
   189 test "-99*x = -81 * (y::rat)";
   190 test "(-99*x) / (-81 * (y::rat)) = z";
   191 test "-99*x <= -81 * (y::rat)";
   192 test "-99*x < -81 * (y::rat)";
   193 
   194 test "-2 * x = -1 * (y::rat)";
   195 test "-2 * x = -(y::rat)";
   196 test "(-2 * x) / (-1 * (y::rat)) = z";
   197 test "-2 * x < -(y::rat)";
   198 test "-2 * x <= -1 * (y::rat)";
   199 test "-x < -23 * (y::rat)";
   200 test "-x <= -23 * (y::rat)";
   201 *)
   202 
   203 
   204 (** Declarations for ExtractCommonTerm **)
   205 
   206 local
   207   open Int_Numeral_Simprocs
   208 in
   209 
   210 (*Find first term that matches u*)
   211 fun find_first_t past u []         = raise TERM ("find_first_t", [])
   212   | find_first_t past u (t::terms) =
   213         if u aconv t then (rev past @ terms)
   214         else find_first_t (t::past) u terms
   215         handle TERM _ => find_first_t (t::past) u terms;
   216 
   217 (** Final simplification for the CancelFactor simprocs **)
   218 val simplify_one = Arith_Data.simplify_meta_eq  
   219   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
   220 
   221 fun cancel_simplify_meta_eq ss cancel_th th =
   222     simplify_one ss (([th, cancel_th]) MRS trans);
   223 
   224 local
   225   val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
   226   fun Eq_True_elim Eq = 
   227     Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
   228 in
   229 fun sign_conv pos_th neg_th ss t =
   230   let val T = fastype_of t;
   231       val zero = Const(@{const_name HOL.zero}, T);
   232       val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
   233       val pos = less $ zero $ t and neg = less $ t $ zero
   234       fun prove p =
   235         Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
   236         handle THM _ => NONE
   237     in case prove pos of
   238          SOME th => SOME(th RS pos_th)
   239        | NONE => (case prove neg of
   240                     SOME th => SOME(th RS neg_th)
   241                   | NONE => NONE)
   242     end;
   243 end
   244 
   245 structure CancelFactorCommon =
   246   struct
   247   val mk_sum            = long_mk_prod
   248   val dest_sum          = dest_prod
   249   val mk_coeff          = mk_coeff
   250   val dest_coeff        = dest_coeff
   251   val find_first        = find_first_t []
   252   val trans_tac         = K Arith_Data.trans_tac
   253   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   254   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   255   val simplify_meta_eq  = cancel_simplify_meta_eq 
   256   end;
   257 
   258 (*mult_cancel_left requires a ring with no zero divisors.*)
   259 structure EqCancelFactor = ExtractCommonTermFun
   260  (open CancelFactorCommon
   261   val prove_conv = Arith_Data.prove_conv
   262   val mk_bal   = HOLogic.mk_eq
   263   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   264   val simp_conv = K (K (SOME @{thm mult_cancel_left}))
   265 );
   266 
   267 (*for ordered rings*)
   268 structure LeCancelFactor = ExtractCommonTermFun
   269  (open CancelFactorCommon
   270   val prove_conv = Arith_Data.prove_conv
   271   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   272   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   273   val simp_conv = sign_conv
   274     @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
   275 );
   276 
   277 (*for ordered rings*)
   278 structure LessCancelFactor = ExtractCommonTermFun
   279  (open CancelFactorCommon
   280   val prove_conv = Arith_Data.prove_conv
   281   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   282   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   283   val simp_conv = sign_conv
   284     @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
   285 );
   286 
   287 (*zdiv_zmult_zmult1_if is for integer division (div).*)
   288 structure IntDivCancelFactor = ExtractCommonTermFun
   289  (open CancelFactorCommon
   290   val prove_conv = Arith_Data.prove_conv
   291   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   292   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   293   val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
   294 );
   295 
   296 structure IntModCancelFactor = ExtractCommonTermFun
   297  (open CancelFactorCommon
   298   val prove_conv = Arith_Data.prove_conv
   299   val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   300   val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
   301   val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
   302 );
   303 
   304 structure IntDvdCancelFactor = ExtractCommonTermFun
   305  (open CancelFactorCommon
   306   val prove_conv = Arith_Data.prove_conv
   307   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   308   val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
   309   val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
   310 );
   311 
   312 (*Version for all fields, including unordered ones (type complex).*)
   313 structure DivideCancelFactor = ExtractCommonTermFun
   314  (open CancelFactorCommon
   315   val prove_conv = Arith_Data.prove_conv
   316   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   317   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   318   val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
   319 );
   320 
   321 val cancel_factors =
   322   map Arith_Data.prep_simproc
   323    [("ring_eq_cancel_factor",
   324      ["(l::'a::{idom}) * m = n",
   325       "(l::'a::{idom}) = m * n"],
   326      K EqCancelFactor.proc),
   327     ("ordered_ring_le_cancel_factor",
   328      ["(l::'a::ordered_ring) * m <= n",
   329       "(l::'a::ordered_ring) <= m * n"],
   330      K LeCancelFactor.proc),
   331     ("ordered_ring_less_cancel_factor",
   332      ["(l::'a::ordered_ring) * m < n",
   333       "(l::'a::ordered_ring) < m * n"],
   334      K LessCancelFactor.proc),
   335     ("int_div_cancel_factor",
   336      ["((l::int) * m) div n", "(l::int) div (m * n)"],
   337      K IntDivCancelFactor.proc),
   338     ("int_mod_cancel_factor",
   339      ["((l::int) * m) mod n", "(l::int) mod (m * n)"],
   340      K IntModCancelFactor.proc),
   341     ("dvd_cancel_factor",
   342      ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
   343      K IntDvdCancelFactor.proc),
   344     ("divide_cancel_factor",
   345      ["((l::'a::{division_by_zero,field}) * m) / n",
   346       "(l::'a::{division_by_zero,field}) / (m * n)"],
   347      K DivideCancelFactor.proc)];
   348 
   349 end;
   350 
   351 Addsimprocs cancel_factors;
   352 
   353 
   354 (*examples:
   355 print_depth 22;
   356 set timing;
   357 set trace_simp;
   358 fun test s = (Goal s; by (Asm_simp_tac 1));
   359 
   360 test "x*k = k*(y::int)";
   361 test "k = k*(y::int)";
   362 test "a*(b*c) = (b::int)";
   363 test "a*(b*c) = d*(b::int)*(x*a)";
   364 
   365 test "(x*k) div (k*(y::int)) = (uu::int)";
   366 test "(k) div (k*(y::int)) = (uu::int)";
   367 test "(a*(b*c)) div ((b::int)) = (uu::int)";
   368 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   369 *)
   370 
   371 (*And the same examples for fields such as rat or real:
   372 print_depth 22;
   373 set timing;
   374 set trace_simp;
   375 fun test s = (Goal s; by (Asm_simp_tac 1));
   376 
   377 test "x*k = k*(y::rat)";
   378 test "k = k*(y::rat)";
   379 test "a*(b*c) = (b::rat)";
   380 test "a*(b*c) = d*(b::rat)*(x*a)";
   381 
   382 
   383 test "(x*k) / (k*(y::rat)) = (uu::rat)";
   384 test "(k) / (k*(y::rat)) = (uu::rat)";
   385 test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   386 test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   387 
   388 (*FIXME: what do we do about this?*)
   389 test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   390 *)