give Nat_Arith simprocs proper name bindings by using simproc_setup
authorhuffman
Fri Jul 27 17:57:31 2012 +0200 (2012-07-27)
changeset 48559686cc7c47589
parent 48558 fabbed3abc1e
child 48560 e0875d956a6b
give Nat_Arith simprocs proper name bindings by using simproc_setup
src/HOL/Nat.thy
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/nat_arith.ML
src/HOL/ex/Simproc_Tests.thy
     1.1 --- a/src/HOL/Nat.thy	Fri Jul 27 17:34:33 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Jul 27 17:57:31 2012 +0200
     1.3 @@ -1494,7 +1494,22 @@
     1.4  setup Arith_Data.setup
     1.5  
     1.6  use "Tools/nat_arith.ML"
     1.7 -declaration {* K Nat_Arith.setup *}
     1.8 +
     1.9 +simproc_setup nateq_cancel_sums
    1.10 +  ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
    1.11 +  {* fn phi => Nat_Arith.nateq_cancel_sums *}
    1.12 +
    1.13 +simproc_setup natless_cancel_sums
    1.14 +  ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
    1.15 +  {* fn phi => Nat_Arith.natless_cancel_sums *}
    1.16 +
    1.17 +simproc_setup natle_cancel_sums
    1.18 +  ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
    1.19 +  {* fn phi => Nat_Arith.natle_cancel_sums *}
    1.20 +
    1.21 +simproc_setup natdiff_cancel_sums
    1.22 +  ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
    1.23 +  {* fn phi => Nat_Arith.natdiff_cancel_sums *}
    1.24  
    1.25  use "Tools/lin_arith.ML"
    1.26  setup {* Lin_Arith.global_setup *}
     2.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Jul 27 17:34:33 2012 +0200
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Jul 27 17:57:31 2012 +0200
     2.3 @@ -815,7 +815,9 @@
     2.4                     @{simproc group_cancel_eq}, @{simproc group_cancel_le},
     2.5                     @{simproc group_cancel_less}]
     2.6         (*abel_cancel helps it work in abstract algebraic domains*)
     2.7 -      addsimprocs Nat_Arith.nat_cancel_sums_add
     2.8 +      addsimprocs [@{simproc nateq_cancel_sums},
     2.9 +                   @{simproc natless_cancel_sums},
    2.10 +                   @{simproc natle_cancel_sums}]
    2.11        |> Simplifier.add_cong @{thm if_weak_cong},
    2.12      number_of = number_of}) #>
    2.13    add_discrete_type @{type_name nat};
     3.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:34:33 2012 +0200
     3.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:57:31 2012 +0200
     3.3 @@ -8,10 +8,10 @@
     3.4    val mk_sum: term list -> term
     3.5    val mk_norm_sum: term list -> term
     3.6    val dest_sum: term -> term list
     3.7 -
     3.8 -  val nat_cancel_sums_add: simproc list
     3.9 -  val nat_cancel_sums: simproc list
    3.10 -  val setup: Context.generic -> Context.generic
    3.11 +  val nateq_cancel_sums: simpset -> cterm -> thm option
    3.12 +  val natless_cancel_sums: simpset -> cterm -> thm option
    3.13 +  val natle_cancel_sums: simpset -> cterm -> thm option
    3.14 +  val natdiff_cancel_sums: simpset -> cterm -> thm option
    3.15  end;
    3.16  
    3.17  structure Nat_Arith: NAT_ARITH =
    3.18 @@ -88,23 +88,9 @@
    3.19    val cancel_rule = mk_meta_eq @{thm diff_cancel};
    3.20  end);
    3.21  
    3.22 -val nat_cancel_sums_add =
    3.23 -  [Simplifier.simproc_global @{theory} "nateq_cancel_sums"
    3.24 -     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
    3.25 -     (K EqCancelSums.proc),
    3.26 -   Simplifier.simproc_global @{theory} "natless_cancel_sums"
    3.27 -     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
    3.28 -     (K LessCancelSums.proc),
    3.29 -   Simplifier.simproc_global @{theory} "natle_cancel_sums"
    3.30 -     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
    3.31 -     (K LeCancelSums.proc)];
    3.32 -
    3.33 -val nat_cancel_sums = nat_cancel_sums_add @
    3.34 -  [Simplifier.simproc_global @{theory} "natdiff_cancel_sums"
    3.35 -    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
    3.36 -    (K DiffCancelSums.proc)];
    3.37 -
    3.38 -val setup =
    3.39 -  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
    3.40 +fun nateq_cancel_sums ss = EqCancelSums.proc ss o Thm.term_of
    3.41 +fun natless_cancel_sums ss = LessCancelSums.proc ss o Thm.term_of
    3.42 +fun natle_cancel_sums ss = LeCancelSums.proc ss o Thm.term_of
    3.43 +fun natdiff_cancel_sums ss = DiffCancelSums.proc ss o Thm.term_of
    3.44  
    3.45  end;
     4.1 --- a/src/HOL/ex/Simproc_Tests.thy	Fri Jul 27 17:34:33 2012 +0200
     4.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Fri Jul 27 17:57:31 2012 +0200
     4.3 @@ -27,21 +27,21 @@
     4.4    fix a b c d :: nat
     4.5    {
     4.6      assume "b = Suc c" have "a + b = Suc (c + a)"
     4.7 -      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 0] *}) fact
     4.8 +      by (tactic {* test [@{simproc nateq_cancel_sums}] *}) fact
     4.9    next
    4.10      assume "b < Suc c" have "a + b < Suc (c + a)"
    4.11 -      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 1] *}) fact
    4.12 +      by (tactic {* test [@{simproc natless_cancel_sums}] *}) fact
    4.13    next
    4.14      assume "b \<le> Suc c" have "a + b \<le> Suc (c + a)"
    4.15 -      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) fact
    4.16 +      by (tactic {* test [@{simproc natle_cancel_sums}] *}) fact
    4.17    next
    4.18      assume "b - Suc c = d" have "a + b - Suc (c + a) = d"
    4.19 -      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 3] *}) fact
    4.20 +      by (tactic {* test [@{simproc natdiff_cancel_sums}] *}) fact
    4.21    }
    4.22  end
    4.23  
    4.24  schematic_lemma "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
    4.25 -  by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) (rule le0)
    4.26 +  by (tactic {* test [@{simproc natle_cancel_sums}] *}) (rule le0)
    4.27  (* TODO: test more simprocs with schematic variables *)
    4.28  
    4.29  subsection {* Abelian group cancellation simprocs *}