lines_3D: THEORY
%----------------------------------------------------------------------------
% The traditional way to defines a line L is by specifying two distinct points,
% P0 and P1, on it.  
% 
% A line L can also be defined by a point and a direction.  Let P0 be a
% point on the line L and let dv be a nonzero vector specifying the direction
% of the line.  This is equivalent to the two point definition, since we
% could just put dv=(P1-P0).
 
% We can also add dynamics to our line.  If we assume a particle is
% moving in a line with a constant velocity, then we can define
% this linear motion using the location of the point at time zero,
% a velocity vector and a time parameter t:
% 
%       p0 + t*vel
% 
% which provides the location of the particle at time t.
%
% Author: Ricky Butler              NASA Langley Research Center
%----------------------------------------------------------------------------
BEGIN

   IMPORTING distance_3D
                                     %     Basic        |   Dynamic
                                     %------------------|-----------------
   Line : Type = [# p: Vect3,        % point on the line| position at time 0
                    v: Nz_vect3 #]   % direction vector | velocity vector

   Line3D: TYPE = Line  ; 

  -(L: Line): Line = (# p := L`p, v := -L`v #)

   p0 (L: Line): MACRO Vect3 = p(L)
   vel(L: Line): MACRO Vect3 = v(L)

   vv: VAR [Vect3,Nz_vect3]
   vecpair_to_Line(vv): MACRO Line = (# p := vv`1, v := vv`2 #)

   CONVERSION vecpair_to_Line ;                        %% NEW %%


   p,p1,p2,u,v,v0,v1,v2: VAR Vect3
   t: VAR nzreal


   loc(L: Line)(tt: real): MACRO Vect3 = p(L) + tt*v(L)

%  ------- generate vector from two points

   vec_from(p1,p2) : Vect3 = p2 - p1

   line_from(p1,(p2:{v| v /= p1})): Line = (p1,vec_from(p1,p2))

   vec_from_eq_args : LEMMA vec_from(p,p) = zero


%  ------- generate velocity vector from two points and transport time

   vel_from_tm(p1,p2,t): { v | p2 = p1 + t*v } = 1/t*(p2 - p1)

   line_from_tm(p1,(p2:{v| v /= p1}),t): Line = (p1,vel_from_tm(p1,p2,t))

   vel_from_tm_nz      : LEMMA p1 /= p2 IMPLIES vel_from_tm(p1,p2,t) /= zero

   vel_from_tm_lem     : LEMMA p2 = p1 + t*vel_from_tm(p1,p2,t)

   vel_from_tm_rew     : LEMMA vel_from_tm(p1,p2,t) = 1/t*(p2 - p1)

   vel_from_tm_eq_args : LEMMA vel_from_tm(p,p,t) = zero

   vel_from_tm_length  : LEMMA sq(norm(vel_from_tm(p1,p2,t))) =
                                 sq_dist(p1,p2)/sq(t)

%  ------- generate velocity vector from two points and speed ------

   s: VAR posreal

   vel_from_spd(p1,p2,s):  Vect3 = IF p1 = p2 then zero
                                   ELSE s/dist(p1,p2)*(p2-p1)
                                   ENDIF
   ps: VAR posreal
   vel_from_spd_lem: LEMMA p1 /= p2 IMPLIES
                     vel_from_spd(p1,p2,ps) = vel_from_tm(p1,p2,dist(p1,p2)/ps)


   vel_from_spd_norm: LEMMA p1 /= p2 IMPLIES
                               vel_from_spd(p1,p2,s) = s*normalize(p2-p1)

   pt: VAR posreal
   gen_speed(p1,(p2:{v| v /= p1}),pt): { s1: nnreal | s1 = 1/pt * dist(p1,p2) }


%  ------- generate velocity vector from a point, heading, speed  ------

%   IMPORTING trig@trig

%   hdg: VAR posreal
%   vel_from_hdg(p1,hdg,s): Vect3 = LET p2 = p1+(cos(hdg),sin(hdg)) IN
%                                       vel_from_spd(p1,p2,s)


%  -------------- Line Predicates -----------------

   L,L1,L2: VAR Line

   on_line?(p,L): bool = EXISTS (x : real) : p = p(L) + x * v(L)

   on_segment?(p,L): bool =
                EXISTS (x : { y: nnreal | y <= 1}) : p = p(L) + x * v(L)

   orthogonal?(L1,L2): bool = ^(v(L1))*^(v(L2)) = 0 

   parallel?(L1,L2)  : bool = ^(v(L1))*^(v(L2)) = 1 OR ^(v(L1))*^(v(L2)) = -1 

   on_line_lem: LEMMA FORALL (p2:{v|v /= p1}): on_line?(p1, line_from(p1,p2)) AND on_line?(p2, line_from(p1,p2))

   on_line_neg: LEMMA on_line?(p, L) IMPLIES on_line?(p, -L)

   on_line_sym: LEMMA FORALL (p2:{v|v /= p1}): on_line?(p, line_from(p1,p2)) IMPLIES on_line?(p, line_from(p2,p1)) 

%  -------------- Generate Dynamic Lines -------

   gen_line_tm(p1,(p2:{v| v /= p1}),t) : Line = (# p := p1,
                                    v := vel_from_tm(p1,p2,t) #)

   gen_line_spd(p1,(p2:{v| v /= p1}),s): Line = (# p := p1,
                                    v := vel_from_spd(p1,p2,s) #)


   test1: LEMMA p1 /= p2 IMPLIES on_line?(p1,gen_line_tm(p1,p2,t))
   test2: LEMMA p1 /= p2 IMPLIES on_line?(p2,gen_line_tm(p1,p2,t))
   test3: LEMMA p1 /= p2 IMPLIES on_line?(p1,gen_line_spd(p1,p2,s))
   test4: LEMMA p1 /= p2 IMPLIES on_line?(p2,gen_line_spd(p1,p2,s))


   vel_from_spd_on_line: LEMMA  LET vv = vel_from_spd(p1,p2,s) IN 
                                  p = p1 + t*vv 
                                    IMPLIES on_line?(p1,p2,p) 



END lines_3D