Isabelle matrix arithmetic: det_linear_row_setsum in library with different notation

Question

I recently started using the Isabelle theorem prover. As I want to prove another lemma, I would like to use a different notation than the one used in the lemma "det_linear_row_setsum", which can be found in the HOL library. More specifically, I would like to use the "χ i j notation" instead of "χ i". I have been trying to formulate an equivalent expression for some time, but couldn't figure it out yet.

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

First, make yourself clear what the original lemma says: a is a family of vectors indexed by i and j, c is a family of vectors indexed by i. The k-th row of the matrix on the left is the sum of the vectors a k j ranged over all j from the set S. The other rows are taken from c. On the right, the matrices are the same except that row k is now a k j and the j is bound in the outer sum.

As you have realised, the family of vectors a is only used for the index i = k, so you can replace a by %_ j. vec1 $ j. Your matrix A yields the family of rows, i.e., c becomes %r. A $ r. Then, you merely have to exploit that (χ n. x $ n) = x (theorem vec_nth_inverse) and push the $ through the if and setsum. The result looks as follows:

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

To prove this, you just have to undo the expansion and the pushing through, the lemmas if_distrib, cond_application_beta, and setsum_component might help you in doing so.