src/HOL/Hyperreal/Transcendental.thy
author paulson
Thu Nov 15 16:12:49 2001 +0100 (2001-11-15)
changeset 12196 a3be6b3a9c0b
child 13958 c1c67582c9b5
permissions -rw-r--r--
new theories from Jacques Fleuriot
paulson@12196
     1
(*  Title       : Transcendental.thy
paulson@12196
     2
    Author      : Jacques D. Fleuriot
paulson@12196
     3
    Copyright   : 1998,1999 University of Cambridge
paulson@12196
     4
                  1999 University of Edinburgh
paulson@12196
     5
    Description : Power Series, transcendental functions etc.
paulson@12196
     6
*)
paulson@12196
     7
paulson@12196
     8
Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim + 
paulson@12196
     9
paulson@12196
    10
constdefs
paulson@12196
    11
    root :: [nat,real] => real
paulson@12196
    12
    "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
paulson@12196
    13
paulson@12196
    14
    sqrt :: real => real
paulson@12196
    15
    "sqrt x == root 2 x"
paulson@12196
    16
paulson@12196
    17
    exp :: real => real
paulson@12196
    18
    "exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))"
paulson@12196
    19
paulson@12196
    20
    sin :: real => real
paulson@12196
    21
    "sin x == suminf(%n. (if even(n) then 0 else
paulson@12196
    22
             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
paulson@12196
    23
 
paulson@12196
    24
    diffs :: (nat => real) => nat => real
paulson@12196
    25
    "diffs c == (%n. real (Suc n) * c(Suc n))"
paulson@12196
    26
paulson@12196
    27
    cos :: real => real
paulson@12196
    28
    "cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
paulson@12196
    29
                          else 0) * x ^ n)"
paulson@12196
    30
  
paulson@12196
    31
    ln :: real => real
paulson@12196
    32
    "ln x == (@u. exp u = x)"
paulson@12196
    33
paulson@12196
    34
    pi :: real
paulson@12196
    35
    "pi == 2 * (@x. 0 <= (x::real) & x <= 2 & cos x = 0)"
paulson@12196
    36
paulson@12196
    37
    tan :: real => real
paulson@12196
    38
    "tan x == (sin x)/(cos x)"
paulson@12196
    39
paulson@12196
    40
    arcsin :: real => real
paulson@12196
    41
    "arcsin y == (@x. -(pi/2) <= x & x <= pi/2 & sin x = y)"
paulson@12196
    42
paulson@12196
    43
    arcos :: real => real
paulson@12196
    44
    "arcos y == (@x. 0 <= x & x <= pi & cos x = y)"
paulson@12196
    45
     
paulson@12196
    46
    arctan :: real => real
paulson@12196
    47
    "arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
paulson@12196
    48
  
paulson@12196
    49
end