author | obua |
Sun, 09 May 2004 23:04:36 +0200 | |
changeset 14722 | 8e739a6eaf11 |
parent 13958 | c1c67582c9b5 |
child 15013 | 34264f5e4691 |
permissions | -rw-r--r-- |
12196 | 1 |
(* Title : Transcendental.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998,1999 University of Cambridge |
|
13958
c1c67582c9b5
New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
12196
diff
changeset
|
4 |
1999,2001 University of Edinburgh |
12196 | 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 |