src/HOL/Real/rat_arith.ML
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27239 f2f42f9fa09d
permissions -rw-r--r--
moved global ML bindings to global place;
webertj@20254
     1
(*  Title:      HOL/Real/rat_arith.ML
paulson@14365
     2
    ID:         $Id$
paulson@14365
     3
    Author:     Lawrence C Paulson
paulson@14365
     4
    Copyright   2004 University of Cambridge
paulson@14365
     5
paulson@14365
     6
Simprocs for common factor cancellation & Rational coefficient handling
paulson@14365
     7
paulson@14365
     8
Instantiation of the generic linear arithmetic package for type rat.
paulson@14365
     9
*)
paulson@14365
    10
paulson@14365
    11
local
paulson@14365
    12
paulson@14390
    13
val simprocs = field_cancel_numeral_factors
paulson@14365
    14
wenzelm@27225
    15
val simps =
wenzelm@27225
    16
 [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
wenzelm@27239
    17
  read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
wenzelm@27225
    18
  @{thm divide_1}, @{thm divide_zero_left},
wenzelm@27225
    19
  @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
wenzelm@27225
    20
  @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
wenzelm@27225
    21
  @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
wenzelm@27225
    22
  @{thm of_int_minus}, @{thm of_int_diff},
wenzelm@27225
    23
  @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
webertj@20254
    24
haftmann@22803
    25
val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
haftmann@22803
    26
                    @{thm of_nat_eq_iff} RS iffD2]
webertj@20254
    27
(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
webertj@20254
    28
                    of_nat_less_iff RS iffD2 *)
webertj@20254
    29
haftmann@22803
    30
val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
haftmann@22803
    31
                    @{thm of_int_eq_iff} RS iffD2]
webertj@20254
    32
(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
webertj@20254
    33
                    of_int_less_iff RS iffD2 *)
paulson@14365
    34
paulson@14365
    35
in
paulson@14365
    36
webertj@20254
    37
val ratT = Type ("Rational.rat", [])
paulson@14387
    38
paulson@14365
    39
val rat_arith_setup =
wenzelm@24093
    40
  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
nipkow@15121
    41
   {add_mono_thms = add_mono_thms,
nipkow@15184
    42
    mult_mono_thms = mult_mono_thms,
webertj@20254
    43
    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
wenzelm@24093
    44
    lessD = lessD,  (*Can't change lessD: the rats are dense!*)
nipkow@15923
    45
    neqE =  neqE,
paulson@14387
    46
    simpset = simpset addsimps simps
wenzelm@18708
    47
                      addsimprocs simprocs}) #>
haftmann@24196
    48
  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #>
haftmann@24196
    49
  arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT)
paulson@14365
    50
paulson@14365
    51
end;