src/HOL/Real/rat_arith.ML
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15121 1198032bad25
child 15184 d2c19aea17bc
permissions -rw-r--r--
New theory header syntax.
     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 (*FIXME: these monomorphic versions are necessary because of a bug in the arith
    12   procedure*)
    13 val rat_mult_strict_left_mono =
    14     read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono;
    15 
    16 val rat_mult_left_mono =
    17  read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono;
    18 
    19 
    20 (****Instantiation of the generic linear arithmetic package for fields****)
    21 
    22 local
    23 
    24 val simprocs = field_cancel_numeral_factors
    25 
    26 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
    27 
    28 val rat_mult_mono_thms =
    29  [(rat_mult_strict_left_mono,
    30    cvar(rat_mult_strict_left_mono, hd(tl(prems_of rat_mult_strict_left_mono)))),
    31   (rat_mult_left_mono,
    32    cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))]
    33 
    34 val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals,
    35              inst "a" "(number_of ?v)" right_distrib,
    36              divide_1, divide_zero_left,
    37              times_divide_eq_right, times_divide_eq_left,
    38              minus_divide_left RS sym, minus_divide_right RS sym,
    39 	     of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
    40 	     of_int_mult, of_int_of_nat_eq];
    41 
    42 in
    43 
    44 val fast_rat_arith_simproc = 
    45  Simplifier.simproc (Theory.sign_of(the_context()))
    46   "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
    47   Fast_Arith.lin_arith_prover;
    48 
    49 val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2,
    50                     of_nat_eq_iff RS iffD2];
    51 
    52 val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2,
    53                     of_int_eq_iff RS iffD2];
    54 
    55 val ratT = Type("Rational.rat", []);
    56 
    57 val rat_arith_setup =
    58  [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    59    {add_mono_thms = add_mono_thms,
    60     mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms,
    61     inj_thms = int_inj_thms @ inj_thms,
    62     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
    63     simpset = simpset addsimps simps
    64                       addsimprocs simprocs}),
    65   arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT),
    66   arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT),
    67   arith_discrete ("Rational.rat",false),
    68   Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]];
    69 
    70 end;