Quelle  law_cos_pos_3D.pvs

law_cos_pos_3D: THEORY
BEGIN

%                                      v2
%                                      .
%                                     / \
%                                   /    \
%                                 /       \
%                               /          \
%                      c      /             \
%                           /                \    b
%                         /                   \
%                       /                      \
%                     /                         \
%                   /                            \
%                 /                           ab  \
%               /                                  \
%               ------------------------------------ 
%               v0                a                   v1


  IMPORTING trig@trig_basic,
            distance_3D


  v0,v1,v2: VAR Vect3

  ab: VAR real

  law_cosines   : LEMMA
                     LET a = dist(v1,v0),
                         b = dist(v2,v1),
                         c = dist(v2,v0)
                     IN
                      a*b*cos(ab) = (v1-v0)*(v1-v2)
                        IMPLIES
                           sq(c) = sq(a) + sq(b) - 2*a*b*cos(ab)


  law_cosines_alt   : LEMMA
                      LET a = dist(v1,v0),
                          b = dist(v2,v1),
                          c = dist(v2,v0)
                      IN
                          sq(c) = sq(a) + sq(b) - 2*(v1-v0)*(v1-v2)

  IMPORTING trig@trig_inverses

  angle_exists: LEMMA (EXISTS ab:  LET  a = dist(v1,v0),
                                        b = dist(v2,v1) IN
                              a*b*cos(ab) = (v1-v0)*(v1-v2))


  angle_between(u,v:Nz_vect3): real = arccos(u*v/(norm(u)*norm(v)))


  law_cosines_bnd : LEMMA
                     LET a = dist(v1,v0),
                         b = dist(v2,v1),
                         c = dist(v2,v0)
                     IN
                         sq(c) >= sq(a-b)

  law_cosines_bnd_abs : LEMMA
                        LET a = dist(v1,v0),
                            b = dist(v2,v1),
                            c = dist(v2,v0)
                        IN
                            c >= abs(a-b)


  law_cosines_le : LEMMA LET  a = dist(v1,v0),
                              b = dist(v2,v1),
                              c = dist(v2,v0)
                         IN
                                 c <= a + b
 


END law_cos_pos_3D