|
28308
|
1 |
(* Title: HOL/NSA/hypreal_arith.ML
|
|
27468
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow, TU Muenchen
|
|
|
4 |
Copyright 1999 TU Muenchen
|
|
|
5 |
|
|
|
6 |
Simprocs for common factor cancellation & Rational coefficient handling
|
|
|
7 |
|
|
|
8 |
Instantiation of the generic linear arithmetic package for type hypreal.
|
|
|
9 |
*)
|
|
|
10 |
|
|
|
11 |
local
|
|
|
12 |
|
|
|
13 |
val simps = [thm "star_of_zero",
|
|
|
14 |
thm "star_of_one",
|
|
|
15 |
thm "star_of_number_of",
|
|
|
16 |
thm "star_of_add",
|
|
|
17 |
thm "star_of_minus",
|
|
|
18 |
thm "star_of_diff",
|
|
|
19 |
thm "star_of_mult"]
|
|
|
20 |
|
|
|
21 |
val real_inj_thms = [thm "star_of_le" RS iffD2,
|
|
|
22 |
thm "star_of_less" RS iffD2,
|
|
|
23 |
thm "star_of_eq" RS iffD2]
|
|
|
24 |
|
|
|
25 |
in
|
|
|
26 |
|
|
|
27 |
val hyprealT = Type ("StarDef.star", [HOLogic.realT]);
|
|
|
28 |
|
|
|
29 |
val fast_hypreal_arith_simproc =
|
|
|
30 |
Simplifier.simproc (the_context ())
|
|
|
31 |
"fast_hypreal_arith"
|
|
|
32 |
["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
|
|
|
33 |
(K LinArith.lin_arith_simproc);
|
|
|
34 |
|
|
|
35 |
val hypreal_arith_setup =
|
|
|
36 |
LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
|
|
|
37 |
{add_mono_thms = add_mono_thms,
|
|
|
38 |
mult_mono_thms = mult_mono_thms,
|
|
|
39 |
inj_thms = real_inj_thms @ inj_thms,
|
|
|
40 |
lessD = lessD, (*Can't change lessD: the hypreals are dense!*)
|
|
|
41 |
neqE = neqE,
|
|
|
42 |
simpset = simpset addsimps simps}) #>
|
|
|
43 |
arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
|
|
|
44 |
Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
|
|
|
45 |
|
|
|
46 |
end;
|