src/HOL/int_factor_simprocs.ML
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24395 8df021f79e0b
child 25481 aa16cd919dcc
permissions -rw-r--r--
moved Finite_Set before Datatype
     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 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         = fn _ => 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 = Int_Numeral_Simprocs.simplify_meta_eq
    45     [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
    46       @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right}];
    47   end
    48 
    49 (*Version for integer division*)
    50 structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
    51  (open CancelNumeralFactorCommon
    52   val prove_conv = Int_Numeral_Base_Simprocs.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 = Int_Numeral_Base_Simprocs.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 = Int_Numeral_Base_Simprocs.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 = Int_Numeral_Base_Simprocs.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 = Int_Numeral_Base_Simprocs.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 Int_Numeral_Base_Simprocs.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 Int_Numeral_Base_Simprocs.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 = Int_Numeral_Simprocs.simplify_meta_eq  
   219   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, numeral_1_eq_1];
   220 
   221 fun cancel_simplify_meta_eq cancel_th ss th =
   222     simplify_one ss (([th, cancel_th]) MRS trans);
   223 
   224 structure CancelFactorCommon =
   225   struct
   226   val mk_sum            = long_mk_prod
   227   val dest_sum          = dest_prod
   228   val mk_coeff          = mk_coeff
   229   val dest_coeff        = dest_coeff
   230   val find_first        = find_first_t []
   231   val trans_tac         = fn _ => trans_tac
   232   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   233   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   234   end;
   235 
   236 (*mult_cancel_left requires a ring with no zero divisors.*)
   237 structure EqCancelFactor = ExtractCommonTermFun
   238  (open CancelFactorCommon
   239   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   240   val mk_bal   = HOLogic.mk_eq
   241   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   242   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
   243 );
   244 
   245 (*zdiv_zmult_zmult1_if is for integer division (div).*)
   246 structure IntDivCancelFactor = ExtractCommonTermFun
   247  (open CancelFactorCommon
   248   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   249   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   250   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   251   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
   252 );
   253 
   254 structure IntModCancelFactor = ExtractCommonTermFun
   255  (open CancelFactorCommon
   256   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   257   val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   258   val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
   259   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
   260 );
   261 
   262 structure IntDvdCancelFactor = ExtractCommonTermFun
   263  (open CancelFactorCommon
   264   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   265   val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
   266   val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.intT
   267   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
   268 );
   269 
   270 (*Version for all fields, including unordered ones (type complex).*)
   271 structure DivideCancelFactor = ExtractCommonTermFun
   272  (open CancelFactorCommon
   273   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   274   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   275   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   276   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
   277 );
   278 
   279 val cancel_factors =
   280   map Int_Numeral_Base_Simprocs.prep_simproc
   281    [("ring_eq_cancel_factor",
   282      ["(l::'a::{idom}) * m = n",
   283       "(l::'a::{idom}) = m * n"],
   284     K EqCancelFactor.proc),
   285     ("int_div_cancel_factor",
   286      ["((l::int) * m) div n", "(l::int) div (m * n)"],
   287      K IntDivCancelFactor.proc),
   288     ("int_mod_cancel_factor",
   289      ["((l::int) * m) mod n", "(l::int) mod (m * n)"],
   290      K IntModCancelFactor.proc),
   291     ("int_dvd_cancel_factor",
   292      ["((l::int) * m) dvd n", "(l::int) dvd (m * n)"],
   293      K IntDvdCancelFactor.proc),
   294     ("divide_cancel_factor",
   295      ["((l::'a::{division_by_zero,field}) * m) / n",
   296       "(l::'a::{division_by_zero,field}) / (m * n)"],
   297      K DivideCancelFactor.proc)];
   298 
   299 end;
   300 
   301 Addsimprocs cancel_factors;
   302 
   303 
   304 (*examples:
   305 print_depth 22;
   306 set timing;
   307 set trace_simp;
   308 fun test s = (Goal s; by (Asm_simp_tac 1));
   309 
   310 test "x*k = k*(y::int)";
   311 test "k = k*(y::int)";
   312 test "a*(b*c) = (b::int)";
   313 test "a*(b*c) = d*(b::int)*(x*a)";
   314 
   315 test "(x*k) div (k*(y::int)) = (uu::int)";
   316 test "(k) div (k*(y::int)) = (uu::int)";
   317 test "(a*(b*c)) div ((b::int)) = (uu::int)";
   318 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   319 *)
   320 
   321 (*And the same examples for fields such as rat or real:
   322 print_depth 22;
   323 set timing;
   324 set trace_simp;
   325 fun test s = (Goal s; by (Asm_simp_tac 1));
   326 
   327 test "x*k = k*(y::rat)";
   328 test "k = k*(y::rat)";
   329 test "a*(b*c) = (b::rat)";
   330 test "a*(b*c) = d*(b::rat)*(x*a)";
   331 
   332 
   333 test "(x*k) / (k*(y::rat)) = (uu::rat)";
   334 test "(k) / (k*(y::rat)) = (uu::rat)";
   335 test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   336 test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   337 
   338 (*FIXME: what do we do about this?*)
   339 test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   340 *)