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: nvectors.pvs   Sprache: PVS

Original von: PVS©
nvectors: THEORY
%----------------------------------------------------------------------------
% N-dimensional vectors of reals and operations (zero-based)
%----------------------------------------------------------------------------
BEGIN
   
%   reals: LIBRARY = "../reals"

   IMPORTING reals@sigma_nat, reals@sqrt
   IMPORTING structures@fseqs_def[real,0]

   n: VAR posnat

   Vector : TYPE = {s: fseq | s`length > 0}
   Vect(n): TYPE = {v: Vector | v`length = n}

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

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


   -(v): Vect(v`length) = 
       (# length := v`length,
          seq    := LAMBDA (i: nat): -v(i) 
       #) ;

   +(u: Vector, v: Vect(u`length)): Vect(u`length) = 
     (# length := u`length,
        seq := (LAMBDA (i: nat): u`seq(i) + v`seq(i))
      #) ;

   -(u: Vector, v: Vect(u`length)): Vect(u`length) = u + -v ;

   *(u: Vector, v: Vect(u`length)): real =
       sigma(0, u`length-1, LAMBDA (i: nat):u(i)*v(i)); % Dot Product

   *(a,v): Vect(v`length) =
       (# length := v`length,
          seq := LAMBDA (i: nat): a*v(i) 
       #)
    

%  ^(nzv): Normalized = (1/norm(nzv))*nzv              % defined ahead

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

   sqv(v): nnreal = v*v

   sq(v): nnreal = sigma(0,v`length-1,LAMBDA (i: nat): sq(v(i)))

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

   zero_vector?(v) : MACRO bool = (norm(v) = 0)
   nz_vector?(v)   : MACRO bool = (norm(v) /= 0)  
   normalized?(v)  : MACRO bool = (norm(v) = 1)

   zero_vect?(n)(v: Vect(n)) : MACRO bool = (norm(v) = 0)
   nz_vect?(n)(v: Vect(n))  : MACRO bool = (norm(v) /= 0)  
   normalized_vect?(n)(v: Vect(n)) : MACRO bool = (norm(v) = 1)
 
   Zero_vector : TYPE = (zero_vector?)
   Nz_vector   : TYPE = (nz_vector?)
   Normalized  : TYPE = (normalized?)

   Zero_vect(n)  : TYPE = (zero_vect?(n))
   Nz_vect(n) : TYPE = (nz_vect?(n))
   Normalized_vect(n) : TYPE = (normalized_vect?(n))

   nzu,nzv     : VAR Nz_vector

%  normalize(nzv) : Normalized = (1/norm(nzv))*nzv

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

   zero(n) : Zero_vect(n) = (# length := n, seq := LAMBDA (i: nat): 0 #)

   unity(n)(i: below(n)): Normalized_vect(n) =
      zero(n) WITH [`seq(i) := 1]

   const_vec(n)(a): Vect(n)  = const_seq(n,a)

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

   comp_distr_add  : LEMMA
     FORALL (v: Vector, w: Vect(v`length), i: nat): i < v`length IMPLIES
       (v + w)`seq(i) = v`seq(i) + w`seq(i)  

   comp_distr_sub  : LEMMA
     FORALL (v: Vector, w: Vect(v`length), i: nat): i < v`length IMPLIES
       (v - w)`seq(i) = v`seq(i) - w`seq(i)  

   comp_distr_scal : LEMMA 
     FORALL (v: Vector, i: nat): i < v`length IMPLIES
       (a*v)`seq(i) = a*(v`seq(i))                %% NEW %%

   comp_zero : LEMMA FORALL (i: below(n)): zero(n)`seq(i) = 0

   comp_eq : LEMMA
     FORALL (u, (w: Vect(u`length))):
        u = w IFF FORALL (i: below(u`length)): u(i) = w(i)   %%%% NEW %%%%

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

   add_zero_left  : LEMMA FORALL (v: Vect(n)): zero(n) + v = v

   add_zero_right : LEMMA FORALL (v: Vect(n)): v + zero(n) = v

   add_comm       : LEMMA FORALL (u: Vector, v: Vect(u`length)): u+v = v+u

   add_assoc      : LEMMA
     FORALL (u: Vector, v, w: Vect(u`length)): u+(v+w) = (u+v)+w

   add_move_right : LEMMA
     FORALL (u: Vector, v, w: Vect(u`length)): u + w = v IFF u = v - w

   add_move_both  : LEMMA
     FORALL (u: Vector, v, w: Vect(u`length)): v = u + w IFF u = v - w

   add_neg_sub    : LEMMA
     FORALL (u: Vector, v: Vect(u`length)): v + -u = v - u

   add_cancel     : LEMMA
     FORALL (v: Vector, w: Vect(v`length)): v + w - v = w
   
   add_cancel_neg : LEMMA
     FORALL (v: Vector, w: Vect(v`length)): -v + w + v = w

   add_cancel2    : LEMMA
     FORALL (v: Vector, w: Vect(v`length)): w - v + v = w
   
   add_cancel_neg2 : LEMMA
     FORALL (v: Vector, w: Vect(v`length)): w + v - v = w


   sub_zero_left  : LEMMA FORALL (v: Vect(n)): zero(n) - v = -v

   sub_zero_right : LEMMA FORALL (v: Vect(n)): v - zero(n) = v

   sub_eq_args    : LEMMA FORALL (v: Vect(n)): v - v = zero(n)

   sub_eq_zero    : LEMMA FORALL (u, v: Vect(n)):
      u - v = zero(n) IFF u = v

   sub_cancel     : LEMMA
      FORALL (v: Vector, w: Vect(v`length)): v - w - v = -w

   sub_cancel_neg : LEMMA
      FORALL (v: Vector, w: Vect(v`length)): -v - w + v = -w


   neg_add_left   : LEMMA FORALL (v: Vect(n)): -v + v = zero(n)

   neg_add_right  : LEMMA FORALL (v: Vect(n)): v + -v = zero(n)

   neg_distr_sub  : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): -(v - u) = u - v

   neg_neg        : LEMMA --v = v

   neg_distr_add  : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): -(u + v) = -u - v


   dot_neg_left        : LEMMA
      FORALL (u: Vector, w: Vect(u`length)): (-u)*w = -(u*w)

   dot_neg_right       : LEMMA
      FORALL (u: Vector, w: Vect(u`length)): u*(-w) = -(u*w)

   dot_neg_sq          : LEMMA (-v)*(-v) = v*v 

   dot_zero_left       : LEMMA zero(v`length) * v = 0

   dot_zero_right      : LEMMA v * zero(v`length)  = 0

   dot_comm            : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): u*v = v*u

   dot_assoc           : LEMMA
      FORALL (w: Vect(v`length)): a*(v*w) = (a*v)*w

   dot_eq_args_ge      : LEMMA u*u >= 0

   dot_distr_add_left  : LEMMA
      FORALL (u: Vector, v, w: Vect(u`length)): u*(v+w) = u*v + u*w

   dot_distr_add_right : LEMMA
      FORALL (u: Vector, v, w: Vect(u`length)): (v+w)*u = v*u + w*u

   dot_distr_sub_left  : LEMMA
      FORALL (u: Vector, v, w: Vect(u`length)): u*(v-w) = u*v - u*w

   dot_distr_sub_right : LEMMA
      FORALL (u: Vector, v, w: Vect(u`length)): (v-w)*u = v*u - w*u

   dot_divby           : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): nza*u = nza*v IMPLIES u = v   %%%% NEW %%%%


   dot_scal_left       : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): (a*u)*v = a*(u*v)

   dot_scal_right      : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): u*(a*v) = a*(u*v)

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

   dot_scal_canon      : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): (a*u)*(b*v) = (a*b)*(u*v)      %% NEW %%x

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

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

   scal_add_distr      : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): a*(u+v) = a*u + a*v 

   scal_sub_distr      : LEMMA 
      FORALL (u, (v: Vect(u`length))): a*(u-v) = a*u - a*v 


   scal_zero      : LEMMA a * zero(n) = zero(n)

   scal_0         : LEMMA 0 * v = zero(v`length)

   scal_1         : LEMMA 1 * v = v

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


   scal_dot_eq_0  : LEMMA
      FORALL (v: Vect(n)): c*v = zero(n) IMPLIES c = 0 OR v = zero(n) %%%% NEW %%%%

   dot_ge_dist    : LEMMA
      FORALL (u: Vector, v, w: Vect(u`length)): w*u >= w*v IMPLIES w*(u-v) >= 0 

   dot_gt_dist    : LEMMA 
      FORALL (u: Vector, v, w: Vect(u`length)): w*u > w*v IMPLIES w*(u-v) > 0 

   sq_dot_eq      : LEMMA
      v*v = 0 IFF v = zero(v`length)

   sqv_sq         : LEMMA sqv(v) = sq(v)

   sq_sqv         : LEMMA sq(v) = sqv(v)

   sq_lem         : LEMMA
      sq(v) = sigma(0,v`length-1,LAMBDA (i: nat): sq(v(i)))

   sqv_lem        : LEMMA
      sqv(u) = sigma(0,u`length-1,(LAMBDA (i: nat): sq(u(i))))

   sqv_zero       : LEMMA sqv(zero(n)) = 0

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

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

   sqv_add        : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): sqv(u+v) = sqv(u) + sqv(v) + 2*u*v

   sqv_sub        : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): sqv(u-v) = sqv(u) + sqv(v) - 2*u*v

   sqv_sym        : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): sqv(u-v) = sqv(v-u)   

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

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


   norm_sym       : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): 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)) = u*u

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


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

   norms_eq_sqv   : LEMMA
      FORALL (u: Vector, v: Vect(u`length)): norm(u) = norm(v) IFF sqv(u) = sqv(v)

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

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

   ^(nzv)         : Normalized = (1/norm(nzv))*nzv              %% NEW %%
   normalize(nzv) : MACRO Normalized = ^(nzv)


   dot_normalize  : LEMMA
       FORALL (nzv: Nz_vect(nzu`length)): ^(nzu) * ^(nzv) %% NEW %%
                               = nzu*nzv/(norm(nzu)*norm(nzv))

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


   sqv_minus_dot   : LEMMA
       FORALL (u: Vector, v: Vect(u`length)): sqv(u-a*v) = sqv(u) - 2*a*u*v + sq(a)*sqv(v)

   cauchy_schwarz : LEMMA
       FORALL (u: Vector, v: Vect(u`length)): sq(u*v) <= sqv(u)*sqv(v)

   dot_norm        : LEMMA
       FORALL (u: Vector, v: Vect(u`length)): -norm(u)*norm(v) <= u*v AND u*v <= norm(u)*norm(v)

   norm_add_le     : LEMMA
       FORALL (u: Vector, v: Vect(u`length)): norm(u+v) <= norm(u) + norm(v)

   norm_sub_le     : LEMMA
       FORALL (u: Vector, v: Vect(u`length)): norm(u-v) <= norm(u) + norm(v)

   norm_sub_ge     : LEMMA
       FORALL (u: Vector, v: Vect(u`length)): norm(u-v) >= norm(u) - norm(v)


   norm_ge_comps   : LEMMA
       FORALL (i: nat): norm(u) >= abs(u`seq(i)) %% NEW %%

   v0,v1,v2 : VAR Vector
   norm_triangle   : LEMMA
      FORALL (v0: Vector, v1, v2: Vect(v0`length)):
        LET a = v1-v0, b = v1-v2, c = v2-v0 IN    %% NEW %%
            sq(norm(c)) = sq(norm(a)) + sq(norm(b)) - 2*a*b

   nzvec_has_nz    : LEMMA (EXISTS (i: below(nzv`length)): nzv`seq(i) /= 0)      %% NEW %%

   nzvec_neq_zero  : LEMMA nzv /= zero(nzv`length) %% NEW %%


   v_neq_0        : LEMMA v /= zero(v`length) IFF sigma(0,v`length-1,(LAMBDA (i: nat): sq(v(i)))) > 0

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

  parallel?(nzu, (nzv: Nz_vect(nzu`length))): bool =
        ^(nzu)*^(nzv) = 1 OR ^(nzu)*^(nzv) = -1  %% NEW %%

  orthogonal?(u,(v: Vect(u`length))): bool =  u * v = 0 ;

%  parallel_lem: LEMMA parallel?(nzu,nzv) IFF (EXISTS (k:nzreal):  nzu = k*nzv)

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


   AUTO_REWRITE+ add_zero_left  
   AUTO_REWRITE+ add_zero_right 
   AUTO_REWRITE+ sub_zero_left  
   AUTO_REWRITE+ sub_zero_right 
   AUTO_REWRITE+ sub_eq_zero                       %% NEW %%

   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+ sqv_zero       
   AUTO_REWRITE+ add_neg_sub    
   AUTO_REWRITE+ neg_neg        
   AUTO_REWRITE+ dot_scal_left      
   AUTO_REWRITE+ dot_scal_right     
   AUTO_REWRITE+ dot_scal_assoc     
   AUTO_REWRITE+ dot_scal_canon                 %% NEW %%
   AUTO_REWRITE+ sqv_neg        
   AUTO_REWRITE+ sqrt_sqv_sq
   AUTO_REWRITE+ norm_neg       
   AUTO_REWRITE+ comp_zero
   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_lem           % LEMMA sqv(u) = u*u
   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 nvectors

¤ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff