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;
paulson@14426
     1
(*  Title:      HOL/Real/real_arith.ML
wenzelm@9436
     2
    ID:         $Id$
wenzelm@9436
     3
    Author:     Tobias Nipkow, TU Muenchen
paulson@14352
     4
    Copyright   1999 TU Muenchen
wenzelm@9436
     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 real.
wenzelm@9436
     9
*)
wenzelm@9436
    10
paulson@14289
    11
local
paulson@14289
    12
huffman@23080
    13
val simps = [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
huffman@23080
    14
             @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
huffman@23080
    15
             @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
huffman@23080
    16
             @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
huffman@23080
    17
             @{thm real_of_nat_number_of}, @{thm real_number_of}]
nipkow@14355
    18
huffman@23080
    19
val nat_inj_thms = [@{thm real_of_nat_le_iff} RS iffD2,
huffman@23080
    20
                    @{thm real_of_nat_inject} RS iffD2]
webertj@20254
    21
(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
webertj@20254
    22
                    real_of_nat_less_iff RS iffD2 *)
nipkow@14355
    23
huffman@23080
    24
val int_inj_thms = [@{thm real_of_int_le_iff} RS iffD2,
huffman@23080
    25
                    @{thm real_of_int_inject} RS iffD2]
webertj@20254
    26
(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
webertj@20254
    27
                    real_of_int_less_iff RS iffD2 *)
paulson@14352
    28
wenzelm@9436
    29
in
wenzelm@9436
    30
wenzelm@9436
    31
val real_arith_setup =
wenzelm@24093
    32
  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
paulson@14368
    33
   {add_mono_thms = add_mono_thms,
nipkow@15184
    34
    mult_mono_thms = mult_mono_thms,
nipkow@14355
    35
    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
wenzelm@24093
    36
    lessD = lessD,  (*Can't change lessD: the reals are dense!*)
nipkow@15923
    37
    neqE = neqE,
wenzelm@18708
    38
    simpset = simpset addsimps simps}) #>
haftmann@27545
    39
  arith_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
haftmann@27545
    40
  arith_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
paulson@14352
    41
wenzelm@9436
    42
end;