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

  by (simp add: setsum_shift_bounds_cl_Suc_ivl)

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,

On 16 Jul 2014, at 11:59, Lars Hupel <hupel at> 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
>    Set_Interval.setsum_head_Suc:
>    ?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)"
>  by (auto simp: setsum_head_Suc)
> 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.