|
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
[ zur Elbe Produktseite wechseln0.1Quellennavigators
Analyse erneut starten
]
|
