--- a/src/HOL/OrderedGroup.ML Sat Feb 04 02:37:09 2006 +0100
+++ b/src/HOL/OrderedGroup.ML Sat Feb 04 03:14:32 2006 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/OrderedGroup.ML
ID: $Id$
- Author: Steven Obua, Tobias Nipkow, Technische Universität München
+ Author: Steven Obua, Tobias Nipkow, Technische Universit� Mnchen
*)
structure ab_group_add_cancel_data :> ABEL_CANCEL =
@@ -12,9 +12,25 @@
fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
-val cancel_ss = HOL_basic_ss settermless termless_agrp addsimps
- [thm "add_assoc", thm "add_commute", thm "add_left_commute",
- thm "add_0", thm "add_0_right",
+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 ("op +",_) $ _ $ _) $ _) =
+ SOME ac1
+ | solve_add_ac thy _ (_ $ x $ (Const ("op +",_) $ 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 (the_context ())
+ "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", thm "add_0_right",
thm "diff_def", thm "minus_add_distrib",
thm "minus_minus", thm "minus_zero",
thm "right_minus", thm "left_minus",