Isabelle矩阵算法:不同符号的库中的det_linear_row_setsum

Question

我最近开始使用Isabelle定理证明器。因为我想证明另一个引理，所以我想使用与引理"det_linear_row_setsum“中使用的不同的符号，它可以在HOL库中找到。更具体地说，我想使用"χi j notation“而不是"χ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-th行是集合S中所有j上排列的向量a k j的总和。其他行取自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可能会帮助您做到这一点。