# HG changeset patch # User huffman # Date 1343396559 -7200 # Node ID 62a3fbf9d35beaf337787c6aadd9f368c57d01d9 # Parent be4bf5f6b2ef9f1a196c20fdda97094aabe1e137 replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones diff -r be4bf5f6b2ef -r 62a3fbf9d35b src/HOL/Groups.thy --- a/src/HOL/Groups.thy Fri Jul 27 14:56:37 2012 +0200 +++ b/src/HOL/Groups.thy Fri Jul 27 15:42:39 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 \ 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 \ (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") = - {* fn phi => Abel_Cancel.rel_proc *} +simproc_setup group_cancel_le ("a \ (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 diff -r be4bf5f6b2ef -r 62a3fbf9d35b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Jul 27 14:56:37 2012 +0200 +++ b/src/HOL/IsaMakefile Fri Jul 27 15:42:39 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 \ diff -r be4bf5f6b2ef -r 62a3fbf9d35b src/HOL/Tools/abel_cancel.ML --- a/src/HOL/Tools/abel_cancel.ML Fri Jul 27 14:56:37 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; diff -r be4bf5f6b2ef -r 62a3fbf9d35b src/HOL/Tools/group_cancel.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/group_cancel.ML Fri Jul 27 15:42:39 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 diff -r be4bf5f6b2ef -r 62a3fbf9d35b src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Jul 27 14:56:37 2012 +0200 +++ b/src/HOL/Tools/lin_arith.ML Fri Jul 27 15:42:39 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}, diff -r be4bf5f6b2ef -r 62a3fbf9d35b src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Fri Jul 27 14:56:37 2012 +0200 +++ b/src/HOL/ex/Simproc_Tests.thy Fri Jul 27 15:42:39 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} *}