Quellverzeichnis 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

quality98%

¤ 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.0.15Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.