Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: trig_aux.prf   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.24 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
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



                                                                                                                                                                                                                                                                                                                                                                                                     


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