|
% ----------------------------------------------------------%
% tca_3D - Time of closest approach for cylindrical distance
% between the two aircraft.
% ----------------------------------------------------------%
tca_3D[D,H:posreal] : THEORY
BEGIN
IMPORTING circle_criterion[D,H],
cd_vertical,
omega_2D,
util,
analysis@metric_space_real_fun[real,real_dist],
analysis@real_fun_continuity_equiv,
analysis@continuity_of_max_min[real,real_dist]
s,v : VAR Vect3
t,t1,t2,r,
B1,B2 : VAR real
eps : VAR Sign
nnt,pt : VAR nnreal
cyl_norm_sq(s): nnreal = max(sqv(vect2(s))/sq(D),sq(s`z)/sq(H))
cyl_norm_sq_diff_cont: LEMMA
continuous?(LAMBDA (t:real): (sqv(vect2(s) + t*vect2(v))/sq(D) - sq(s`z+t*v`z)/sq(H)),fullset[real])
cyl_norm_sq_IVT1: LEMMA cyl_norm_sq(s+t1*v) = sqv(vect2(s)+t1*vect2(v))/sq(D) AND cyl_norm_sq(s+t2*v) /= sqv(vect2(s)+t2*vect2(v))/sq(D)
IMPLIES (EXISTS (t:real): ((t1<=t AND t<=t2) OR (t2<=t AND t<=t1)) AND sqv(vect2(s)+t*vect2(v))/sq(D) = sq(s`z+t*v`z)/sq(H))
cyl_norm_sq_IVT2: LEMMA cyl_norm_sq(s+t1*v) = sq(s`z+t1*v`z)/sq(H) AND cyl_norm_sq(s+t2*v) /= sq(s`z+t2*v`z)/sq(H)
IMPLIES (EXISTS (t:real): ((t1<=t AND t<=t2) OR (t2<=t AND t<=t1)) AND sqv(vect2(s)+t*vect2(v))/sq(D) = sq(s`z+t*v`z)/sq(H))
cyl_norm_sq_fun(s,v)(t) : nnreal = cyl_norm_sq(s+t*v)
cyl_norm_sq_fun_convex: LEMMA convex?(cyl_norm_sq_fun(s,v))
cyl_norm_sq_fun_cont: LEMMA continuous?(cyl_norm_sq_fun(s,v),fullset[real])
cyl_norm_min_exists: LEMMA B1<=B2 IMPLIES (EXISTS (t:real): B1<=t AND t<=B2 AND (FORALL (r:real): B1<=r AND r<=B2 IMPLIES cyl_norm_sq_fun(s,v)(r) >= cyl_norm_sq_fun(s,v)(t)))
cyl_norm_min_exists_inf: LEMMA EXISTS (tz: nnreal): FORALL (nnt:nnreal): cyl_norm_sq_fun(s,v)(nnt) >= cyl_norm_sq_fun(s,v)(tz)
conflict_at_cyl_norm_sq: LEMMA
conflict_at?(s,v,t) IFF cyl_norm_sq(s+t*v) < 1
Min_Info: TYPE = [# min_time : nnreal , min_dist : nnreal #]
info(s,v,nnt): Min_Info = (# min_time := nnt, min_dist := cyl_norm_sq(s+nnt*v) #)
MI1,MI2 : VAR Min_Info
minimum_info(MI1,MI2): {MI : Min_Info | (MI = MI1 OR MI = MI2) AND MI`min_dist <= MI1`min_dist AND MI`min_dist <= MI2`min_dist}
= IF MI1`min_dist <= MI2`min_dist THEN MI1
ELSE MI2 ENDIF
horizontal_min_info(s,v) : {MI : Min_Info | MI`min_dist <= info(s,v,0)`min_dist AND
(vect2(v) /= zero AND horizontal_tca(s,v)>=0 IMPLIES MI`min_dist<=info(s,v,horizontal_tca(s,v))`min_dist)}=
IF vect2(v) = zero OR (vect2(v) /= zero AND horizontal_tca(s,v) <= 0) THEN
info(s,v,0)
ELSE minimum_info(info(s,v,horizontal_tca(s,v)),info(s,v,0))
ENDIF
horiz_vert_min_info(s,v) : {MI : Min_Info | MI`min_dist <= info(s,v,0)`min_dist AND
(vect2(v) /= zero AND horizontal_tca(s,v)>=0 IMPLIES MI`min_dist<=info(s,v,horizontal_tca(s,v))`min_dist)
AND (v`z/=0 AND -s`z/v`z>=0 IMPLIES MI`min_dist <= info(s,v,-s`z/v`z)`min_dist)} =
IF v`z = 0 OR (v`z /= 0 AND -s`z/v`z <= 0) THEN
horizontal_min_info(s,v)
ELSE
minimum_info(horizontal_min_info(s,v),info(s,v,-s`z/v`z))
ENDIF
cyl_intersect_time(s,v,eps) : real =
LET
a = sqv(vect2(v))/sq(D) - sq(v`z)/sq(H),
b = vect2(s)*vect2(v)/sq(D) - s`z*v`z/sq(H),
c = sqv(vect2(s))/sq(D) - sq(s`z)/sq(H)
IN
IF a = 0 AND b = 0 THEN 0
ELSIF a = 0 THEN -c/(2*b)
ELSIF discr2b(a,b,c) < 0 THEN 0
ELSE root2b(a,b,c,sign(a)*eps) ENDIF % This uses sign(a)*eps instead of just eps, so that the LT lemma will prove
cyl_intersect_time_lt: LEMMA
cyl_intersect_time(s,v,-1) <= cyl_intersect_time(s,v,1)
cyl_intersect_time_id : LEMMA
(EXISTS (t1:real): sqv(vect2(s+t1*v))/sq(D) /= sq((s+t1*v)`z)/sq(H))
AND
sqv(vect2(s + t*v))/sq(D) = sq((s+t*v)`z)/sq(H) IMPLIES
(EXISTS (eps): t = cyl_intersect_time(s,v,eps))
cyl_intersect_min_info(s,v) : {MI : Min_Info | FORALL (eps:Sign): cyl_intersect_time(s,v,eps)>0 IMPLIES
MI`min_dist<=info(s,v,cyl_intersect_time(s,v,eps))`min_dist} =
LET
mt1 = cyl_intersect_time(s,v,-1),
mt2 = cyl_intersect_time(s,v,1)
IN
IF mt2 <= 0 THEN horizontal_min_info(s,v)
ELSIF mt1 <=0 THEN (# min_time := mt2, min_dist := cyl_norm_sq(s+mt2*v) #)
ELSE
minimum_info((# min_time := mt1, min_dist := cyl_norm_sq(s+mt1*v) #),
(# min_time := mt2, min_dist := cyl_norm_sq(s+mt2*v) #))
ENDIF
tca_3D(s,v) : nnreal = minimum_info(horiz_vert_min_info(s,v),cyl_intersect_min_info(s,v))`min_time
tca_3D_id : LEMMA nnt = 0 OR (vect2(v) /= zero AND nnt = -(vect2(s)*vect2(v))/sqv(vect2(v))) OR (v`z /= 0 AND nnt = -(s`z*v`z)/sq(v`z))
OR sqv(vect2(s+nnt*v))/sq(D) = sq((s+nnt*v)`z)/sq(H) IMPLIES
cyl_norm_sq(s + nnt*v) >= cyl_norm_sq(s+tca_3D(s,v)*v)
tca_3D_vect2_zero: LEMMA vect2(v)=zero AND cyl_norm_sq_fun(s,v)(nnt) = sqv(vect2(s+nnt*v))/sq(D) IMPLIES
cyl_norm_sq_fun(s,v)(nnt) >= cyl_norm_sq_fun(s,v)(tca_3D(s,v))
tca_3D_vz_zero: LEMMA v`z=0 AND cyl_norm_sq_fun(s,v)(nnt) = sq((s+nnt*v)`z)/sq(H) IMPLIES
cyl_norm_sq_fun(s,v)(nnt) >= cyl_norm_sq_fun(s,v)(tca_3D(s,v))
tca_3D_def: LEMMA cyl_norm_sq(s + nnt*v) >= cyl_norm_sq(s+tca_3D(s,v)*v)
tca_3D_conflict: LEMMA conflict?(s,v) IFF cyl_norm_sq(s + tca_3D(s,v)*v) < 1
tca_3D_conflict_at: LEMMA conflict?(s,v) IFF conflict_at?(s,v,tca_3D(s,v))
% for nonnegative times, cyl_norm_sq_fun is decreasing to the left of tca_3D
% and increasing to the right.
tca_3D_left_decreasing: LEMMA nnt<=pt AND pt<=tca_3D(s,v) IMPLIES
cyl_norm_sq_fun(s,v)(nnt)>=cyl_norm_sq_fun(s,v)(pt)
tca_3D_right_increasing: LEMMA tca_3D(s,v)<=nnt AND nnt<=pt IMPLIES
cyl_norm_sq_fun(s,v)(nnt)<=cyl_norm_sq_fun(s,v)(pt)
END tca_3D
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
