track.pvs

track : THEORY
BEGIN 

  IMPORTING trig_fnd@to2pi,
            definitions

   trk        : VAR real
   s,v,vi,nvo : VAR Nz_vect2
   gsp        : VAR posreal

  trkgs2vect(trk,gsp) : Nz_vect2 =
    gsp*(sin(trk),cos(trk))

  track(v) : nnreal_lt_2pi =
    atan2(v`y,v`x)

  sin_track : LEMMA
    sin(track(v)) = v`x/norm(v)

  cos_track : LEMMA
    cos(track(v)) = v`y/norm(v)

  norm_id : LEMMA
    norm(trkgs2vect(trk,gsp)) = gsp

  track_id : LEMMA
    track(trkgs2vect(trk,gsp)) = to2pi(trk)

  trkgs2vect_id : LEMMA
    trkgs2vect(track(v),norm(v)) = v

  %% ordered eps=1 
  ordered_eps_1 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) IFF
     0 < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < beta)

  ordered_det_ge : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) >= det(vi,s) IFF
     0 <= to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) <= beta)

  ordered_eps_neg_1 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) < det(vi,s) IFF
     beta < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < 2*pi)

  %% ordered within eps = 1
  ordered_eps_1_dot_gt_0 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) AND nvo*s > 0 IFF
     0 < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < beta/2)

  ordered_eps_1_dot_ge_0 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) AND nvo*s >= 0 IFF
     0 < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) <= beta/2)

  ordered_eps_1_dot_lt_0 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) AND nvo*s < 0 IFF
     beta/2 < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < beta)

  ordered_eps_1_dot_le_0 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) AND nvo*s <= 0 IFF
     beta/2 <= to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < beta)

END track