*To*: Hauser Bruno <bhauser at student.ethz.ch>*Subject*: Re: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 09 Dec 2008 15:48:49 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <B902E52AFFC79B4CAD0A9A6F0134AA5717910F@EX6.d.ethz.ch>*References*: <B902E52AFFC79B4CAD0A9A6F0134AA5717910F@EX6.d.ethz.ch>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Here is a direct proof, without preconditions: lemma "(i - (1::int)) * i div 2 + i = i * (i + 1) div 2"

apply(simp add: ring_simps) apply arith done Regards Tobias Hauser Bruno wrote:

Hi I want to prove the following lemma: ((i - (1::int)) * i div 2) + i = i * (i + 1) div 2. Proving the property for naturals succeeds. I now want to proof it for positive, nonzero integers. Trying to solve the lemma (i_equation_int) automatically with sledgehammer did not succeed. So, no "trivial" solution seems to exist yet. lemma i_equation_int: "[|(n - (1::nat)) * n div 2 + n = n * (n + 1) div 2; int n = i; i > 0|] ==> ((i - (1::int)) * i div 2) + i = i * (i + 1) div 2" Can someone give me a hint how to proof it by (maybe) using the facts, that i > 0 and the equation holds for naturals? Is there a general way for proofing lemmas like: (i>0) & (int n = i) & P(n) ==> P(i) ? Thank you, Bruno Hauser

**References**:**[isabelle] (i>0) & (int n = i) & P(n) ==> P(i)***From:*Hauser Bruno

- Previous by Date: Re: [isabelle] Isabelle and Beamer
- Next by Date: Re: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)
- Previous by Thread: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)
- Next by Thread: Re: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)
- Cl-isabelle-users December 2008 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