# HG changeset patch # User wenzelm # Date 1309363954 -7200 # Node ID 7ae4a23b5be69c0314588b918569678e662f760a # Parent ef1ddc59b825071e957e184f2461aed202635c21 modernized some simproc setup; diff -r ef1ddc59b825 -r 7ae4a23b5be6 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Jun 29 17:35:46 2011 +0200 +++ b/src/HOL/Int.thy Wed Jun 29 18:12:34 2011 +0200 @@ -1545,9 +1545,13 @@ of_int_0 of_int_1 of_int_add of_int_mult use "Tools/int_arith.ML" -setup {* Int_Arith.global_setup *} declaration {* K Int_Arith.setup *} +simproc_setup fast_arith ("(m::'a::{linordered_idom,number_ring}) < n" | + "(m::'a::{linordered_idom,number_ring}) <= n" | + "(m::'a::{linordered_idom,number_ring}) = n") = + {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *} + setup {* Reorient_Proc.add (fn Const (@{const_name number_of}, _) $ _ => true | _ => false) diff -r ef1ddc59b825 -r 7ae4a23b5be6 src/HOL/NSA/HyperDef.thy --- a/src/HOL/NSA/HyperDef.thy Wed Jun 29 17:35:46 2011 +0200 +++ b/src/HOL/NSA/HyperDef.thy Wed Jun 29 18:12:34 2011 +0200 @@ -348,12 +348,12 @@ #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one}, @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}] - #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \ hypreal"}) - #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc_global @{theory} - "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] - (K Lin_Arith.simproc)])) + #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \ hypreal"})) *} +simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") = + {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *} + subsection {* Exponentials on the Hyperreals *} diff -r ef1ddc59b825 -r 7ae4a23b5be6 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Jun 29 17:35:46 2011 +0200 +++ b/src/HOL/Nat.thy Wed Jun 29 18:12:34 2011 +0200 @@ -1433,6 +1433,15 @@ setup {* Lin_Arith.global_setup *} declaration {* K Lin_Arith.setup *} +simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") = + {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *} +(* Because of this simproc, the arithmetic solver is really only +useful to detect inconsistencies among the premises for subgoals which are +*not* themselves (in)equalities, because the latter activate +fast_nat_arith_simproc anyway. However, it seems cheaper to activate the +solver all the time rather than add the additional check. *) + + lemmas [arith_split] = nat_diff_split split_min split_max context order diff -r ef1ddc59b825 -r 7ae4a23b5be6 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Jun 29 17:35:46 2011 +0200 +++ b/src/HOL/Product_Type.thy Wed Jun 29 18:12:34 2011 +0200 @@ -556,6 +556,7 @@ if Pair_pat k i (t $ u) then incr_boundvars k arg else (subst arg k i t $ subst arg k i u) | subst arg k i t = t; +in fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) = (case split_pat beta_term_pat 1 t of SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f)) @@ -566,13 +567,10 @@ SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end)) | NONE => NONE) | eta_proc _ _ = NONE; -in - val split_beta_proc = Simplifier.simproc_global @{theory} "split_beta" ["split f z"] (K beta_proc); - val split_eta_proc = Simplifier.simproc_global @{theory} "split_eta" ["split f"] (K eta_proc); end; - -Addsimprocs [split_beta_proc, split_eta_proc]; *} +simproc_setup split_beta ("split f z") = {* fn _ => fn ss => fn ct => beta_proc ss (term_of ct) *} +simproc_setup split_eta ("split f") = {* fn _ => fn ss => fn ct => eta_proc ss (term_of ct) *} lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)" by (subst surjective_pairing, rule split_conv) diff -r ef1ddc59b825 -r 7ae4a23b5be6 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Wed Jun 29 17:35:46 2011 +0200 +++ b/src/HOL/Tools/int_arith.ML Wed Jun 29 18:12:34 2011 +0200 @@ -6,7 +6,6 @@ signature INT_ARITH = sig val setup: Context.generic -> Context.generic - val global_setup: theory -> theory end structure Int_Arith : INT_ARITH = @@ -78,16 +77,6 @@ make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", proc = sproc, identifier = []} -val fast_int_arith_simproc = - Simplifier.simproc_global @{theory} "fast_int_arith" - ["(m::'a::{linordered_idom,number_ring}) < n", - "(m::'a::{linordered_idom,number_ring}) <= n", - "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc); - -val global_setup = - Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]); - - fun number_of thy T n = if not (Sign.of_sort thy (T, @{sort number})) then raise CTERM ("number_of", []) diff -r ef1ddc59b825 -r 7ae4a23b5be6 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Wed Jun 29 17:35:46 2011 +0200 +++ b/src/HOL/Tools/lin_arith.ML Wed Jun 29 18:12:34 2011 +0200 @@ -894,15 +894,8 @@ val setup = init_arith_data #> - Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc_global @{theory} "fast_nat_arith" - ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)] - (* Because of fast_nat_arith_simproc, the arithmetic solver is really only - useful to detect inconsistencies among the premises for subgoals which are - *not* themselves (in)equalities, because the latter activate - fast_nat_arith_simproc anyway. However, it seems cheaper to activate the - solver all the time rather than add the additional check. *) - addSolver (mk_solver' "lin_arith" - (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) + Simplifier.map_ss (fn ss => ss + addSolver (mk_solver' "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))); val global_setup = Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))