CODEWITHSUNDEEP
isabelle
mrsteve
mrsteve

Reputation: 4132

Isabelle: If statement inside a sum

I have a problem with an if-statement within a sum.

I checked the solution in another question on if statements in isabelle but it did not help.

Here is an example:

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
  }

How can I prove the lemma where the "sorry" is?

Upvotes: 0

Views: 193

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8248

The theorem you are looking for is setsum_delta:

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

If you write k = i instead of i = k in your sum, it can even be solved automatically:

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

The find_theorems command is very useful for this. If you type

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

You get setsum_delta as one of the matches – that's how I found it.

Upvotes: 2

Related Questions