Матричная арифметика Изабель: det_linear_row_setsum в библиотеке с другой системой обозначений

Question

Недавно я начал использовать доказатель теоремы Изабель. Поскольку я хочу доказать другую лемму, я хотел бы использовать нотацию, отличную от той, которая используется в лемме "det_linear_row_setsum", которую можно найти в библиотеке HOL. Более конкретно, я хотел бы использовать "обозначение χ i j" вместо "χ i". Я пытался сформулировать эквивалентное выражение в течение некоторого времени, но пока не мог понять.

(* ORIGINAL lemma from library *)
(* from HOL/Multivariate_Analysis/Determinants.thy *)
lemma det_linear_row_setsum:
  assumes fS: "finite S"
  shows "det ((χ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (λj. det ((χ i. if i = k then a  i j else c i)::'a^'n^'n)) S"
proof(induct rule: finite_induct[OF fS])
  case 1 thus ?case apply simp  unfolding setsum_empty det_row_0[of k] ..
next
  case (2 x F)
  then  show ?case by (simp add: det_row_add cong del: if_weak_cong)
qed

..

(* My approach to rewrite the above lemma in χ i j matrix notation *)
lemma mydet_linear_row_setsum:
  assumes fS: "finite S"
  fixes A :: "'a::comm_ring_1^'n^'n" and k :: "'n"  and vec1 :: "'vec1 ⇒ ('a, 'n) vec"
  shows "det ( χ r c . if r = k then (setsum (λj .vec1 j $ c) S) else A $ r $ c ) =
    (setsum (λj . (det( χ r c . if r = k then vec1 j $ c else A $ r $ c ))) S)" 
proof-
  show ?thesis sorry
qed

Answer 1

Во-первых, проясните, что говорится в оригинальной лемме: a это семейство векторов, проиндексированных i а также j, c это семейство векторов, проиндексированных i, k-я строка матрицы слева является суммой векторов a k j охватил все j из набора S, Другие строки взяты из c, Справа матрицы такие же, кроме этой строки k сейчас a k j и j связан во внешней сумме.

Как вы уже поняли, семейство векторов a используется только для индекса i = k, так что вы можете заменить a от %_ j. vec1 $ j, Ваша матрица A дает семейство строк, т. е. c становится %r. A $ r, Тогда вам просто нужно использовать это (χ n. x $ n) = x (теорема vec_nth_inverse) и нажмите $ сквозь if а также setsum, Результат выглядит следующим образом:

lemma mydet_linear_row_setsum:
  assumes fS: "finite S"
  fixes A :: "'a::comm_ring_1^'n^'n" and k :: "'n" and vec1 :: "'vec1 => 'a^'n"
  shows "det (χ r c . if r = k then setsum (%j. vec1 j $ c) S else A $ r $ c) =
    (setsum (%j. (det(χ r c . if r = k then vec1 j $ c else A $ r $ c))) S)"

Чтобы доказать это, вам просто нужно отменить расширение и проталкивание лемм if_distrib, cond_application_beta, а также setsum_component может помочь вам в этом.