products/sources/formale Sprachen/PVS/vectors/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: main.dcu   Sprache: PVS

Original von: PVS©
vectors_4D: THEORY
%----------------------------------------------------------------------------
%
%  The Vect4 type is a record [#  x, y, z, t: real  #]
%  but the vect4 conversion allows one to write (x,y,z,t) 
%
%----------------------------------------------------------------------------
BEGIN

   IMPORTING reals@sqrt, vectors_4D_def

   Vector   : TYPE = Vect4
   u,v,w    : VAR Vector
   a,b,c,d  : VAR real
   nza      : VAR nzreal 

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

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

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

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

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

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

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

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

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

   sqv(v): nnreal = v*v

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

   sqv_rew        : LEMMA v*v = sqv(v)

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

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

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

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

   zero_vect4? : MACRO PRED[Vector] = zero_vector?
   nz_vect4?   : MACRO PRED[Vector] = nz_vector?

   normalized?(v): MACRO bool = 
     norm(v) = 1
 
   Nz_vector   : TYPE = (nz_vector?)
   Nz_vect4    : TYPE = Nz_vector
   Normalized  : TYPE = (normalized?)

   iv: Vector = (1,0,0,0)
   jv: Vector = (0,1,0,0)
   kv: Vector = (0,0,1,0)
   lv: Vector = (0,0,0,1)

   nzu,nzv     : VAR Nz_vector

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

   basis          : LEMMA a*iv + b*jv +c*kv + d*lv  = (a,b,c,d)

   vx_distr_add   : LEMMA (v + w)`x = v`x + w`x  
   vy_distr_add   : LEMMA (v + w)`y = v`y + w`y  
   vz_distr_add   : LEMMA (v + w)`z = v`z + w`z  
   vt_distr_add   : LEMMA (v + w)`t = v`t + w`t  

   vx_distr_sub   : LEMMA (v - w)`x = v`x - w`x  
   vy_distr_sub   : LEMMA (v - w)`y = v`y - w`y  
   vz_distr_sub   : LEMMA (v - w)`z = v`z - w`z  
   vt_distr_sub   : LEMMA (v - w)`t = v`t - w`t  

   vx_scal        : LEMMA (a*v)`x = a*v`x                       
   vy_scal        : LEMMA (a*v)`y = a*v`y                       
   vz_scal        : LEMMA (a*v)`z = a*v`z                       
   vt_scal        : LEMMA (a*v)`t = a*v`t                       

   vx_neg         : LEMMA (-v)`x = -v`x
   vy_neg         : LEMMA (-v)`y = -v`y
   vz_neg         : LEMMA (-v)`z = -v`z
   vt_neg         : LEMMA (-v)`t = -v`t

   comp_eq_x      : LEMMA u = w IMPLIES u`x = w`x       
   comp_eq_y      : LEMMA u = w IMPLIES u`y = w`y       
   comp_eq_z      : LEMMA u = w IMPLIES u`z = w`z       
   comp_eq_t      : LEMMA u = w IMPLIES u`t = w`t       

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

   comp_zero_x    : LEMMA zero`x = 0
   comp_zero_y    : LEMMA zero`y = 0
   comp_zero_z    : LEMMA zero`z = 0
   comp_zero_t    : LEMMA zero`t = 0

   norm_xyz_eq_0  : LEMMA norm(v) = 0 IFF v`x =0 AND v`y=0 AND v`z=0 AND v`t=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_xyz_neq_0  : LEMMA nz_vector?(v) IFF v`x /= 0 OR v`y /= 0 OR v`z /= 0 OR v`t /= 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_vect4(nza,b,c,d) HAS_TYPE Nz_vector

   nz_nvz_middle : JUDGEMENT
     mk_vect4(b,nza,c,d) HAS_TYPE Nz_vector

   nz_nvz_right : JUDGEMENT
     mk_vect4(b,c,nza,d) HAS_TYPE Nz_vector

   nz_nvz_time : JUDGEMENT
     mk_vect4(b,c,d,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

   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_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_assoc     : LEMMA a*(b*u) = (a*b)*u  

   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)

   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)

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

   schwartz_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) AND               
                           norm(u) >= abs(u`z) AND                      
                           norm(u) >= abs(u`t)

   v0,v1,v2  : VAR Vect4
   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)

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

   AUTO_REWRITE+ neg_zero
   AUTO_REWRITE+ add_zero_left  
   AUTO_REWRITE+ add_zero_right 
   AUTO_REWRITE+ sub_zero_left  
   AUTO_REWRITE+ sub_zero_right 
   AUTO_REWRITE+ sub_eq_args    
   AUTO_REWRITE+ neg_add_left   
   AUTO_REWRITE+ neg_add_right  
   AUTO_REWRITE+ dot_zero_left  
   AUTO_REWRITE+ dot_zero_right 
   AUTO_REWRITE+ scal_zero      
   AUTO_REWRITE+ scal_0         
   AUTO_REWRITE+ scal_1 
   AUTO_REWRITE+ scal_neg_1        
   AUTO_REWRITE+ sqv_zero
   AUTO_REWRITE+ norm_zero      
   AUTO_REWRITE+ add_neg_sub    
   AUTO_REWRITE+ neg_neg        
   AUTO_REWRITE+ dot_scal_left      
   AUTO_REWRITE+ dot_scal_right     
   AUTO_REWRITE+ dot_scal_canon                 
   AUTO_REWRITE+ scal_assoc     
   AUTO_REWRITE+ sqv_neg        
   AUTO_REWRITE+ sqrt_sqv_sq
   AUTO_REWRITE+ norm_neg 
   AUTO_REWRITE+ norm_normalize      
   AUTO_REWRITE+ comp_zero_x
   AUTO_REWRITE+ comp_zero_y
   AUTO_REWRITE+ comp_zero_z
   AUTO_REWRITE+ add_cancel
   AUTO_REWRITE+ sub_cancel
   AUTO_REWRITE+ add_cancel_neg
   AUTO_REWRITE+ sub_cancel_neg
   AUTO_REWRITE+ add_cancel2
   AUTO_REWRITE+ add_cancel_neg2

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

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

END vectors_4D


¤ Dauer der Verarbeitung: 0.42 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff