Quelle tangent_line.pvs Sprache: PVS

%------------------------------------------------------------------------------
% tangent_line.pvs
% ACCoRD v1.0
%
% This file provides a simple framework to compute line solutions.
% By definition all line solutions lay on the tangent lines to the
% protected zone. We consider two cases, if sq(s) = sq(D), tangent
% solutions lay on a vector perpendicular to s. Otherwise, tangent solutions
% lay on the line defined by the two points s and Q(s,eps), where
% eps = +-1.
%------------------------------------------------------------------------------

tangent_line[D: posreal] : THEORY
BEGIN

  IMPORTING line_solutions[D],
            vectors@parallel_2D

  sp       : VAR Sp_vect2
  ss       : VAR Ss_vect2
  eps      : VAR Sign
  vo,vi,v,
  nvo,nvi  : VAR Vect2
  nzv      : VAR Nz_vect2

  alpha(ss) : {x:posreal | x < 1} =  sq(D)/sqv(ss)

  beta(ss)  : nnreal =  D*sqrt(sqv(ss)-sq(D))/sqv(ss)

  alpha_neg : LEMMA
    alpha(-ss) = alpha(ss)

  beta_neg : LEMMA
    beta(-ss) = beta(ss)

  sq_alpha_beta : LEMMA
    sq(alpha(ss)) + sq(beta(ss)) = alpha(ss)

  Q(ss,eps) : Vect2 = alpha(ss)*ss+eps*beta(ss)*perpR(ss)

  Q_on_D : LEMMA
    sqv(Q(ss,eps)) = sq(D)

  Q_asymm : LEMMA
    Q(-ss,eps) = -Q(ss,eps)

  Qs(ss,eps) : Vect2 =
    Q(ss,eps)-ss

  Qs_asymm : LEMMA
    Qs(-ss,eps) = -Qs(ss,eps)

  sqv_Qs : LEMMA
    sqv(Qs(ss,eps)) =  sqv(ss) - sq(D)

  Qs_nzv : JUDGEMENT
    Qs(ss,eps) HAS_TYPE Nz_vect2

  s_dot_Qs_lt_0 : LEMMA
   ss*Qs(ss,eps) < 0

  det_s_Qs_lt_0 : LEMMA
   eps*det(ss,Qs(ss,eps)) < 0

  alpha_D : LEMMA
    alpha(ss)*sqv(ss) = sq(D)

  beta_R  : LEMMA
    beta(ss)*sqv(ss)*R(ss) = sqv(ss)-sq(D)

  alpha_beta: LEMMA
    alpha(ss)*R(ss) = beta(ss)

  beta_alpha : LEMMA
    -beta(ss)*R(ss) = alpha(ss)-1

  det_v_Q : LEMMA
    det(v,Q(ss,eps)) = alpha(ss)*(det(v,ss)) - eps*beta(ss)*(ss*v)

  s_dot_Q : LEMMA
    ss*Q(ss,eps) = alpha(ss)*sqv(ss)

  det_s_Qs : LEMMA
    det(ss,Qs(ss,eps)) = -eps*(beta(ss)*sqv(ss))

  det_Q_s : LEMMA
    det(Q(ss,eps),ss) = eps*D*sqrt(sqv(ss)-sq(D))

  Q_eq_Qs_perp : LEMMA
    Q(ss,eps) = -eps*(D/sqrt(sqv(ss)-sq(D)))*perpR(Qs(ss,eps))

  line_solution_Qs: LEMMA
    line_solution?(ss,Qs(ss,eps),eps)

  parallel_nzv_Qs : LEMMA
    line_solution?(ss,nzv,eps) IMPLIES
    dir_parallel?(nzv,Qs(ss,eps))

  parallel_nzv_perp : LEMMA
    on_D?(sp) AND
    line_solution?(sp,nzv,eps) IMPLIES
    dir_parallel?(nzv,eps*perpR(sp))

  tangent_line(sp,eps) : Nz_vect2 =
    IF on_D?(sp) THEN
      eps*perpR(sp)
    ELSE
      Qs(sp,eps)
    ENDIF

  tangent_line_asymm : LEMMA
    tangent_line(-sp,eps) = -tangent_line(sp,eps)

  line_solution_tangent_line: LEMMA
    line_solution?(sp,tangent_line(sp,eps),eps)

  parallel_nzv_tangent_line: LEMMA
    line_solution?(sp,nzv,eps) IMPLIES
    dir_parallel?(nzv,tangent_line(sp,eps))

  tangent_line?(sp,v,eps) : bool =
    EXISTS (nnk:nnreal): v = nnk*tangent_line(sp,eps)

  tangent_line_solution : LEMMA
    tangent_line?(sp,v,eps) IFF
    line_solution?(sp,v,eps)

  tangent_line_independence : LEMMA
    tangent_line?(sp,v,eps) IMPLIES
       NOT horizontal_conflict_ever?(sp,v)

  tangent_line_coordination: LEMMA
     horizontal_conflict?(sp,vo-vi) AND
     tangent_line?(sp,nvo-vi,eps) AND
     tangent_line?(-sp,nvi-vo,eps)
     IMPLIES
       NOT horizontal_conflict?(sp,nvo-nvi)

END tangent_line

quality100%

¤ Dauer der Verarbeitung: 0.1 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.