author huffman Sat, 04 Feb 2006 03:14:32 +0100 changeset 18925 2e3d508ba8dc parent 18924 83acd39b1bab child 18926 4227b1510552
speedup: use simproc for AC rules
 src/HOL/OrderedGroup.ML file | annotate | diff | comparison | revisions
```--- 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
*)

@@ -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
+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 ())