Isabelle: transpose a matrix that includes a const

问题:

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)

I can calculate the transposed matrix:

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

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

回答1:

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)