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