# HG changeset patch
# User huffman
# Date 1321011028 -3600
# Node ID 5a5a6e6c6789481904eae6b9baa4a099036a5f7a
# Parent  9a588a835c1e83dd0aef9228e9b972c33a7a8ffa
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
add tests for abel_cancel simprocs

diff -r 9a588a835c1e -r 5a5a6e6c6789 src/HOL/Tools/abel_cancel.ML
--- a/src/HOL/Tools/abel_cancel.ML	Fri Nov 11 11:30:31 2011 +0100
+++ b/src/HOL/Tools/abel_cancel.ML	Fri Nov 11 12:30:28 2011 +0100
@@ -24,6 +24,7 @@
       add_atoms pos x #> add_atoms (not pos) y
   | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) =
       add_atoms (not pos) x
+  | add_atoms pos (Const (@{const_name Groups.zero}, _)) = I
   | add_atoms pos x = cons (pos, x);
 
 fun atoms t = add_atoms true t [];
diff -r 9a588a835c1e -r 5a5a6e6c6789 src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 11:30:31 2011 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 12:30:28 2011 +0100
@@ -21,12 +21,33 @@
   fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
 *}
 
+subsection {* Abelian group cancellation simprocs *}
+
+notepad begin
+  fix a b c u :: "'a::ab_group_add"
+  {
+    assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u"
+      by (tactic {* test [@{simproc abel_cancel_sum}] *}) fact
+  next
+    assume "a + 0 = b + 0" have "a + c = b + c"
+      by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact
+  }
+end
+(* TODO: more tests for Groups.abel_cancel_{sum,relation} *)
 
 subsection {* @{text int_combine_numerals} *}
 
+(* FIXME: int_combine_numerals often unnecessarily regroups addition
+and rewrites subtraction to negation. Ideally it should behave more
+like Groups.abel_cancel_sum, preserving the shape of terms as much as
+possible. *)
+
 notepad begin
   fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring"
   {
+    assume "a + - b = u" have "(a + c) - (b + c) = u"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
     assume "10 + (2 * l + oo) = uu"
     have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact