src/HOL/Hyperreal/HSeries.thy
author wenzelm
Wed, 24 Jul 2002 22:13:02 +0200
changeset 13419 902ec83c1ca9
parent 10834 a7897aebbffc
child 14413 7ce47ab455eb
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : HSeries.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     4
    Description : Finite summation and infinite series
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
                  for hyperreals
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     6
*) 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     7
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     8
HSeries = Series +
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     9
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    10
consts 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    11
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    12
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    13
defs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    14
   sumhr_def
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    15
   "sumhr p
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    16
       == Abs_hypreal(UN X:Rep_hypnat(fst p). 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    17
              UN Y: Rep_hypnat(fst(snd p)).
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
    18
              hyprel``{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    19
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    20
constdefs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    21
   NSsums  :: [nat=>real,real] => bool     (infixr 80)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    22
   "f NSsums s  == (%n. sumr 0 n f) ----NS> s"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    23
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    24
   NSsummable :: (nat=>real) => bool
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    25
   "NSsummable f == (EX s. f NSsums s)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    26
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    27
   NSsuminf   :: (nat=>real) => real
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    28
   "NSsuminf f == (@s. f NSsums s)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    29
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    30
end