*To*: Felix Breuer <felix at fbreuer.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] newbie questions: theory for sums and Isar syntax*From*: Lars Hupel <hupel at in.tum.de>*Date*: Wed, 16 Jul 2014 11:59:02 +0200*In-reply-to*: <D4D2F234-CE47-49BC-A145-B0D58B8E929E@fbreuer.de>*References*: <D4D2F234-CE47-49BC-A145-B0D58B8E929E@fbreuer.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

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

**Follow-Ups**:**Re: [isabelle] newbie questions: theory for sums and Isar syntax***From:*Felix Breuer

**References**:**[isabelle] newbie questions: theory for sums and Isar syntax***From:*Felix Breuer

- Previous by Date: Re: [isabelle] newbie questions: theory for sums and Isar syntax
- Next by Date: [isabelle] Isabelle2014-RC0: Computations with rational numbers
- Previous by Thread: Re: [isabelle] newbie questions: theory for sums and Isar syntax
- Next by Thread: Re: [isabelle] newbie questions: theory for sums and Isar syntax
- Cl-isabelle-users July 2014 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