replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
authorhuffman
Fri Jul 27 15:42:39 2012 +0200 (2012-07-27)
changeset 4855662a3fbf9d35b
parent 48555 be4bf5f6b2ef
child 48557 2aa8bab841d7
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
src/HOL/Groups.thy
src/HOL/IsaMakefile
src/HOL/Tools/abel_cancel.ML
src/HOL/Tools/group_cancel.ML
src/HOL/Tools/lin_arith.ML
src/HOL/ex/Simproc_Tests.thy
     1.1 --- a/src/HOL/Groups.thy	Fri Jul 27 14:56:37 2012 +0200
     1.2 +++ b/src/HOL/Groups.thy	Fri Jul 27 15:42:39 2012 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  theory Groups
     1.6  imports Orderings
     1.7 -uses ("Tools/abel_cancel.ML")
     1.8 +uses ("Tools/group_cancel.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Fact collections *}
    1.12 @@ -472,6 +472,9 @@
    1.13  lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
    1.14    by (rule right_minus_eq)
    1.15  
    1.16 +lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
    1.17 +  by (simp add: diff_minus add_ac)
    1.18 +
    1.19  end
    1.20  
    1.21  
    1.22 @@ -827,15 +830,22 @@
    1.23  
    1.24  end
    1.25  
    1.26 -use "Tools/abel_cancel.ML"
    1.27 +use "Tools/group_cancel.ML"
    1.28 +
    1.29 +simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
    1.30 +  {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
    1.31 +
    1.32 +simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
    1.33 +  {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}
    1.34  
    1.35 -simproc_setup abel_cancel_sum
    1.36 -  ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
    1.37 -  {* fn phi => Abel_Cancel.sum_proc *}
    1.38 +simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
    1.39 +  {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}
    1.40  
    1.41 -simproc_setup abel_cancel_relation
    1.42 -  ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
    1.43 -  {* fn phi => Abel_Cancel.rel_proc *}
    1.44 +simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
    1.45 +  {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}
    1.46 +
    1.47 +simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
    1.48 +  {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}
    1.49  
    1.50  class linordered_ab_semigroup_add =
    1.51    linorder + ordered_ab_semigroup_add
     2.1 --- a/src/HOL/IsaMakefile	Fri Jul 27 14:56:37 2012 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Jul 27 15:42:39 2012 +0200
     2.3 @@ -245,10 +245,10 @@
     2.4    Tools/Metis/metis_generate.ML \
     2.5    Tools/Metis/metis_reconstruct.ML \
     2.6    Tools/Metis/metis_tactic.ML \
     2.7 -  Tools/abel_cancel.ML \
     2.8    Tools/arith_data.ML \
     2.9    Tools/cnf_funcs.ML \
    2.10    Tools/enriched_type.ML \
    2.11 +  Tools/group_cancel.ML \
    2.12    Tools/inductive.ML \
    2.13    Tools/inductive_realizer.ML \
    2.14    Tools/inductive_set.ML \
     3.1 --- a/src/HOL/Tools/abel_cancel.ML	Fri Jul 27 14:56:37 2012 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,132 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/abel_cancel.ML
     3.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.6 -    Copyright   1998  University of Cambridge
     3.7 -
     3.8 -Simplification procedures for abelian groups:
     3.9 -- Cancel complementary terms in sums.
    3.10 -- Cancel like terms on opposite sides of relations.
    3.11 -*)
    3.12 -
    3.13 -signature ABEL_CANCEL =
    3.14 -sig
    3.15 -  val sum_proc: simpset -> cterm -> thm option
    3.16 -  val rel_proc: simpset -> cterm -> thm option
    3.17 -end;
    3.18 -
    3.19 -structure Abel_Cancel: ABEL_CANCEL =
    3.20 -struct
    3.21 -
    3.22 -(** compute cancellation **)
    3.23 -
    3.24 -fun add_atoms pos (Const (@{const_name Groups.plus}, _) $ x $ y) =
    3.25 -      add_atoms pos x #> add_atoms pos y
    3.26 -  | add_atoms pos (Const (@{const_name Groups.minus}, _) $ x $ y) =
    3.27 -      add_atoms pos x #> add_atoms (not pos) y
    3.28 -  | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) =
    3.29 -      add_atoms (not pos) x
    3.30 -  | add_atoms pos (Const (@{const_name Groups.zero}, _)) = I
    3.31 -  | add_atoms pos x = cons (pos, x);
    3.32 -
    3.33 -fun atoms t = add_atoms true t [];
    3.34 -
    3.35 -fun zerofy pt ((c as Const (@{const_name Groups.plus}, _)) $ x $ y) =
    3.36 -      (case zerofy pt x of NONE =>
    3.37 -        (case zerofy pt y of NONE => NONE
    3.38 -         | SOME z => SOME (c $ x $ z))
    3.39 -       | SOME z => SOME (c $ z $ y))
    3.40 -  | zerofy pt ((c as Const (@{const_name Groups.minus}, _)) $ x $ y) =
    3.41 -      (case zerofy pt x of NONE =>
    3.42 -        (case zerofy (apfst not pt) y of NONE => NONE
    3.43 -         | SOME z => SOME (c $ x $ z))
    3.44 -       | SOME z => SOME (c $ z $ y))
    3.45 -  | zerofy pt ((c as Const (@{const_name Groups.uminus}, _)) $ x) =
    3.46 -      (case zerofy (apfst not pt) x of NONE => NONE
    3.47 -       | SOME z => SOME (c $ z))
    3.48 -  | zerofy (pos, t) u =
    3.49 -      if pos andalso (t aconv u)
    3.50 -        then SOME (Const (@{const_name Groups.zero}, fastype_of t))
    3.51 -        else NONE
    3.52 -
    3.53 -exception Cancel;
    3.54 -
    3.55 -fun find_common _ [] _ = raise Cancel
    3.56 -  | find_common opp ((p, l) :: ls) rs =
    3.57 -      let val pr = if opp then not p else p
    3.58 -      in if exists (fn (q, r) => pr = q andalso l aconv r) rs then (p, l)
    3.59 -         else find_common opp ls rs
    3.60 -      end
    3.61 -
    3.62 -(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
    3.63 -   If OP = +, it must be t2(-t) rather than t2(t)
    3.64 -*)
    3.65 -fun cancel (c $ lhs $ rhs) =
    3.66 -  let
    3.67 -    val opp = case c of Const(@{const_name Groups.plus}, _) => true | _ => false;
    3.68 -    val (pos, l) = find_common opp (atoms lhs) (atoms rhs);
    3.69 -    val posr = if opp then not pos else pos;
    3.70 -  in c $ the (zerofy (pos, l) lhs) $ the (zerofy (posr, l) rhs) end;
    3.71 -
    3.72 -
    3.73 -(** prove cancellation **)
    3.74 -
    3.75 -fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
    3.76 -      [@{const_name Groups.zero}, @{const_name Groups.plus},
    3.77 -        @{const_name Groups.uminus}, @{const_name Groups.minus}]
    3.78 -  | agrp_ord _ = ~1;
    3.79 -
    3.80 -fun less_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
    3.81 -
    3.82 -fun solve (_ $ (Const (@{const_name Groups.plus}, _) $ _ $ _) $ _) =
    3.83 -      SOME @{thm add_assoc [THEN eq_reflection]}
    3.84 -  | solve (_ $ x $ (Const (@{const_name Groups.plus}, _) $ y $ _)) =
    3.85 -      if less_agrp (y, x) then
    3.86 -        SOME @{thm add_left_commute [THEN eq_reflection]}
    3.87 -        else NONE
    3.88 -  | solve (_ $ x $ y) =
    3.89 -      if less_agrp (y, x) then
    3.90 -        SOME @{thm add_commute [THEN eq_reflection]} else
    3.91 -        NONE
    3.92 -  | solve _ = NONE;
    3.93 -  
    3.94 -val simproc = Simplifier.simproc_global @{theory}
    3.95 -  "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
    3.96 -
    3.97 -val cancel_ss = (HOL_basic_ss |> Simplifier.set_termless less_agrp)
    3.98 -  addsimprocs [simproc] addsimps
    3.99 -  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
   3.100 -   @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
   3.101 -   @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
   3.102 -   @{thm minus_add_cancel}];
   3.103 -
   3.104 -fun cancel_simp_tac ss = simp_tac (Simplifier.inherit_context ss cancel_ss);
   3.105 -
   3.106 -
   3.107 -(** simprocs **)
   3.108 -
   3.109 -(* cancel complementary terms in arbitrary sums *)
   3.110 -
   3.111 -fun sum_proc ss ct =
   3.112 -  let
   3.113 -    val t = Thm.term_of ct;
   3.114 -    val prop = Logic.mk_equals (t, cancel t);
   3.115 -    val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
   3.116 -      (fn _ => cancel_simp_tac ss 1)
   3.117 -  in SOME thm end handle Cancel => NONE;
   3.118 -
   3.119 -
   3.120 -(* cancel like terms on the opposite sides of relations:
   3.121 -    (x + y - z < -z + x) = (y < 0)
   3.122 -   Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
   3.123 -   Reduces the problem to subtraction. *)
   3.124 -
   3.125 -fun rel_proc ss ct =
   3.126 -  let
   3.127 -    val t = Thm.term_of ct;
   3.128 -    val prop = Logic.mk_equals (t, cancel t);
   3.129 -    val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
   3.130 -      (fn _ => rtac @{thm eq_reflection} 1 THEN
   3.131 -        resolve_tac [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}] 1 THEN
   3.132 -        cancel_simp_tac ss 1)
   3.133 -  in SOME thm end handle Cancel => NONE;
   3.134 -
   3.135 -end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/group_cancel.ML	Fri Jul 27 15:42:39 2012 +0200
     4.3 @@ -0,0 +1,89 @@
     4.4 +(*  Title:      HOL/Tools/group_cancel.ML
     4.5 +    Author:     Brian Huffman, TU Munich
     4.6 +
     4.7 +Simplification procedures for abelian groups:
     4.8 +- Cancel complementary terms in sums.
     4.9 +- Cancel like terms on opposite sides of relations.
    4.10 +*)
    4.11 +
    4.12 +signature GROUP_CANCEL =
    4.13 +sig
    4.14 +  val cancel_diff_conv: conv
    4.15 +  val cancel_eq_conv: conv
    4.16 +  val cancel_le_conv: conv
    4.17 +  val cancel_less_conv: conv
    4.18 +  val cancel_add_conv: conv
    4.19 +end
    4.20 +
    4.21 +structure Group_Cancel: GROUP_CANCEL =
    4.22 +struct
    4.23 +
    4.24 +val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
    4.25 +      by (simp only: add_ac)}
    4.26 +val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
    4.27 +      by (simp only: add_ac)}
    4.28 +val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
    4.29 +      by (simp only: add_diff_eq)}
    4.30 +val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
    4.31 +      by (simp only: diff_minus minus_add add_ac)}
    4.32 +val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
    4.33 +      by (simp only: minus_add_distrib)}
    4.34 +val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
    4.35 +      by (simp only: add_0_right)}
    4.36 +val minus_minus = mk_meta_eq @{thm minus_minus}
    4.37 +
    4.38 +fun move_to_front path = Conv.every_conv
    4.39 +    [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
    4.40 +     Conv.arg1_conv (Conv.repeat_conv (Conv.rewr_conv minus_minus))]
    4.41 +
    4.42 +fun add_atoms pos path (Const (@{const_name Groups.plus}, _) $ x $ y) =
    4.43 +      add_atoms pos (add1::path) x #> add_atoms pos (add2::path) y
    4.44 +  | add_atoms pos path (Const (@{const_name Groups.minus}, _) $ x $ y) =
    4.45 +      add_atoms pos (sub1::path) x #> add_atoms (not pos) (sub2::path) y
    4.46 +  | add_atoms pos path (Const (@{const_name Groups.uminus}, _) $ x) =
    4.47 +      add_atoms (not pos) (neg1::path) x
    4.48 +  | add_atoms _ _ (Const (@{const_name Groups.zero}, _)) = I
    4.49 +  | add_atoms pos path x = cons ((pos, x), path)
    4.50 +
    4.51 +fun atoms t = add_atoms true [] t []
    4.52 +
    4.53 +val coeff_ord = prod_ord bool_ord Term_Ord.term_ord
    4.54 +
    4.55 +exception Cancel
    4.56 +
    4.57 +fun find_common ord xs ys =
    4.58 +  let
    4.59 +    fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
    4.60 +        (case ord (x, y) of
    4.61 +          EQUAL => (px, py)
    4.62 +        | LESS => find xs' ys
    4.63 +        | GREATER => find xs ys')
    4.64 +      | find _ _ = raise Cancel
    4.65 +    fun ord' ((x, _), (y, _)) = ord (x, y)
    4.66 +  in
    4.67 +    find (sort ord' xs) (sort ord' ys)
    4.68 +  end
    4.69 +
    4.70 +fun cancel_conv rule ct =
    4.71 +  let
    4.72 +    val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
    4.73 +    val (lpath, rpath) = find_common coeff_ord (atoms lhs) (atoms rhs)
    4.74 +    val lconv = move_to_front lpath
    4.75 +    val rconv = move_to_front rpath
    4.76 +    val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
    4.77 +    val conv = conv1 then_conv Conv.rewr_conv rule
    4.78 +  in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
    4.79 +
    4.80 +val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm add_diff_cancel_left})
    4.81 +val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
    4.82 +val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
    4.83 +val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})
    4.84 +
    4.85 +val diff_minus_eq_add = mk_meta_eq @{thm diff_minus_eq_add}
    4.86 +val add_eq_diff_minus = Thm.symmetric diff_minus_eq_add
    4.87 +val cancel_add_conv = Conv.every_conv
    4.88 +  [Conv.rewr_conv add_eq_diff_minus,
    4.89 +   cancel_diff_conv,
    4.90 +   Conv.rewr_conv diff_minus_eq_add]
    4.91 +
    4.92 +end
     5.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Jul 27 14:56:37 2012 +0200
     5.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Jul 27 15:42:39 2012 +0200
     5.3 @@ -811,7 +811,9 @@
     5.4          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
     5.5          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
     5.6          @{thm "not_one_less_zero"}]
     5.7 -      addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
     5.8 +      addsimprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff},
     5.9 +                   @{simproc group_cancel_eq}, @{simproc group_cancel_le},
    5.10 +                   @{simproc group_cancel_less}]
    5.11         (*abel_cancel helps it work in abstract algebraic domains*)
    5.12        addsimprocs Nat_Arith.nat_cancel_sums_add
    5.13        |> Simplifier.add_cong @{thm if_weak_cong},
     6.1 --- a/src/HOL/ex/Simproc_Tests.thy	Fri Jul 27 14:56:37 2012 +0200
     6.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Fri Jul 27 15:42:39 2012 +0200
     6.3 @@ -50,13 +50,13 @@
     6.4    fix a b c u :: "'a::ab_group_add"
     6.5    {
     6.6      assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u"
     6.7 -      by (tactic {* test [@{simproc abel_cancel_sum}] *}) fact
     6.8 +      by (tactic {* test [@{simproc group_cancel_diff}] *}) fact
     6.9    next
    6.10      assume "a + 0 = b + 0" have "a + c = b + c"
    6.11 -      by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact
    6.12 +      by (tactic {* test [@{simproc group_cancel_eq}] *}) fact
    6.13    }
    6.14  end
    6.15 -(* TODO: more tests for Groups.abel_cancel_{sum,relation} *)
    6.16 +(* TODO: more tests for Groups.group_cancel_{add,diff,eq,less,le} *)
    6.17  
    6.18  subsection {* @{text int_combine_numerals} *}
    6.19