| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle distance.pvs Sprache: PVS |
|||||||||
|
distance[n: posnat]: THEORY
BEGIN IMPORTING vectors p,p0,p1,p2,u,v,v0,v1,v2: VAR Vector[n] t: VAR posreal i: VAR Index[n] % ------- distance function ----- sq_dist(p1,p2): nnreal = sigma(0,n-1, LAMBDA i: sq(p1(i)-p2(i))) 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) %% NEW %% sq_dist_lt : LEMMA sq_dist(v1,v2) < sq_dist(p1,p2) IMPLIES dist(v1,v2) < dist(p1,p2) %% NEW %% dist_gt_comp : LEMMA (FORALL i: dist(v1,v2) >= abs(v1(i) - v2(i))) %% NEW % sq_dist_dist : LEMMA sq(dist(p2,p0)) = sq(dist(p1,p0)) + sq(dist(p1,p2)) - 2*(p1-p0)*(p1-p2) %% NEW %% % 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 ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28