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