src/HOL/Hyperreal/Transcendental.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/Transcendental.thy	Thu Nov 15 16:12:49 2001 +0100
@@ -0,0 +1,49 @@
+(*  Title       : Transcendental.thy
+    Author      : Jacques D. Fleuriot
+    Copyright   : 1998,1999 University of Cambridge
+                  1999 University of Edinburgh
+    Description : Power Series, transcendental functions etc.
+*)
+
+Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim + 
+
+constdefs
+    root :: [nat,real] => real
+    "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
+
+    sqrt :: real => real
+    "sqrt x == root 2 x"
+
+    exp :: real => real
+    "exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))"
+
+    sin :: real => real
+    "sin x == suminf(%n. (if even(n) then 0 else
+             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
+ 
+    diffs :: (nat => real) => nat => real
+    "diffs c == (%n. real (Suc n) * c(Suc n))"
+
+    cos :: real => real
+    "cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
+                          else 0) * x ^ n)"
+  
+    ln :: real => real
+    "ln x == (@u. exp u = x)"
+
+    pi :: real
+    "pi == 2 * (@x. 0 <= (x::real) & x <= 2 & cos x = 0)"
+
+    tan :: real => real
+    "tan x == (sin x)/(cos x)"
+
+    arcsin :: real => real
+    "arcsin y == (@x. -(pi/2) <= x & x <= pi/2 & sin x = y)"
+
+    arcos :: real => real
+    "arcos y == (@x. 0 <= x & x <= pi & cos x = y)"
+     
+    arctan :: real => real
+    "arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
+  
+end