*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Indexed Sum/Product Operator*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 04 Dec 2012 09:01:31 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAPnxw34ziFh_AjQwWN8UKcVeB+OkutvYPpPa8gdiDVZurHPvA@mail.gmail.com>*Organization*: TU München*References*: <CAAPnxw34ziFh_AjQwWN8UKcVeB+OkutvYPpPa8gdiDVZurHPvA@mail.gmail.com>

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 not found when you just search "∑ A". Luckily with the jEdit interface for Isabelle this gets much easier as you can Ctrl-click on the constant and jump to its definition. -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 >

**Follow-Ups**:**Re: [isabelle] Indexed Sum/Product Operator***From:*Makarius

**References**:**[isabelle] Indexed Sum/Product Operator***From:*Alfio Martini

- Previous by Date: [isabelle] Indexed Sum/Product Operator
- Next by Date: Re: [isabelle] nat_code Equation
- Previous by Thread: [isabelle] Indexed Sum/Product Operator
- Next by Thread: Re: [isabelle] Indexed Sum/Product Operator
- Cl-isabelle-users December 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list