Quelle  angles_2D.pvs   Sprache: unbekannt

angles_2D: THEORY
%------------------------------------------------------------------------------
%
%    Provides:
%        vfrom(a): Vect2   returns a unit vector given an angle
%        vfrom(a,k): Vect2 returns a vector given an angle and a magnitude
%
%        angle(u): nnreal_lt_2pi returns an angle between 0,2*pi given a vector
%        Angle(u): nnreal_lt_2pi returns an angle between 0,2*pi given a vector
%                                    (defined used atan2)
%        See angle_Angle which proves equivalence
%
%    Author:
%        Rick Butler            NASA Langley Research Center
%
%    EXPERIMENTAL
%
%------------------------------------------------------------------------------
BEGIN

   IMPORTING vectors_2D, trig@trig_inverses,
             reals@abs_lems, angles_2D_scaf, 
             trig@trig_values,
             trig@trig_inverses,
             trig@atan2

   Angle: NONEMPTY_TYPE = nnreal_lt_2pi

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

%  -------- Vector from an angle -------------

   v_from(a: real): Vect2 = (# x := cos(a), y := sin(a) #)

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

   v_from_k_1: LEMMA v_from(a,1) = v_from(a)

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

   angle_exists_x: LEMMA  (EXISTS (a: real): u`x = norm(u) * cos(a) AND
                                             u`y = norm(u) * sin(a))

%  -------- Angle from a vector -------------

   vec_from(a: Angle, k: posreal): MACRO Vect2 = v_from(a,k)
   
   norm_vec_from : LEMMA norm(vec_from(alpha,k)) = k

   vec_from_inj  : LEMMA injective?(vec_from)

   angle_exists: LEMMA  (EXISTS (alpha: Angle): 
                              u`x = norm(u) * cos(alpha) AND
                              u`y = norm(u) * sin(alpha))

   angle(u: Nz_vect2): {alpha: Angle | u = vec_from(alpha, norm(u))} 
                       = choose({alpha: Angle | u = vec_from(alpha, norm(u))})

   vec_from_angle   : LEMMA vec_from(angle(u),norm(u)) = u

   angle_vec_from : LEMMA angle(vec_from(alpha,k)) = alpha

   Angle(u: Nz_vect2): Angle = atan2(u`x,u`y)

   angle_Angle: LEMMA angle(u) = Angle(u)

   vec_from_Angle: LEMMA vec_from(Angle(u), norm(u)) = u

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

   x: VAR posreal
   angle_x0: LEMMA angle(mk_vect2(x,0)) = 0
   angle_0x: LEMMA angle(mk_vect2(0,x)) = pi/2
   angle_xx: LEMMA angle(mk_vect2(x,x)) = pi/4

   ngr: VAR negreal
   angle_n0: LEMMA angle(mk_vect2(ngr,0)) = pi
   angle_0n: LEMMA angle(mk_vect2(0,ngr)) = 3*pi/2

   angle_nx: LEMMA angle(mk_vect2(-x,x)) = 3*pi/4
   angle_xn: LEMMA angle(mk_vect2(x,-x)) = 7*pi/4
   angle_nn: LEMMA angle(mk_vect2(-x,-x)) = 5*pi/4

%  --------- Properties ------------------

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

   v_from_dot         : LEMMA v_from(a)*v_from(b) = 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_angles    : LEMMA LET s = v_from(c),
                                  nv = v_from(a),
                                  v = v_from(b) IN
                             s*(nv-v) = cos(a-c) - cos(b-c) 


END angles_2D