src/HOL/Tools/int_arith.ML
changeset 31100 6a2e67fe4488
parent 31082 54a442b2d727
child 31101 26c7bb764a38
     1.1 --- a/src/HOL/Tools/int_arith.ML	Mon May 11 11:53:21 2009 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Mon May 11 15:18:32 2009 +0200
     1.3 @@ -5,8 +5,8 @@
     1.4  
     1.5  signature INT_ARITH =
     1.6  sig
     1.7 -  val fast_int_arith_simproc: simproc
     1.8    val setup: Context.generic -> Context.generic
     1.9 +  val global_setup: theory -> theory
    1.10  end
    1.11  
    1.12  structure Int_Arith : INT_ARITH =
    1.13 @@ -49,17 +49,15 @@
    1.14    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
    1.15    proc = proc1, identifier = []};
    1.16  
    1.17 -val allowed_consts =
    1.18 -  [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
    1.19 -   @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
    1.20 -   @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
    1.21 -   @{const_name "HOL.less_eq"}];
    1.22 -
    1.23 -fun check t = case t of
    1.24 -   Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
    1.25 -                else s mem_string allowed_consts
    1.26 - | a$b => check a andalso check b
    1.27 - | _ => false;
    1.28 +fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
    1.29 +  | check (Const (@{const_name "HOL.one"}, _)) = true
    1.30 +  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
    1.31 +      @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
    1.32 +      @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
    1.33 +      @{const_name "HOL.zero"},
    1.34 +      @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
    1.35 +  | check (a $ b) = check a andalso check b
    1.36 +  | check _ = false;
    1.37  
    1.38  val conv =
    1.39    Simplifier.rewrite
    1.40 @@ -80,35 +78,24 @@
    1.41    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
    1.42    proc = sproc, identifier = []}
    1.43  
    1.44 -val add_rules =
    1.45 -    simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
    1.46 -    @{thms int_arith_rules}
    1.47 -
    1.48 -val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    1.49 -
    1.50 -val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
    1.51 -  :: Numeral_Simprocs.combine_numerals
    1.52 -  :: Numeral_Simprocs.cancel_numerals;
    1.53 -
    1.54 -val setup =
    1.55 -  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.56 -   {add_mono_thms = add_mono_thms,
    1.57 -    mult_mono_thms = (*@{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: *)mult_mono_thms,
    1.58 -    inj_thms = nat_inj_thms @ inj_thms,
    1.59 -    lessD = lessD @ [@{thm zless_imp_add1_zle}],
    1.60 -    neqE = neqE,
    1.61 -    simpset = simpset addsimps add_rules
    1.62 -                      addsimprocs numeral_base_simprocs}) #>
    1.63 -  Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
    1.64 -  Lin_Arith.add_discrete_type @{type_name Int.int}
    1.65 -
    1.66  val fast_int_arith_simproc =
    1.67 -  Simplifier.simproc (the_context ())
    1.68 -  "fast_int_arith" 
    1.69 +  Simplifier.simproc @{theory} "fast_int_arith"
    1.70       ["(m::'a::{ordered_idom,number_ring}) < n",
    1.71        "(m::'a::{ordered_idom,number_ring}) <= n",
    1.72        "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
    1.73  
    1.74 -end;
    1.75 +val global_setup = Simplifier.map_simpset
    1.76 +  (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
    1.77  
    1.78 -Addsimprocs [Int_Arith.fast_int_arith_simproc];
    1.79 +val setup =
    1.80 +  Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    1.81 +  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
    1.82 +  #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
    1.83 +      @ @{thms arith_special} @ @{thms int_arith_rules})
    1.84 +  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
    1.85 +      :: Numeral_Simprocs.combine_numerals
    1.86 +      :: Numeral_Simprocs.cancel_numerals)
    1.87 +  #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
    1.88 +  #> Lin_Arith.add_discrete_type @{type_name Int.int}
    1.89 +
    1.90 +end;