Quelle  line_solutions.pvs

%------------------------------------------------------------------------------
% line_solutions.pvs
% ACCoRD v1.0
%
% Line solutions are a special case of horizontal solutions. They are
% are tangent to the protected zone. In this case, eps determines the 
% side of the protected zone that the is touched.
% It is proven that line solutions satisfy independence and (implicit)
% coordination.
%------------------------------------------------------------------------------

line_solutions[D: posreal]: THEORY
BEGIN

  IMPORTING horizontal_criteria[D],
           vectors@linear_transformations_2D

  sp,s2         : VAR Sp_vect2
  s,v,v1,v2,v3,
  vo,vi,nvo,nvi : VAR Vect2
  eps,eps1,eps2 : VAR Sign
  t,t2,t3    : VAR real
  nzv,nzv1,nzv2 : VAR Nz_vect2
  k             : VAR real
  pk            : VAR posreal
  tt  : VAR nnreal

  line_solution?(sp,v,eps):bool =
      R(sp)*eps*det(sp,v) = sp*v AND eps*det(sp,v) <= 0

  line_solution_dot_neg : LEMMA
    line_solution?(sp,v,eps) IMPLIES
    sp*v <= 0

  line_solution_sep_dot_negative: LEMMA
    sqv(sp) > sq(D) AND v /= zero AND
    line_solution?(sp,v,eps) IMPLIES
    sp*v < 0

  line_solution?(sp,v) : MACRO bool =
     EXISTS (eps: Sign): line_solution?(sp,v,eps)

  line_solution_on_D: LEMMA
    on_D?(s) IMPLIES
    line_solution?(s,eps*perpR(s),eps)

  on_D_line : LEMMA
    on_D?(s) AND s*v = 0 IMPLIES line_solution?(s,v) 

  line_solution_scal : LEMMA
    line_solution?(sp,v,eps) IFF line_solution?(sp,pk*v,eps)

  line_solution_zero_eps : LEMMA
    line_solution?(sp,zero,eps)

  line_solution_zero : LEMMA
    line_solution?(sp,zero)

  line_solution_Delta: LEMMA
    line_solution?(sp,v) IFF Delta(sp,v) = 0 AND horizontal_entry?(sp,v)

  det_neq_0 : LEMMA
    line_solution?(sp,nzv) IMPLIES
    det(sp,nzv) /= 0

  eps_line(s,v): Sign = -sign(det(s,v))

  line_solution_eps : LEMMA
    line_solution?(sp,nzv,eps) IMPLIES
    eps = eps_line(sp,nzv)

  line_solution_eps_line : LEMMA
    line_solution?(sp,v) IMPLIES 
    line_solution?(sp,v,eps_line(sp,v))

  line_solution_meets_horizontal_criterion: LEMMA
    line_solution?(sp,v,eps) IMPLIES
    horizontal_criterion?(sp,eps)(v)

  line_solution_independence : THEOREM
    line_solution?(sp,v) IMPLIES
    NOT horizontal_conflict_ever?(sp,v)

  line_solution_invariant: LEMMA
    sign(-(sp*v)) = sign(-((sp+t*v)*v)) IMPLIES
   (line_solution?(sp,v) IMPLIES line_solution?(sp+t*v,v))

  line_solution_rewrite: LEMMA line_solution?(sp,nzv) IFF
    EXISTS (tt): on_D?(sp+tt*nzv) AND (sp+tt*nzv)*nzv = 0

  line_solution_det: LEMMA line_solution?(sp,v,eps)
    IFF (-eps*det(sp,v) = D*norm(v) AND horizontal_entry?(sp,v))

  line_solution_scal_unique: LEMMA
    line_solution?(sp,nzv1,eps) AND line_solution?(sp,nzv2,eps)
    AND
    sqv(sp) > sq(D)
    IMPLIES
    EXISTS (pk:posreal): nzv1 = pk*nzv2

  line_solution_coordination : THEOREM
     horizontal_conflict?(sp,vo-vi) AND
     line_solution?(sp,nvo-vi,eps) AND
     line_solution?(-sp,nvi-vo,eps)
     IMPLIES
     NOT horizontal_conflict?(sp,nvo-nvi)

  line_solution_along_line: LEMMA 
    det(v1,v2) /= 0 IMPLIES
    LET t1 = ((-eps)*D*norm(v2) - det(sp,v2))/det(v1,v2) IN
    (sp + t1*v1)*v2 <= 0 IMPLIES line_solution?(sp + t1*v1,v2,eps)

END line_solutions