# HG changeset patch
# User wenzelm
# Date 880558957 -3600
# Node ID 014771692751ded878288c7fc1c13aea8f56f0cc
# Parent  6e13b5427de0766ed5ad0804feb3656b0328b839
Cancel common constant factor from balanced exression.

diff -r 6e13b5427de0 -r 014771692751 src/Provers/Arith/cancel_factor.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/Arith/cancel_factor.ML	Wed Nov 26 16:42:37 1997 +0100
@@ -0,0 +1,76 @@
+(*  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 -> Sign.sg -> term * term -> thm
+  val norm_tac: tactic			(*AC0 etc.*)
+  val multiply_tac: 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 Logic.termless 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;