# HG changeset patch
# User haftmann
# Date 1280318996 -7200
# Node ID 04a8de29e8f7dce98fc8c7abd79afc802ced775f
# Parent  ac704f1c8dde2ed641e159c0b7418291a0a29d40
dropped dead code

diff -r ac704f1c8dde -r 04a8de29e8f7 src/Provers/Arith/cancel_factor.ML
--- a/src/Provers/Arith/cancel_factor.ML	Wed Jul 28 11:42:48 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-(*  Title:      Provers/Arith/cancel_factor.ML
-    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 -> Proof.context -> term * term -> thm
-  val norm_tac: tactic (*AC0 etc.*)
-  val multiply_tac: integer -> tactic
-    (*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
-end;
-
-signature CANCEL_FACTOR =
-sig
-  val proc: simpset -> term -> thm option
-end;
-
-
-functor CancelFactorFun(Data: CANCEL_FACTOR_DATA): CANCEL_FACTOR =
-struct
-
-
-(* 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_Ord.term_ord ts, []);
-
-
-(* divide sum *)
-
-fun div_sum d =
-  Data.mk_sum o maps (fn (t, k) => replicate (k div d) t);
-
-
-(* the simplification procedure *)
-
-fun proc ss 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 = 0
-              |> fold (Integer.gcd o snd) tks
-              |> fold (Integer.gcd o snd) uks;
-          in
-            if d = 0 orelse d = 1 then NONE
-            else SOME
-              (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss)
-                (t, Data.mk_bal (div_sum d tks, div_sum d uks)))
-          end));
-
-
-end;
diff -r ac704f1c8dde -r 04a8de29e8f7 src/Provers/Arith/cancel_sums.ML
--- a/src/Provers/Arith/cancel_sums.ML	Wed Jul 28 11:42:48 2010 +0200
+++ b/src/Provers/Arith/cancel_sums.ML	Wed Jul 28 14:09:56 2010 +0200
@@ -35,7 +35,6 @@
 
 fun cons1 x (xs, y, z) = (x :: xs, y, z);
 fun cons2 y (x, ys, z) = (x, y :: ys, z);
-fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
 
 (*symmetric difference of multisets -- assumed to be sorted wrt. Term_Ord.term_ord*)
 fun cancel ts [] vs = (ts, [], vs)
diff -r ac704f1c8dde -r 04a8de29e8f7 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jul 28 11:42:48 2010 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jul 28 14:09:56 2010 +0200
@@ -211,7 +211,7 @@
 fun ratexact up (r, exact) =
   if exact then r else
   let
-    val (p, q) = Rat.quotient_of_rat r;
+    val (_, q) = Rat.quotient_of_rat r;
     val nth = Rat.inv (Rat.rat_of_int q);
   in Rat.add r (if up then nth else Rat.neg nth) end;
 
@@ -306,7 +306,7 @@
 (* Add together (in)equations.                                               *)
 (* ------------------------------------------------------------------------- *)
 
-fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
+fun add_ineq (Lineq (k1,ty1,l1,just1)) (Lineq (k2,ty2,l2,just2)) =
   let val l = map2 Integer.add l1 l2
   in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end;
 
@@ -335,7 +335,7 @@
 
 fun is_trivial (Lineq(_,_,l,_)) = forall (fn i => i=0) l;
 
-fun is_contradictory (ans as Lineq(k,ty,l,_)) =
+fun is_contradictory (Lineq(k,ty,_,_)) =
   case ty  of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
 
 fun calc_blowup l =
@@ -550,7 +550,7 @@
         in (t,i * (m div j)) end
 in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
 
-fun mklineq n atoms =
+fun mklineq atoms =
   fn (item, k) =>
   let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item
       val lhsa = map (coeff lhs) atoms
@@ -705,7 +705,7 @@
           let
             val atoms = atoms_of (map fst initems)
             val n = length atoms
-            val mkleq = mklineq n atoms
+            val mkleq = mklineq atoms
             val ixs = 0 upto (n - 1)
             val iatoms = atoms ~~ ixs
             val natlineqs = map_filter (mknat Ts ixs) iatoms
diff -r ac704f1c8dde -r 04a8de29e8f7 src/Provers/README
--- a/src/Provers/README	Wed Jul 28 11:42:48 2010 +0200
+++ b/src/Provers/README	Wed Jul 28 14:09:56 2010 +0200
@@ -13,10 +13,8 @@
   typedsimp.ML          basic simplifier for explicitly typed logics
 
 directory Arith:
-  abel_cancel.ML	cancel complementary terms in sums of Abelian groups
   assoc_fold.ML		fold numerals in nested products
   cancel_numerals.ML	cancel common coefficients in balanced expressions
-  cancel_factor.ML	cancel common constant factor
   cancel_sums.ML	cancel common summands
   combine_numerals.ML	combine coefficients in expressions
   fast_lin_arith.ML	generic linear arithmetic package