src/HOL/Real/Hyperreal/Series.thy
changeset 10045 c76b73e16711
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/Series.thy	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,27 @@
     1.4 +(*  Title       : Series.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Finite summation and infinite series
     1.8 +*) 
     1.9 +
    1.10 +
    1.11 +Series = SEQ + Lim +
    1.12 +
    1.13 +consts sumr :: "[nat,nat,(nat=>real)] => real"
    1.14 +primrec
    1.15 +   sumr_0   "sumr m 0 f = #0"
    1.16 +   sumr_Suc "sumr m (Suc n) f = (if n < m then #0 
    1.17 +                               else sumr m n f + f(n))"
    1.18 +
    1.19 +constdefs
    1.20 +   sums  :: [nat=>real,real] => bool     (infixr 80)
    1.21 +   "f sums s  == (%n. sumr 0 n f) ----> s"
    1.22 +
    1.23 +   summable :: (nat=>real) => bool
    1.24 +   "summable f == (EX s. f sums s)"
    1.25 +
    1.26 +   suminf   :: (nat=>real) => real
    1.27 +   "suminf f == (@s. f sums s)"
    1.28 +end
    1.29 +
    1.30 +