| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle vectors_dot_alt.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28