|
vectors[n: posnat]: THEORY
%----------------------------------------------------------------------------
% N-dimensional vectors of reals and operations (zero-based)
%----------------------------------------------------------------------------
BEGIN
IMPORTING reals@sigma_below[n], reals@sqrt
Index : TYPE = below(n)
Vector : TYPE = [Index -> real]
VectN : TYPE = Vector
a,b,c : VAR real
nza : VAR nzreal
u,v,w : VAR Vector
i : VAR Index
% ----------- Special vectors ---------------------------------------------
zero: Vector = LAMBDA(i):(0)
const_vec(a): Vector = LAMBDA(i):(a) ;
% ----------- Vector Operations -------------------------------------------
-(v): Vector = LAMBDA i: -v(i) ;
+(u,v)(i): real = u(i) + v(i) ;
-(u,v)(i): real = u(i) - v(i) ;
*(u,v): real = sigma(0,n-1,LAMBDA i:u(i)*v(i)) ; % Dot Product
*(a,v): Vector = LAMBDA i:a*v(i) ;
% ----------- Vector Functions -------------------------------------------
sqv(v): nnreal = v*v
sos(v): nnreal = sigma(0,n-1,LAMBDA i:sq(v(i)))
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
normalized?(v) : MACRO bool =
norm(v) = 1
Nz_vector : TYPE = (nz_vector?)
Normalized : TYPE = (normalized?)
unity(i): Normalized = zero WITH [i := 1]
nzu,nzv : VAR Nz_vector
% ----------- Vector Component Lemmas -------------------------------------
comp_distr_add : LEMMA (u + v)(i) = u(i) + v(i)
comp_distr_sub : LEMMA (u - v)(i) = u(i) - v(i)
comp_distr_scal : LEMMA (a*v)(i) = a*v(i)
comp_distr_neg : LEMMA (-v)(i) = -v(i)
comp_zero : LEMMA zero(i) = 0
comps_eq : LEMMA u = v IFF FORALL i: u(i) = v(i)
norm_comp_eq_0 : LEMMA norm(v) = 0 IFF FORALL i: v(i)=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
v_neq_0 : LEMMA v /= zero IFF sigma(0,n-1,(LAMBDA i: sq(v(i)))) > 0
sq_dot_eq_0 : LEMMA v*v = 0 IFF v = zero
nzv_comp_neq_0 : LEMMA nz_vector?(v) IFF EXISTS(i): v(i) /= 0
% ----------- JUDGEMENTS -------------------------------------
nz_norm_gt_0 : JUDGEMENT
norm(nzu) HAS_TYPE posreal
nz_sqv_gt_0 : JUDGEMENT
sqv(nzu) HAS_TYPE posreal
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_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_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_eq_zero : LEMMA a*v = zero IMPLIES a = 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)
schwarz : LEMMA abs(u*v) <= norm(u)*norm(v)
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(i))
v0,v1,v2 : VAR Vector
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+ norm_normalize
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+ 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_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
¤ Dauer der Verarbeitung: 0.2 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.
|
