Quelle  law_cosines.pvs

law_cosines: THEORY
BEGIN

%   Version 1.2 27/10/03  Foundational Version David Lester

%                                   (x2,y2)
%                                      .
%                                     / \
%                                   /    \
%                                 /       \
%                               /          \
%                      b      /             \
%                           /                \    c
%                         /                   \
%                       /                      \
%                     /                         \
%                   /                            \
%                 /                           ac  \
%               /                                  \
%               ------------------------------------ 
%           (x0,y0)               a               (x1,y1)

  IMPORTING trig_basic, atan2

  x0,x1,x2,y0,y1,y2,ac : VAR real
  pz                   : VAR posreal

  sq_dist(x0,y0,x1,y1) : nonneg_real = sq(x0-x1)+sq(y0-y1)

  dist(x0,y0,x1,y1)    : nonneg_real = sqrt(sq_dist(x0,y0,x1,y1))

  distance_refl : LEMMA  dist(x0,y0,x0,y0) = 0

  distance_symm : LEMMA  dist(x0,y0,x1,y1) = dist(x1,y1,x0,y0)

  distance_trans: LEMMA  dist(x0,y0,x1,y1) = dist(x0+x2,y0+y2,x1+x2,y1+y2)

  distance_scale: LEMMA  pz*dist(x0,y0,x1,y1) = dist(pz*x0,pz*y0,pz*x1,pz*y1)

  distance_rot:   LEMMA  dist(x0,y0,x1,y1)
                           = dist(cos(ac)*x0-sin(ac)*y0, cos(ac)*y0+sin(ac)*x0,
                                  cos(ac)*x1-sin(ac)*y1, cos(ac)*y1+sin(ac)*x1)

  dot_product   : LEMMA
                     LET a = dist(x1,y1,x0,y0),
                         b = dist(x2,y2,x0,y0),
                         c = dist(x2,y2,x1,y1) IN
                     EXISTS (ac) : 
                         a*c*cos(ac) = ((x0-x1)*(x2-x1) + (y0-y1)*(y2-y1))

  Law_Cosines   : LEMMA
                     LET a = dist(x1,y1,x0,y0),
                         b = dist(x2,y2,x0,y0),
                         c = dist(x2,y2,x1,y1) IN
                         a*c*cos(ac) = ((x0-x1)*(x2-x1) + (y0-y1)*(y2-y1))
                     IMPLIES
                           sq(b) = sq(c) + sq(a) - 2*a*c*cos(ac)
                       
  triangle      : LEMMA  dist(x0,y0,x1,y1) <= 
                              dist(x2,y2,x1,y1) + dist(x2,y2,x0,y0)
 
END law_cosines