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 : LEMMAFORALL (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 : LEMMAFORALL (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 : LEMMAFORALL (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.11 Sekunden
(vorverarbeitet)
¤
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.
