26 "fast_hypreal_arith" |
26 "fast_hypreal_arith" |
27 ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] |
27 ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] |
28 Fast_Arith.lin_arith_prover; |
28 Fast_Arith.lin_arith_prover; |
29 |
29 |
30 val hypreal_arith_setup = |
30 val hypreal_arith_setup = |
31 [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, neqE, simpset} => |
32 {add_mono_thms = add_mono_thms, |
32 {add_mono_thms = add_mono_thms, |
33 mult_mono_thms = mult_mono_thms, |
33 mult_mono_thms = mult_mono_thms, |
34 inj_thms = inj_thms @ real_inj_thms, |
34 inj_thms = inj_thms @ real_inj_thms, |
35 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!*) |
|
36 neqE = neqE, |
36 simpset = simpset}), |
37 simpset = simpset}), |
37 arith_inj_const ("HyperDef.hypreal_of_real", HOLogic.realT --> hyprealT), |
38 arith_inj_const ("HyperDef.hypreal_of_real", HOLogic.realT --> hyprealT), |
38 Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; |
39 Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; |
39 |
40 |
40 end; |
41 end; |