--- a/src/HOL/Groups.thy Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Groups.thy Mon Jul 19 16:09:43 2010 +0200
@@ -6,7 +6,7 @@
theory Groups
imports Orderings
-uses ("~~/src/Provers/Arith/abel_cancel.ML")
+uses ("~~/src/HOL/Tools/abel_cancel.ML")
begin
subsection {* Fact collections *}
@@ -146,8 +146,6 @@
class times =
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-use "~~/src/Provers/Arith/abel_cancel.ML"
-
subsection {* Semigroups and Monoids *}
@@ -453,8 +451,13 @@
lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
by (simp add: algebra_simps)
+lemma diff_eq_diff_eq:
+ "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
+ by (auto simp add: algebra_simps)
+
end
+
subsection {* (Partially) Ordered Groups *}
text {*
@@ -755,14 +758,16 @@
lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
by (auto simp add: le_less minus_less_iff)
-lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
+lemma diff_less_0_iff_less [simp, no_atp]:
+ "a - b < 0 \<longleftrightarrow> a < b"
proof -
- have "(a < b) = (a + (- b) < b + (-b))"
- by (simp only: add_less_cancel_right)
- also have "... = (a - b < 0)" by (simp add: diff_minus)
+ have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
+ also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
finally show ?thesis .
qed
+lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
+
lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
apply (subst less_iff_diff_less_0 [of a])
apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
@@ -781,11 +786,32 @@
lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
-lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
-by (simp add: algebra_simps)
+lemma diff_le_0_iff_le [simp, no_atp]:
+ "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
+ by (simp add: algebra_simps)
+
+lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
+
+lemma diff_eq_diff_less:
+ "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
+ by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
+
+lemma diff_eq_diff_less_eq': -- "FIXME orientation"
+ "a - b = c - d \<Longrightarrow> b \<le> a \<longleftrightarrow> d \<le> c"
+proof -
+ assume "a - b = c - d"
+ then have "b - a = d - c" by (simp add: algebra_simps)
+ 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])
+qed
end
+use "~~/src/HOL/Tools/abel_cancel.ML"
+
+ML {*
+ Addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv];
+*}
+
class linordered_ab_semigroup_add =
linorder + ordered_ab_semigroup_add
@@ -1167,42 +1193,6 @@
end
-text {* Needed for abelian cancellation simprocs: *}
-
-lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
-apply (subst add_left_commute)
-apply (subst add_left_cancel)
-apply simp
-done
-
-lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
-apply (subst add_cancel_21[of _ _ _ 0, simplified])
-apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
-done
-
-lemma less_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
-by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
-
-lemma le_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
-apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of y' x'])
-apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
-done
-
-lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
-by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
-
-lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
-by (simp add: diff_minus)
-
-lemma le_add_right_mono:
- assumes
- "a <= b + (c::'a::ordered_ab_group_add)"
- "c <= d"
- shows "a <= b + d"
- apply (rule_tac order_trans[where y = "b+c"])
- apply (simp_all add: prems)
- done
-
subsection {* Tools setup *}
@@ -1224,64 +1214,6 @@
by (auto intro: add_strict_right_mono add_strict_left_mono
add_less_le_mono add_le_less_mono add_strict_mono)
-text{*Simplification of @{term "x-y < 0"}, etc.*}
-lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
-
-ML {*
-structure ab_group_add_cancel = Abel_Cancel
-(
-
-(* 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);
-
-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;
-
-val eq_reflection = @{thm eq_reflection};
-
-val T = @{typ "'a::ab_group_add"};
-
-val cancel_ss = HOL_basic_ss settermless termless_agrp
- addsimprocs [add_ac_proc] addsimps
- [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
- @{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 sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
-
-val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
-
-val dest_eqI =
- fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
-
-);
-*}
-
-ML {*
- Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
-*}
-
code_modulename SML
Groups Arith
--- a/src/HOL/IsaMakefile Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 19 16:09:43 2010 +0200
@@ -168,6 +168,7 @@
SAT.thy \
Set.thy \
Sum_Type.thy \
+ Tools/abel_cancel.ML \
Tools/arith_data.ML \
Tools/cnf_funcs.ML \
Tools/Datatype/datatype_abs_proofs.ML \
@@ -219,7 +220,6 @@
Transitive_Closure.thy \
Typedef.thy \
Wellfounded.thy \
- $(SRC)/Provers/Arith/abel_cancel.ML \
$(SRC)/Provers/Arith/cancel_div_mod.ML \
$(SRC)/Provers/Arith/cancel_sums.ML \
$(SRC)/Provers/Arith/fast_lin_arith.ML \
--- a/src/HOL/Library/Lattice_Algebras.thy Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy Mon Jul 19 16:09:43 2010 +0200
@@ -376,9 +376,10 @@
"a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b"
proof -
assume "a+b <= c"
- hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
- have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
- show ?thesis by (rule le_add_right_mono[OF 2 3])
+ then have "a <= c+(-b)" by (simp add: algebra_simps)
+ have "(-b) <= abs b" by (rule abs_ge_minus_self)
+ then have "c + (- b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono)
+ with `a \<le> c + (- b)` show ?thesis by (rule order_trans)
qed
class lattice_ring = ordered_ring + lattice_ab_group_add_abs
@@ -411,7 +412,7 @@
apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
done
have yx: "?y <= ?x"
- apply (simp add:diff_def)
+ apply (simp add:diff_minus)
apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
done
--- a/src/HOL/Matrix/LP.thy Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Matrix/LP.thy Mon Jul 19 16:09:43 2010 +0200
@@ -6,6 +6,15 @@
imports Main Lattice_Algebras
begin
+lemma le_add_right_mono:
+ assumes
+ "a <= b + (c::'a::ordered_ab_group_add)"
+ "c <= d"
+ shows "a <= b + d"
+ apply (rule_tac order_trans[where y = "b+c"])
+ apply (simp_all add: prems)
+ done
+
lemma linprog_dual_estimate:
assumes
"A * x \<le> (b::'a::lattice_ring)"
@@ -49,8 +58,8 @@
done
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"
by (simp)
- show ?thesis
- apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
+ show ?thesis
+ apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
done
qed
@@ -138,9 +147,9 @@
then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
have s2: "c - y * A <= c2 - y * A1"
- by (simp add: diff_def prems add_mono mult_left_mono)
+ by (simp add: diff_minus prems add_mono mult_left_mono)
have s1: "c1 - y * A2 <= c - y * A"
- by (simp add: diff_def prems add_mono mult_left_mono)
+ by (simp add: diff_minus prems add_mono mult_left_mono)
have prts: "(c - y * A) * x <= ?C"
apply (simp add: Let_def)
apply (rule mult_le_prts)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/abel_cancel.ML Mon Jul 19 16:09:43 2010 +0200
@@ -0,0 +1,139 @@
+(* Title: HOL/Tools/abel_cancel.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Simplification procedures for abelian groups:
+- Cancel complementary terms in sums.
+- Cancel like terms on opposite sides of relations.
+*)
+
+signature ABEL_CANCEL =
+sig
+ val sum_conv: simproc
+ val rel_conv: simproc
+end;
+
+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);
+
+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;
+
+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 sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
+
+val eqI_rules = [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq'}, @{thm diff_eq_diff_eq}];
+
+val dest_eqI =
+ fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
+
+fun zero t = Const (@{const_name Groups.zero}, t);
+fun minus t = Const (@{const_name Groups.uminus}, t --> t);
+
+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) =
+ (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
+
+exception Cancel;
+
+fun find_common _ [] _ = raise Cancel
+ | 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)
+ else find_common opp ls rs
+ end
+
+(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
+ If OP = +, it must be t2(-t) rather than t2(t)
+*)
+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;
+
+
+(*A simproc to cancel complementary terms in arbitrary sums.*)
+fun sum_proc ss t =
+ let
+ 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)
+ in SOME thm end handle Cancel => NONE;
+
+val sum_conv =
+ Simplifier.mk_simproc "cancel_sums"
+ (map (Drule.cterm_fun Logic.varify_global) sum_pats) (K sum_proc);
+
+
+(*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.*)
+fun rel_proc ss t =
+ let
+ 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)
+ in SOME thm end handle Cancel => NONE;
+
+val rel_conv =
+ Simplifier.mk_simproc "cancel_relations"
+ (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (dest_eqI th)) eqI_rules) (K rel_proc);
+
+end;
--- a/src/HOL/Tools/lin_arith.ML Mon Jul 19 12:17:38 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon Jul 19 16:09:43 2010 +0200
@@ -818,7 +818,7 @@
@{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
@{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
@{thm "not_one_less_zero"}]
- addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
+ addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv]
(*abel_cancel helps it work in abstract algebraic domains*)
addsimprocs Nat_Arith.nat_cancel_sums_add
addcongs [@{thm if_weak_cong}],
--- a/src/Provers/Arith/abel_cancel.ML Mon Jul 19 12:17:38 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Title: Provers/Arith/abel_cancel.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Simplification procedures for abelian groups (e.g. integers, reals,
-polymorphic types).
-
-- Cancel complementary terms in sums
-- Cancel like terms on opposite sides of relations
-*)
-
-signature ABEL_CANCEL =
-sig
- val eq_reflection : thm (*object-equality to meta-equality*)
- val T : typ (*the type of group elements*)
- val cancel_ss : simpset (*abelian group cancel simpset*)
- val sum_pats : cterm list
- val eqI_rules : thm list
- val dest_eqI : thm -> term
-end;
-
-
-functor Abel_Cancel (Data: ABEL_CANCEL) =
-struct
-
-open Data;
-
-(* FIXME dependent on abstract syntax *)
-
-fun zero t = Const (@{const_name Groups.zero}, t);
-fun minus t = Const (@{const_name Groups.uminus}, t --> t);
-
-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) =
- (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
-
-exception Cancel;
-
-fun find_common _ [] _ = raise Cancel
- | 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)
- else find_common opp ls rs
- end
-
-(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
- If OP = +, it must be t2(-t) rather than t2(t)
-*)
-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;
-
-
-(*A simproc to cancel complementary terms in arbitrary sums.*)
-fun sum_proc ss t =
- let
- 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)
- in SOME thm end handle Cancel => NONE;
-
-val sum_conv =
- Simplifier.mk_simproc "cancel_sums"
- (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc);
-
-
-(*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.*)
-fun rel_proc ss t =
- let
- val t' = cancel t
- val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
- (fn _ => rtac eq_reflection 1 THEN
- resolve_tac eqI_rules 1 THEN
- simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
- in SOME thm end handle Cancel => NONE;
-
-val rel_conv =
- Simplifier.mk_simproc "cancel_relations"
- (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc);
-
-end;