12196

1 
(* Title : Transcendental.thy


2 
Author : Jacques D. Fleuriot


3 
Copyright : 1998,1999 University of Cambridge


4 
1999 University of Edinburgh


5 
Description : Power Series, transcendental functions etc.


6 
*)


7 


8 
Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim +


9 


10 
constdefs


11 
root :: [nat,real] => real


12 
"root n x == (@u. ((0::real) < x > 0 < u) & (u ^ n = x))"


13 


14 
sqrt :: real => real


15 
"sqrt x == root 2 x"


16 


17 
exp :: real => real


18 
"exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))"


19 


20 
sin :: real => real


21 
"sin x == suminf(%n. (if even(n) then 0 else


22 
(( 1) ^ ((n  Suc 0) div 2))/(real (fact n))) * x ^ n)"


23 


24 
diffs :: (nat => real) => nat => real


25 
"diffs c == (%n. real (Suc n) * c(Suc n))"


26 


27 
cos :: real => real


28 
"cos x == suminf(%n. (if even(n) then (( 1) ^ (n div 2))/(real (fact n))


29 
else 0) * x ^ n)"


30 


31 
ln :: real => real


32 
"ln x == (@u. exp u = x)"


33 


34 
pi :: real


35 
"pi == 2 * (@x. 0 <= (x::real) & x <= 2 & cos x = 0)"


36 


37 
tan :: real => real


38 
"tan x == (sin x)/(cos x)"


39 


40 
arcsin :: real => real


41 
"arcsin y == (@x. (pi/2) <= x & x <= pi/2 & sin x = y)"


42 


43 
arcos :: real => real


44 
"arcos y == (@x. 0 <= x & x <= pi & cos x = y)"


45 


46 
arctan :: real => real


47 
"arctan y == (@x. (pi/2) < x & x < pi/2 & tan x = y)"


48 


49 
end
