341 FIXME: we should declare this, as for type int, but many proofs would break. |
340 FIXME: we should declare this, as for type int, but many proofs would break. |
342 It replaces x+-y by x-y. |
341 It replaces x+-y by x-y. |
343 Addsimps [symmetric hypreal_diff_def] |
342 Addsimps [symmetric hypreal_diff_def] |
344 *) |
343 *) |
345 |
344 |
346 use "hypreal_arith.ML" |
345 declaration {* |
347 declaration {* K hypreal_arith_setup *} |
346 K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2, |
|
347 @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2] |
|
348 #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one}, |
|
349 @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus}, |
|
350 @{thm star_of_diff}, @{thm star_of_mult}] |
|
351 #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}) |
|
352 #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory} |
|
353 "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] |
|
354 (K Lin_Arith.lin_arith_simproc)])) |
|
355 *} |
348 |
356 |
349 |
357 |
350 subsection {* Exponentials on the Hyperreals *} |
358 subsection {* Exponentials on the Hyperreals *} |
351 |
359 |
352 lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" |
360 lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" |