*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)*From*: "W. Douglas Maurer" <maurer at gwu.edu>*Date*: Wed, 22 Apr 2015 20:29:00 -0400*Cc*: maurer at gwu.edu*In-reply-to*: <mailman.39335.1429716197.13101.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.39335.1429716197.13101.cl-isabelle-users@lists.cam.ac.uk>

On 22 Apr 2015, Alfio Martini <alfio.martini at acm.org> wrote:

While trying to prove the correctness of a simple function that returns the sum of the values between integers l and u, I stumbled upon an unexpected problem: I was not able to prove that (Sum k=l..(u+1). k) = (u+1) + (Sum k=l...u) if l<u+1, which should hold by the definition of an indexed sum.

I asked this question on March 6th, 2015, in the following more general form:

I am having problems with forward proofs by induction. I would likefor Isar to be able to prove that 1+4+9+...+n*n =(n*(n+1)*(2*n+1))/6 and the like. In order to do the inductiveproof, I have to know that m<=n implies (f(m)+f(m+1)+...+f(n+1)) =(f(m)+f(m+1)+...+f(n))+f(n+1), for integers m and n. In Isar, thisbecomes that m<=n implies (setsum f {m..n+1} = (setsum f {m..n}) +f(n+1)). This would seem to be a fundamental rule, and yet I cannotseem to find it anywhere in either the library or the supplementallibrary.

There are far fewer theorems about setsum over intervals of integersthan over natural numbers. Still, there are enough theorems in thelibrary to prove what you want. Sledgehammer finds the followingproof for me:lemma "m ? n ? setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 :: int)" by(metis add.commute atLeastAtMostPlus1_int_conv atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_ifffinite_atLeastAtMost_int linear not_less setsum.insertzle_add1_eq_le)Hope this helps, Andreas

This appeared in Cl-isabelle-users Digest, Vol 117, Issue 10, #7. -- Prof. W. Douglas Maurer Washington, DC 20052, USA Department of Computer Science Tel. (1-202)994-5921 The George Washington University Fax (1-202)994-4875

- Previous by Date: Re: [isabelle] Difficulties with "setsum"
- Next by Date: Re: [isabelle] Isabelle2015-RC1: Rule instantiation in Eisbach
- Previous by Thread: [isabelle] function package: tactic failed
- Next by Thread: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- Cl-isabelle-users April 2015 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