trackAngles_2D.pvs

trackAngles_2D: THEORY
%------------------------------------------------------------------------------
%
%    Provides:
%        vec_from(a,k): Vect2 returns a vector given an track and a magnitude
%
%        track(u): Track returns an track angle between 0,2*pi given a vector
%                                    (defined used atan2)
% 
%        trk(u): atan2(u`y,u`x) is equivalent
%
%    Author:
%        Rick Butler            NASA Langley Research Center
%
%    EXPERIMENTAL
%
%------------------------------------------------------------------------------
BEGIN

   IMPORTING trackAngles_scaf

   a,b,c : VAR real
   alpha : VAR Track
   k     : VAR posreal
   v     : VAR Vect2
   u     : VAR Nz_vect2

%  -------- Vector from an track angle 0 to 2 PI

   v_from(a: real, k: posreal): MACRO Nz_vect2 = (# x := k*sin(a), y := k*cos(a) #)

   vec_from(a: Track, k: posreal): Vect2 = v_from(a,k)

   trk(u: Nz_vect2)  : Track = atan2(u`y,u`x)

%%   sqrt_scal      : LEMMA FORALL (x: nnreal): abs(a)*sqrt(x) = sqrt(sq(a)*x)

   track(u: Nz_vect2): {alpha: Track | u = vec_from(alpha, norm(u))} 

   norm_v_from    : LEMMA norm(v_from(a,k)) = k

   vec_from_nz    : LEMMA vec_from(alpha,k) /= zero

   norm_vec_from  : LEMMA norm(vec_from(alpha,k)) = k
 
   vec_from_inj   : LEMMA injective?(vec_from)

   vec_from_track : LEMMA vec_from(track(u),norm(u)) = u

   track_vec_from : LEMMA track(vec_from(alpha,k)) = alpha

   track_trk      : LEMMA track(u) = trk(u)

   vec_from_trk   : LEMMA vec_from(trk(u), norm(u)) = u

%  -------- Special Values ------------------

   x: VAR posreal
   track_x0: LEMMA track(mk_vect2(x,0)) = pi/2
   track_0x: LEMMA track(mk_vect2(0,x)) = 0
   track_xx: LEMMA track(mk_vect2(x,x)) = pi/4

   ngr: VAR negreal
   track_n0: LEMMA track(mk_vect2(ngr,0)) = 3*pi/2
   track_0n: LEMMA track(mk_vect2(0,ngr)) = pi

   track_nx: LEMMA track(mk_vect2(-x,x)) = 7*pi/4
   track_xn: LEMMA track(mk_vect2(x,-x)) = 3*pi/4
   track_nn: LEMMA track(mk_vect2(-x,-x)) = 5*pi/4


%  -------- Properties of v_from -------------

   vfrom_sub          : LEMMA v_from(a-b,1) = (sin(a-b),cos(a-b))  

   v_from_dot         : LEMMA v_from(a,1)*v_from(b,1) = cos(a-b)  

   ka,kb: VAR posreal
   v_from_dot_k       : LEMMA v_from(a,ka)*v_from(b,kb) = ka*kb*cos(a-b)  

   dot_prod_tracks    : LEMMA LET s = v_from(c,1),
                                  nv = v_from(a,1),
                                  v = v_from(b,1) IN
                             s*(nv-v) = cos(a-c) - cos(b-c) 


END trackAngles_2D