|
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
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
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.
|
