Quelle  vect2_cont_dot.pvs   Sprache: unbekannt

vect2_cont_dot[T: TYPE from real] : THEORY
%----------------------------------------------------------------------------
%
%   AUTHOR: Rick Butler         NASA langley Research Center
%
%   The proofs in this theory are tricky.
%   
%   f,g: [real -> vect2] are continuous
%
%     || f(x) * g(x) - f(x0) * g(x0) || <= ||f(x) || || f(x) * g(x) - g(x0) || 
%                                          + || g(x0) || || f(x)  - f(x0) || 
%
%     need || f(x)  - f(x0) || < eps/(2*||g(x0)||)
%
%     need || g(x)  - g(x0) || < eps/(2*r) where || f(x) || < r near x0
%
%     EXISTS delta1: | x - x0 | < delta1 IMPLIES
%                                   || f(x)|| < ||f(x0)|| + 1 = r
%
%     EXISTS delta2: | x - x0 | < delta2 IMPLIES
%                       || f(x)  - f(x0) || < eps/(2*||g(x0)||)
%
%     EXISTS delta3: | x - x0 | < delta3 IMPLIES
%               || g(x)  - g(x0) || < eps/(2*r) 
%
%     let delta = min(delta1,delta2,delta3)
%
%     || f(x) * g(x) - f(x0) * g(x0) || <= ||f(x) || || f(x) * g(x) - g(x0) || 
%                                          + || g(x0) || || f(x)  - f(x0) || 
%                                  < r * eps    + eps || g(x0)||
%                                        ---      ---
%                                         2r     (2||g(x0)||)  
%                                  = eps                    
%
%----------------------------------------------------------------------------
BEGIN 

  IMPORTING cont_vect2_real, 
            cont_vect2_vect2,
            analysis@continuous_lambda[T], 
            cont_real_vect2[T] 

  frr : VAR [T -> real]
  continuous_rr?(frr): MACRO bool = continuous?(frr)

  v   : VAR Vect2
  x,y : VAR T

   vv,vv1,vv2 : VAR { f:[Vect2->Vect2] | continuous_vv?(f) }
   vr,vr1,vr2 : VAR { f:[Vect2->real] | continuous_vr?(f) }
   rr         : VAR continuous_fun
   rv,rv1,rv2 : VAR { f:[T->Vect2] | continuous_rv?(f) }

  dot_cont_vr : LEMMA 
    continuous_vr?(LAMBDA(v):vv1(v)*vv2(v)) 

  dot_cont_rr : LEMMA 
    continuous?[T](LAMBDA(x):rv1(x)*rv2(x)) 

  scal_cont_rv : LEMMA 
    continuous_rv?(LAMBDA(x):rr(x)*rv(x)) 

  scal_cont_vv : LEMMA 
    continuous_vv?(LAMBDA(v):vr(v)*vv(v)) 

  scal_scal_cont_rv : LEMMA 
    continuous_rv?(LAMBDA(x):y*rv(x))

END vect2_cont_dot