SSL basis_2D.pvs Sprache: PVS

basis_2D: THEORY
%------------------------------------------------------------------------------
%     Orthonormal Basis for 2D Vectors      3-4-2010
%
%     Authors: Anthony Narkawicz     NASA Langley
%              Ricky Butler          NASA Langley
%------------------------------------------------------------------------------

BEGIN

   IMPORTING vectors_2D

   e1,e2  : VAR Vect2
   w,w1,w2: VAR Vect2
   a1,a2,b1,b2  : VAR real

   orthogonal_basis: LEMMA
     e1 /= zero AND
     e2 /= zero AND
     orthogonal?(e1,e2) IMPLIES
     w = ((w*e1)/sqv(e1))*e1 + ((w*e2)/sqv(e2))*e2

   orthonormal?(e1,e2): bool =
     orthogonal?(e1,e2) AND e1 /= zero AND norm(e1) = 1 AND
     e2 /= zero AND norm(e2) = 1

   orthonormal_basis: LEMMA FORALL (w:Vect2):
     orthonormal?(e1,e2) IMPLIES
     w = (w*e1)*e1 + (w*e2)*e2

   basis_two_dot_zero: LEMMA
     w /= zero AND e1 /= zero AND w*e1 = 0 AND w*e2 = 0
     IMPLIES
     (EXISTS (c:real): c*e1 = e2)

   basis_add: LEMMA
     %% orthonormal?(e1,e2) AND
     w1 = (w1*e1)*e1 + (w1*e2)*e2 AND
     w2 = (w2*e1)*e1 + (w2*e2)*e2
   IMPLIES
     w1+w2 = ((w1+w2)*e1)*e1 + ((w1+w2)*e2)*e2

   basis_sub: LEMMA
     %% orthonormal?(e1,e2) AND
     w1 = (w1*e1)*e1 + (w1*e2)*e2 AND
     w2 = (w2*e1)*e1 + (w2*e2)*e2
   IMPLIES
     w1-w2 = ((w1-w2)*e1)*e1 + ((w1-w2)*e2)*e2

   basis_sqv: LEMMA FORALL (a,b: real,w: Vect2):
     orthonormal?(e1,e2) AND
     w = (a)*e1 + (b)*e2
     IMPLIES
        sqv(w) = sq(a) + sq(b)

   basis_dot: LEMMA  FORALL (a,b,c,d: real):
     orthonormal?(e1,e2) IMPLIES
     LET s = (a)*e1 + (b)*e2,
         v = (c)*e1 + (d)*e2
     IN
        s*v = a*c + b*d


   IMPORTING perpendicular_2D

   basis_perpR: LEMMA  FORALL (a,b: real):
     LET e2 = perpR(e1),
         s = (a)*e1 + (b)*e2
     IN
        perpR(s) = (a)*e2 - b*e1

   vh_vp_orthon: LEMMA FORALL (v: Nz_vect2):
     LET
       vh = ^(v),
       vp = perpR(vh)
     IN
      orthonormal?(vh, vp)

  orthogonal_basis_sqv: LEMMA
    orthogonal?(e1,e2) AND
    w = a1*e1 + a2*e2 IMPLIES
    sqv(w) = sq(a1)*sqv(e1) + sq(a2)*sqv(e2)

  orthonormal_basis_sqv: LEMMA
    orthonormal?(e1,e2) AND
    w = a1*e1 + a2*e2 IMPLIES
    sqv(w) = sq(a1) + sq(a2)

  orthogonal_basis_norm: LEMMA
    orthogonal?(e1,e2) AND
    w = a1*e1 + a2*e2 IMPLIES
    norm(w) = sqrt(sq(a1)*sqv(e1) + sq(a2)*sqv(e2))

  orthonormal_basis_norm: LEMMA
    orthonormal?(e1,e2) AND
    w = a1*e1 + a2*e2 IMPLIES
    norm(w) = sqrt(sq(a1) + sq(a2))

  orthogonal_basis_norm_ge: LEMMA
    orthogonal?(e1,e2) AND
    w = a1*e1 + a2*e2 IMPLIES
    norm(w) >= abs(a1)*norm(e1)

  orthonormal_basis_norm_ge: LEMMA
    orthonormal?(e1,e2) AND
    w = a1*e1 + a2*e2 IMPLIES
    norm(w) >= abs(a1)

  orthogonal_basis_dot: LEMMA
    orthogonal?(e1,e2) AND
    w1 = a1*e1 + a2*e2 AND
    w2 = b1*e1 + b2*e2 IMPLIES
    w1*w2 = (a1*b1)*sqv(e1) + (a2*b2)*sqv(e2)

  orthonormal_basis_dot: LEMMA
    orthonormal?(e1,e2) AND
    w1 = a1*e1 + a2*e2 AND
    w2 = b1*e1 + b2*e2 IMPLIES
    w1*w2 = a1*b1 + a2*b2

END basis_2D

quality97%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.