Class MATRIX

Slots on this class:

Documentation:
A matrix is a binary function mapping pairs of integers (its indices) to some value. It is total for integers from 1 to some constant bound, for its row and column indices. Each matrix has a row and a column dimension
Instance-Of: Class
Subclass-Of: Function
Domain-Of: Column-dimension, Row-dimension, Transpose
Range-Of: Matrix-of-columns, Matrix-of-rows, Transpose
Superclass-Of:
Column-matrix, Diagonal-matrix, Row-matrix, Square-matrix

Slots on instances of this class:

Arity: 3
Column-Dimension:
Slot-Cardinality: 1
Slot-Value-Type: Positive-integer
Row-Dimension:
Slot-Cardinality: 1
Slot-Value-Type: Positive-integer

Implication Axioms:

(=> (And (Positive-Integer ?I)
         (Positive-Integer ?J)
         (=< ?I (Row-Dimension ?M))
         (=< ?J (Column-Dimension ?M)))
    (Defined (Value ?M ?I ?J)))

Equivalence Axioms:

(<=> (Matrix ?M)
     (And (Function ?M)
          (= (Arity ?M) 3)
          (Value-Type ?M Row-Dimension Positive-Integer)
          (Value-Cardinality ?M Row-Dimension 1)
          (Value-Type ?M Column-Dimension Positive-Integer)
          (Value-Cardinality ?M Column-Dimension 1)
          (=> (And (Positive-Integer ?I)
                   (Positive-Integer ?J)
                   (=< ?I (Row-Dimension ?M))
                   (=< ?J (Column-Dimension ?M)))
              (Defined (Value ?M ?I ?J)))))

Axioms:

(Function ?M)

Other Related Axioms:

(<= (Arity $X 3) (Matrix $X))

(<=> (Matrix ?M)
     (And (Function ?M)
          (= (Arity ?M) 3)
          (Value-Type ?M Row-Dimension Positive-Integer)
          (Value-Cardinality ?M Row-Dimension 1)
          (Value-Type ?M Column-Dimension Positive-Integer)
          (Value-Cardinality ?M Column-Dimension 1)
          (=> (And (Positive-Integer ?I)
                   (Positive-Integer ?J)
                   (=< ?I (Row-Dimension ?M))
                   (=< ?J (Column-Dimension ?M)))
              (Defined (Value ?M ?I ?J)))))

(=> (Row-Dimension $X $Y) (Matrix $X))

(=> (Column-Dimension $X $Y) (Matrix $X))

(<=> (Row-Matrix ?M) (And (Matrix ?M) (= (Row-Dimension ?M) 1)))

(<=> (Column-Matrix ?M)
     (And (Matrix ?M) (= (Column-Dimension ?M) 1)))

(=> (Matrix-Of-Rows $X $Y) (Matrix $Y))

(=> (= (Matrix-Of-Rows @Elements) ?M) (Matrix ?M))

(=> (Matrix-Of-Columns $X $Y) (Matrix $Y))

(=> (= (Matrix-Of-Columns @Elements) ?M) (Matrix ?M))

(=> (Transpose $X $Y) (Matrix $Y))

(=> (Transpose $X $Y) (Matrix $X))

(=> (= (Transpose ?A) ?B) (Matrix ?B))

(=> (= (Transpose ?A) ?B) (Matrix ?A))

(Nth-Domain Row 1 Matrix)

(=> (= (Row ?M ?I) ?L) (Matrix ?M))

(Nth-Domain Column 1 Matrix)

(=> (= (Column ?M ?I) ?L) (Matrix ?M))

(<=> (Square-Matrix ?M)
     (And (Matrix ?M)
          (Same-Values ?M Column-Dimension Row-Dimension)))

(<=> (Diagonal-Matrix ?M)
     (And (Matrix ?M)
          (Square-Matrix ?M)
          (Forall (?I ?J)
                  (=> (And (Defined (Value ?M ?I ?J)) (/= ?I ?J))
                      (Zero-Element (Value ?M ?I ?J))))))

(=> (And (Matrix ?A)
         (Matrix ?B)
         (= (Column-Dimension ?A) (Row-Dimension ?B)))
    (<=> (* ?A ?B ?C)
         (And (Matrix ?C)
              (= (Row-Dimension ?A) (Row-Dimension ?C))
              (= (Column-Dimension ?B) (Column-Dimension ?C))
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J)
                             (Summation (Lambda (?K)
                                                (* (Value ?A ?I ?K)
                                                   (Value ?B ?K ?J)))
                                        1
                                        (Column-Dimension ?A))))))))

(=> (And (Matrix ?A)
         (Matrix ?B)
         (= (Row-Dimension ?A) (Row-Dimension ?B))
         (= (Column-Dimension ?A) (Column-Dimension ?B)))
    (<=> (+ ?A ?B ?C)
         (And (Matrix ?C)
              (= (Row-Dimension ?A) (Row-Dimension ?C))
              (= (Column-Dimension ?A) (Column-Dimension ?C))
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J)
                             (+ (Value ?A ?I ?J) (Value ?B ?I ?J))))))))

(=> (Matrix ?A)
    (<=> (- ?A ?C)
         (And (Matrix ?C)
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J) (- (Value ?A ?I ?J))))))))

(=> (And (Matrix ?A)
         (Matrix ?B)
         (= (Row-Dimension ?A) (Row-Dimension ?B))
         (= (Column-Dimension ?A) (Column-Dimension ?B)))
    (<=> (- ?A ?B ?C)
         (And (Matrix ?C)
              (= (Row-Dimension ?A) (Row-Dimension ?C))
              (= (Column-Dimension ?A) (Column-Dimension ?C))
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J)
                             (- (Value ?A ?I ?J) (Value ?B ?I ?J))))))))

(Nth-Domain Matrix-Less-Row-And-Column 4 Matrix)

(Nth-Domain Matrix-Less-Row-And-Column 1 Matrix)

(=> (= (Matrix-Less-Row-And-Column ?A ?I ?J) ?B) (Matrix ?B))

(=> (= (Matrix-Less-Row-And-Column ?A ?I ?J) ?B) (Matrix ?A))

(Nth-Domain Matrix-Less-Row 3 Matrix)

(Nth-Domain Matrix-Less-Row 1 Matrix)

(=> (= (Matrix-Less-Row ?A ?I) ?B) (Matrix ?B))

(=> (= (Matrix-Less-Row ?A ?I) ?B) (Matrix ?A))

(Nth-Domain Matrix-Less-Column 3 Matrix)

(Nth-Domain Matrix-Less-Column 1 Matrix)

(=> (= (Matrix-Less-Column ?A ?I) ?B) (Matrix ?B))

(=> (= (Matrix-Less-Column ?A ?I) ?B) (Matrix ?A))