SSL vectors_dot_alt.pvs

vectors_dot_alt[n: posnat]: THEORY
%------------------------------------------------------------------------------
% The n-dimensional dot-product  is defined as follows:
%
%    Vector    : TYPE = [below(n) -> real]
%
%    *(u,v): real = sigma[below(n)](0,n-1,LAMBDA i:u(i)*v(i)) 
%
%
% For many situations this is a good definition.   But, the summation
% function is defined with parameter [below(n)] which can be a real nuisance when trying
% to perform induction proofs (e.g. See deriv_dot_prod in the vect_analysis library).
% The following alternate definition uses a sigma[nat] which eliminates this problem
% though it is uglier because of the need to guard the u(j)*v(j) with an IF-THEN-ELSE
%------------------------------------------------------------------------------

BEGIN
   
   IMPORTING vectors[n], reals@sigma_nat

   u,v,w     : VAR Vector
   i         : VAR Index

   dot(u,v): real = sigma[nat](0,n-1, LAMBDA (j: nat): IF j < n THEN u(j)*v(j)
                                      ELSE 0 ENDIF)

   m: VAR nat
   dot_rew_prep: LEMMA m < n IMPLIES
                       sigma[nat](0, m, LAMBDA (j: nat): IF j < n THEN u(j) * v(j) ELSE 0 ENDIF)
                       = sigma(0, m, LAMBDA (i: Index[n]): u(i) * v(i))

   dot_rew: LEMMA dot(u,v) = u*v

END vectors_dot_alt