(* Title: HOL/Real/rat_arith.ML
ID: $Id$
Author: Lawrence C Paulson
Copyright 2004 University of Cambridge
Simprocs for common factor cancellation & Rational coefficient handling
Instantiation of the generic linear arithmetic package for type rat.
*)
local
val simprocs = field_cancel_numeral_factors
val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
inst "a" "(number_of ?v)" @{thm right_distrib},
@{thm divide_1}, @{thm divide_zero_left},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
of_int_0, of_int_1, @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
@{thm of_int_mult}, @{thm of_int_of_nat_eq}]
val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
@{thm of_nat_eq_iff} RS iffD2]
(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
of_nat_less_iff RS iffD2 *)
val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
@{thm of_int_eq_iff} RS iffD2]
(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
of_int_less_iff RS iffD2 *)
in
val fast_rat_arith_simproc = Simplifier.simproc @{theory}
"fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
Fast_Arith.lin_arith_prover
val ratT = Type ("Rational.rat", [])
val rat_arith_setup =
Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms,
inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
neqE = neqE,
simpset = simpset addsimps simps
addsimprocs simprocs}) #>
arith_inj_const ("Nat.of_nat", HOLogic.natT --> ratT) #>
arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT) #>
(fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy))
end;