Quelle  distance_3D.pvs

distance_3D: THEORY
BEGIN

   IMPORTING vectors_3D

   p,p0,p1,p2,u,v,v0,v1,v2: VAR Vect3

   t: VAR posreal

%  ------- distance function -----

   sq_dist(p1,p2): nnreal = sq(p1`x-p2`x) + sq(p1`y-p2`y) + sq(p1`z-p2`z) 

   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)  

   dist_ge_z    : LEMMA dist(p1,p2) >= abs(p1`z - p2`z)  

   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_3D