6 Simprocs for common factor cancellation & Rational coefficient handling |
6 Simprocs for common factor cancellation & Rational coefficient handling |
7 |
7 |
8 Instantiation of the generic linear arithmetic package for type hypreal. |
8 Instantiation of the generic linear arithmetic package for type hypreal. |
9 *) |
9 *) |
10 |
10 |
11 (*FIXME DELETE*) |
|
12 val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2"; |
|
13 |
|
14 val hypreal_mult_left_mono = |
|
15 read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono; |
|
16 |
|
17 |
|
18 (****Instantiation of the generic linear arithmetic package****) |
11 (****Instantiation of the generic linear arithmetic package****) |
19 |
12 |
20 |
13 |
21 local |
14 local |
22 |
|
23 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
|
24 |
|
25 val hypreal_mult_mono_thms = |
|
26 [(rotate_prems 1 hypreal_mult_less_mono2, |
|
27 cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), |
|
28 (hypreal_mult_left_mono, |
|
29 cvar(hypreal_mult_left_mono, hd(tl(prems_of hypreal_mult_left_mono))))] |
|
30 |
15 |
31 val real_inj_thms = [hypreal_of_real_le_iff RS iffD2, |
16 val real_inj_thms = [hypreal_of_real_le_iff RS iffD2, |
32 hypreal_of_real_less_iff RS iffD2, |
17 hypreal_of_real_less_iff RS iffD2, |
33 hypreal_of_real_eq_iff RS iffD2]; |
18 hypreal_of_real_eq_iff RS iffD2]; |
34 |
19 |
43 Fast_Arith.lin_arith_prover; |
28 Fast_Arith.lin_arith_prover; |
44 |
29 |
45 val hypreal_arith_setup = |
30 val hypreal_arith_setup = |
46 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
31 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
47 {add_mono_thms = add_mono_thms, |
32 {add_mono_thms = add_mono_thms, |
48 mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, |
33 mult_mono_thms = mult_mono_thms, |
49 inj_thms = inj_thms @ real_inj_thms, |
34 inj_thms = inj_thms @ real_inj_thms, |
50 lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*) |
35 lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*) |
51 simpset = simpset}), |
36 simpset = simpset}), |
52 arith_inj_const ("HyperDef.hypreal_of_real", HOLogic.realT --> hyprealT), |
37 arith_inj_const ("HyperDef.hypreal_of_real", HOLogic.realT --> hyprealT), |
53 arith_discrete ("HyperDef.hypreal",false), |
38 arith_discrete ("HyperDef.hypreal",false), |