|
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
[ Seitenstruktur0.4Drucken
etwas mehr zur Ethik
]
|
