src/HOL/Real/rat_arith.ML
author wenzelm
Tue Jul 31 19:40:24 2007 +0200 (2007-07-31)
changeset 24093 5d0ecd0c8f3c
parent 23346 1517207ec8b9
child 24196 f1dbfd7e3223
permissions -rw-r--r--
tuned LinArith setup;
     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 = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
    16              inst "a" "(number_of ?v)" @{thm right_distrib},
    17              @{thm divide_1}, @{thm divide_zero_left},
    18              @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    19              @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    20              @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
    21              @{thm of_int_minus}, @{thm of_int_diff},
    22              @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
    23 
    24 val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
    25                     @{thm of_nat_eq_iff} RS iffD2]
    26 (* not needed because x < (y::nat) can be rewritten as Suc x <= y:
    27                     of_nat_less_iff RS iffD2 *)
    28 
    29 val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
    30                     @{thm of_int_eq_iff} RS iffD2]
    31 (* not needed because x < (y::int) can be rewritten as x + 1 <= y:
    32                     of_int_less_iff RS iffD2 *)
    33 
    34 in
    35 
    36 val ratT = Type ("Rational.rat", [])
    37 
    38 val rat_arith_setup =
    39   LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    40    {add_mono_thms = add_mono_thms,
    41     mult_mono_thms = mult_mono_thms,
    42     inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
    43     lessD = lessD,  (*Can't change lessD: the rats are dense!*)
    44     neqE =  neqE,
    45     simpset = simpset addsimps simps
    46                       addsimprocs simprocs}) #>
    47   arith_inj_const ("Nat.of_nat", HOLogic.natT --> ratT) #>
    48   arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT)
    49 
    50 end;