Function SIMPLE-ROTATION


Slots on this function:

Documentation:
Shorthand for the commonly used direction cosine matrices that represent rotations about the three axes in 3D space.
Instance-Of: Function
Arity: 3

Equivalence Axioms:

(<=> (Simple-Rotation ?Axis ?Angle)
     (And (Member ?Axis (Setof 1 2 3))
          (Scalar-Quantity ?Angle)
          (Quantity.Dimension ?Angle Identity-Dimension)
          (3d-Direction-Cosine ?Dircos)
          (=> (= ?Axis 1)
              (= ?Dircos
                 (Matrix-Of-Rows (Matrix-Of-Columns 1 0 0)
                                 (Matrix-Of-Columns 0
                                                    (Cos ?Angle)
                                                    (- (Sin ?Angle)))
                                 (Matrix-Of-Columns 0
                                                    (Sin ?Angle)
                                                    (Cos ?Angle)))))
          (=> (= ?Axis 2)
              (= ?Dircos
                 (Matrix-Of-Rows (Matrix-Of-Columns (Cos ?Angle)
                                                    0
                                                    (- (Sin ?Angle)))
                                 (Matrix-Of-Columns 0 1 0)
                                 (Matrix-Of-Columns (Sin ?Angle)
                                                    0
                                                    (Cos ?Angle)))))
          (=> (= ?Axis 3)
              (= ?Dircos
                 (Matrix-Of-Rows (Matrix-Of-Columns (Cos ?Angle)
                                                    (- (Sin ?Angle))
                                                    0)
                                 (Matrix-Of-Columns (Sin ?Angle)
                                                    (Cos ?Angle)
                                                    0)
                                 (Matrix-Of-Columns 0 0 1))))))


Axioms:

(Nth-Domain Simple-Rotation 3 3d-Direction-Cosine)

(Nth-Domain Simple-Rotation 2 Scalar-Quantity)


Other Related Axioms:

(=> (= (Simple-Rotation ?Axis ?Angle) ?Dircos)
    (=> (= ?Axis 3)
        (= ?Dircos
           (Matrix-Of-Rows (Matrix-Of-Columns (Cos ?Angle)
                                              (- (Sin ?Angle))
                                              0)
                           (Matrix-Of-Columns (Sin ?Angle)
                                              (Cos ?Angle)
                                              0)
                           (Matrix-Of-Columns 0 0 1)))))

(=> (= (Simple-Rotation ?Axis ?Angle) ?Dircos)
    (=> (= ?Axis 2)
        (= ?Dircos
           (Matrix-Of-Rows (Matrix-Of-Columns (Cos ?Angle)
                                              0
                                              (- (Sin ?Angle)))
                           (Matrix-Of-Columns 0 1 0)
                           (Matrix-Of-Columns (Sin ?Angle)
                                              0
                                              (Cos ?Angle))))))

(=> (= (Simple-Rotation ?Axis ?Angle) ?Dircos)
    (=> (= ?Axis 1)
        (= ?Dircos
           (Matrix-Of-Rows (Matrix-Of-Columns 1 0 0)
                           (Matrix-Of-Columns 0
                                              (Cos ?Angle)
                                              (- (Sin ?Angle)))
                           (Matrix-Of-Columns 0
                                              (Sin ?Angle)
                                              (Cos ?Angle))))))

(=> (= (Simple-Rotation ?Axis ?Angle) ?Dircos)
    (3d-Direction-Cosine ?Dircos))

(=> (= (Simple-Rotation ?Axis ?Angle) ?Dircos)
    (Quantity.Dimension ?Angle Identity-Dimension))

(=> (= (Simple-Rotation ?Axis ?Angle) ?Dircos)
    (Scalar-Quantity ?Angle))

(=> (= (Simple-Rotation ?Axis ?Angle) ?Dircos)
    (Member ?Axis (Setof 1 2 3)))