# Re: [isabelle] newbie questions: theory for sums and Isar syntax

Hi Lars and Larry,

thank you for your help! Just knowing that the right name to search for was “setsum” helped a lot. Just searching for theorems containing “sum” (in the JEdit Query Panel) - as I had done before - finds nothing.

After some more work, I am now thoroughly stuck again, though: I want to prove:

lemma "( ∑ k∈{0..m}. ((f (Suc k)) * (recip f (n - (Suc k)))) ) = ( ∑ k∈{(Suc 0)..(Suc m)}. ((f k) * (recip f (n - k))) )"

Whatever f and recip are, this should follow simply from setsum_shift_bounds_cl_Suc_ivl, which reads:

corollary setsum_shift_bounds_cl_Suc_ivl:
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}”

However, I cannot figure out how to get Isabelle to instantiate the corollary in the right way. When I try to prove the lemma using

I get

Failed to finish proof⌂:
goal (1 subgoal):
1. (∑k = 0..m. f (Suc k) * recip f (n - Suc k)) = (∑k = Suc 0..m. f k * recip f (n - k)) + f (Suc m) * recip f (n - Suc m)

So simp applies a wrong rewrite rule and then gets stuck. Using Sledgehammer to get some hints on how to do it right, only resulted in time outs. So what am I missing?

Thanks again,
Felix

On 16 Jul 2014, at 11:59, Lars Hupel <hupel at in.tum.de> wrote:

> Hello Felix,
>
>> 1) Does Isabelle have a theory for finite sums of numbers?
>
> indeed it does:
>
>  term "∑i ∈ {0..n}. f i"
>
>> What is the best way to represent in Isabelle/HOL the sum of all
>> integers from 1 to n or the sum of all integers in a given list?
>
> The sum of all integers from 1 to n can be written like this:
>
>  term "∑i ∈ {1..n}. i"
>
> (although here, the types of "1", "n" and "i" are polymorphic; so they
> can be "int" or "nat" or ...)
>
> You can write the above even shorter:
>
>  term "∑{1..n}"
>
> The underlying constant for sums of sets is called "setsum", and by
> analogy, there's also "listsum" to compute the sum of the elements in a
> list.
>
>> Are there theorems for working with sums available? For example, is the
>> rewrite rule (in mathematical/TeX notation):
>>
>> \sum_{i=0}^n a_i = a_0 + \sum_{i=1}^n
>
> Let's state this more generally:
>
>  lemma "k ≤ n ⟹ (∑i ∈ {k..n}. f i) = f k + (∑i ∈ {Suc k..n}. f i)"
>
> Isabelle/jEdit tells us:
>
>  Auto solve_direct: The current goal can be solved directly with
>    ?m ≤ ?n ⟹ setsum ?f {?m..?n} = ?f ?m + setsum ?f {Suc ?m..?n}
>
> Your original rule can be proved like this:
>
>  lemma "0 < (n::nat) ⟹ (∑i ∈ {0..n}. f i) = f 0 + (∑i ∈ {1..n}. f i)"
>
> For these kinds of things, you might want to try the "find_theorems"
> command. For example, the query
>
>  find_theorems "setsum ?f _ = ?f _ + setsum ?f _"
>
> finds the relevant theorem and some more.
>
> Cheers
> Lars



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.