Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Equivalence.v Sprache: PVS

Original von: PVS^©

wedge_optimum_2D: THEORY
%------------------------------------------------------------------------------
%  This file defines an algorithm that finds the point on a line
%  with the largest norm such that it lies between two half planes
%  that are inputs
%
%             /-half plane 1
%           /
%         / |
%       /   |
%     0     |
%       \   |
%   \ X-point
%     \
%       \
%         \
%
%------------------------------------------------------------------------------

BEGIN

   IMPORTING vectors@vectors_2D,
         horizontal,
      vectors@law_cos_pos_2D,
      vectors@basis_2D,
      analysis@interm_value_thm,
      analysis@continuous_lambda,
      reals@quad_minmax

   v,u,w,c,p,s : VAR Vect2
   e1,e2  : VAR Nz_vect2
   R,k    : VAR posreal
   t    : VAR nnreal
   a,b  : VAR real

  intersects_segment?(p,w,v,a,b,e1,e2): bool =
    EXISTS (t:real): a<=t AND t<=b AND
              (w+t*v-p)*e1>=0 AND
       (w+t*v-p)*e2>=0

  intersects_segment_fun?(p,w,v,a,b,e1,e2): bool =
    LET
      tlow1  = IF v*e1>0 THEN ((p-w)*e1)/(v*e1) ELSIF v*e1 = 0 AND (w-p)*e1<0 THEN b+1 ELSE a ENDIF,
      thigh1 = IF v*e1<0 THEN ((p-w)*e1)/(v*e1) ELSIF v*e1 = 0 AND (w-p)*e1<0 THEN a-1 ELSE b ENDIF,
      tlow2  = IF v*e2>0 THEN ((p-w)*e2)/(v*e2) ELSIF v*e2 = 0 AND (w-p)*e2<0 THEN b+2 ELSE a ENDIF,
      thigh2 = IF v*e2<0 THEN ((p-w)*e2)/(v*e2) ELSIF v*e2 = 0 AND (w-p)*e2<0 THEN a-2 ELSE b ENDIF,
      tlow   = max(max(tlow1,tlow2),a),
      thigh  = min(min(thigh1,thigh2),b)
    IN (tlow <= thigh)

  intersects_segment_fun_def: LEMMA
    intersects_segment_fun? = intersects_segment?

  on_segment?(w,v,a,b)(s): bool =
    EXISTS (t:real): a<=t AND t<=b AND
              s = w+t*v

  on_segment_in_wedge?(p,w,v,a,b,e1,e2)(s): bool =
    EXISTS (t:real): a<=t AND t<=b AND
              s = w+t*v AND
       (s-p)*e1>=0 AND
       (s-p)*e2>=0

  intersects_segment_sym: LEMMA
    intersects_segment?(p,w,v,a,b,e2,e1) IFF
    intersects_segment?(p,w,v,a,b,e1,e2)

  on_segment_in_wedge_sym: LEMMA
    on_segment_in_wedge?(p,w,v,a,b,e2,e1) =
    on_segment_in_wedge?(p,w,v,a,b,e1,e2)

  %%% The line segment is w+tv, where t is in [a,b]

  max_segment_point_in_slice(p,w,v,a,b,e1,e2): Vect2 =
    LET
      tlow1  = IF v*e1>0 THEN ((p-w)*e1)/(v*e1) ELSIF v*e1 = 0 AND (w-p)*e1<0 THEN b+1 ELSE a ENDIF,
      thigh1 = IF v*e1<0 THEN ((p-w)*e1)/(v*e1) ELSIF v*e1 = 0 AND (w-p)*e1<0 THEN a-1 ELSE b ENDIF,
      tlow2  = IF v*e2>0 THEN ((p-w)*e2)/(v*e2) ELSIF v*e2 = 0 AND (w-p)*e2<0 THEN b+2 ELSE a ENDIF,
      thigh2 = IF v*e2<0 THEN ((p-w)*e2)/(v*e2) ELSIF v*e2 = 0 AND (w-p)*e2<0 THEN a-2 ELSE b ENDIF,
      tlow   = max(max(tlow1,tlow2),a),
      thigh  = min(min(thigh1,thigh2),b),
      aa     = sqv(v),
      bb     = 2*(v*(w-p)),
      cc     = sqv(w-p),
      qmint  = IF v = zero THEN 0 ELSE -bb/(2*aa) ENDIF,
      maxt   = IF aa*tlow^2 + bb*tlow <= aa*thigh^2+bb*thigh THEN thigh
              ELSE tlow ENDIF
    IN w + maxt*v

  % max_segment_point_in_slice_symm: LEMMA
  %   max_segment_point_in_slice(p,w,v,a,b,e1,e2) =
  %   max_segment_point_in_slice(p,w,v,a,b,e2,e1)

  max_segment_point_in_slice_def: LEMMA
    Let s = max_segment_point_in_slice(p,w,v,a,b,e1,e2) IN
    (intersects_segment?(p,w,v,a,b,e1,e2)
    IMPLIES on_segment_in_wedge?(p,w,v,a,b,e1,e2)(s)) AND
    (FORALL (u): on_segment_in_wedge?(p,w,v,a,b,e1,e2)(u)
           IMPLIES norm(u-p) <= norm(s-p))

  max_segment_point_in_slice_complete: LEMMA
    LET s = max_segment_point_in_slice(p,w,v,a,b,e1,e2) IN
    FORALL (u): on_segment_in_wedge?(p,w,v,a,b,e1,e2)(u)
         IMPLIES
  on_segment_in_wedge?(p,w,v,a,b,e1,e2)(s)

END wedge_optimum_2D

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.