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