src/HOL/Tools/int_arith.ML

 Instantiation of the generic linear arithmetic package for int.
 *)
 
 signature INT_ARITH =
 sig
-  val fast_int_arith_simproc: simproc
   val setup: Context.generic -> Context.generic
+  val global_setup: theory -> theory
 end
 
 structure Int_Arith : INT_ARITH =
 struct
 

 
 val one_to_of_int_one_simproc =
   make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   proc = proc1, identifier = []};
 
-val allowed_consts =
-  [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
-   @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
-   @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
-   @{const_name "HOL.less_eq"}];
-
-fun check t = case t of
-   Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
-                else s mem_string allowed_consts
- | a$b => check a andalso check b
- | _ => false;
+fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
+  | check (Const (@{const_name "HOL.one"}, _)) = true
+  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
+      @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
+      @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
+      @{const_name "HOL.zero"},
+      @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
+  | check (a $ b) = check a andalso check b
+  | check _ = false;
 
 val conv =
   Simplifier.rewrite
    (HOL_basic_ss addsimps
      ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},

 
 val zero_one_idom_simproc =
   make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   proc = sproc, identifier = []}
 
-val add_rules =
-    simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
-    @{thms int_arith_rules}
-
-val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
-
-val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
-  :: Numeral_Simprocs.combine_numerals
-  :: Numeral_Simprocs.cancel_numerals;
-
-val setup =
-  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
-   {add_mono_thms = add_mono_thms,
-    mult_mono_thms = (*@{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: *)mult_mono_thms,
-    inj_thms = nat_inj_thms @ inj_thms,
-    lessD = lessD @ [@{thm zless_imp_add1_zle}],
-    neqE = neqE,
-    simpset = simpset addsimps add_rules
-                      addsimprocs numeral_base_simprocs}) #>
-  Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
-  Lin_Arith.add_discrete_type @{type_name Int.int}
-
 val fast_int_arith_simproc =
-  Simplifier.simproc (the_context ())
-  "fast_int_arith" 
+  Simplifier.simproc @{theory} "fast_int_arith"
      ["(m::'a::{ordered_idom,number_ring}) < n",
       "(m::'a::{ordered_idom,number_ring}) <= n",
       "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
 
+val global_setup = Simplifier.map_simpset
+  (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
+
+val setup =
+  Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
+  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
+  #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
+      @ @{thms arith_special} @ @{thms int_arith_rules})
+  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
+      :: Numeral_Simprocs.combine_numerals
+      :: Numeral_Simprocs.cancel_numerals)
+  #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
+  #> Lin_Arith.add_discrete_type @{type_name Int.int}
+
 end;
-
-Addsimprocs [Int_Arith.fast_int_arith_simproc];