src/HOL/Real/real_arith.ML
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27545 7165068bb61f
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (*  Title:      HOL/Real/real_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 real.
     9 *)
    10 
    11 local
    12 
    13 val simps = [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
    14              @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
    15              @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
    16              @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
    17              @{thm real_of_nat_number_of}, @{thm real_number_of}]
    18 
    19 val nat_inj_thms = [@{thm real_of_nat_le_iff} RS iffD2,
    20                     @{thm real_of_nat_inject} RS iffD2]
    21 (* not needed because x < (y::nat) can be rewritten as Suc x <= y:
    22                     real_of_nat_less_iff RS iffD2 *)
    23 
    24 val int_inj_thms = [@{thm real_of_int_le_iff} RS iffD2,
    25                     @{thm real_of_int_inject} RS iffD2]
    26 (* not needed because x < (y::int) can be rewritten as x + 1 <= y:
    27                     real_of_int_less_iff RS iffD2 *)
    28 
    29 in
    30 
    31 val real_arith_setup =
    32   LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    33    {add_mono_thms = add_mono_thms,
    34     mult_mono_thms = mult_mono_thms,
    35     inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
    36     lessD = lessD,  (*Can't change lessD: the reals are dense!*)
    37     neqE = neqE,
    38     simpset = simpset addsimps simps}) #>
    39   arith_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
    40   arith_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
    41 
    42 end;