Арифметика матрицы Isabelle: 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 используется только для индекса , так что вы можете заменить 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 может помочь вам в этом.