src/Provers/Arith/cancel_factor.ML
author paulson
Fri Jun 16 13:13:55 2000 +0200 (2000-06-16)
changeset 9073 40d8dfac96b8
parent 4452 b2ee34200dab
child 15531 08c8dad8e399
permissions -rw-r--r--
tracing flag for arith_tac
     1 (*  Title:      Provers/Arith/cancel_factor.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     4 
     5 Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
     6 *)
     7 
     8 signature CANCEL_FACTOR_DATA =
     9 sig
    10   (*abstract syntax*)
    11   val mk_sum: term list -> term
    12   val dest_sum: term -> term list
    13   val mk_bal: term * term -> term
    14   val dest_bal: term -> term * term
    15   (*rules*)
    16   val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
    17   val norm_tac: tactic			(*AC0 etc.*)
    18   val multiply_tac: int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
    19 end;
    20 
    21 signature CANCEL_FACTOR =
    22 sig
    23   val proc: Sign.sg -> thm list -> term -> thm option
    24 end;
    25 
    26 
    27 functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR =
    28 struct
    29 
    30 
    31 (* greatest common divisor *)
    32 
    33 fun gcd (0, n) = n
    34   | gcd (m, n) = gcd (n mod m, m);
    35 
    36 val gcds = foldl gcd;
    37 
    38 
    39 (* count terms *)
    40 
    41 fun ins_term (t, []) = [(t, 1)]
    42   | ins_term (t, (u, k) :: uks) =
    43       if t aconv u then (u, k + 1) :: uks
    44       else (t, 1) :: (u, k) :: uks;
    45 
    46 fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []);
    47 
    48 
    49 (* divide sum *)
    50 
    51 fun div_sum d tks =
    52   Data.mk_sum (flat (map (fn (t, k) => replicate (k div d) t) tks));
    53 
    54 
    55 (* the simplification procedure *)
    56 
    57 fun proc sg _ t =
    58   (case try Data.dest_bal t of
    59     None => None
    60   | Some bal =>
    61       (case pairself Data.dest_sum bal of
    62         ([_], _) => None
    63       | (_, [_]) => None
    64       | ts_us =>
    65           let
    66             val (tks, uks) = pairself count_terms ts_us;
    67             val d = gcds (gcds (0, map snd tks), map snd uks);
    68           in
    69             if d = 0 orelse d = 1 then None
    70             else Some
    71               (Data.prove_conv (Data.multiply_tac d) Data.norm_tac sg
    72                 (t, Data.mk_bal (div_sum d tks, div_sum d uks)))
    73           end));
    74 
    75 
    76 end;