matrix - Isabelle：转置包含常数因子的矩阵

Question

在我的伊莎贝尔理论中，我有一个具有常数因子的矩阵：

... 
k :: 'n and c :: 'a
(χ i j. if j = k then c * (A $ i $ j) else A $ i $ j)

我可以计算转置矩阵：

(transpose (χ i j. if j = k then c * (A $ i $ j) else A $ i $ j))

在我看来，后者应该相当于

(χ i j. if i = k then c * (A $ j $ i) else A $ j $ i))

根据 的定义transpose。但是这是错误的。我的错误是什么？

顺便说一下，转置的定义是：

definition transpose where 
  "(transpose::'a^'n^'m ⇒ 'a^'m^'n) A = (χ i j. ((A$j)$i))"

Answer 1

我不确定你的意思：但这不是真的。您所期望的是正确的，并且可以在 Isabelle 中证明如下：

lemma "transpose (χ i j. if j = k then c * (A $ i $ j) else A $ i $ j) =
  (χ i j. if i = k then c * (A $ j $ i) else A $ j $ i)"
  by (simp add: transpose_def)