1.1 --- a/src/HOL/Tools/abel_cancel.ML	Mon Jul 19 20:23:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/abel_cancel.ML	Mon Jul 19 20:23:52 2010 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  
     1.5  signature ABEL_CANCEL =
     1.6  sig
     1.7 -  val sum_conv: simproc
     1.8 -  val rel_conv: simproc
     1.9 +  val sum_proc: simpset -> cterm -> thm option
    1.10 +  val rel_proc: simpset -> cterm -> thm option
    1.11  end;
    1.12  
    1.13  structure Abel_Cancel: ABEL_CANCEL =
    1.14 @@ -48,12 +48,7 @@
    1.15     @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
    1.16     @{thm minus_add_cancel}];
    1.17  
    1.18 -val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
    1.19 -  
    1.20 -val eqI_rules = [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq'}, @{thm diff_eq_diff_eq}];
    1.21 -
    1.22 -val dest_eqI = 
    1.23 -  fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
    1.24 +val eqI_rules = [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}];
    1.25  
    1.26  fun zero t = Const (@{const_name Groups.zero}, t);
    1.27  fun minus t = Const (@{const_name Groups.uminus}, t --> t);
    1.28 @@ -106,34 +101,28 @@
    1.29  
    1.30  
    1.31  (*A simproc to cancel complementary terms in arbitrary sums.*)
    1.32 -fun sum_proc ss t =
    1.33 -   let
    1.34 -     val t' = cancel t
    1.35 -     val thm =
    1.36 -       Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
    1.37 -         (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
    1.38 -   in SOME thm end handle Cancel => NONE;
    1.39 -
    1.40 -val sum_conv =
    1.41 -  Simplifier.mk_simproc "cancel_sums"
    1.42 -    (map (Drule.cterm_fun Logic.varify_global) sum_pats) (K sum_proc);
    1.43 +fun sum_proc ss ct =
    1.44 +  let
    1.45 +    val t = Thm.term_of ct;
    1.46 +    val t' = cancel t;
    1.47 +    val thm =
    1.48 +      Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
    1.49 +        (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
    1.50 +  in SOME thm end handle Cancel => NONE;
    1.51  
    1.52  
    1.53  (*A simproc to cancel like terms on the opposite sides of relations:
    1.54     (x + y - z < -z + x) = (y < 0)
    1.55    Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
    1.56    Reduces the problem to subtraction.*)
    1.57 -fun rel_proc ss t =
    1.58 +fun rel_proc ss ct =
    1.59    let
    1.60 -    val t' = cancel t
    1.61 +    val t = Thm.term_of ct;
    1.62 +    val t' = cancel t;
    1.63      val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
    1.64        (fn _ => rtac @{thm eq_reflection} 1 THEN
    1.65                      resolve_tac eqI_rules 1 THEN
    1.66                      simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
    1.67 -   in SOME thm end handle Cancel => NONE;
    1.68 -
    1.69 -val rel_conv =
    1.70 -  Simplifier.mk_simproc "cancel_relations"
    1.71 -    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (dest_eqI th)) eqI_rules) (K rel_proc);
    1.72 +  in SOME thm end handle Cancel => NONE;
    1.73  
    1.74  end;

     2.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Jul 19 20:23:49 2010 +0200
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Jul 19 20:23:52 2010 +0200
     2.3 @@ -818,7 +818,7 @@
     2.4          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
     2.5          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
     2.6          @{thm "not_one_less_zero"}]
     2.7 -      addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv]
     2.8 +      addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
     2.9         (*abel_cancel helps it work in abstract algebraic domains*)
    2.10        addsimprocs Nat_Arith.nat_cancel_sums_add
    2.11        addcongs [@{thm if_weak_cong}],