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.