isabelle - 伊莎贝尔：总和中的如果语句

Question

我对总和中的 if 语句有疑问。

我在另一个关于isabelle 中的 if 语句的问题中检查了解决方案， 但它没有帮助。

这是一个例子：

theorem dummy:
  fixes a :: "('a::comm_ring_1 poly)" 
    and B :: "(('a::comm_ring_1 poly)^'n∷finite^'n∷finite)"
  shows "1=1"
proof-
  { fix i j
   have "(∑k∈UNIV. if i = k then (B $ i $ j) else 0) = B $ i $ j" sorry
  }

我如何证明“对不起”所在的引理？

Answer 1

您正在寻找的定理是setsum_delta：

finite ?S ⟹
(∑k∈?S. if k = ?a then ?b k else 0) =
    (if ?a ∈ ?S then ?b ?a else 0)

如果你写k = i而不是i = k你的总和，它甚至可以自动解决：

have "(∑k∈UNIV. if k = i then (B $ i $ j) else 0) = B $ i $ j" 
    by (simp add: setsum_delta)

该find_theorems命令对此非常有用。如果你输入

find_theorems "∑_∈_. if _ then _ else _"

你得到setsum_delta了匹配之一——这就是我找到它的方式。