Quelle perpendicular_3D.pvs Sprache: PVS

perpendicular_3D: THEORY
%----------------------------------------------------------------------------
%
%         Q.
%         .\  .
%         . \   .
%         .  \    .  d
%         .   \     .            .
%         .    \      .       .                 W  = Q - P0
%       W .   c \       .  .
%         .      \       *   P0 + t*v
%         .       \   .                         del = (t-tp)*v
%         .        *
%         .      .   P0 + tp*v
%         .   .
%         ..
%         P0
%
%
%    determine tp  = intersection of perpendicular line from Q to line (P0,v)
%                  = perp_pt(Q-P0,nzv) = (W*v)/(v*v)
%               c  = length of this perpendicular line
%              del = (t-tp)*v
%
%    dist(q,L)     = distance from point q to line defined by perpendicular
%
%  Author: Ricky Butler              NASA Langley Research Center
%
%----------------------------------------------------------------------------
BEGIN

    IMPORTING distance_3D

    t,tp: VAR real
    P0,Q,v,w,c,d,x,y,del: VAR Vect3

%  In three dimensions, there are an infinite number of vectors perpendicular to a given vector
%  but given a line and a point (not on line), the perpendicular line is uniquely determined.

    nzv: VAR Nz_vect3
    perp_pt(Q,P0,nzv): real = (Q-P0)*nzv/(nzv*nzv)

    perp_is_normal: LEMMA tp = perp_pt(Q,P0,nzv)
                           IMPLIES
                              LET c = (P0 + tp*nzv) - Q,
                                  del = (t-tp)*nzv       IN
                                     del*c = 0

    perp_is_min: LEMMA tp = perp_pt(Q,P0,nzv)
                       IMPLIES
                           LET d = (P0 + t*nzv) - Q,
                               c = (P0 + tp*nzv) - Q  IN
                             norm(d) >= norm(c)

    perp_gt_del: LEMMA tp = perp_pt(Q,P0,nzv)
                        IMPLIES
                           LET d = (P0 + t*nzv) - Q,
                               del = (t-tp)*nzv   IN
                             norm(d) >= norm(del)

    perp_comps: LEMMA tp = perp_pt(Q, P0,nzv)
                      IMPLIES
                         LET d = (P0 + t*nzv) - Q,
                             c = (P0 + tp*nzv) - Q,
                             del = (t-tp)*nzv   IN
                      sq(norm(d)) = sq(norm(del)) + sq(norm(c))

%----------------------------------------------------------------------------

    IMPORTING lines_3D

%   ----- distance from a point to a line --------

    p,q: VAR Vect3
    L: Var Line

    perp_pt(q,L): real = (q-p(L))*v(L)/(v(L)*v(L))

    dist(q,L): nnreal =  LET tp = perp_pt(q,L) IN
                                dist(p(L) + tp*v(L),q)

    dist_is_min: THEOREM on_line?(p,L) IMPLIES
                          dist(q,p) >= dist(q,L)

    L1, L2: Var Line
    perpendicular?(L1,L2): bool = orthogonal?(v(L1),v(L2))

    perp_pt_perp: LEMMA q /= p(L) + perp_pt(q,L)*v(L) IMPLIES
                           perpendicular?(L,line_from(q,p(L)
                                                       + perp_pt(q,L)*v(L)))

%    perp_pt_parallel_perp: LEMMA LET tp = perp_pt(q,L1),
%                                  L2 = line_from(q,p(L1)+tp*v(L1)) IN
%                                     parallel?(v(L2),perp(v))

END perpendicular_3D

quality100%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

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.