|
10751
|
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 |
*)
|