Quelle  product_fseq.pvs

product_fseq[T: TYPE+ FROM real]: THEORY
%-------------------------------------------------------------------------------
%
%     products over finite sequences of reals
%
%     Author: Rick Butler    NASA Langley
%
%-------------------------------------------------------------------------------
BEGIN

   

   IMPORTING structures@fseqs[T], product_nat

   unk: VAR fsq[T]
   fs,fs1,fs2: VAR fseq    

   product(fs): real = IF length(fs) = 0 THEN 1
                       ELSE product(0,length(fs)-1,fs`seq)
                       ENDIF

   n,m: VAR nat

   len0: LEMMA length(fs) = 0 IMPLIES product(fs) = 1

   l1,l2: VAR nat

   product_fseq_shift: LEMMA  product(l1, l1 + l2 - 1,
                                 LAMBDA (n: nat): IF n < l1 THEN unk`seq(n)
                                                  ELSE fs`seq(n - l1)  ENDIF)
                         = product(0, l2 - 1, fs`seq)


   product_fseq_concat: LEMMA product(fs1 o fs2) = product(fs1) * product(fs2)


   product_fseq_empty_seq: LEMMA product(empty_seq) = 1

   product_fseq_split: LEMMA length(fs) > 1 IMPLIES
                            product(fs) = product(fs ^ (0, length(fs) - 2)) * 
                                           seq(fs)(length(fs) - 1) 

   x: VAR T
   product_fseq1:  LEMMA product(fseq1(x)) = x

END product_fseq