src/HOL/Hyperreal/HTranscendental.thy
author paulson
Mon May 05 18:23:40 2003 +0200 (2003-05-05)
changeset 13958 c1c67582c9b5
child 14420 4e72cd222e0b
permissions -rw-r--r--
New material on integration, etc. Moving Hyperreal/ex
to directory Complex
paulson@13958
     1
(*  Title       : HTranscendental.thy
paulson@13958
     2
    Author      : Jacques D. Fleuriot
paulson@13958
     3
    Copyright   : 2001 University of Edinburgh
paulson@13958
     4
    Description : Nonstandard extensions of transcendental functions
paulson@13958
     5
*)
paulson@13958
     6
paulson@13958
     7
HTranscendental = Transcendental + IntFloor + 
paulson@13958
     8
paulson@13958
     9
constdefs
paulson@13958
    10
paulson@13958
    11
paulson@13958
    12
    (* define exponential function using standard part *)
paulson@13958
    13
    exphr :: real => hypreal
paulson@13958
    14
    "exphr x ==  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" 
paulson@13958
    15
paulson@13958
    16
    sinhr :: real => hypreal
paulson@13958
    17
    "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
paulson@13958
    18
             ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
paulson@13958
    19
  
paulson@13958
    20
    coshr :: real => hypreal
paulson@13958
    21
    "coshr x == st(sumhr (0, whn, %n. (if even(n) then
paulson@13958
    22
            ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
paulson@13958
    23
end