src/HOL/Hyperreal/hypreal_arith.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17876 b9c92f384109
child 20254 58b71535ed00
permissions -rw-r--r--
setup: theory -> theory;
paulson@14309
     1
(*  Title:      HOL/Hyperreal/hypreal_arith.ML
paulson@10751
     2
    ID:         $Id$
paulson@10751
     3
    Author:     Tobias Nipkow, TU Muenchen
paulson@10751
     4
    Copyright   1999 TU Muenchen
paulson@10751
     5
paulson@14352
     6
Simprocs for common factor cancellation & Rational coefficient handling
paulson@14352
     7
paulson@14352
     8
Instantiation of the generic linear arithmetic package for type hypreal.
paulson@10751
     9
*)
paulson@10751
    10
paulson@14352
    11
(****Instantiation of the generic linear arithmetic package****)
paulson@14352
    12
paulson@14309
    13
paulson@10751
    14
local
paulson@10751
    15
huffman@17318
    16
val real_inj_thms = [thm "star_of_le" RS iffD2, 
huffman@17318
    17
                     thm "star_of_less" RS iffD2,
huffman@17318
    18
                     thm "star_of_eq" RS iffD2];
paulson@14369
    19
paulson@10751
    20
in
paulson@10751
    21
huffman@17431
    22
val hyprealT = Type("StarDef.star", [HOLogic.realT]);
paulson@14387
    23
paulson@14352
    24
val fast_hypreal_arith_simproc =
paulson@14352
    25
    Simplifier.simproc (Theory.sign_of (the_context ()))
paulson@14352
    26
      "fast_hypreal_arith" 
paulson@14352
    27
      ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
paulson@14352
    28
    Fast_Arith.lin_arith_prover;
paulson@14352
    29
paulson@10751
    30
val hypreal_arith_setup =
wenzelm@18708
    31
  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
paulson@14369
    32
   {add_mono_thms = add_mono_thms,
nipkow@15184
    33
    mult_mono_thms = mult_mono_thms,
paulson@14369
    34
    inj_thms = inj_thms @ real_inj_thms, 
paulson@14352
    35
    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
nipkow@15923
    36
    neqE = neqE,
wenzelm@18708
    37
    simpset = simpset}) #>
wenzelm@18708
    38
  arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
wenzelm@18708
    39
  (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy));
paulson@10751
    40
paulson@10751
    41
end;
paulson@10751
    42
paulson@14352
    43
paulson@14352
    44