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