--- 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;
--- 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)
--- 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
--- 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