|
vectors_3D: THEORY
%----------------------------------------------------------------------------
%
% The Vect3 type is a record [# x, y, z: real #]
% but the vect3 conversion allows one to write (x,y,z)
%
%----------------------------------------------------------------------------
BEGIN
IMPORTING reals@sqrt, vectors_3D_def
Vector : TYPE = Vect3
u,v,w : VAR Vector
a,b,c : VAR real
nza : VAR nzreal
% ----------- Special vectors ---------------------------------------------
zero: Vector = (0,0,0)
const_vec(a): Vector = (a,a,a) ;
% ----------- Vector Operations -------------------------------------------
-(v) : Vector = ( -v`x, -v`y, -v`z ) ;
+(u,v): Vector = ( u`x + v`x, u`y + v`y, u`z + v`z ) ;
-(u,v): Vector = ( u`x - v`x, u`y - v`y, u`z - v`z ) ;
*(u,v): real = u`x * v`x + u`y * v`y + u`z * v`z ; % dot product
*(a,v): Vector = ( a * v`x, a * v`y, a * v`z ) ;
% ----------- Vector Functions -------------------------------------------
sqv(v): nnreal = v*v
sos(v): nnreal = sq(v`x)+sq(v`y)+sq(v`z)
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
zero_vect3? : MACRO PRED[Vector] = zero_vector?
nz_vect3? : MACRO PRED[Vector] = nz_vector?
normalized?(v): MACRO bool =
norm(v) = 1
Nz_vector : TYPE = (nz_vector?)
Nz_vect3 : TYPE = Nz_vector
Normalized : TYPE = (normalized?)
iv: Vector = (1,0,0)
jv: Vector = (0,1,0)
kv: Vector = (0,0,1)
nzu,nzv : VAR Nz_vector
% ----------- Vector Component Lemmas
basis : LEMMA a*iv + b*jv +c*kv = (a,b,c)
vx_distr_add : LEMMA (v + w)`x = v`x + w`x
vy_distr_add : LEMMA (v + w)`y = v`y + w`y
vz_distr_add : LEMMA (v + w)`z = v`z + w`z
vx_distr_sub : LEMMA (v - w)`x = v`x - w`x
vy_distr_sub : LEMMA (v - w)`y = v`y - w`y
vz_distr_sub : LEMMA (v - w)`z = v`z - w`z
vx_scal : LEMMA (a*v)`x = a*v`x
vy_scal : LEMMA (a*v)`y = a*v`y
vz_scal : LEMMA (a*v)`z = a*v`z
vx_neg : LEMMA (-v)`x = -v`x
vy_neg : LEMMA (-v)`y = -v`y
vz_neg : LEMMA (-v)`z = -v`z
comp_eq_x : LEMMA u = w IMPLIES u`x = w`x
comp_eq_y : LEMMA u = w IMPLIES u`y = w`y
comp_eq_z : LEMMA u = w IMPLIES u`z = w`z
comps_eq : LEMMA u = w IFF u`x = w`x AND u`y = w`y AND u`z = w`z
comp_zero_x : LEMMA zero`x = 0
comp_zero_y : LEMMA zero`y = 0
comp_zero_z : LEMMA zero`z = 0
norm_xyz_eq_0 : LEMMA norm(v) = 0 IFF v`x =0 AND v`y=0 AND v`z=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_xyz_neq_0 : LEMMA nz_vector?(v) IFF v`x /= 0 OR v`y /= 0 OR v`z /= 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_vect3(nza,b,c) HAS_TYPE Nz_vector
nz_nvz_middle : JUDGEMENT
mk_vect3(b,nza,c) HAS_TYPE Nz_vector
nz_nvz_right : JUDGEMENT
mk_vect3(b,c,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
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_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)
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`x) AND
norm(u) >= abs(u`y) AND
norm(u) >= abs(u`z)
v0,v1,v2 : VAR Vect3
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+ 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+ norm_normalize
AUTO_REWRITE+ comp_zero_x
AUTO_REWRITE+ comp_zero_y
AUTO_REWRITE+ comp_zero_z
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_3D
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.23Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
