|
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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
