Изабель: транспонировать матрицу, включающую постоянный множитель

В моей теории Изабель у меня есть матрица с постоянным множителем:

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

matrix theorem-proving isabelle
person mrsteve    schedule 30.05.2013    source источник
comment
Какую матричную теорию вы используете?   -  person chris    schedule 30.05.2013
comment
Нашел! Один из HOL-Multivariate_Analysis, верно?   -  person chris    schedule 30.05.2013
comment
Я работал до 6 утра (Европа), чтобы найти свою проблему, потом написал вопрос и лег спать.   -  person mrsteve    schedule 30.05.2013

Ответы (1)


arrow_upward
1
arrow_downward

Я не совсем понимаю, что вы имеете в виду под: Но это неправда. То, что вы ожидали, верно верно и может быть доказано в Изабель следующим образом:

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)
person chris    schedule 30.05.2013
comment
большое спасибо. В самом деле! Я не изложил прямо лемму, которую вы написали в своем ответе. С ним теперь работает мой шаг сокращения в доказательстве Изара. Я подумал, что для моего шага сокращения будет достаточно некоторой эвристики автоматического доказательства, и попытался просто указать unfolding transpose_def в моем шаге сокращения. еще раз спасибо! - person mrsteve; 30.05.2013
comment
unfolding на самом деле просто переписывает заданные уравнения слева направо. Он никогда не может завершить доказательство. - person Lars Noschinski; 07.06.2013