# HG changeset patch
# User haftmann
# Date 1279548583 -7200
# Node ID 314a88278715680e2e3d8686d2b778a3d194c4c0
# Parent  f869bb8574255950d51720e71aca49113da0e585
discontinued pretending that abel_cancel is logic-independent; cleaned up junk

diff -r f869bb857425 -r 314a88278715 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Groups.thy	Mon Jul 19 16:09:43 2010 +0200
@@ -6,7 +6,7 @@
 
 theory Groups
 imports Orderings
-uses ("~~/src/Provers/Arith/abel_cancel.ML")
+uses ("~~/src/HOL/Tools/abel_cancel.ML")
 begin
 
 subsection {* Fact collections *}
@@ -146,8 +146,6 @@
 class times =
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
 
-use "~~/src/Provers/Arith/abel_cancel.ML"
-
 
 subsection {* Semigroups and Monoids *}
 
@@ -453,8 +451,13 @@
 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
 by (simp add: algebra_simps)
 
+lemma diff_eq_diff_eq:
+  "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
+  by (auto simp add: algebra_simps)
+  
 end
 
+
 subsection {* (Partially) Ordered Groups *} 
 
 text {*
@@ -755,14 +758,16 @@
 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
 by (auto simp add: le_less minus_less_iff)
 
-lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
+lemma diff_less_0_iff_less [simp, no_atp]:
+  "a - b < 0 \<longleftrightarrow> a < b"
 proof -
-  have  "(a < b) = (a + (- b) < b + (-b))"  
-    by (simp only: add_less_cancel_right)
-  also have "... =  (a - b < 0)" by (simp add: diff_minus)
+  have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
+  also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   finally show ?thesis .
 qed
 
+lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
+
 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
 apply (subst less_iff_diff_less_0 [of a])
 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
@@ -781,11 +786,32 @@
 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
 
-lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
-by (simp add: algebra_simps)
+lemma diff_le_0_iff_le [simp, no_atp]:
+  "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
+  by (simp add: algebra_simps)
+
+lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
+
+lemma diff_eq_diff_less:
+  "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
+  by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
+
+lemma diff_eq_diff_less_eq': -- "FIXME orientation"
+  "a - b = c - d \<Longrightarrow> b \<le> a \<longleftrightarrow> d \<le> c"
+proof -
+  assume "a - b = c - d"
+  then have "b - a = d - c" by (simp add: algebra_simps)
+  then show "b \<le> a \<longleftrightarrow> d \<le> c" by (auto simp only: le_iff_diff_le_0 [of b a] le_iff_diff_le_0 [of d c])
+qed
 
 end
 
+use "~~/src/HOL/Tools/abel_cancel.ML"
+
+ML {*
+  Addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv];
+*}
+
 class linordered_ab_semigroup_add =
   linorder + ordered_ab_semigroup_add
 
@@ -1167,42 +1193,6 @@
 
 end
 
-text {* Needed for abelian cancellation simprocs: *}
-
-lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
-apply (subst add_left_commute)
-apply (subst add_left_cancel)
-apply simp
-done
-
-lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
-apply (subst add_cancel_21[of _ _ _ 0, simplified])
-apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
-done
-
-lemma less_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
-by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
-
-lemma le_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
-apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])
-apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
-done
-
-lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
-by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
-
-lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
-by (simp add: diff_minus)
-
-lemma le_add_right_mono: 
-  assumes 
-  "a <= b + (c::'a::ordered_ab_group_add)"
-  "c <= d"    
-  shows "a <= b + d"
-  apply (rule_tac order_trans[where y = "b+c"])
-  apply (simp_all add: prems)
-  done
-
 
 subsection {* Tools setup *}
 
@@ -1224,64 +1214,6 @@
 by (auto intro: add_strict_right_mono add_strict_left_mono
   add_less_le_mono add_le_less_mono add_strict_mono)
 
-text{*Simplification of @{term "x-y < 0"}, etc.*}
-lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
-
-ML {*
-structure ab_group_add_cancel = Abel_Cancel
-(
-
-(* term order for abelian groups *)
-
-fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
-      [@{const_name Groups.zero}, @{const_name Groups.plus},
-        @{const_name Groups.uminus}, @{const_name Groups.minus}]
-  | agrp_ord _ = ~1;
-
-fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
-
-local
-  val ac1 = mk_meta_eq @{thm add_assoc};
-  val ac2 = mk_meta_eq @{thm add_commute};
-  val ac3 = mk_meta_eq @{thm add_left_commute};
-  fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
-        SOME ac1
-    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
-        if termless_agrp (y, x) then SOME ac3 else NONE
-    | solve_add_ac thy _ (_ $ x $ y) =
-        if termless_agrp (y, x) then SOME ac2 else NONE
-    | solve_add_ac thy _ _ = NONE
-in
-  val add_ac_proc = Simplifier.simproc @{theory}
-    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
-end;
-
-val eq_reflection = @{thm eq_reflection};
-  
-val T = @{typ "'a::ab_group_add"};
-
-val cancel_ss = HOL_basic_ss settermless termless_agrp
-  addsimprocs [add_ac_proc] addsimps
-  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
-   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
-   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
-   @{thm minus_add_cancel}];
-
-val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
-  
-val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
-
-val dest_eqI = 
-  fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
-
-);
-*}
-
-ML {*
-  Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
-*}
-
 code_modulename SML
   Groups Arith
 
diff -r f869bb857425 -r 314a88278715 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Jul 19 16:09:43 2010 +0200
@@ -168,6 +168,7 @@
   SAT.thy \
   Set.thy \
   Sum_Type.thy \
+  Tools/abel_cancel.ML \
   Tools/arith_data.ML \
   Tools/cnf_funcs.ML \
   Tools/Datatype/datatype_abs_proofs.ML \
@@ -219,7 +220,6 @@
   Transitive_Closure.thy \
   Typedef.thy \
   Wellfounded.thy \
-  $(SRC)/Provers/Arith/abel_cancel.ML \
   $(SRC)/Provers/Arith/cancel_div_mod.ML \
   $(SRC)/Provers/Arith/cancel_sums.ML \
   $(SRC)/Provers/Arith/fast_lin_arith.ML \
diff -r f869bb857425 -r 314a88278715 src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy	Mon Jul 19 16:09:43 2010 +0200
@@ -376,9 +376,10 @@
   "a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" 
 proof -
   assume "a+b <= c"
-  hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
-  have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
-  show ?thesis by (rule le_add_right_mono[OF 2 3])
+  then have "a <= c+(-b)" by (simp add: algebra_simps)
+  have "(-b) <= abs b" by (rule abs_ge_minus_self)
+  then have "c + (- b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono)
+  with `a \<le> c + (- b)` show ?thesis by (rule order_trans)
 qed
 
 class lattice_ring = ordered_ring + lattice_ab_group_add_abs
@@ -411,7 +412,7 @@
     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
     done
   have yx: "?y <= ?x"
-    apply (simp add:diff_def)
+    apply (simp add:diff_minus)
     apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
     apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
     done
diff -r f869bb857425 -r 314a88278715 src/HOL/Matrix/LP.thy
--- a/src/HOL/Matrix/LP.thy	Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Matrix/LP.thy	Mon Jul 19 16:09:43 2010 +0200
@@ -6,6 +6,15 @@
 imports Main Lattice_Algebras
 begin
 
+lemma le_add_right_mono: 
+  assumes 
+  "a <= b + (c::'a::ordered_ab_group_add)"
+  "c <= d"    
+  shows "a <= b + d"
+  apply (rule_tac order_trans[where y = "b+c"])
+  apply (simp_all add: prems)
+  done
+
 lemma linprog_dual_estimate:
   assumes
   "A * x \<le> (b::'a::lattice_ring)"
@@ -49,8 +58,8 @@
     done    
   from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
     by (simp)
-  show ?thesis 
-    apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
+  show ?thesis
+    apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
     apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
     done
 qed
@@ -138,9 +147,9 @@
   then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
   have s2: "c - y * A <= c2 - y * A1"
-    by (simp add: diff_def prems add_mono mult_left_mono)
+    by (simp add: diff_minus prems add_mono mult_left_mono)
   have s1: "c1 - y * A2 <= c - y * A"
-    by (simp add: diff_def prems add_mono mult_left_mono)
+    by (simp add: diff_minus prems add_mono mult_left_mono)
   have prts: "(c - y * A) * x <= ?C"
     apply (simp add: Let_def)
     apply (rule mult_le_prts)
diff -r f869bb857425 -r 314a88278715 src/HOL/Tools/abel_cancel.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/abel_cancel.ML	Mon Jul 19 16:09:43 2010 +0200
@@ -0,0 +1,139 @@
+(*  Title:      HOL/Tools/abel_cancel.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Simplification procedures for abelian groups:
+- Cancel complementary terms in sums.
+- Cancel like terms on opposite sides of relations.
+*)
+
+signature ABEL_CANCEL =
+sig
+  val sum_conv: simproc
+  val rel_conv: simproc
+end;
+
+structure Abel_Cancel: ABEL_CANCEL =
+struct
+
+(* term order for abelian groups *)
+
+fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
+      [@{const_name Groups.zero}, @{const_name Groups.plus},
+        @{const_name Groups.uminus}, @{const_name Groups.minus}]
+  | agrp_ord _ = ~1;
+
+fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
+
+local
+  val ac1 = mk_meta_eq @{thm add_assoc};
+  val ac2 = mk_meta_eq @{thm add_commute};
+  val ac3 = mk_meta_eq @{thm add_left_commute};
+  fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
+        SOME ac1
+    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
+        if termless_agrp (y, x) then SOME ac3 else NONE
+    | solve_add_ac thy _ (_ $ x $ y) =
+        if termless_agrp (y, x) then SOME ac2 else NONE
+    | solve_add_ac thy _ _ = NONE
+in
+  val add_ac_proc = Simplifier.simproc @{theory}
+    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
+end;
+
+val cancel_ss = HOL_basic_ss settermless termless_agrp
+  addsimprocs [add_ac_proc] addsimps
+  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
+   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
+   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
+   @{thm minus_add_cancel}];
+
+val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
+  
+val eqI_rules = [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq'}, @{thm diff_eq_diff_eq}];
+
+val dest_eqI = 
+  fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
+
+fun zero t = Const (@{const_name Groups.zero}, t);
+fun minus t = Const (@{const_name Groups.uminus}, t --> t);
+
+fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
+      add_terms pos (x, add_terms pos (y, ts))
+  | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
+      add_terms pos (x, add_terms (not pos) (y, ts))
+  | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
+      add_terms (not pos) (x, ts)
+  | add_terms pos (x, ts) = (pos,x) :: ts;
+
+fun terms fml = add_terms true (fml, []);
+
+fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
+      (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
+                                   | SOME z => SOME(c $ x $ z))
+       | SOME z => SOME(c $ z $ y))
+  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
+      (case zero1 (pos,t) x of
+         NONE => (case zero1 (not pos,t) y of NONE => NONE
+                  | SOME z => SOME(c $ x $ z))
+       | SOME z => SOME(c $ z $ y))
+  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
+      (case zero1 (not pos,t) x of NONE => NONE
+       | SOME z => SOME(c $ z))
+  | zero1 (pos,t) u =
+      if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE
+
+exception Cancel;
+
+fun find_common _ [] _ = raise Cancel
+  | find_common opp ((p,l)::ls) rs =
+      let val pr = if opp then not p else p
+      in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l)
+         else find_common opp ls rs
+      end
+
+(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
+   If OP = +, it must be t2(-t) rather than t2(t)
+*)
+fun cancel t =
+  let
+    val c $ lhs $ rhs = t
+    val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
+    val (pos,l) = find_common opp (terms lhs) (terms rhs)
+    val posr = if opp then not pos else pos
+    val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
+  in t' end;
+
+
+(*A simproc to cancel complementary terms in arbitrary sums.*)
+fun sum_proc ss t =
+   let
+     val t' = cancel t
+     val thm =
+       Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
+         (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
+   in SOME thm end handle Cancel => NONE;
+
+val sum_conv =
+  Simplifier.mk_simproc "cancel_sums"
+    (map (Drule.cterm_fun Logic.varify_global) sum_pats) (K sum_proc);
+
+
+(*A simproc to cancel like terms on the opposite sides of relations:
+   (x + y - z < -z + x) = (y < 0)
+  Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
+  Reduces the problem to subtraction.*)
+fun rel_proc ss t =
+  let
+    val t' = cancel t
+    val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
+      (fn _ => rtac @{thm eq_reflection} 1 THEN
+                    resolve_tac eqI_rules 1 THEN
+                    simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
+   in SOME thm end handle Cancel => NONE;
+
+val rel_conv =
+  Simplifier.mk_simproc "cancel_relations"
+    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (dest_eqI th)) eqI_rules) (K rel_proc);
+
+end;
diff -r f869bb857425 -r 314a88278715 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Mon Jul 19 16:09:43 2010 +0200
@@ -818,7 +818,7 @@
         @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
         @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
         @{thm "not_one_less_zero"}]
-      addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
+      addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv]
        (*abel_cancel helps it work in abstract algebraic domains*)
       addsimprocs Nat_Arith.nat_cancel_sums_add
       addcongs [@{thm if_weak_cong}],
diff -r f869bb857425 -r 314a88278715 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Mon Jul 19 12:17:38 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(*  Title:      Provers/Arith/abel_cancel.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Simplification procedures for abelian groups (e.g. integers, reals,
-polymorphic types).
-
-- Cancel complementary terms in sums
-- Cancel like terms on opposite sides of relations
-*)
-
-signature ABEL_CANCEL =
-sig
-  val eq_reflection   : thm           (*object-equality to meta-equality*)
-  val T               : typ           (*the type of group elements*)
-  val cancel_ss       : simpset       (*abelian group cancel simpset*)
-  val sum_pats        : cterm list
-  val eqI_rules       : thm list
-  val dest_eqI        : thm -> term
-end;
-
-
-functor Abel_Cancel (Data: ABEL_CANCEL) =
-struct
-
-open Data;
-
-(* FIXME dependent on abstract syntax *)
-
-fun zero t = Const (@{const_name Groups.zero}, t);
-fun minus t = Const (@{const_name Groups.uminus}, t --> t);
-
-fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
-      add_terms pos (x, add_terms pos (y, ts))
-  | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
-      add_terms pos (x, add_terms (not pos) (y, ts))
-  | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
-      add_terms (not pos) (x, ts)
-  | add_terms pos (x, ts) = (pos,x) :: ts;
-
-fun terms fml = add_terms true (fml, []);
-
-fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
-      (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
-                                   | SOME z => SOME(c $ x $ z))
-       | SOME z => SOME(c $ z $ y))
-  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
-      (case zero1 (pos,t) x of
-         NONE => (case zero1 (not pos,t) y of NONE => NONE
-                  | SOME z => SOME(c $ x $ z))
-       | SOME z => SOME(c $ z $ y))
-  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
-      (case zero1 (not pos,t) x of NONE => NONE
-       | SOME z => SOME(c $ z))
-  | zero1 (pos,t) u =
-      if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE
-
-exception Cancel;
-
-fun find_common _ [] _ = raise Cancel
-  | find_common opp ((p,l)::ls) rs =
-      let val pr = if opp then not p else p
-      in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l)
-         else find_common opp ls rs
-      end
-
-(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
-   If OP = +, it must be t2(-t) rather than t2(t)
-*)
-fun cancel t =
-  let
-    val c $ lhs $ rhs = t
-    val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
-    val (pos,l) = find_common opp (terms lhs) (terms rhs)
-    val posr = if opp then not pos else pos
-    val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
-  in t' end;
-
-
-(*A simproc to cancel complementary terms in arbitrary sums.*)
-fun sum_proc ss t =
-   let
-     val t' = cancel t
-     val thm =
-       Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
-         (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
-   in SOME thm end handle Cancel => NONE;
-
-val sum_conv =
-  Simplifier.mk_simproc "cancel_sums"
-    (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc);
-
-
-(*A simproc to cancel like terms on the opposite sides of relations:
-   (x + y - z < -z + x) = (y < 0)
-  Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
-  Reduces the problem to subtraction.*)
-fun rel_proc ss t =
-  let
-    val t' = cancel t
-    val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
-      (fn _ => rtac eq_reflection 1 THEN
-                    resolve_tac eqI_rules 1 THEN
-                    simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
-   in SOME thm end handle Cancel => NONE;
-
-val rel_conv =
-  Simplifier.mk_simproc "cancel_relations"
-    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc);
-
-end;