src/HOL/Complex/CSeries.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex/CSeries.thy	Mon May 05 18:22:31 2003 +0200
@@ -0,0 +1,30 @@
+(*  Title       : CSeries.thy
+    Author      : Jacques D. Fleuriot
+    Copyright   : 2002  University of Edinburgh
+    Description : Finite summation and infinite series for complex numbers
+*)
+
+CSeries = CStar +
+
+consts sumc :: "[nat,nat,(nat=>complex)] => complex"
+primrec
+   sumc_0   "sumc m 0 f = 0"
+   sumc_Suc "sumc m (Suc n) f = (if n < m then 0 else sumc m n f + f(n))"
+
+(*  
+constdefs
+
+   needs convergence of complex sequences  
+
+  csums  :: [nat=>complex,complex] => bool     (infixr 80)
+   "f sums s  == (%n. sumr 0 n f) ----C> s"
+  
+   csummable :: (nat=>complex) => bool
+   "csummable f == (EX s. f csums s)"
+
+   csuminf   :: (nat=>complex) => complex
+   "csuminf f == (@s. f csums s)"
+*)
+
+end
+