src/HOL/Tools/int_arith.ML
changeset 31510 e0f2bb4b0021
parent 31101 26c7bb764a38
child 32603 e08fdd615333
     1.1 --- a/src/HOL/Tools/int_arith.ML	Mon Jun 08 20:43:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Jun 08 22:29:37 2009 +0200
     1.3 @@ -87,6 +87,12 @@
     1.4  val global_setup = Simplifier.map_simpset
     1.5    (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
     1.6  
     1.7 +
     1.8 +fun number_of thy T n =
     1.9 +  if not (Sign.of_sort thy (T, @{sort number}))
    1.10 +  then raise CTERM ("number_of", [])
    1.11 +  else Numeral.mk_cnumber (Thm.ctyp_of thy T) n
    1.12 +
    1.13  val setup =
    1.14    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    1.15    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
    1.16 @@ -95,6 +101,7 @@
    1.17    #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
    1.18        :: Numeral_Simprocs.combine_numerals
    1.19        :: Numeral_Simprocs.cancel_numerals)
    1.20 +  #> Lin_Arith.set_number_of number_of
    1.21    #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
    1.22    #> Lin_Arith.add_discrete_type @{type_name Int.int}
    1.23