isabelle - Isabelle: A * 1 と A ** mat 1 の違い

Question

*行列の場合と**A * 1 andA ** mat 1`の違いは何ですか?

例：

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)

Answer 1

Isabelle の行列は単純にベクトルのベクトルとして定義されているため、*on 行列はベクトルから継承され、*on ベクトルは成分ごとの乗算です。(A*B) $ i $ j = A $ i $ j * B $ i $ jつまり、*行列のエントリごとの乗算です。これが実際にどこでも役立つかどうかはわかりませんが、そうは思いません。これはおそらく、行列をベクトルのベクトルとして定義した結果にすぎません。行列に対して適切な typedef を実行し、適切な行列乗算として定義する方がよかったかもしれませんが、*それが行われなかったのには何らかの理由があったに違いありません。おそらく、より多くの作業とコピーペーストされたコードが多いためです。

**は適切な行列の乗算です。mat xはx、対角線上と0それ以外の場所に がある行列です。もちろん、mat 1は恒等行列 とA ** mat 1 = Aです。

ただし、この行列1も、ベクトル定義からのアーティファクトです。n 次元ベクトル1は、n 個の成分を持つベクトルとして単純に定義され、そのすべてが1です。したがって、行列1はエントリがすべて1である行列であり、もちろん ですA * 1 = A。これは私には何の役にも立たないようです。