Impressum angles_2D.pvs Sprache: PVS

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

quality98%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.