src/HOL/Real/rat_arith.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17876 b9c92f384109
child 20254 58b71535ed00
permissions -rw-r--r--
setup: theory -> theory;
     1 (*  Title:      HOL/Real/rat_arith0.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 (****Instantiation of the generic linear arithmetic package for fields****)
    12 
    13 local
    14 
    15 val simprocs = field_cancel_numeral_factors
    16 
    17 val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals,
    18              inst "a" "(number_of ?v)" right_distrib,
    19              divide_1, divide_zero_left,
    20              times_divide_eq_right, times_divide_eq_left,
    21              minus_divide_left RS sym, minus_divide_right RS sym,
    22 	     of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
    23 	     of_int_mult, of_int_of_nat_eq];
    24 
    25 in
    26 
    27 val fast_rat_arith_simproc = 
    28  Simplifier.simproc (Theory.sign_of(the_context()))
    29   "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
    30   Fast_Arith.lin_arith_prover;
    31 
    32 val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2,
    33                     of_nat_eq_iff RS iffD2];
    34 
    35 val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2,
    36                     of_int_eq_iff RS iffD2];
    37 
    38 val ratT = Type("Rational.rat", []);
    39 
    40 val rat_arith_setup =
    41   Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    42    {add_mono_thms = add_mono_thms,
    43     mult_mono_thms = mult_mono_thms,
    44     inj_thms = int_inj_thms @ inj_thms,
    45     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
    46     neqE =  neqE,
    47     simpset = simpset addsimps simps
    48                       addsimprocs simprocs}) #>
    49   arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT) #>
    50   arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT) #>
    51   (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy));
    52 
    53 end;