src/HOL/Hyperreal/hypreal_arith.ML
author wenzelm
Tue Jul 31 19:40:24 2007 +0200 (2007-07-31)
changeset 24093 5d0ecd0c8f3c
parent 24075 366d4d234814
permissions -rw-r--r--
tuned LinArith setup;
     1 (*  Title:      HOL/Hyperreal/hypreal_arith.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, TU Muenchen
     4     Copyright   1999 TU Muenchen
     5 
     6 Simprocs for common factor cancellation & Rational coefficient handling
     7 
     8 Instantiation of the generic linear arithmetic package for type hypreal.
     9 *)
    10 
    11 local
    12 
    13 val simps = [thm "star_of_zero",
    14              thm "star_of_one",
    15              thm "star_of_number_of",
    16              thm "star_of_add",
    17              thm "star_of_minus",
    18              thm "star_of_diff",
    19              thm "star_of_mult"]
    20 
    21 val real_inj_thms = [thm "star_of_le" RS iffD2,
    22                      thm "star_of_less" RS iffD2,
    23                      thm "star_of_eq" RS iffD2]
    24 
    25 in
    26 
    27 val hyprealT = Type ("StarDef.star", [HOLogic.realT]);
    28 
    29 val fast_hypreal_arith_simproc =
    30     Simplifier.simproc (the_context ())
    31       "fast_hypreal_arith" 
    32       ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
    33     (K LinArith.lin_arith_simproc);
    34 
    35 val hypreal_arith_setup =
    36   LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    37    {add_mono_thms = add_mono_thms,
    38     mult_mono_thms = mult_mono_thms,
    39     inj_thms = real_inj_thms @ inj_thms,
    40     lessD = lessD,  (*Can't change lessD: the hypreals are dense!*)
    41     neqE = neqE,
    42     simpset = simpset addsimps simps}) #>
    43   arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
    44   Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
    45 
    46 end;