Quelle between_2D.pvs Sprache: PVS

between_2D: THEORY
%------------------------------------------------------------------------------
%
%    Provides:
%       between?(v1,v2)(xx)  -- true iff xx is between? v1 and v2 (within 180 of each other)
%       betw?(v1,v2)(xx)     -- true iff xx is between? v1 and v2
%
%    Author:
%        Rick Butler            NASA Langley Research Center
%
%    VERY EXPERIMENTAL !!!!
%
%------------------------------------------------------------------------------
BEGIN

   %% --------- between? assuming v1 and v2 are within 180 of each other ----------

   IMPORTING vectors_2D, trig@trig_basic, trig@trig_ineq, angles_2D

   between?(v1,v2: Vect2)(xx: Vect2): bool =
       LET k1 = norm(v1),
           k2 = norm(v2),
           kx = norm(xx) IN
          v1*(kx*v2-k2*xx) <= 0 AND
          v2*(kx*v1-k1*xx) <= 0

   a1,a2,a3: VAR real
   v,v1,v2,v3: VAR Vect2
   k: VAR posreal
   k1,k2,k3: VAR posreal

   between_sym: LEMMA between?(v1,v3)(v2) IFF between?(v3,v1)(v2)

   between_cos: LEMMA LET v1 = v_from(a1,k1),
                          v2 = v_from(a2,k2),
                          v3 = v_from(a3,k3) IN
                      between?(v1,v3)(v2) IFF
                          ( cos(a3 - a1) <= cos(a3 - a2) AND
                            cos(a3 - a1) <= cos(a2 - a1) )

   is_between: LEMMA  a1 <= a2 AND a2 <= a3 AND
                      a3 - a1 <= pi AND a2 - a1 <= pi
                   IMPLIES
                      LET v1 = v_from(a1,k1),
                          v2 = v_from(a2,k2),
                          v3 = v_from(a3,k3) IN
                        between?(v1,v3)(v2)

   is_between2: COROLLARY 0 <= a1 AND a1 <= a2 AND a2 <= a3 AND a3 <= pi IMPLIES
                    LET v1 = v_from(a1,k1),
                        v2 = v_from(a2,k2),
                        v3 = v_from(a3,k3) IN
                    between?(v1,v3)(v2)

   between_lem: LEMMA LET v1 = v_from(a1,k1),
                       v2 = v_from(a2,k2),
                       v3 = v_from(a3,k3) IN
                    0 <= a1 AND a1 <= pi AND
                    0 <= a2 AND a2 <= pi AND
                    0 <= a3 AND a3 <= pi AND
                    a1 <= a3 AND
                    between?(v1,v3)(v2)
                        IMPLIES (a1 <= a2 AND a2 <= a3)

   between_thm: THEOREM LET v1 = v_from(a1,k1),
                       v2 = v_from(a2,k2),
                       v3 = v_from(a3,k3) IN
                    0 <= a1 AND a1 <= pi AND
                    0 <= a2 AND a2 <= pi AND
                    0 <= a3 AND a3 <= pi AND
                    between?(v1,v3)(v2)
                        IMPLIES (a1 <= a2 AND a2 <= a3) OR
                                (a3 <= a2 AND a2 <= a1)

%% ------------ betw ----------------

   betw?(v1,v2: Nz_vect2)(xx: Nz_vect2): bool =
           angle(v1) <= angle(xx) AND angle(xx) <= angle(v2)

   betw_between: LEMMA FORALL (v1,v2,xx: Nz_vect2):
                          angle(v2) - angle(v1) <= pi AND
                          angle(xx) - angle(v1) <= pi AND
                          betw?(v1,v2)(xx) IMPLIES between?(v1,v2)(xx)

   between_betw: LEMMA FORALL (v1,v2,xx: Nz_vect2):
                       angle(v1) <= pi AND angle(xx) <= pi AND angle(v2) <= pi AND
                       angle(v1) <= angle(v2) AND
                       between?(v1,v2)(xx) IMPLIES betw?(v1,v2)(xx)

END between_2D

quality94%

¤ Dauer der Verarbeitung: 0.13 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.