(*  Title:      Provers/Arith/cancel_factor.ML
    ID:         $Id: cancel_factor.ML,v 1.4 2005/05/16 08:29:16 paulson Exp $
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen

Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
*)

signature CANCEL_FACTOR_DATA =
sig
  (*abstract syntax*)
  val mk_sum: term list -> term
  val dest_sum: term -> term list
  val mk_bal: term * term -> term
  val dest_bal: term -> term * term
  (*rules*)
  val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
  val norm_tac: tactic			(*AC0 etc.*)
  val multiply_tac: IntInf.int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
end;

signature CANCEL_FACTOR =
sig
  val proc: Sign.sg -> thm list -> term -> thm option
end;


functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR =
struct


(* greatest common divisor *)

fun gcd (0, n) = n
  | gcd (m, n) = gcd (n mod m, m);

val gcds = foldl gcd;


(* count terms *)

fun ins_term (t, []) = [(t, 1)]
  | ins_term (t, (u, k) :: uks) =
      if t aconv u then (u, k + 1) :: uks
      else (t, 1) :: (u, k) :: uks;

fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []);


(* divide sum *)

fun div_sum d tks =
  Data.mk_sum (flat (map (fn (t, k) => replicate (k div d) t) tks));


(* the simplification procedure *)

fun proc sg _ t =
  (case try Data.dest_bal t of
    NONE => NONE
  | SOME bal =>
      (case pairself Data.dest_sum bal of
        ([_], _) => NONE
      | (_, [_]) => NONE
      | ts_us =>
          let
            val (tks, uks) = pairself count_terms ts_us;
            val d = gcds (gcds (0, map snd tks), map snd uks);
          in
            if d = 0 orelse d = 1 then NONE
            else SOME
              (Data.prove_conv (Data.multiply_tac d) Data.norm_tac sg
                (t, Data.mk_bal (div_sum d tks, div_sum d uks)))
          end));


end;