# HG changeset patch
# User haftmann
# Date 1279614258 -7200
# Node ID b22db9ecf416bd4b466ba5f003e1daf504aba131
# Parent  0dbbc4c5a67e81b31579160c371d0943ff4b0abc
tuned code

diff -r 0dbbc4c5a67e -r b22db9ecf416 src/HOL/Tools/abel_cancel.ML
--- 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}
-    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
-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
-  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 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
+  addsimprocs [simproc] 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}];
+
+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;