src/Provers/Arith/cancel_factor.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
permissions -rw-r--r--
modernized structure Object_Logic;
     1 (*  Title:      Provers/Arith/cancel_factor.ML
     2     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     3 
     4 Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
     5 *)
     6 
     7 signature CANCEL_FACTOR_DATA =
     8 sig
     9   (*abstract syntax*)
    10   val mk_sum: term list -> term
    11   val dest_sum: term -> term list
    12   val mk_bal: term * term -> term
    13   val dest_bal: term -> term * term
    14   (*rules*)
    15   val prove_conv: tactic -> tactic -> Proof.context -> term * term -> thm
    16   val norm_tac: tactic (*AC0 etc.*)
    17   val multiply_tac: integer -> tactic
    18     (*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
    19 end;
    20 
    21 signature CANCEL_FACTOR =
    22 sig
    23   val proc: simpset -> term -> thm option
    24 end;
    25 
    26 
    27 functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR =
    28 struct
    29 
    30 
    31 (* count terms *)
    32 
    33 fun ins_term (t, []) = [(t, 1)]
    34   | ins_term (t, (u, k) :: uks) =
    35       if t aconv u then (u, k + 1) :: uks
    36       else (t, 1) :: (u, k) :: uks;
    37 
    38 fun count_terms ts = foldr ins_term (sort Term_Ord.term_ord ts, []);
    39 
    40 
    41 (* divide sum *)
    42 
    43 fun div_sum d =
    44   Data.mk_sum o maps (fn (t, k) => replicate (k div d) t);
    45 
    46 
    47 (* the simplification procedure *)
    48 
    49 fun proc ss t =
    50   (case try Data.dest_bal t of
    51     NONE => NONE
    52   | SOME bal =>
    53       (case pairself Data.dest_sum bal of
    54         ([_], _) => NONE
    55       | (_, [_]) => NONE
    56       | ts_us =>
    57           let
    58             val (tks, uks) = pairself count_terms ts_us;
    59             val d = 0
    60               |> fold (Integer.gcd o snd) tks
    61               |> fold (Integer.gcd o snd) uks;
    62           in
    63             if d = 0 orelse d = 1 then NONE
    64             else SOME
    65               (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss)
    66                 (t, Data.mk_bal (div_sum d tks, div_sum d uks)))
    67           end));
    68 
    69 
    70 end;