|
13958
|
1 |
(* Title : HTranscendental.thy
|
|
|
2 |
Author : Jacques D. Fleuriot
|
|
|
3 |
Copyright : 2001 University of Edinburgh
|
|
|
4 |
Description : Nonstandard extensions of transcendental functions
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
HTranscendental = Transcendental + IntFloor +
|
|
|
8 |
|
|
|
9 |
constdefs
|
|
|
10 |
|
|
|
11 |
|
|
|
12 |
(* define exponential function using standard part *)
|
|
|
13 |
exphr :: real => hypreal
|
|
|
14 |
"exphr x == st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
|
|
|
15 |
|
|
|
16 |
sinhr :: real => hypreal
|
|
|
17 |
"sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
|
|
|
18 |
((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
|
|
|
19 |
|
|
|
20 |
coshr :: real => hypreal
|
|
|
21 |
"coshr x == st(sumhr (0, whn, %n. (if even(n) then
|
|
|
22 |
((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
|
|
|
23 |
end |