Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: vectors_2D.pvs   Sprache: PVS

vectors_2D: THEORY
%----------------------------------------------------------------------------
%
%  The Vect2 type is a record [#  x, y: real  #]
%  but the vect2 conversion allows one to write (x,y) 
%
%----------------------------------------------------------------------------
BEGIN

   IMPORTING reals@sqrt,vectors_2D_def

   Vector    : TYPE = Vect2
   u,v,w,z   : VAR Vector
   a,b,c     : VAR real
   nza       : VAR nzreal

%  ----------- Special vectors ---------------------------------------------

   zero: Vector = (0,0) 
   const_vec(a): Vector = (a,a)

   zero_vector?(v): MACRO bool =
     v = zero

   nz_vector?(v): MACRO bool = 
     v /= zero

   zero_vect2? : MACRO PRED[Vector] = zero_vector?
   nz_vect2?   : MACRO PRED[Vector] = nz_vector?

   Nz_vector   : TYPE = (nz_vector?)
   Nz_vect2    : TYPE = Nz_vector

%  ----------- Vector Operations -------------------------------------------

   -(v)  : Vector = (-v`x, -v`y) ;

   +(u,v): Vector = (u`x + v`x, u`y + v`y) ;

   -(u,v): Vector = (u`x - v`x, u`y - v`y) ;

   *(u,v): real  =  u`x * v`x + u`y * v`y ;         % dot product

   *(a,v): Vector = (a * v`x, a * v`y) ;

%  ----------- Vector Functions  -------------------------------------------

   sqv(v): nnreal = v*v

   sos(v): nnreal = sq(v`x) + sq(v`y)        

   sqv_rew    : LEMMA v*v = sqv(v)

   sqv_sos    : LEMMA sqv(v) = sos(v)

   norm(v): nnreal = sqrt(sqv(v))

   normalized?(v): MACRO bool = 
     norm(v) = 1
  
   Normalized  : TYPE = (normalized?)
  
   iv: Normalized = (1,0)
   jv: Normalized = (0,1)

   nzu,nzv     : VAR Nz_vector

%  ----------- Vector Component Lemmas

   basis          : LEMMA a*iv + b*jv  = (a,b)

   vx_distr_add   : LEMMA (v + w)`x = v`x + w`x  
   vy_distr_add   : LEMMA (v + w)`y = v`y + w`y  

   vx_distr_sub   : LEMMA (v - w)`x = v`x - w`x  
   vy_distr_sub   : LEMMA (v - w)`y = v`y - w`y  

   vx_scal        : LEMMA (a*v)`x = a*v`x              
   vy_scal        : LEMMA (a*v)`y = a*v`y              

   vx_neg         : LEMMA (-v)`x = -v`x
   vy_neg         : LEMMA (-v)`y = -v`y

   comp_eq_x      : LEMMA u = w IMPLIES u`x = w`x      
   comp_eq_y      : LEMMA u = w IMPLIES u`y = w`y      

   comps_eq       : LEMMA u = w IFF u`x = w`x AND u`y = w`y       

   comp_zero_x    : LEMMA zero`x = 0
   comp_zero_y    : LEMMA zero`y = 0

   norm_xy_eq_0   : LEMMA norm(v) = 0 IFF v`x =0 AND v`y=0
    
   norm_sqv_eq_0  : LEMMA norm(v) = 0 IFF sqv(v) = 0

   norm_eq_0      : LEMMA norm(v) = 0 IFF v = zero

   norm_zero      : LEMMA norm(zero) = 0 

   sqv_zero       : LEMMA sqv(zero) = 0

   sqv_eq_0       : LEMMA sqv(v) = 0 IFF v = zero

   v_neq_zero     : LEMMA v /= zero IFF sqv(v) > 0

   sq_dot_eq_0    : LEMMA v*v = 0 IFF v = zero

   nzv_xy_neq_0   : LEMMA nz_vector?(v) IFF v`x /= 0 OR v`y /= 0 
  
%  ----------- JUDGEMENTS -------------------------------------

   nz_norm_gt_0 : JUDGEMENT 
     norm(nzu) HAS_TYPE posreal

   nz_sqv_gt_0 : JUDGEMENT 
     sqv(nzu) HAS_TYPE posreal

   nz_nvz_left : JUDGEMENT
     mk_vect2(nza,b) HAS_TYPE Nz_vector

   nz_nvz_right : JUDGEMENT
     mk_vect2(b,nza) HAS_TYPE Nz_vector

   normalized_nz : JUDGEMENT
     Normalized SUBTYPE_OF Nz_vector

   neg_nzv : JUDGEMENT
     -(nzu) HAS_TYPE Nz_vector

   nz_nzv : JUDGEMENT
     *(nza,nzv) HAS_TYPE Nz_vector

%  ----------- Vector Operation Lemmas -------------------------------------

   neg_zero         : LEMMA -zero=zero

   add_zero_left    : LEMMA zero + v = v

   add_zero_right   : LEMMA v + zero = v

   add_comm         : LEMMA u+v = v+u

   add_assoc        : LEMMA u+(v+w) = (u+v)+w

   add_move_left    : LEMMA u + w = v IFF w = v - u   

   add_move_right   : LEMMA u + w = v IFF u = v - w

   add_move_both    : LEMMA v = u + w IFF u = v - w

   add_neg_sub      : LEMMA v + -u = v - u

   add_cancel       : LEMMA v + w - v = w
    
   add_cancel_neg   : LEMMA -v + w + v = w

   add_cancel2      : LEMMA w - v + v = w
    
   add_cancel_neg2  : LEMMA w + v - v = w

   add_cancel_left  : LEMMA u + v = u + w IMPLIES v = w  

   add_cancel_right : LEMMA u + v = w + v IMPLIES u = w  

   add_eq_zero      : LEMMA u + v = zero IFF u = -v
 
   neg_shift        : LEMMA u = -v IFF -u = v

   sub_cancel_left  : LEMMA u - v = u - w IMPLIES v = w  

   sub_cancel_right : LEMMA u - v = w - v IMPLIES u = w 

   sub_zero_left    : LEMMA zero - v = -v

   sub_zero_right   : LEMMA v - zero = v

   sub_eq_args      : LEMMA v - v = zero

   sub_eq_zero      : LEMMA u - v = zero IFF u = v

   sub_cancel       : LEMMA v - w - v = -w

   sub_cancel_neg   : LEMMA -v - w + v = -w

   neg_add_left     : LEMMA -v + v = zero

   neg_add_right    : LEMMA v + -v = zero

   neg_distr_sub    : LEMMA -(v - u) = u - v

   neg_neg          : LEMMA --v = v

   neg_distr_add    : LEMMA -(u + v) = -u - v

   dot_neg_left     : LEMMA (-u)*w = -(u*w)

   dot_neg_right    : LEMMA u*(-w) = -(u*w)

   neg_dot_neg      : LEMMA (-u)*(-v) = u*v 

   dot_zero_left    : LEMMA zero * v = 0

   dot_zero_right   : LEMMA v * zero  = 0

   dot_comm         : LEMMA u*v = v*u

   dot_assoc        : LEMMA a*(v*w) = (a*v)*w

   dot_eq_args_ge   : LEMMA u*u >= 0

   add_comm_assoc_left : LEMMA (u+v)+w = (u+w)+v   

   add_comm_assoc_right: LEMMA u+(v+w) = v+(u+w)   

   dot_add_right    : LEMMA u*(v+w) = u*v + u*w

   dot_add_left     : LEMMA (v+w)*u = v*u + w*u

   dot_sub_right    : LEMMA u*(v-w) = u*v - u*w

   dot_sub_left     : LEMMA (v-w)*u = v*u - w*u

   add_dot_add      : LEMMA (u+v)*(w+z) = u*w+u*z+v*w+v*z


   dot_divby           : LEMMA nza*u = nza*v IMPLIES u = v  

   dot_scal_left       : LEMMA (a*u)*v = a*(u*v)

   dot_scal_right      : LEMMA u*(a*v) = a*(u*v)

   dot_scal_comm_assoc : LEMMA (a*u)*v = (a*v)*u  
   
   scal_assoc          : LEMMA a*(b*u) = (a*b)*u 

   scal_comm_assoc     : LEMMA a*(b*u) = b*(a*u)  

   dot_scal_canon      : LEMMA (a*u)*(b*v) = (a*b)*(u*v)    

   scal_add_left       : LEMMA (a+b)*u = a*u + b*u 

   scal_sub_left       : LEMMA (a-b)*u = a*u - b*u 

   scal_add_right      : LEMMA a*(u+v) = a*u + a*v 

   scal_sub_right      : LEMMA a*(u-v) = a*u - a*v 
   
   scal_neg       : LEMMA a*(-v) = (-a)*v  

   scal_cross     : LEMMA (1/nza) * v = w IFF v = nza*w 

   scal_zero      : LEMMA a * zero = zero

   scal_0         : LEMMA 0 * v = zero 

   scal_1         : LEMMA 1 * v = v 

   scal_neg_1     : LEMMA -1 * v = -v

   scal_cancel    : LEMMA a*nzv = b*nzv IMPLIES a = b  

   scal_div_mult_left  : LEMMA (a/nza)*u = v IFF a*u = nza*v  

   scal_div_mult_right : LEMMA u = (a/nza)*v IFF nza*u = a*v  

   scal_eq_zero   : LEMMA c*v = zero IMPLIES c = 0 OR v = zero 

   dot_ge_dist    : LEMMA w*u >= w*v IMPLIES w*(u-v) >= 0 

   dot_gt_dist    : LEMMA w*u > w*v  IMPLIES w*(u-v) > 0 

   idem_right     : LEMMA a * v = v IFF (a = 1 OR v = zero)

   sqv_neg        : LEMMA sqv(-v) = sqv(v)

   sqv_add        : LEMMA sqv(u+v) = sqv(u) + sqv(v) + 2*u*v

   sqv_scal       : LEMMA sqv(a*v) = sq(a)*sqv(v)

   sqv_sub        : LEMMA sqv(u-v) = sqv(u) + sqv(v) - 2*u*v

   sqv_sub_scal    : LEMMA sqv(u-a*v) = sqv(u) - 2*a*u*v + sq(a)*sqv(v) 

   sqv_sym        : LEMMA sqv(u-v) = sqv(v-u) 

   sqrt_sqv_sq    : LEMMA sqrt(sqv(v)) * sqrt(sqv(v)) = sqv(v)

   norm_sym       : LEMMA norm(u-v) = norm(v-u)

   norm_neg       : LEMMA norm(-u)  = norm(u)

   dot_sq_norm    : LEMMA u*u = sq(norm(u))

   sq_norm        : LEMMA sq(norm(u)) = sqv(u)

   sqv_eq_norm_eq : LEMMA FORALL (Dnn:nnreal): sqv(u) = sq(Dnn) IMPLIES norm(u) = Dnn

   norm_eq_sqv_eq : LEMMA FORALL (Dnn:nnreal): norm(u) = Dnn IMPLIES sqv(u) = sq(Dnn)

   sqrt_sqv_norm  : LEMMA sqrt(sqv(v)) = norm(v)

   norms_eq_sqv   : LEMMA norm(u) = norm(v) IFF sqv(u) = sqv(v)

   norms_eq_sos    : LEMMA norm(u) = norm(v) IFF sos(u) = sos(v)

   norm_le_sqv    : LEMMA norm(u) <= norm(v) IFF sqv(u) <= sqv(v)

   norm_lt_sqv    : LEMMA norm(u) < norm(v) IFF sqv(u) < sqv(v)

   norm_scal      : LEMMA norm(a*v) = abs(a)*norm(v) 

   ;^(nzv)         : Normalized = (1/norm(nzv))*nzv        

   normalize(nzv) : MACRO Normalized = ^(nzv)

   norm_normalize : LEMMA
     norm(^(nzv)) = 1     

   dot_normalize  : LEMMA 
     ^(nzu) * ^(nzv) = nzu*nzv/(norm(nzu)*norm(nzv))

   normalize_normalize: LEMMA ^(^(nzv)) = ^(nzv)    

   normalized_id  : LEMMA norm(nzv)*^(nzv) = nzv

   normalize_scal : LEMMA ^(nza*nzv) = sign(nza)*^(nzv)

   cauchy_schwarz : LEMMA sq(u*v) <= sqv(u)*sqv(v)

   dot_norm        : LEMMA -norm(u)*norm(v) <= u*v AND u*v <= norm(u)*norm(v)

   schwarz        : LEMMA abs(u*v) <= norm(u)*norm(v)

   schwarz_converse: LEMMA norm(u)*norm(nzv) = abs(u*nzv) IMPLIES 
                EXISTS (cr:real): cr*nzv = u

   schwarz_cor    : LEMMA sqrt(sqv(u+v)) <= sqrt(sqv(u)) + sqrt(sqv(v))

   norm_triangle   : LEMMA norm(u-w) <= norm(u-v) + norm(v-w) 

   norm_add_le     : LEMMA norm(u+v) <= norm(u) + norm(v)

   norm_sub_le     : LEMMA norm(u-v) <= norm(u) + norm(v)

   norm_sub_ge     : LEMMA norm(u-v) >= norm(u) - norm(v)

   norm_ge_comps   : LEMMA norm(u) >= abs(u`x) AND
                           norm(u) >= abs(u`y)                 

   v0,v1,v2  : VAR Vect2

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

% ---------- Predicates over vectors ---------

   parallel?(u,v): bool = 
     EXISTS (nzk:nzreal):  u = nzk*v

   dir_parallel?(u,v): bool = 
     EXISTS (pk:posreal):  u = pk*v 

   parallel_refl : LEMMA
     parallel?(u,u)

   parallel_symm : LEMMA
     parallel?(u,v) IFF parallel?(v,u)

   parallel_trans : LEMMA
     parallel?(u,v) AND parallel?(v,w) IMPLIES
     parallel?(u,w)

   parallel_zero : LEMMA
     parallel?(u,zero) IFF u = zero

   dir_parallel : LEMMA
     dir_parallel?(u,v) IMPLIES parallel?(u,v) 

   orthogonal?(u,v): bool =  u * v = 0 
  
   pythagorean : LEMMA
     orthogonal?(u,v) IMPLIES
     sqv(u+v) = sqv(u) + sqv(v)

   norm_add_ge_left : LEMMA
     orthogonal?(u,v) IMPLIES
     norm(u+v) >= norm(u) 

   norm_add_ge_right : LEMMA
     orthogonal?(u,v) IMPLIES
     norm(u+v) >= norm(v)

%  ----- following moved to basis_2D.pvs ----------------
%
%    orthogonal_basis: LEMMA
%      u /= zero AND
%      v /= zero AND
%      orthogonal?(u,v) IMPLIES
%      w = ((w*u)/sqv(u))*u + ((w*v)/sqv(v))*v

% ---------- Auto Rewrites  -----------------------

   AUTO_REWRITE+ neg_zero              % -zero=zero
   AUTO_REWRITE+ add_zero_left         % zero + v = -v
   AUTO_REWRITE+ add_zero_right        % v + zero = v
   AUTO_REWRITE+ sub_zero_left         % zero - v = -v
   AUTO_REWRITE+ sub_zero_right        % v - zero = v
   AUTO_REWRITE+ sub_eq_args           % v - v = zero
   AUTO_REWRITE+ neg_add_left          % -v + v = zero
   AUTO_REWRITE+ neg_add_right         % v + -v = zero
   AUTO_REWRITE+ dot_zero_left         % zero * v = 0
   AUTO_REWRITE+ dot_zero_right        % v * zero  = 0
   AUTO_REWRITE+ scal_zero             % a * zero = zero
   AUTO_REWRITE+ scal_0                % 0 * v = zero   
   AUTO_REWRITE+ scal_1                % 1 * v = v
   AUTO_REWRITE+ scal_neg_1            % -1 * v = -v
   AUTO_REWRITE+ sqv_zero              % sqv(zero) = 0
   AUTO_REWRITE+ norm_zero             % norm(zero) = 0 
   AUTO_REWRITE+ add_neg_sub           % v + -u = v - u
   AUTO_REWRITE+ neg_neg               % --v = v
   AUTO_REWRITE+ dot_scal_left         % (a*u)*v = a*(u*v)
   AUTO_REWRITE+ dot_scal_right        % u*(a*v) = a*(u*v)
   AUTO_REWRITE+ dot_scal_canon        % (a*u)*(b*v) = (a*b)*(u*v)   
   AUTO_REWRITE+ scal_assoc            % a*(b*u) = (a*b)*u 
   AUTO_REWRITE+ sqv_neg               % sqv(-v) = sqv(v)
   AUTO_REWRITE+ sqrt_sqv_sq           % sqrt(sqv(v)) * sqrt(sqv(v)) = sqv(v)  
   AUTO_REWRITE+ norm_neg              % norm(-u) = norm(u)
   AUTO_REWRITE+ norm_normalize        % norm(^(nzv)) = 1
   AUTO_REWRITE+ comp_zero_x           % zero`x = 0
   AUTO_REWRITE+ comp_zero_y           % zero`y = 0
   AUTO_REWRITE+ add_cancel            % v + w - v = w
   AUTO_REWRITE+ sub_cancel            % v - w - v = -w
   AUTO_REWRITE+ add_cancel_neg        % -v + w + v = w
   AUTO_REWRITE+ sub_cancel_neg        % -v - w + v = -w
   AUTO_REWRITE+ add_cancel2           % w - v + v = w
   AUTO_REWRITE+ add_cancel_neg2       % w + v - v = w

%  ---- Turn off dangerous and unhelpful rewrites for auto-rewrite-theory --

   AUTO_REWRITE-    zero
   AUTO_REWRITE-    add_comm           % u+v = v+u
   AUTO_REWRITE-    dot_comm           % u*v = v*u
   AUTO_REWRITE-    dot_assoc          % a*(v*w) = (a*v)*w   
   AUTO_REWRITE-    sqv_sym            % sqv(u-v) = sqv(v-u) 
   AUTO_REWRITE-    norm_sym           % norm(u-v) = norm(v-u)
   AUTO_REWRITE-    dot_sq_norm        % u*u = sq(norm(u))

  bolzano_weierstrass: LEMMA
    FORALL (M:posnat,VS:[nat->Vect2]):
      (FORALL (i:nat): norm(VS(i))<=M)
      IMPLIES (EXISTS (ns:[nat->nat],acp:Vect2):
        (FORALL (j:nat): ns(j)>=j) AND
        (FORALL (epsil:posreal): EXISTS (K:posnat):
   FORALL (j:nat): j>=K IMPLIES norm(VS(ns(j))-acp)<epsil)
 AND norm(acp)<=M)

END vectors_2D


[ Seitenstruktur0.33Drucken  etwas mehr zur Ethik  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik