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 