|
circles_and_lines: THEORY
%------------------------------------------------------------------------
%
% ------ Intersection of parametric line and a circle -----
%
% See related theorems in vectors@closest_approach_2D
%
% Author: Cesar Munoz National Institute for Aerospace
%
%------------------------------------------------------------------------
BEGIN
IMPORTING quad_minmax
sx,sy,vx,vy : VAR real
% The first lemma states that if t1 and t2 are the intersection
% points with a circle of radius D, then the distance for all times
% between t1 and t2 is less than D
t1_lt_t2_lt_D : LEMMA FORALL (t,t1,t2,D:real):
vx*vx + vy*vy /= 0 AND
t1 < t2 AND
(sx+vx*t1)*(sx+vx*t1) + (sy+vy*t1)*(sy+vy*t1) = D AND
(sx+vx*t2)*(sx+vx*t2) + (sy+vy*t2)*(sy+vy*t2) = D AND
t1 < t AND t < t2 IMPLIES
(sx+vx*t)*(sx+vx*t) + (sy+vy*t)*(sy+vy*t) < D
% The second lemma is the reciprocal of the previous lemma. It states that
% if the distance at time t is less than D, then t is between t1 and
% t2.
lt_D_t1_lt_t2 : LEMMA FORALL (t,t1,t2,D:real):
vx*vx + vy*vy /= 0 AND
t1 < t2 AND
(sx+vx*t1)*(sx+vx*t1) + (sy+vy*t1)*(sy+vy*t1) = D
AND
(sx+vx*t2)*(sx+vx*t2) + (sy+vy*t2)*(sy+vy*t2) = D
AND
(sx+vx*t)*(sx+vx*t) + (sy+vy*t)*(sy+vy*t) < D IMPLIES
t1 < t AND t < t2
% The third lemma states that if there are no intersection points with
% a circle of radius D then the distance at any time is greater than D.
discr_le_0 : LEMMA FORALL (t,discrm,D:real):
discrm = 2*sx*vx*sy*vy + D*(vx*vx+vy*vy) -
(sx*sx*vy*vy + sy*sy*vx*vx) AND
discrm <= 0 AND vx*vx + vy*vy /= 0
IMPLIES
(sx+vx*t)*(sx+vx*t) + (sy+vy*t)*(sy+vy*t) >= D
END circles_and_lines
¤ Dauer der Verarbeitung: 0.20 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.
|
