Re: [isabelle] Forward inductive proofs

Use the Query panel to search for theorems. For example, searching for setsum and Suc returns several theorems that match your needs:



PS: You should direct your questions not privately to me but to the mailing lists such that other people also have a chance to answer and profit from the answers themselves.

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!
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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.