;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*- 

;;; Vector Quantities 
;;; (c) 1993 Greg Olsen and Thomas Gruber 

(in-package "ONTOLINGUA-USER") 

(define-theory vector-quantities (scalar-quantities) 

  "This theory is used to represent vectors of n spatial dimensions 
which are physical quantities with physical dimensions, such as 'the 
velocity of particle p'.  The theory supports arbitrary numbers of 
basis vector sets and hence vectors are not isomorphic to n-tuples as 
is the case in some textbook representations of vectors (Note: 
Multi-basis vector spaces are essential to many theories such as 
kinematics).  Standard vector operations such as vector addition, 
scalar multiplication, and scalar or dot product are supported. 
Operators on vector-quantities must take into account the associated 
units and dimensions.") 

(in-theory 'vector-quantities) 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
;;; N-Dimensional Vector Quantities 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

(define-class VECTOR-QUANTITY (?v) 

  "The class of quantities which are n-dimensional vectors. Each 
vector has an associated spatial dimension and an associated physical 
dimension.  Each vector-quantity can be decomposed into scalar 
components for a given orthonormal basis of the proper dimension.  The 
physical-dimension of a scalar component of the vector-quantity is 
equivalent to the physical-dimension of the vector-quantity." 

  :iff-def (and (constant-quantity ?v) 
		(defined (vector.dimension ?v)) 
		(forall (?b ?i) 
			(=> (and (orthonormal-basis ?b) 
				 (= (basis.dimension ?b)  
				    (vector.dimension ?v)) 
				 (positive-integer ?i) 
				 (=< ?i (vector.dimension ?v))) 
			    (and (defined (vector-component ?v ?i ?b))  
				 (= (quantity.dimension (vector-component ?v ?i ?b)) 
				    (quantity.dimension ?v))))) 

		(forall ?u (=> (and (unit-of-measure ?u) 
                                    (= (quantity.dimension ?u)  
                                       (quantity.dimension ?v))) 
			       (numeric-vector (magnitude ?v ?u)))))) 

(define-class NUMERIC-VECTOR (?x) 

  "A numeric-valued vector.  Its components expressed in any basis are 
numeric or non-dimensional." 

  :def (and (vector-quantity ?x) 
	    (nondimensional-constant-quantity ?x))) 


(define-class UNIT-VEC (?v) 

  "Unit length vectors." 
  :iff-def (and (vector-quantity ?v) 
		(= (quantity.dimension ?v) identity-dimension) 
		(= (dot ?v ?v) 1))) 

(define-function VECTOR.DIMENSION (?v) :-> ?n 

  "Function that returns the spatial dimension associated with a vector." 

  :def (and (vector-quantity ?v) 
	    (positive-integer ?n))) 

(define-class ORTHONORMAL-BASIS (?b) 

  "A set of n vector-quantities in an n-dimensional vector space which 
form an ortho-normal basis, the n vector-quantities are linearly 
independent and the scalar product of any two is the identity-scalar." 

  :def (and (defined (basis.dimension ?b)) 
	    (forall ?n (=> (and (positive-integer ?n) 
				(=< ?n (basis.dimension ?b))) 
			   (defined (basis.vec ?b ?n)))) 
	    (forall (?n1 ?n2) 
		    (=> (and (positive-integer ?n1) 
			     (positive-integer ?n2) 
			     (=< ?n1 (basis.dimension ?b)) 
			     (=< ?n2 (basis.dimension ?b))) 
			(=> (= ?n1 ?n2) 
			    (= (dot (basis.vec ?b ?n1) (basis.vec ?b ?n2)) 
			       1)) 
			(=> (/= ?n1 ?n2) 
			    (= (dot (basis.vec ?b ?n1) (basis.vec ?b ?n2)) 
			       0)))))) 

(define-function BASIS.VEC (?basis ?n) :-> ?uv 

  "Function to select the individual unit vectors of a basis." 

  :def (and (orthonormal-basis ?basis) 
	    (positive-integer ?n) 
	    (=< ?n (basis.dimension ?basis)) 
	    (unit-vec ?uv))) 

(define-function BASIS.DIMENSION (?b) :-> ?n 

  "Function that returns the spatial dimension associated with a basis 
set of vectors." 

  :def (and (orthonormal-basis ?b) 
	    (positive-integer ?n))) 

(define-function VECTOR-COMPONENT (?v ?i ?b) :-> ?s 

  "Function to generate the ith scalar component for a vector-quantity in 
a particular basis." 

  :iff-def (and (vector-quantity ?v) 
		(positive-integer ?i) 
		(orthonormal-basis ?b) 
		(scalar-quantity ?s) 
		(= (quantity.dimension ?s) (quantity.dimension ?v)) 
		(= (vector.dimension ?v) (basis.dimension ?b)) 
		(=< ?i (vector.dimension ?v)) 
		(= ?s (dot ?v (basis.vec ?b ?i))))) 

(define-function THE-VECTOR-QUANTITY (?sl ?b) :-> ?v 

  "Constructor function for a vector-quantity with scalar components ?sl in 
ortonormal basis ?b." 

  :iff-def (and (scalar-list ?sl) 
		(orthonormal-basis ?b) 
		(vector-quantity ?v) 
		(= (quantity.dimension ?v) 
		   (quantity.dimension (first ?sl))) 
		(= (length ?sl) (basis.dimension ?b)) 
		(= (vector.dimension ?v) (length ?sl)) 
		(= (nth ?sl ?i) (vector-component ?v ?i ?b)) 
		(= ?v (summation 
		       (lambda (?j) (* (nth ?sl ?j) 
					(basis.vec ?b ?j))) 
		       1 
		       (vector.dimension ?v)))) 

  :issues ((:example 
            (= (the-vector-quantity (listof (* 3 feet)  
					    (* 1 yard)) 
				    2D-frame-n) 
	       (*  
		(the-vector-quantity (listof 3 3) 2D-frame-n) 
		feet))))) 

(define-class SCALAR-LIST (?sl) 

  "Class of ordered sequences of the scalars of a common physical 
dimension." 

  :iff-def (and (list ?sl) 
		(forall ?s (=> (item ?s ?sl) 
			       (scalar-quantity ?s))) 
		(forall (?s1 ?s2) 
			(=> (and (item ?s1 ?sl) (item ?s2 ?sl)) 
			    (compatible-quantities ?s1 ?s2))))) 

(define-function THE-ZERO-VECTOR-OF-TYPE (?spatdim ?physdim) :-> ?v0 

  "The ?spatdim dimensional zero vector of physical dimension ?physdim." 

  :def (and (vector-quantity ?v0) 
	    (positive-integer ?spatdim) 
	    (physical-dimension ?physdim) 
	    (forall ?v 
	       (=> (vector-quantity ?v) 
		   (= (dot ?v (the-zero-vector-of-type ?spatdim ?physdim)) 
		      (the-zero-scalar-for-dimension ?physdim)))))) 

(define-function VECTOR-QUANTITIES-OF-DIMENSIONS (?physim ?spatdim) :-> ?class 

   := (if (and (physical-dimension ?physim) 
	       (positive-integer ?spatdim)) 
	  (kappa (?vq) 
		 (and (vector-quantity ?vq) 
		      (= (vector.dimension ?vq) ?spatdim) 
		      (= (quantity.dimension ?vq) ?physim))))) 

(define-function + (?x ?y) :-> ?z 

  "Addition operator for vectors." 

  :when (and (vector-quantity ?x) 
	     (vector-quantity ?y)) 
  :def (and  
	(vector-quantity ?z) 
	(= (vector.dimension ?x) (vector.dimension ?y)) 
	(= (vector.dimension ?x) (vector.dimension ?z)) 
	 
	(forall (?b ?i) 
		(=> (and (orthonormal-basis ?b) 
			 (= (vector.dimension ?x) (basis.dimension ?b)) 
			 (positive-integer ?i) 
			 (=< ?i (vector.dimension ?x))) 
		    (= (vector-component ?z ?i ?b) 
		       (+ (vector-component ?x ?i ?b) 
			   (vector-component ?y ?i ?b)))))) 

  :axiom-def (forall (?physdim ?spatdim) 
		(abelian-group  
                  (vector-quantities-of-dimensions ?physdim ?spatdim) 
                  +  
                  (the-zero-vector-of-type ?spatdim ?physdim)))) 

(define-function - (?x) :-> ?y 

  "The specializaion of the additive inverse operator for 
vector-quantities.  It specializes the generic - operator." 

  :when (vector-quantity ?x) 
  :def (and (vector-quantity ?y) 
		(= (+ ?x ?y)  
		   (the-zero-vector-of-type (quantity.dimension ?x)  
                                            (vector.dimension ?x))))) 

(define-function DOT (?v1 ?v2) :-> ?s 

  "Vector-Quantity dot or scalar product.  Generalizes to 
inner-product.  This product is only defined for vectors of a common 
spatial dimension.  The physical dimension of the product is the 
product of the dimensions of the argument vectors.  The product is the 
sum of the products of the corresponding scalar components of the 
argument vectors for a common basis." 
   
  :def (and (vector-quantity ?v1) 
	    (vector-quantity ?v2) 
	    (= (vector.dimension ?v1) (vector.dimension ?v2)) 
	    (scalar-quantity ?s) 
	    (= (quantity.dimension ?s)  
	      (* (quantity.dimension ?v1) (quantity.dimension ?v2))) 
	    (forall ?b  
		    (=> (= (basis.dimension ?b) (vector.dimension ?v1)) 
			(= ?s  
			   (summation 
			    (lambda (?j)  
			      (* (vector-component ?v1 ?j ?b) 
				 (vector-component ?v2 ?j ?b))) 
			    1 
			    (vector.dimension ?v1))))))) 

	     
(define-function * (?s ?v1) :-> ?v 

  "The specialization of * for multiplication of a vector-quantity by 
a scalar." 

  :when (and (scalar-quantity ?s) 
	    (vector-quantity ?v1)) 
  :def (and (vector-quantity ?v) 
	    (= (vector.dimension ?v1) (vector.dimension ?v)) 
	    (forall (?b ?i) 
		    (=> (= (basis.dimension ?b) (vector.dimension ?v1)) 
			(= (vector-component ?v ?i ?b) 
			   (* ?s (vector-component ?v1 ?i ?b))))))) 

(define-function * (?v1 ?s) :-> ?v 
    "* is communtative for scalar/vector pairs." 
    :when (and (vector-quantity ?v1) 
               (scalar-quantity ?s)) 
    := (* ?s ?v1)) 



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
;; 3-Dimensional Vector-Quantity Algebra 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

(define-class 3D-VECTOR-QUANTITY (?x) 

  "Vectors of 3-dimensions. (These vectors have important properities 
and are of particular interest to engineering analysis)." 

  :def (and (vector-quantity ?x) 
	    (vector.dimension ?x 3))) 

(define-function CROSS (?v1 ?v2) :-> ?v 

  "Vector or cross product of two three dimensional vectors.  If we 
know the components of two vectors with respect to a common basis, we 
can determine the components of the cross product in that basis." 

  :def (and (3d-vector-quantity ?v1) 
	    (3d-vector-quantity ?v2) 
	    (3d-vector-quantity ?v) 

	    (= (quantity.dimension ?v)  
	       (* (quantity.dimension ?v1) (quantity.dimension ?v2))) 
	    (= (dot ?v1 ?v)  
	       (the-zero-scalar-for-dimension (* (quantity.dimension ?v1) 
                                                (quantity.dimension ?v)))) 
	    (= (dot ?v2 ?v) 
	       (the-zero-scalar-for-dimension (* (quantity.dimension ?v2) 
                                                (quantity.dimension ?v)))) 
	    (and 
	     (= (vector-component ?v 1 ?b) 
		(-  
		 (* (vector-component ?v1 2 ?b) 
		     (vector-component ?v2 3 ?b)) 
		 (* (vector-component ?v2 2 ?b) 
		     (vector-component ?v1 3 ?b)))) 
	     (= (vector-component ?v 2 ?b)		 
		(- 
		 (* (vector-component ?v2 1 ?b) 
		     (vector-component ?v1 3 ?b)) 
		 (* (vector-component ?v1 1 ?b) 
		     (vector-component ?v2 3 ?b)))) 
	     (= (vector-component ?v 3 ?b)		 
		(-  
		 (* (vector-component ?v1 1 ?b) 
		     (vector-component ?v2 2 ?b)) 
		 (* (vector-component ?v2 1 ?b) 
		     (vector-component ?v1 2 ?b)))))))