(*  Title:      Provers/Arith/cancel_factor.ML

    ID:         $Id$

    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 -> theory -> 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: theory -> 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;