replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
authorhuffman
Fri Jul 27 17:59:18 2012 +0200 (2012-07-27)
changeset 48560e0875d956a6b
parent 48559 686cc7c47589
child 48561 12aa0cb2b447
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
src/HOL/IsaMakefile
src/HOL/Nat.thy
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/nat_arith.ML
src/Provers/Arith/cancel_sums.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jul 27 17:57:31 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jul 27 17:59:18 2012 +0200
     1.3 @@ -171,7 +171,6 @@
     1.4  
     1.5  PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
     1.6    $(SRC)/Provers/Arith/cancel_div_mod.ML \
     1.7 -  $(SRC)/Provers/Arith/cancel_sums.ML \
     1.8    $(SRC)/Provers/Arith/fast_lin_arith.ML \
     1.9    $(SRC)/Provers/order.ML \
    1.10    $(SRC)/Provers/trancl.ML \
     2.1 --- a/src/HOL/Nat.thy	Fri Jul 27 17:57:31 2012 +0200
     2.2 +++ b/src/HOL/Nat.thy	Fri Jul 27 17:59:18 2012 +0200
     2.3 @@ -11,7 +11,6 @@
     2.4  imports Inductive Typedef Fun Fields
     2.5  uses
     2.6    "~~/src/Tools/rat.ML"
     2.7 -  "~~/src/Provers/Arith/cancel_sums.ML"
     2.8    "Tools/arith_data.ML"
     2.9    ("Tools/nat_arith.ML")
    2.10    "~~/src/Provers/Arith/fast_lin_arith.ML"
    2.11 @@ -1497,19 +1496,19 @@
    2.12  
    2.13  simproc_setup nateq_cancel_sums
    2.14    ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
    2.15 -  {* fn phi => Nat_Arith.nateq_cancel_sums *}
    2.16 +  {* fn phi => fn ss => try Nat_Arith.cancel_eq_conv *}
    2.17  
    2.18  simproc_setup natless_cancel_sums
    2.19    ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
    2.20 -  {* fn phi => Nat_Arith.natless_cancel_sums *}
    2.21 +  {* fn phi => fn ss => try Nat_Arith.cancel_less_conv *}
    2.22  
    2.23  simproc_setup natle_cancel_sums
    2.24    ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
    2.25 -  {* fn phi => Nat_Arith.natle_cancel_sums *}
    2.26 +  {* fn phi => fn ss => try Nat_Arith.cancel_le_conv *}
    2.27  
    2.28  simproc_setup natdiff_cancel_sums
    2.29    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
    2.30 -  {* fn phi => Nat_Arith.natdiff_cancel_sums *}
    2.31 +  {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
    2.32  
    2.33  use "Tools/lin_arith.ML"
    2.34  setup {* Lin_Arith.global_setup *}
     3.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Jul 27 17:57:31 2012 +0200
     3.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Jul 27 17:59:18 2012 +0200
     3.3 @@ -805,8 +805,9 @@
     3.4        addsimps @{thms ring_distribs}
     3.5        addsimps [@{thm if_True}, @{thm if_False}]
     3.6        addsimps
     3.7 -       [@{thm add_0_left},
     3.8 -        @{thm add_0_right},
     3.9 +       [@{thm add_0_left}, @{thm add_0_right},
    3.10 +        @{thm add_Suc}, @{thm add_Suc_right},
    3.11 +        @{thm nat.inject}, @{thm Suc_le_mono}, @{thm Suc_less_eq},
    3.12          @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
    3.13          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
    3.14          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
     4.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:57:31 2012 +0200
     4.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:59:18 2012 +0200
     4.3 @@ -1,17 +1,19 @@
     4.4  (* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     4.5 +   Author: Brian Huffman
     4.6  
     4.7  Basic arithmetic for natural numbers.
     4.8  *)
     4.9  
    4.10  signature NAT_ARITH =
    4.11  sig
    4.12 +  val cancel_diff_conv: conv
    4.13 +  val cancel_eq_conv: conv
    4.14 +  val cancel_le_conv: conv
    4.15 +  val cancel_less_conv: conv
    4.16 +  (* legacy functions: *)
    4.17    val mk_sum: term list -> term
    4.18    val mk_norm_sum: term list -> term
    4.19    val dest_sum: term -> term list
    4.20 -  val nateq_cancel_sums: simpset -> cterm -> thm option
    4.21 -  val natless_cancel_sums: simpset -> cterm -> thm option
    4.22 -  val natle_cancel_sums: simpset -> cterm -> thm option
    4.23 -  val natdiff_cancel_sums: simpset -> cterm -> thm option
    4.24  end;
    4.25  
    4.26  structure Nat_Arith: NAT_ARITH =
    4.27 @@ -42,55 +44,58 @@
    4.28            SOME (t, u) => dest_sum t @ dest_sum u
    4.29          | NONE => [tm]));
    4.30  
    4.31 +val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
    4.32 +      by (simp only: add_ac)}
    4.33 +val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
    4.34 +      by (simp only: add_ac)}
    4.35 +val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
    4.36 +      by (simp only: add_Suc_right)}
    4.37 +val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
    4.38 +      by (simp only: add_0_right)}
    4.39  
    4.40 -(** cancel common summands **)
    4.41 +val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
    4.42  
    4.43 -structure CommonCancelSums =
    4.44 -struct
    4.45 -  val mk_sum = mk_norm_sum;
    4.46 -  val dest_sum = dest_sum;
    4.47 -  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    4.48 -  val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
    4.49 -    @{thm Nat.add_0}, @{thm Nat.add_0_right}];
    4.50 -  val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    4.51 -  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    4.52 -end;
    4.53 +fun move_to_front path = Conv.every_conv
    4.54 +    [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
    4.55 +     Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
    4.56  
    4.57 -structure EqCancelSums = CancelSumsFun
    4.58 -(struct
    4.59 -  open CommonCancelSums;
    4.60 -  val mk_bal = HOLogic.mk_eq;
    4.61 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
    4.62 -  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel};
    4.63 -end);
    4.64 +fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
    4.65 +      add_atoms (add1::path) x #> add_atoms (add2::path) y
    4.66 +  | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) =
    4.67 +      add_atoms (suc1::path) x
    4.68 +  | add_atoms _ (Const (@{const_name Groups.zero}, _)) = I
    4.69 +  | add_atoms path x = cons (x, path)
    4.70 +
    4.71 +fun atoms t = add_atoms [] t []
    4.72 +
    4.73 +exception Cancel
    4.74  
    4.75 -structure LessCancelSums = CancelSumsFun
    4.76 -(struct
    4.77 -  open CommonCancelSums;
    4.78 -  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
    4.79 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
    4.80 -  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less};
    4.81 -end);
    4.82 +fun find_common ord xs ys =
    4.83 +  let
    4.84 +    fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
    4.85 +        (case ord (x, y) of
    4.86 +          EQUAL => (px, py)
    4.87 +        | LESS => find xs' ys
    4.88 +        | GREATER => find xs ys')
    4.89 +      | find _ _ = raise Cancel
    4.90 +    fun ord' ((x, _), (y, _)) = ord (x, y)
    4.91 +  in
    4.92 +    find (sort ord' xs) (sort ord' ys)
    4.93 +  end
    4.94  
    4.95 -structure LeCancelSums = CancelSumsFun
    4.96 -(struct
    4.97 -  open CommonCancelSums;
    4.98 -  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
    4.99 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
   4.100 -  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le};
   4.101 -end);
   4.102 +fun cancel_conv rule ct =
   4.103 +  let
   4.104 +    val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
   4.105 +    val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
   4.106 +    val lconv = move_to_front lpath
   4.107 +    val rconv = move_to_front rpath
   4.108 +    val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
   4.109 +    val conv = conv1 then_conv Conv.rewr_conv rule
   4.110 +  in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
   4.111  
   4.112 -structure DiffCancelSums = CancelSumsFun
   4.113 -(struct
   4.114 -  open CommonCancelSums;
   4.115 -  val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
   4.116 -  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
   4.117 -  val cancel_rule = mk_meta_eq @{thm diff_cancel};
   4.118 -end);
   4.119 -
   4.120 -fun nateq_cancel_sums ss = EqCancelSums.proc ss o Thm.term_of
   4.121 -fun natless_cancel_sums ss = LessCancelSums.proc ss o Thm.term_of
   4.122 -fun natle_cancel_sums ss = LeCancelSums.proc ss o Thm.term_of
   4.123 -fun natdiff_cancel_sums ss = DiffCancelSums.proc ss o Thm.term_of
   4.124 +val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
   4.125 +val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
   4.126 +val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
   4.127 +val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})
   4.128  
   4.129  end;
     5.1 --- a/src/Provers/Arith/cancel_sums.ML	Fri Jul 27 17:57:31 2012 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,78 +0,0 @@
     5.4 -(*  Title:      Provers/Arith/cancel_sums.ML
     5.5 -    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     5.6 -
     5.7 -Cancel common summands of balanced expressions:
     5.8 -
     5.9 -  A + x + B ~~ A' + x + B'  ==  A + B ~~ A' + B'
    5.10 -
    5.11 -where + is AC0 and ~~ an appropriate balancing operation (e.g. =, <=, <, -).
    5.12 -*)
    5.13 -
    5.14 -signature CANCEL_SUMS_DATA =
    5.15 -sig
    5.16 -  (*abstract syntax*)
    5.17 -  val mk_sum: term list -> term
    5.18 -  val dest_sum: term -> term list
    5.19 -  val mk_plus: term * term -> term
    5.20 -  val mk_bal: term * term -> term
    5.21 -  val dest_bal: term -> term * term
    5.22 -  (*rules*)
    5.23 -  val norm_tac: simpset -> tactic            (*AC0 etc.*)
    5.24 -  val cancel_rule: thm                       (* x + A ~~ x + B == A ~~ B *)
    5.25 -end;
    5.26 -
    5.27 -signature CANCEL_SUMS =
    5.28 -sig
    5.29 -  val proc: simpset -> term -> thm option
    5.30 -end;
    5.31 -
    5.32 -
    5.33 -functor CancelSumsFun(Data: CANCEL_SUMS_DATA): CANCEL_SUMS =
    5.34 -struct
    5.35 -
    5.36 -
    5.37 -(* cancel *)
    5.38 -
    5.39 -fun cons1 x (xs, y, z) = (x :: xs, y, z);
    5.40 -fun cons2 y (x, ys, z) = (x, y :: ys, z);
    5.41 -
    5.42 -(*symmetric difference of multisets -- assumed to be sorted wrt. Term_Ord.term_ord*)
    5.43 -fun cancel ts [] vs = (ts, [], vs)
    5.44 -  | cancel [] us vs = ([], us, vs)
    5.45 -  | cancel (t :: ts) (u :: us) vs =
    5.46 -      (case Term_Ord.term_ord (t, u) of
    5.47 -        EQUAL => cancel ts us (t :: vs)
    5.48 -      | LESS => cons1 t (cancel ts (u :: us) vs)
    5.49 -      | GREATER => cons2 u (cancel (t :: ts) us vs));
    5.50 -
    5.51 -
    5.52 -(* the simplification procedure *)
    5.53 -
    5.54 -fun proc ss t =
    5.55 -  (case try Data.dest_bal t of
    5.56 -    NONE => NONE
    5.57 -  | SOME bal =>
    5.58 -      let
    5.59 -        val thy = Proof_Context.theory_of (Simplifier.the_context ss);
    5.60 -        val (ts, us) = pairself (sort Term_Ord.term_ord o Data.dest_sum) bal;
    5.61 -        val (ts', us', vs) = cancel ts us [];
    5.62 -      in
    5.63 -        if null vs then NONE
    5.64 -        else
    5.65 -          let
    5.66 -            val cert = Thm.cterm_of thy
    5.67 -            val t' = Data.mk_sum ts'
    5.68 -            val u' = Data.mk_sum us'
    5.69 -            val v = Data.mk_sum vs
    5.70 -            val t1 = Data.mk_bal (Data.mk_plus (v, t'), Data.mk_plus (v, u'))
    5.71 -            val t2 = Data.mk_bal (t', u')
    5.72 -            val goal1 = Thm.cterm_of thy (Logic.mk_equals (t, t1))
    5.73 -            val goal2 = Thm.cterm_of thy (Logic.mk_equals (t1, t2))
    5.74 -            val thm1 = Goal.prove_internal [] goal1 (K (Data.norm_tac ss))
    5.75 -            val thm2 = Goal.prove_internal [] goal2 (K (rtac Data.cancel_rule 1))
    5.76 -          in
    5.77 -            SOME (Thm.transitive thm1 thm2)
    5.78 -          end
    5.79 -      end);
    5.80 -
    5.81 -end;