Isabelle:转置包含常数因子的矩阵 [英] Isabelle: transpose a matrix that includes a constant factor

问题描述

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

In my Isabelle theory I have a matrix with a constant factor:

... 
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))

在我看来，后者应该等同于

In my eyes the latter should be equivalent to

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

由transpose定义.但是这是错误的.我这是什么错误?

by the definition of transpose. But this is not true. What is my error here?

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

By the way, the definition of transposed is:

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

推荐答案

我不确定您的意思是什么:但这不是真的.您所期望的是是正确的，并且可以在Isabelle中得到证明，如下所示:

I'm not sure what you mean by: But this is not true. What you expected is true and can be proven in Isabelle as follows:

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)

这篇关于Isabelle:转置包含常数因子的矩阵的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！