|
1 (* Title: HOL/Real/hypreal_arith.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, TU Muenchen |
|
4 Copyright 1999 TU Muenchen |
|
5 |
|
6 Augmentation of hypreal linear arithmetic with rational coefficient handling |
|
7 *) |
|
8 |
|
9 local |
|
10 |
|
11 (* reduce contradictory <= to False *) |
|
12 val simps = [True_implies_equals,inst "w" "number_of ?v" hypreal_add_mult_distrib2, |
|
13 hypreal_divide_1,hypreal_times_divide1_eq,hypreal_times_divide2_eq]; |
|
14 |
|
15 val simprocs = [hypreal_cancel_numeral_factors_divide]; |
|
16 |
|
17 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
|
18 |
|
19 val hypreal_mult_mono_thms = |
|
20 [(rotate_prems 1 hypreal_mult_less_mono2, |
|
21 cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), |
|
22 (hypreal_mult_le_mono2, |
|
23 cvar(hypreal_mult_le_mono2, hd(tl(prems_of hypreal_mult_le_mono2))))] |
|
24 |
|
25 in |
|
26 |
|
27 val hypreal_arith_setup = |
|
28 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
|
29 {add_mono_thms = add_mono_thms, |
|
30 mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, |
|
31 inj_thms = inj_thms, |
|
32 lessD = lessD, |
|
33 simpset = simpset addsimps simps addsimprocs simprocs})]; |
|
34 |
|
35 end; |
|
36 |
|
37 (* |
|
38 Procedure "assoc_fold" needed? |
|
39 *) |