*To*: "W. Douglas Maurer" <maurer at gwu.edu>*Subject*: Re: [isabelle] Forward inductive proofs*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 6 Mar 2015 08:23:46 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <a06200776d11d1ddd8838@[192.168.1.20]>*References*: <a06200751d10980831257@[192.168.1.20]> <54E431C4.4090708@inf.ethz.ch> <a06200755d10a772bc6da@[192.168.1.20]> <54E4CFE2.8020207@inf.ethz.ch> <a06200756d10aa5699d51@[192.168.1.20]> <54E58E70.2040501@inf.ethz.ch> <a06200757d10bc1679a18@[192.168.1.20]> <54E6182D.6080505@inf.ethz.ch> <a0620075ad10d0f36ad42@[192.168.1.20]> <54EAD274.6000702@inf.ethz.ch> <a06200764d112b21330ce@[192.168.1.20]> <54ED7440.9050304@inf.ethz.ch> <a06200776d11d1ddd8838@[192.168.1.20]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0

setsum_op_ivl_Suc setsum_head_upt_Suc setsum_head_Suc setsum_cl_ivl_Suc Best, Andreas

On 05/03/15 21:30, W. Douglas Maurer wrote:

Thank you again for helping me with forward proofs by contradiction. I have now gotten one of those to work, as well as a forward proof by cases. Now I am starting on forward proofs by induction. I would like for 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 inductive proof, 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, this becomes 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 cannot seem to find it anywhere in either the library or the supplemental library. The closest I have come to it is a lemma called setsum_atMost_Suc in section 59.8 (Summation Indexed over Intervals) of the library. This says that (SUM i<=Suc n. f i) = (SUM i<=n. f i)+f(Suc n), where SUM represents the upper-case sigma. It works for m = 0, but not in the general case; and not every induction with an integer index starts with 0. How do I get this to work? Thanks! -WDMaurer -- 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: [isabelle] ACL2 2015 - Call for papers
- Next by Date: [isabelle] Forward proofs by induction
- Previous by Thread: [isabelle] ACL2 2015 - Call for papers
- Next by Thread: [isabelle] Forward proofs by induction
- Cl-isabelle-users March 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