|
vect3D : THEORY
%------------------------------------------------------------------------------
%
% This theory creates a special 3D version of vectors from the generic vectors
% library by importing vectors[3]. Note that this is nearly equivalent
% to the vectors_3D library. Since lemma names are the same this theory
% it is hoped that switching between them will be seemless. This theory
% seeks to bridge the gap between the generic vectors type:
%
% Index : TYPE = below(3)
% Vector : TYPE = [Index -> real]
%
% and the record structure of vectors_3D:
%
% Vect3: TYPE = [# x, y, z: real #]
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING vectors[3]
Vect3 : TYPE = Vector
x,y,z : VAR real
u,v : VAR Vect3
vect3(x,y,z) : Vect3 = LAMBDA(i:Index):
IF i=0 THEN x ELSIF i=1 THEN y ELSE z ENDIF
put_x(v,x) : Vect3 = v WITH [`0 := x]
put_y(v,y) : Vect3 = v WITH [`1 := y]
put_z(v,z) : Vect3 = v WITH [`2 := z]
x(v) : MACRO real = v(0)
y(v) : MACRO real = v(1)
z(v) : MACRO real = v(2)
% --------- Basis vectors
iv : Vect3 = vect3(1,0,0)
jv : Vect3 = vect3(0,1,0)
kv : Vect3 = vect3(0,0,1)
% ----------- Equality
eq3D?(u,v): bool= x(u)=x(v) AND y(u) = y(v) AND z(u)=z(v)
Eq3D : LEMMA eq3D?(u,v) IFF u = v
vect3D_0 : LEMMA vect3(x,y,z)(0) = x
vect3D_1 : LEMMA vect3(x,y,z)(1) = y
vect3D_2 : LEMMA vect3(x,y,z)(2) = z
pp3D(v) :[real,real,real] = (x(v),y(v),z(v))
END vect3D
¤ Dauer der Verarbeitung: 0.13 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.
|
