SSL product_seq.pvs

product_seq: THEORY
%------------------------------------------------------------------------------
% 
%  Obsolete theory for computing a product over a finite sequence
%  See new product theories and product_fseq in structures library
%
%  Author: Rick Butler NASA Langley
%
%------------------------------------------------------------------------------
BEGIN


   IMPORTING finite_sequences[posnat],
             product_seq_scaf

   fs: VAR finite_sequence

   product(fs): posnat = IF length(fs) = 0 THEN 1
                         ELSE product_rec(fs,length(fs)-1)
                         ENDIF

   fs1,fs2: VAR finite_sequence
   n,m: VAR nat

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

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


   product_empty_seq: LEMMA product(empty_seq) = 1

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

   product_ge: LEMMA FORALL (n: below(length(fs))): product(fs) >= seq(fs)(n)

   gen_seq1(n: posnat): finite_sequence[posnat] =
                               (# length := 1,
                                  seq := (LAMBDA (ii: below(1)): n) #)


   nn: VAR posnat
   product_concat1:  LEMMA nn * product(fs)  = product(fs o gen_seq1(nn))

%   IMPORTING product_nat

%   product_def: LEMMA product(fs) = product(0,length(fs)-1,fs`seq)

END product_seq