--- a/src/HOL/Groups.thy Fri Jul 27 16:33:32 2012 +0200
+++ b/src/HOL/Groups.thy Fri Jul 27 16:35:02 2012 +0200
@@ -6,7 +6,7 @@
theory Groups
imports Orderings
-uses ("Tools/abel_cancel.ML")
+uses ("Tools/group_cancel.ML")
begin
subsection {* Fact collections *}
@@ -472,6 +472,9 @@
lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
by (rule right_minus_eq)
+lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
+ by (simp add: diff_minus add_ac)
+
end
@@ -827,15 +830,22 @@
end
-use "Tools/abel_cancel.ML"
+use "Tools/group_cancel.ML"
+
+simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
+ {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
+
+simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
+ {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}
-simproc_setup abel_cancel_sum
- ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
- {* fn phi => Abel_Cancel.sum_proc *}
+simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
+ {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}
-simproc_setup abel_cancel_relation
- ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
- {* fn phi => Abel_Cancel.rel_proc *}
+simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
+ {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}
+
+simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
+ {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}
class linordered_ab_semigroup_add =
linorder + ordered_ab_semigroup_add
--- a/src/HOL/IsaMakefile Fri Jul 27 16:33:32 2012 +0200
+++ b/src/HOL/IsaMakefile Fri Jul 27 16:35:02 2012 +0200
@@ -245,10 +245,10 @@
Tools/Metis/metis_generate.ML \
Tools/Metis/metis_reconstruct.ML \
Tools/Metis/metis_tactic.ML \
- Tools/abel_cancel.ML \
Tools/arith_data.ML \
Tools/cnf_funcs.ML \
Tools/enriched_type.ML \
+ Tools/group_cancel.ML \
Tools/inductive.ML \
Tools/inductive_realizer.ML \
Tools/inductive_set.ML \
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Jul 27 16:33:32 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Jul 27 16:35:02 2012 +0200
@@ -237,17 +237,9 @@
val parse_time_option = Sledgehammer_Util.parse_time_option
val string_from_time = ATP_Util.string_from_time
-val i_subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
-fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
+val i_subscript = implode o map (prefix "\<^isub>") o Symbol.explode
fun nat_subscript n =
- let val s = signed_string_of_int n in
- if print_mode_active Symbol.xsymbolsN then
- (* cheap trick to ensure proper alphanumeric ordering for one- and
- two-digit numbers *)
- (if n <= 9 then be_subscript else i_subscript) s
- else
- s
- end
+ n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? i_subscript
fun flip_polarity Pos = Neg
| flip_polarity Neg = Pos
--- a/src/HOL/Tools/abel_cancel.ML Fri Jul 27 16:33:32 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,132 +0,0 @@
-(* 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_proc: simpset -> cterm -> thm option
- val rel_proc: simpset -> cterm -> thm option
-end;
-
-structure Abel_Cancel: ABEL_CANCEL =
-struct
-
-(** compute cancellation **)
-
-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 (Const (@{const_name Groups.zero}, _)) = I
- | add_atoms pos x = cons (pos, x);
-
-fun atoms t = add_atoms true t [];
-
-fun zerofy pt ((c as Const (@{const_name Groups.plus}, _)) $ x $ y) =
- (case zerofy pt x of NONE =>
- (case zerofy pt y of NONE => NONE
- | SOME z => SOME (c $ x $ z))
- | SOME z => SOME (c $ z $ y))
- | zerofy pt ((c as Const (@{const_name Groups.minus}, _)) $ x $ y) =
- (case zerofy pt x of NONE =>
- (case zerofy (apfst not pt) y of NONE => NONE
- | SOME z => SOME (c $ x $ z))
- | SOME z => SOME (c $ z $ y))
- | zerofy pt ((c as Const (@{const_name Groups.uminus}, _)) $ x) =
- (case zerofy (apfst not pt) x of NONE => NONE
- | SOME z => SOME (c $ z))
- | zerofy (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 =
- 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 (c $ lhs $ rhs) =
- let
- 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 (zerofy (pos, l) lhs) $ the (zerofy (posr, l) rhs) end;
-
-
-(** 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_global @{theory}
- "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
-
-val cancel_ss = (HOL_basic_ss |> Simplifier.set_termless 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 prop = Logic.mk_equals (t, cancel t);
- val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
- (fn _ => cancel_simp_tac ss 1)
- in SOME thm end handle Cancel => NONE;
-
-
-(* 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 prop = Logic.mk_equals (t, cancel t);
- val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
- (fn _ => rtac @{thm eq_reflection} 1 THEN
- 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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/group_cancel.ML Fri Jul 27 16:35:02 2012 +0200
@@ -0,0 +1,89 @@
+(* Title: HOL/Tools/group_cancel.ML
+ Author: Brian Huffman, TU Munich
+
+Simplification procedures for abelian groups:
+- Cancel complementary terms in sums.
+- Cancel like terms on opposite sides of relations.
+*)
+
+signature GROUP_CANCEL =
+sig
+ val cancel_diff_conv: conv
+ val cancel_eq_conv: conv
+ val cancel_le_conv: conv
+ val cancel_less_conv: conv
+ val cancel_add_conv: conv
+end
+
+structure Group_Cancel: GROUP_CANCEL =
+struct
+
+val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
+ by (simp only: add_ac)}
+val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
+ by (simp only: add_ac)}
+val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
+ by (simp only: add_diff_eq)}
+val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
+ by (simp only: diff_minus minus_add add_ac)}
+val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
+ by (simp only: minus_add_distrib)}
+val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
+ by (simp only: add_0_right)}
+val minus_minus = mk_meta_eq @{thm minus_minus}
+
+fun move_to_front path = Conv.every_conv
+ [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
+ Conv.arg1_conv (Conv.repeat_conv (Conv.rewr_conv minus_minus))]
+
+fun add_atoms pos path (Const (@{const_name Groups.plus}, _) $ x $ y) =
+ add_atoms pos (add1::path) x #> add_atoms pos (add2::path) y
+ | add_atoms pos path (Const (@{const_name Groups.minus}, _) $ x $ y) =
+ add_atoms pos (sub1::path) x #> add_atoms (not pos) (sub2::path) y
+ | add_atoms pos path (Const (@{const_name Groups.uminus}, _) $ x) =
+ add_atoms (not pos) (neg1::path) x
+ | add_atoms _ _ (Const (@{const_name Groups.zero}, _)) = I
+ | add_atoms pos path x = cons ((pos, x), path)
+
+fun atoms t = add_atoms true [] t []
+
+val coeff_ord = prod_ord bool_ord Term_Ord.term_ord
+
+exception Cancel
+
+fun find_common ord xs ys =
+ let
+ fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
+ (case ord (x, y) of
+ EQUAL => (px, py)
+ | LESS => find xs' ys
+ | GREATER => find xs ys')
+ | find _ _ = raise Cancel
+ fun ord' ((x, _), (y, _)) = ord (x, y)
+ in
+ find (sort ord' xs) (sort ord' ys)
+ end
+
+fun cancel_conv rule ct =
+ let
+ val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
+ val (lpath, rpath) = find_common coeff_ord (atoms lhs) (atoms rhs)
+ val lconv = move_to_front lpath
+ val rconv = move_to_front rpath
+ val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
+ val conv = conv1 then_conv Conv.rewr_conv rule
+ in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
+
+val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm add_diff_cancel_left})
+val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
+val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
+val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})
+
+val diff_minus_eq_add = mk_meta_eq @{thm diff_minus_eq_add}
+val add_eq_diff_minus = Thm.symmetric diff_minus_eq_add
+val cancel_add_conv = Conv.every_conv
+ [Conv.rewr_conv add_eq_diff_minus,
+ cancel_diff_conv,
+ Conv.rewr_conv diff_minus_eq_add]
+
+end
--- a/src/HOL/Tools/lin_arith.ML Fri Jul 27 16:33:32 2012 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Jul 27 16:35:02 2012 +0200
@@ -811,7 +811,9 @@
@{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 [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
+ addsimprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff},
+ @{simproc group_cancel_eq}, @{simproc group_cancel_le},
+ @{simproc group_cancel_less}]
(*abel_cancel helps it work in abstract algebraic domains*)
addsimprocs Nat_Arith.nat_cancel_sums_add
|> Simplifier.add_cong @{thm if_weak_cong},
--- a/src/HOL/ex/Simproc_Tests.thy Fri Jul 27 16:33:32 2012 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy Fri Jul 27 16:35:02 2012 +0200
@@ -50,13 +50,13 @@
fix a b c u :: "'a::ab_group_add"
{
assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u"
- by (tactic {* test [@{simproc abel_cancel_sum}] *}) fact
+ by (tactic {* test [@{simproc group_cancel_diff}] *}) fact
next
assume "a + 0 = b + 0" have "a + c = b + c"
- by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact
+ by (tactic {* test [@{simproc group_cancel_eq}] *}) fact
}
end
-(* TODO: more tests for Groups.abel_cancel_{sum,relation} *)
+(* TODO: more tests for Groups.group_cancel_{add,diff,eq,less,le} *)
subsection {* @{text int_combine_numerals} *}