equal
deleted
inserted
replaced
29 qed |
29 qed |
30 qed |
30 qed |
31 |
31 |
32 |
32 |
33 definition |
33 definition |
34 exphr :: "real => hypreal" |
34 exphr :: "real => hypreal" where |
35 --{*define exponential function using standard part *} |
35 --{*define exponential function using standard part *} |
36 "exphr x = st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" |
36 "exphr x = st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" |
37 |
37 |
38 sinhr :: "real => hypreal" |
38 definition |
|
39 sinhr :: "real => hypreal" where |
39 "sinhr x = st(sumhr (0, whn, %n. (if even(n) then 0 else |
40 "sinhr x = st(sumhr (0, whn, %n. (if even(n) then 0 else |
40 ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))" |
41 ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))" |
41 |
42 |
42 coshr :: "real => hypreal" |
43 definition |
|
44 coshr :: "real => hypreal" where |
43 "coshr x = st(sumhr (0, whn, %n. (if even(n) then |
45 "coshr x = st(sumhr (0, whn, %n. (if even(n) then |
44 ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))" |
46 ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))" |
45 |
47 |
46 |
48 |
47 subsection{*Nonstandard Extension of Square Root Function*} |
49 subsection{*Nonstandard Extension of Square Root Function*} |