Re: [isabelle] Indexed Sum/Product Operator

```Hi Alfio,

in this case the problem is that "∑ A" (named "Setsum") is a special
syntax for "∑x∈A. x" (named "setsum", note that symbol names are
case-sensitive). It is defined in src/HOL/Big_Operators.thy.

To find "Setsum" using find_consts or find_theorem is quiet hard as it
is just a syntax abbreviation and its more general form "∑x∈A. f x" is

Luckily with the jEdit interface for Isabelle this gets much easier as

-Johannes

Am Montag, den 03.12.2012, 22:41 -0200 schrieb Alfio Martini:
> Dear Isabelle Users,
>
> I was playing with the exercise below, and I wanted to find the
> theory where the indexed sum operator is defined.
>
> I tried  find_consts name: Sum, but this does not seem to
> be the way.
>
> Thanks for any help!
>
> theorem sum02: "∑{0..n::nat} = n * (n+1) div 2" (is "?P n")
>   proof (induction n)
>     show "?P 0"
>        proof -
>          have "∑{0..0::nat} = 0" by simp
>          also have "...= 0 * 0" by simp
>          also have "... = 0 * (0 + 1)" by simp
>          also have "... = (0 * (0 + 1)) div 2" by simp
>          finally show ?thesis by this
>        qed
>     next
>       fix x0::nat
>       assume IH: "?P x0"
>       show "?P (Suc x0)"
>         proof -
>             have "∑{0..(Suc x0)} = ∑{0..x0} + Suc x0" by simp
>             also have  "...= ∑{0..x0} + (x0 + 1)" by simp
>             also have  "...= (x0 * (x0 + 1) div 2) + (x0 + 1)" by (simp
> only: IH)
>             also have  "...= (x0 * (x0 + 1) + 2 * x0 + 2) div 2" by simp
>             also have  "...= (x0 * x0 + x0 + 2*x0 + 2) div 2" by simp
>             also have  "...= (x0 * x0 + 3*x0 +2) div 2" by simp
>             also have  "...= (x0 + 1) * (x0 + 2) div 2" by simp
>             also have  "...= Suc x0 * (Suc x0 + 1) div 2" by simp
>             finally show ?thesis by this
>         qed
>   qed
>

```

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