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