author haftmann Tue, 20 Jul 2010 10:24:18 +0200 changeset 37894 b22db9ecf416 parent 37893 0dbbc4c5a67e child 37895 d1ddd0269bae
tuned code
```--- a/src/HOL/Tools/abel_cancel.ML	Tue Jul 20 08:54:21 2010 +0200
+++ b/src/HOL/Tools/abel_cancel.ML	Tue Jul 20 10:24:18 2010 +0200
@@ -16,74 +16,41 @@
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);
+(** compute cancellation **)

-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}
-end;
+fun add_atoms pos (Const (@{const_name Groups.plus}, _) \$ x \$ y) =
+      add_atoms pos x #> add_atoms pos y
+  | add_atoms pos (Const (@{const_name Groups.minus}, _) \$ x \$ y) =
+      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 x = cons (pos, x);

-val cancel_ss = HOL_basic_ss settermless termless_agrp
-  [@{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},
-
-val eqI_rules = [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}];
-
-fun zero t = Const (@{const_name Groups.zero}, t);
-fun minus t = Const (@{const_name Groups.uminus}, t --> t);
+fun atoms fml = add_atoms true fml [];

-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) =
+fun zero1 pt (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
+       | SOME z => SOME (c \$ z \$ y))
+  | zero1 pt (c as Const (@{const_name Groups.minus}, _) \$ x \$ y) =
+      (case zero1 pt x of
+         NONE => (case zero1 (apfst not pt) y of NONE => NONE
+                  | SOME z => SOME (c \$ x \$ z))
+       | SOME z => SOME (c \$ z \$ y))
+  | zero1 pt (c as Const (@{const_name Groups.uminus}, _) \$ x) =
+      (case zero1 (apfst not pt) x of NONE => NONE
+       | SOME z => SOME (c \$ z))
+  | zero1 (pos, t) u =
+      if pos andalso (t aconv u)
+        then SOME (Const (@{const_name Groups.zero}, fastype_of t))
+        else NONE

exception Cancel;

fun find_common _ [] _ = raise Cancel
-  | find_common opp ((p,l)::ls) rs =
+  | 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)
+      in if exists (fn (q, r) => pr = q andalso l aconv r) rs then (p, l)
else find_common opp ls rs
end

@@ -93,36 +60,73 @@
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;
+    val opp = case c of Const(@{const_name Groups.plus}, _) => true | _ => false;
+    val (pos, l) = find_common opp (atoms lhs) (atoms rhs);
+    val posr = if opp then not pos else pos;
+  in c \$ the (zero1 (pos, l) lhs) \$ the (zero1 (posr, l) rhs) end;

-(*A simproc to cancel complementary terms in arbitrary sums.*)
+(** prove cancellation **)
+
+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 less_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
+
+fun solve (_ \$ (Const (@{const_name Groups.plus}, _) \$ _ \$ _) \$ _) =
+      SOME @{thm add_assoc [THEN eq_reflection]}
+  | solve (_ \$ x \$ (Const (@{const_name Groups.plus}, _) \$ y \$ _)) =
+      if less_agrp (y, x) then
+        SOME @{thm add_left_commute [THEN eq_reflection]}
+        else NONE
+  | solve (_ \$ x \$ y) =
+      if less_agrp (y, x) then
+        SOME @{thm add_commute [THEN eq_reflection]} else
+        NONE
+  | solve _ = NONE;
+
+val simproc = Simplifier.simproc @{theory}
+  "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
+
+val cancel_ss = HOL_basic_ss settermless less_agrp
+  [@{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},
+
+fun cancel_simp_tac ss = simp_tac (Simplifier.inherit_context ss cancel_ss);
+
+
+(** simprocs **)
+
+(* cancel complementary terms in arbitrary sums *)
+
fun sum_proc ss ct =
let
val t = Thm.term_of ct;
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)
+        (fn _ => cancel_simp_tac ss 1)
in SOME thm end handle Cancel => NONE;

-(*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.*)
+(* 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 ct =
let
val t = Thm.term_of ct;
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)
+                    resolve_tac [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}] 1 THEN
+                    cancel_simp_tac ss 1)
in SOME thm end handle Cancel => NONE;

end;```