*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] newbie questions: theory for sums and Isar syntax*From*: Felix Breuer <felix at fbreuer.de>*Date*: Fri, 18 Jul 2014 20:54:54 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <53C64CE6.1020402@in.tum.de>*References*: <D4D2F234-CE47-49BC-A145-B0D58B8E929E@fbreuer.de> <53C64CE6.1020402@in.tum.de>

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, 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 > 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:*Lars Noschinski

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

**Re: [isabelle] newbie questions: theory for sums and Isar syntax***From:*Lars Hupel

- Previous by Date: [isabelle] CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call)
- Next by Date: [isabelle] new in the AFP: CISC-Kernel
- 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