|
distance_2D: THEORY
BEGIN
IMPORTING vectors_2D
p,p0,p1,p2,u,v,v0,v1,v2: VAR Vect2
t: VAR posreal
% ------- distance function -----
sq_dist(p1,p2): nnreal = sq(p1`x - p2`x) + sq(p1`y - p2`y)
dist(p1,p2) : nnreal = sqrt(sq_dist(p1,p2))
dist_eq_args : LEMMA dist(p,p) = 0
dist_zero_l : LEMMA dist(zero,p) = norm(p)
dist_zero_r : LEMMA dist(p,zero) = norm(p)
dist_sym : LEMMA dist(p1,p2) = dist(p2,p1)
dist_eq_0 : LEMMA dist(p1,p2) = 0 IFF p1 = p2
dist_norm : LEMMA dist(u,v) = norm(u-v)
dist_rel : LEMMA dist(p+p1,p+p2) = dist(p1,p2)
sq_dist_is_dist_sq: LEMMA sq_dist(p1,p2) = sq(dist(p1,p2))
sq_dist_norm : LEMMA sq_dist(p1,p2) = sq(norm(p1-p2))
sq_dist_sym : LEMMA sq_dist(p1,p2) = sq_dist(p2,p1)
sq_dist_le : LEMMA sq_dist(v1,v2) <= sq_dist(p1,p2) IMPLIES
dist(v1,v2) <= dist(p1,p2)
sq_dist_lt : LEMMA sq_dist(v1,v2) < sq_dist(p1,p2) IMPLIES
dist(v1,v2) < dist(p1,p2)
dist_ge_x : LEMMA dist(p1,p2) >= abs(p1`x - p2`x)
dist_ge_y : LEMMA dist(p1,p2) >= abs(p1`y - p2`y)
sq_dist_dist : LEMMA sq(dist(p2,p0)) = sq(dist(p1,p0)) + sq(dist(p1,p2))
- 2*(p1-p0)*(p1-p2)
dist_triangle: LEMMA dist(p0,p2) <= dist(p0,p1) + dist(p1,p2)
dist_tri_sub: LEMMA abs(dist(p0,p2) - dist(p1,p2)) <= dist(p0,p1)
AUTO_REWRITE+ dist_eq_args
% AUTO_REWRITE+ dist_zero_l
% AUTO_REWRITE+ dist_zero_r
% ------- Predicates
r: VAR real
on_circle?(p,r): bool = dist(p,zero) = r
on_line?(p1,p2,p): bool =
EXISTS (x : real) : p = p1 + x * (p2 - p1)
on_segment?(p1,p2,p): bool =
EXISTS (x : { y: nnreal | y <= 1}) : p = p1 + x * (p2 - p1)
on_segment_beg: LEMMA on_segment?(p1,p2,p1)
on_segment_end: LEMMA on_segment?(p1,p2,p2)
on_line_beg : LEMMA on_line?(p1,p2,p1)
on_line_end : LEMMA on_line?(p1,p2,p2)
AUTO_REWRITE+ on_segment_beg
AUTO_REWRITE+ on_segment_end
AUTO_REWRITE+ on_line_beg
AUTO_REWRITE+ on_line_end
on_segment_on_line: LEMMA on_segment?(p1,p2,p1) IMPLIES on_line?(p1,p2,p1)
END distance_2D
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
