%------------------------------------------------------------------------------
% Powerseries
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

powerseries: THEORY

BEGIN

  IMPORTING prelude_aux, appendix, cauchy, mul, power, sum


  i,n,m: VAR nat
  cxs:   VAR [nat->cauchy_real]
  cx:    VAR cauchy_real
  x:     VAR real
  xs:    VAR [nat->real]

  powerseries (x,xs,n): real
   = sigma(0,n,(LAMBDA i: IF i = 0 THEN xs(i) ELSE xs(i)*x^i ENDIF))

  cauchy_powerseries (cx:cauchy_real,cxs:cauchys_real,n): cauchy_real
   = cauchy_sum ((LAMBDA i: IF i = 0 THEN cxs(i)
                            ELSE cauchy_mul(cxs(i),
                                 cauchy_power(cx,i)) ENDIF), n)

  powerseries_lemma: LEMMA (FORALL n: cauchy_prop(xs(n),cxs(n))) AND
                           cauchy_prop(x,cx) =>
                           cauchy_prop(powerseries(x,xs,m),
           cauchy_powerseries(cx,cxs,m))

END powerseries