Isabelle: difference between A * 1 and A ** mat 1

问题:

What is the difference between * and ** for matrices and also A * 1andA ** mat 1`?

Example:

lemma myexample:
  fixes A :: "('a::comm_ring_1)^'n∷finite^'n∷finite"
  shows "(A * 1 = A) ∧ (A ** (mat 1) = A)" 
 by (metis comm_semiring_1_class.normalizing_semiring_rules(12) matrix_mul_rid)

回答1:

Matrices in Isabelle are defined simply as vectors of vectors, so the * on matrices is inherited from vectors, and * on vectors is just componentwise multiplication. Therefore, you have (A*B) $ i $ j = A $ i $ j * B $ i $ j, i.e. * is entry-by-entry multiplication of a matrix. Whether this is actually useful anywhere, I do not know – I don't think so. It's probably just an artifact of defining matrices as vectors of vectors. It might have been better to do a proper typedef for matrices and define * as the right matrix multiplication on them, but there must have been some reason why that was not done – maybe just because it's more work and a lot of copypasted code.

** is the proper matrix multiplication. mat x is simply the matrix that has x on its diagonal and 0 everywhere else, so of course, mat 1 is the identity matrix and A ** mat 1 = A.

The matrix 1 however is, again, an artifact from the vector definition; the n-dimensional vector 1 is simply defined as the vector that has n components, all of which are 1. Consequently, the matrix 1 is the matrix whose entries are all 1, and then of course, A * 1 = A. This does not seem useful to me in any way.