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