modernized some simproc setup;
authorwenzelm
Wed Jun 29 18:12:34 2011 +0200 (2011-06-29)
changeset 435957ae4a23b5be6
parent 43594 ef1ddc59b825
child 43596 78211f66cf8d
modernized some simproc setup;
src/HOL/Int.thy
src/HOL/NSA/HyperDef.thy
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
     1.1 --- a/src/HOL/Int.thy	Wed Jun 29 17:35:46 2011 +0200
     1.2 +++ b/src/HOL/Int.thy	Wed Jun 29 18:12:34 2011 +0200
     1.3 @@ -1545,9 +1545,13 @@
     1.4    of_int_0 of_int_1 of_int_add of_int_mult
     1.5  
     1.6  use "Tools/int_arith.ML"
     1.7 -setup {* Int_Arith.global_setup *}
     1.8  declaration {* K Int_Arith.setup *}
     1.9  
    1.10 +simproc_setup fast_arith ("(m::'a::{linordered_idom,number_ring}) < n" |
    1.11 +  "(m::'a::{linordered_idom,number_ring}) <= n" |
    1.12 +  "(m::'a::{linordered_idom,number_ring}) = n") =
    1.13 +  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
    1.14 +
    1.15  setup {*
    1.16    Reorient_Proc.add
    1.17      (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
     2.1 --- a/src/HOL/NSA/HyperDef.thy	Wed Jun 29 17:35:46 2011 +0200
     2.2 +++ b/src/HOL/NSA/HyperDef.thy	Wed Jun 29 18:12:34 2011 +0200
     2.3 @@ -348,12 +348,12 @@
     2.4    #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
     2.5        @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
     2.6        @{thm star_of_diff}, @{thm star_of_mult}]
     2.7 -  #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
     2.8 -  #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc_global @{theory}
     2.9 -      "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
    2.10 -      (K Lin_Arith.simproc)]))
    2.11 +  #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
    2.12  *}
    2.13  
    2.14 +simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") =
    2.15 +  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
    2.16 +
    2.17  
    2.18  subsection {* Exponentials on the Hyperreals *}
    2.19  
     3.1 --- a/src/HOL/Nat.thy	Wed Jun 29 17:35:46 2011 +0200
     3.2 +++ b/src/HOL/Nat.thy	Wed Jun 29 18:12:34 2011 +0200
     3.3 @@ -1433,6 +1433,15 @@
     3.4  setup {* Lin_Arith.global_setup *}
     3.5  declaration {* K Lin_Arith.setup *}
     3.6  
     3.7 +simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") =
     3.8 +  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
     3.9 +(* Because of this simproc, the arithmetic solver is really only
    3.10 +useful to detect inconsistencies among the premises for subgoals which are
    3.11 +*not* themselves (in)equalities, because the latter activate
    3.12 +fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    3.13 +solver all the time rather than add the additional check. *)
    3.14 +
    3.15 +
    3.16  lemmas [arith_split] = nat_diff_split split_min split_max
    3.17  
    3.18  context order
     4.1 --- a/src/HOL/Product_Type.thy	Wed Jun 29 17:35:46 2011 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Wed Jun 29 18:12:34 2011 +0200
     4.3 @@ -556,6 +556,7 @@
     4.4          if Pair_pat k i (t $ u) then incr_boundvars k arg
     4.5          else (subst arg k i t $ subst arg k i u)
     4.6      | subst arg k i t = t;
     4.7 +in
     4.8    fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
     4.9          (case split_pat beta_term_pat 1 t of
    4.10            SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
    4.11 @@ -566,13 +567,10 @@
    4.12            SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
    4.13          | NONE => NONE)
    4.14      | eta_proc _ _ = NONE;
    4.15 -in
    4.16 -  val split_beta_proc = Simplifier.simproc_global @{theory} "split_beta" ["split f z"] (K beta_proc);
    4.17 -  val split_eta_proc = Simplifier.simproc_global @{theory} "split_eta" ["split f"] (K eta_proc);
    4.18  end;
    4.19 -
    4.20 -Addsimprocs [split_beta_proc, split_eta_proc];
    4.21  *}
    4.22 +simproc_setup split_beta ("split f z") = {* fn _ => fn ss => fn ct => beta_proc ss (term_of ct) *}
    4.23 +simproc_setup split_eta ("split f") = {* fn _ => fn ss => fn ct => eta_proc ss (term_of ct) *}
    4.24  
    4.25  lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
    4.26    by (subst surjective_pairing, rule split_conv)
     5.1 --- a/src/HOL/Tools/int_arith.ML	Wed Jun 29 17:35:46 2011 +0200
     5.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Jun 29 18:12:34 2011 +0200
     5.3 @@ -6,7 +6,6 @@
     5.4  signature INT_ARITH =
     5.5  sig
     5.6    val setup: Context.generic -> Context.generic
     5.7 -  val global_setup: theory -> theory
     5.8  end
     5.9  
    5.10  structure Int_Arith : INT_ARITH =
    5.11 @@ -78,16 +77,6 @@
    5.12    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
    5.13    proc = sproc, identifier = []}
    5.14  
    5.15 -val fast_int_arith_simproc =
    5.16 -  Simplifier.simproc_global @{theory} "fast_int_arith"
    5.17 -     ["(m::'a::{linordered_idom,number_ring}) < n",
    5.18 -      "(m::'a::{linordered_idom,number_ring}) <= n",
    5.19 -      "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
    5.20 -
    5.21 -val global_setup =
    5.22 -  Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
    5.23 -
    5.24 -
    5.25  fun number_of thy T n =
    5.26    if not (Sign.of_sort thy (T, @{sort number}))
    5.27    then raise CTERM ("number_of", [])
     6.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Jun 29 17:35:46 2011 +0200
     6.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 29 18:12:34 2011 +0200
     6.3 @@ -894,15 +894,8 @@
     6.4  
     6.5  val setup =
     6.6    init_arith_data #>
     6.7 -  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc_global @{theory} "fast_nat_arith"
     6.8 -    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
     6.9 -    (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
    6.10 -    useful to detect inconsistencies among the premises for subgoals which are
    6.11 -    *not* themselves (in)equalities, because the latter activate
    6.12 -    fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    6.13 -    solver all the time rather than add the additional check. *)
    6.14 -    addSolver (mk_solver' "lin_arith"
    6.15 -      (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
    6.16 +  Simplifier.map_ss (fn ss => ss
    6.17 +    addSolver (mk_solver' "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
    6.18  
    6.19  val global_setup =
    6.20    Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))