discontinued pretending that abel_cancel is logic-independent; cleaned up junk
authorhaftmann
Mon Jul 19 16:09:43 2010 +0200 (2010-07-19)
changeset 37884314a88278715
parent 37883 f869bb857425
child 37885 c43805c80eb6
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
src/HOL/Groups.thy
src/HOL/IsaMakefile
src/HOL/Library/Lattice_Algebras.thy
src/HOL/Matrix/LP.thy
src/HOL/Tools/abel_cancel.ML
src/HOL/Tools/lin_arith.ML
src/Provers/Arith/abel_cancel.ML
     1.1 --- a/src/HOL/Groups.thy	Mon Jul 19 12:17:38 2010 +0200
     1.2 +++ b/src/HOL/Groups.thy	Mon Jul 19 16:09:43 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  theory Groups
     1.6  imports Orderings
     1.7 -uses ("~~/src/Provers/Arith/abel_cancel.ML")
     1.8 +uses ("~~/src/HOL/Tools/abel_cancel.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Fact collections *}
    1.12 @@ -146,8 +146,6 @@
    1.13  class times =
    1.14    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    1.15  
    1.16 -use "~~/src/Provers/Arith/abel_cancel.ML"
    1.17 -
    1.18  
    1.19  subsection {* Semigroups and Monoids *}
    1.20  
    1.21 @@ -453,8 +451,13 @@
    1.22  lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
    1.23  by (simp add: algebra_simps)
    1.24  
    1.25 +lemma diff_eq_diff_eq:
    1.26 +  "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
    1.27 +  by (auto simp add: algebra_simps)
    1.28 +  
    1.29  end
    1.30  
    1.31 +
    1.32  subsection {* (Partially) Ordered Groups *} 
    1.33  
    1.34  text {*
    1.35 @@ -755,14 +758,16 @@
    1.36  lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
    1.37  by (auto simp add: le_less minus_less_iff)
    1.38  
    1.39 -lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
    1.40 +lemma diff_less_0_iff_less [simp, no_atp]:
    1.41 +  "a - b < 0 \<longleftrightarrow> a < b"
    1.42  proof -
    1.43 -  have  "(a < b) = (a + (- b) < b + (-b))"  
    1.44 -    by (simp only: add_less_cancel_right)
    1.45 -  also have "... =  (a - b < 0)" by (simp add: diff_minus)
    1.46 +  have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
    1.47 +  also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
    1.48    finally show ?thesis .
    1.49  qed
    1.50  
    1.51 +lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
    1.52 +
    1.53  lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
    1.54  apply (subst less_iff_diff_less_0 [of a])
    1.55  apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
    1.56 @@ -781,11 +786,32 @@
    1.57  lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
    1.58  by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
    1.59  
    1.60 -lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
    1.61 -by (simp add: algebra_simps)
    1.62 +lemma diff_le_0_iff_le [simp, no_atp]:
    1.63 +  "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
    1.64 +  by (simp add: algebra_simps)
    1.65 +
    1.66 +lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
    1.67 +
    1.68 +lemma diff_eq_diff_less:
    1.69 +  "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
    1.70 +  by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
    1.71 +
    1.72 +lemma diff_eq_diff_less_eq': -- "FIXME orientation"
    1.73 +  "a - b = c - d \<Longrightarrow> b \<le> a \<longleftrightarrow> d \<le> c"
    1.74 +proof -
    1.75 +  assume "a - b = c - d"
    1.76 +  then have "b - a = d - c" by (simp add: algebra_simps)
    1.77 +  then show "b \<le> a \<longleftrightarrow> d \<le> c" by (auto simp only: le_iff_diff_le_0 [of b a] le_iff_diff_le_0 [of d c])
    1.78 +qed
    1.79  
    1.80  end
    1.81  
    1.82 +use "~~/src/HOL/Tools/abel_cancel.ML"
    1.83 +
    1.84 +ML {*
    1.85 +  Addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv];
    1.86 +*}
    1.87 +
    1.88  class linordered_ab_semigroup_add =
    1.89    linorder + ordered_ab_semigroup_add
    1.90  
    1.91 @@ -1167,42 +1193,6 @@
    1.92  
    1.93  end
    1.94  
    1.95 -text {* Needed for abelian cancellation simprocs: *}
    1.96 -
    1.97 -lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
    1.98 -apply (subst add_left_commute)
    1.99 -apply (subst add_left_cancel)
   1.100 -apply simp
   1.101 -done
   1.102 -
   1.103 -lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
   1.104 -apply (subst add_cancel_21[of _ _ _ 0, simplified])
   1.105 -apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
   1.106 -done
   1.107 -
   1.108 -lemma less_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
   1.109 -by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
   1.110 -
   1.111 -lemma le_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
   1.112 -apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])
   1.113 -apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
   1.114 -done
   1.115 -
   1.116 -lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
   1.117 -by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
   1.118 -
   1.119 -lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
   1.120 -by (simp add: diff_minus)
   1.121 -
   1.122 -lemma le_add_right_mono: 
   1.123 -  assumes 
   1.124 -  "a <= b + (c::'a::ordered_ab_group_add)"
   1.125 -  "c <= d"    
   1.126 -  shows "a <= b + d"
   1.127 -  apply (rule_tac order_trans[where y = "b+c"])
   1.128 -  apply (simp_all add: prems)
   1.129 -  done
   1.130 -
   1.131  
   1.132  subsection {* Tools setup *}
   1.133  
   1.134 @@ -1224,64 +1214,6 @@
   1.135  by (auto intro: add_strict_right_mono add_strict_left_mono
   1.136    add_less_le_mono add_le_less_mono add_strict_mono)
   1.137  
   1.138 -text{*Simplification of @{term "x-y < 0"}, etc.*}
   1.139 -lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]
   1.140 -lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
   1.141 -
   1.142 -ML {*
   1.143 -structure ab_group_add_cancel = Abel_Cancel
   1.144 -(
   1.145 -
   1.146 -(* term order for abelian groups *)
   1.147 -
   1.148 -fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
   1.149 -      [@{const_name Groups.zero}, @{const_name Groups.plus},
   1.150 -        @{const_name Groups.uminus}, @{const_name Groups.minus}]
   1.151 -  | agrp_ord _ = ~1;
   1.152 -
   1.153 -fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
   1.154 -
   1.155 -local
   1.156 -  val ac1 = mk_meta_eq @{thm add_assoc};
   1.157 -  val ac2 = mk_meta_eq @{thm add_commute};
   1.158 -  val ac3 = mk_meta_eq @{thm add_left_commute};
   1.159 -  fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
   1.160 -        SOME ac1
   1.161 -    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
   1.162 -        if termless_agrp (y, x) then SOME ac3 else NONE
   1.163 -    | solve_add_ac thy _ (_ $ x $ y) =
   1.164 -        if termless_agrp (y, x) then SOME ac2 else NONE
   1.165 -    | solve_add_ac thy _ _ = NONE
   1.166 -in
   1.167 -  val add_ac_proc = Simplifier.simproc @{theory}
   1.168 -    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
   1.169 -end;
   1.170 -
   1.171 -val eq_reflection = @{thm eq_reflection};
   1.172 -  
   1.173 -val T = @{typ "'a::ab_group_add"};
   1.174 -
   1.175 -val cancel_ss = HOL_basic_ss settermless termless_agrp
   1.176 -  addsimprocs [add_ac_proc] addsimps
   1.177 -  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
   1.178 -   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
   1.179 -   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
   1.180 -   @{thm minus_add_cancel}];
   1.181 -
   1.182 -val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
   1.183 -  
   1.184 -val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
   1.185 -
   1.186 -val dest_eqI = 
   1.187 -  fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
   1.188 -
   1.189 -);
   1.190 -*}
   1.191 -
   1.192 -ML {*
   1.193 -  Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
   1.194 -*}
   1.195 -
   1.196  code_modulename SML
   1.197    Groups Arith
   1.198  
     2.1 --- a/src/HOL/IsaMakefile	Mon Jul 19 12:17:38 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Jul 19 16:09:43 2010 +0200
     2.3 @@ -168,6 +168,7 @@
     2.4    SAT.thy \
     2.5    Set.thy \
     2.6    Sum_Type.thy \
     2.7 +  Tools/abel_cancel.ML \
     2.8    Tools/arith_data.ML \
     2.9    Tools/cnf_funcs.ML \
    2.10    Tools/Datatype/datatype_abs_proofs.ML \
    2.11 @@ -219,7 +220,6 @@
    2.12    Transitive_Closure.thy \
    2.13    Typedef.thy \
    2.14    Wellfounded.thy \
    2.15 -  $(SRC)/Provers/Arith/abel_cancel.ML \
    2.16    $(SRC)/Provers/Arith/cancel_div_mod.ML \
    2.17    $(SRC)/Provers/Arith/cancel_sums.ML \
    2.18    $(SRC)/Provers/Arith/fast_lin_arith.ML \
     3.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Mon Jul 19 12:17:38 2010 +0200
     3.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Mon Jul 19 16:09:43 2010 +0200
     3.3 @@ -376,9 +376,10 @@
     3.4    "a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" 
     3.5  proof -
     3.6    assume "a+b <= c"
     3.7 -  hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
     3.8 -  have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
     3.9 -  show ?thesis by (rule le_add_right_mono[OF 2 3])
    3.10 +  then have "a <= c+(-b)" by (simp add: algebra_simps)
    3.11 +  have "(-b) <= abs b" by (rule abs_ge_minus_self)
    3.12 +  then have "c + (- b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono)
    3.13 +  with `a \<le> c + (- b)` show ?thesis by (rule order_trans)
    3.14  qed
    3.15  
    3.16  class lattice_ring = ordered_ring + lattice_ab_group_add_abs
    3.17 @@ -411,7 +412,7 @@
    3.18      apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
    3.19      done
    3.20    have yx: "?y <= ?x"
    3.21 -    apply (simp add:diff_def)
    3.22 +    apply (simp add:diff_minus)
    3.23      apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
    3.24      apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
    3.25      done
     4.1 --- a/src/HOL/Matrix/LP.thy	Mon Jul 19 12:17:38 2010 +0200
     4.2 +++ b/src/HOL/Matrix/LP.thy	Mon Jul 19 16:09:43 2010 +0200
     4.3 @@ -6,6 +6,15 @@
     4.4  imports Main Lattice_Algebras
     4.5  begin
     4.6  
     4.7 +lemma le_add_right_mono: 
     4.8 +  assumes 
     4.9 +  "a <= b + (c::'a::ordered_ab_group_add)"
    4.10 +  "c <= d"    
    4.11 +  shows "a <= b + d"
    4.12 +  apply (rule_tac order_trans[where y = "b+c"])
    4.13 +  apply (simp_all add: prems)
    4.14 +  done
    4.15 +
    4.16  lemma linprog_dual_estimate:
    4.17    assumes
    4.18    "A * x \<le> (b::'a::lattice_ring)"
    4.19 @@ -49,8 +58,8 @@
    4.20      done    
    4.21    from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
    4.22      by (simp)
    4.23 -  show ?thesis 
    4.24 -    apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
    4.25 +  show ?thesis
    4.26 +    apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
    4.27      apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
    4.28      done
    4.29  qed
    4.30 @@ -138,9 +147,9 @@
    4.31    then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
    4.32    then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
    4.33    have s2: "c - y * A <= c2 - y * A1"
    4.34 -    by (simp add: diff_def prems add_mono mult_left_mono)
    4.35 +    by (simp add: diff_minus prems add_mono mult_left_mono)
    4.36    have s1: "c1 - y * A2 <= c - y * A"
    4.37 -    by (simp add: diff_def prems add_mono mult_left_mono)
    4.38 +    by (simp add: diff_minus prems add_mono mult_left_mono)
    4.39    have prts: "(c - y * A) * x <= ?C"
    4.40      apply (simp add: Let_def)
    4.41      apply (rule mult_le_prts)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/abel_cancel.ML	Mon Jul 19 16:09:43 2010 +0200
     5.3 @@ -0,0 +1,139 @@
     5.4 +(*  Title:      HOL/Tools/abel_cancel.ML
     5.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.6 +    Copyright   1998  University of Cambridge
     5.7 +
     5.8 +Simplification procedures for abelian groups:
     5.9 +- Cancel complementary terms in sums.
    5.10 +- Cancel like terms on opposite sides of relations.
    5.11 +*)
    5.12 +
    5.13 +signature ABEL_CANCEL =
    5.14 +sig
    5.15 +  val sum_conv: simproc
    5.16 +  val rel_conv: simproc
    5.17 +end;
    5.18 +
    5.19 +structure Abel_Cancel: ABEL_CANCEL =
    5.20 +struct
    5.21 +
    5.22 +(* term order for abelian groups *)
    5.23 +
    5.24 +fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
    5.25 +      [@{const_name Groups.zero}, @{const_name Groups.plus},
    5.26 +        @{const_name Groups.uminus}, @{const_name Groups.minus}]
    5.27 +  | agrp_ord _ = ~1;
    5.28 +
    5.29 +fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
    5.30 +
    5.31 +local
    5.32 +  val ac1 = mk_meta_eq @{thm add_assoc};
    5.33 +  val ac2 = mk_meta_eq @{thm add_commute};
    5.34 +  val ac3 = mk_meta_eq @{thm add_left_commute};
    5.35 +  fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
    5.36 +        SOME ac1
    5.37 +    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
    5.38 +        if termless_agrp (y, x) then SOME ac3 else NONE
    5.39 +    | solve_add_ac thy _ (_ $ x $ y) =
    5.40 +        if termless_agrp (y, x) then SOME ac2 else NONE
    5.41 +    | solve_add_ac thy _ _ = NONE
    5.42 +in
    5.43 +  val add_ac_proc = Simplifier.simproc @{theory}
    5.44 +    "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
    5.45 +end;
    5.46 +
    5.47 +val cancel_ss = HOL_basic_ss settermless termless_agrp
    5.48 +  addsimprocs [add_ac_proc] addsimps
    5.49 +  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
    5.50 +   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
    5.51 +   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
    5.52 +   @{thm minus_add_cancel}];
    5.53 +
    5.54 +val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
    5.55 +  
    5.56 +val eqI_rules = [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq'}, @{thm diff_eq_diff_eq}];
    5.57 +
    5.58 +val dest_eqI = 
    5.59 +  fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
    5.60 +
    5.61 +fun zero t = Const (@{const_name Groups.zero}, t);
    5.62 +fun minus t = Const (@{const_name Groups.uminus}, t --> t);
    5.63 +
    5.64 +fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
    5.65 +      add_terms pos (x, add_terms pos (y, ts))
    5.66 +  | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
    5.67 +      add_terms pos (x, add_terms (not pos) (y, ts))
    5.68 +  | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
    5.69 +      add_terms (not pos) (x, ts)
    5.70 +  | add_terms pos (x, ts) = (pos,x) :: ts;
    5.71 +
    5.72 +fun terms fml = add_terms true (fml, []);
    5.73 +
    5.74 +fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
    5.75 +      (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
    5.76 +                                   | SOME z => SOME(c $ x $ z))
    5.77 +       | SOME z => SOME(c $ z $ y))
    5.78 +  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
    5.79 +      (case zero1 (pos,t) x of
    5.80 +         NONE => (case zero1 (not pos,t) y of NONE => NONE
    5.81 +                  | SOME z => SOME(c $ x $ z))
    5.82 +       | SOME z => SOME(c $ z $ y))
    5.83 +  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
    5.84 +      (case zero1 (not pos,t) x of NONE => NONE
    5.85 +       | SOME z => SOME(c $ z))
    5.86 +  | zero1 (pos,t) u =
    5.87 +      if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE
    5.88 +
    5.89 +exception Cancel;
    5.90 +
    5.91 +fun find_common _ [] _ = raise Cancel
    5.92 +  | find_common opp ((p,l)::ls) rs =
    5.93 +      let val pr = if opp then not p else p
    5.94 +      in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l)
    5.95 +         else find_common opp ls rs
    5.96 +      end
    5.97 +
    5.98 +(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
    5.99 +   If OP = +, it must be t2(-t) rather than t2(t)
   5.100 +*)
   5.101 +fun cancel t =
   5.102 +  let
   5.103 +    val c $ lhs $ rhs = t
   5.104 +    val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
   5.105 +    val (pos,l) = find_common opp (terms lhs) (terms rhs)
   5.106 +    val posr = if opp then not pos else pos
   5.107 +    val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
   5.108 +  in t' end;
   5.109 +
   5.110 +
   5.111 +(*A simproc to cancel complementary terms in arbitrary sums.*)
   5.112 +fun sum_proc ss t =
   5.113 +   let
   5.114 +     val t' = cancel t
   5.115 +     val thm =
   5.116 +       Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
   5.117 +         (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
   5.118 +   in SOME thm end handle Cancel => NONE;
   5.119 +
   5.120 +val sum_conv =
   5.121 +  Simplifier.mk_simproc "cancel_sums"
   5.122 +    (map (Drule.cterm_fun Logic.varify_global) sum_pats) (K sum_proc);
   5.123 +
   5.124 +
   5.125 +(*A simproc to cancel like terms on the opposite sides of relations:
   5.126 +   (x + y - z < -z + x) = (y < 0)
   5.127 +  Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
   5.128 +  Reduces the problem to subtraction.*)
   5.129 +fun rel_proc ss t =
   5.130 +  let
   5.131 +    val t' = cancel t
   5.132 +    val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
   5.133 +      (fn _ => rtac @{thm eq_reflection} 1 THEN
   5.134 +                    resolve_tac eqI_rules 1 THEN
   5.135 +                    simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
   5.136 +   in SOME thm end handle Cancel => NONE;
   5.137 +
   5.138 +val rel_conv =
   5.139 +  Simplifier.mk_simproc "cancel_relations"
   5.140 +    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (dest_eqI th)) eqI_rules) (K rel_proc);
   5.141 +
   5.142 +end;
     6.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Jul 19 12:17:38 2010 +0200
     6.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Jul 19 16:09:43 2010 +0200
     6.3 @@ -818,7 +818,7 @@
     6.4          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
     6.5          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
     6.6          @{thm "not_one_less_zero"}]
     6.7 -      addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
     6.8 +      addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv]
     6.9         (*abel_cancel helps it work in abstract algebraic domains*)
    6.10        addsimprocs Nat_Arith.nat_cancel_sums_add
    6.11        addcongs [@{thm if_weak_cong}],
     7.1 --- a/src/Provers/Arith/abel_cancel.ML	Mon Jul 19 12:17:38 2010 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,111 +0,0 @@
     7.4 -(*  Title:      Provers/Arith/abel_cancel.ML
     7.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.6 -    Copyright   1998  University of Cambridge
     7.7 -
     7.8 -Simplification procedures for abelian groups (e.g. integers, reals,
     7.9 -polymorphic types).
    7.10 -
    7.11 -- Cancel complementary terms in sums
    7.12 -- Cancel like terms on opposite sides of relations
    7.13 -*)
    7.14 -
    7.15 -signature ABEL_CANCEL =
    7.16 -sig
    7.17 -  val eq_reflection   : thm           (*object-equality to meta-equality*)
    7.18 -  val T               : typ           (*the type of group elements*)
    7.19 -  val cancel_ss       : simpset       (*abelian group cancel simpset*)
    7.20 -  val sum_pats        : cterm list
    7.21 -  val eqI_rules       : thm list
    7.22 -  val dest_eqI        : thm -> term
    7.23 -end;
    7.24 -
    7.25 -
    7.26 -functor Abel_Cancel (Data: ABEL_CANCEL) =
    7.27 -struct
    7.28 -
    7.29 -open Data;
    7.30 -
    7.31 -(* FIXME dependent on abstract syntax *)
    7.32 -
    7.33 -fun zero t = Const (@{const_name Groups.zero}, t);
    7.34 -fun minus t = Const (@{const_name Groups.uminus}, t --> t);
    7.35 -
    7.36 -fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
    7.37 -      add_terms pos (x, add_terms pos (y, ts))
    7.38 -  | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
    7.39 -      add_terms pos (x, add_terms (not pos) (y, ts))
    7.40 -  | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
    7.41 -      add_terms (not pos) (x, ts)
    7.42 -  | add_terms pos (x, ts) = (pos,x) :: ts;
    7.43 -
    7.44 -fun terms fml = add_terms true (fml, []);
    7.45 -
    7.46 -fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
    7.47 -      (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
    7.48 -                                   | SOME z => SOME(c $ x $ z))
    7.49 -       | SOME z => SOME(c $ z $ y))
    7.50 -  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
    7.51 -      (case zero1 (pos,t) x of
    7.52 -         NONE => (case zero1 (not pos,t) y of NONE => NONE
    7.53 -                  | SOME z => SOME(c $ x $ z))
    7.54 -       | SOME z => SOME(c $ z $ y))
    7.55 -  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
    7.56 -      (case zero1 (not pos,t) x of NONE => NONE
    7.57 -       | SOME z => SOME(c $ z))
    7.58 -  | zero1 (pos,t) u =
    7.59 -      if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE
    7.60 -
    7.61 -exception Cancel;
    7.62 -
    7.63 -fun find_common _ [] _ = raise Cancel
    7.64 -  | find_common opp ((p,l)::ls) rs =
    7.65 -      let val pr = if opp then not p else p
    7.66 -      in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l)
    7.67 -         else find_common opp ls rs
    7.68 -      end
    7.69 -
    7.70 -(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
    7.71 -   If OP = +, it must be t2(-t) rather than t2(t)
    7.72 -*)
    7.73 -fun cancel t =
    7.74 -  let
    7.75 -    val c $ lhs $ rhs = t
    7.76 -    val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
    7.77 -    val (pos,l) = find_common opp (terms lhs) (terms rhs)
    7.78 -    val posr = if opp then not pos else pos
    7.79 -    val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
    7.80 -  in t' end;
    7.81 -
    7.82 -
    7.83 -(*A simproc to cancel complementary terms in arbitrary sums.*)
    7.84 -fun sum_proc ss t =
    7.85 -   let
    7.86 -     val t' = cancel t
    7.87 -     val thm =
    7.88 -       Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
    7.89 -         (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
    7.90 -   in SOME thm end handle Cancel => NONE;
    7.91 -
    7.92 -val sum_conv =
    7.93 -  Simplifier.mk_simproc "cancel_sums"
    7.94 -    (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc);
    7.95 -
    7.96 -
    7.97 -(*A simproc to cancel like terms on the opposite sides of relations:
    7.98 -   (x + y - z < -z + x) = (y < 0)
    7.99 -  Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
   7.100 -  Reduces the problem to subtraction.*)
   7.101 -fun rel_proc ss t =
   7.102 -  let
   7.103 -    val t' = cancel t
   7.104 -    val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
   7.105 -      (fn _ => rtac eq_reflection 1 THEN
   7.106 -                    resolve_tac eqI_rules 1 THEN
   7.107 -                    simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
   7.108 -   in SOME thm end handle Cancel => NONE;
   7.109 -
   7.110 -val rel_conv =
   7.111 -  Simplifier.mk_simproc "cancel_relations"
   7.112 -    (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc);
   7.113 -
   7.114 -end;