*To*: Rustom Mody <rustompmody at gmail.com>*Subject*: Re: [isabelle] Sum of first n integers*From*: Harry Butterworth <heb1001 at gmail.com>*Date*: Wed, 21 Oct 2015 17:31:29 +0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAJ+TeodLCpOG-whbat6BKhV+NOet6HfVOEJyB4Nrb7o7GaQFdQ@mail.gmail.com>*References*: <CAJ+TeofX7WZJ+ubA1dvXs=MNQmGDdr2KzchDHe8bY6p=D6NKSQ@mail.gmail.com> <56272622.1000400@in.tum.de> <CAJ+Teofw1L-vUOe0zU+etRrAopQp+rxUKYmM8FmHG3=-4EbRQg@mail.gmail.com> <CAMUwPhyNFCG97H4OEiMJ3202VycZ-1h_YC5M=7CGBznCN2Gnag@mail.gmail.com> <CAJ+TeodLCpOG-whbat6BKhV+NOet6HfVOEJyB4Nrb7o7GaQFdQ@mail.gmail.com>

Here you go... theory sum imports Main begin theorem fixes n :: nat shows "(\<Sum> i =0.. n . i ) = n * ( n + 1) div 2" proof ( induct n ) case 0 have "(\<Sum> i =0..0. i ) = (0:: nat )" by simp also have "â = 0 * (0 + 1) div 2" by simp finally show ?case . next case ( Suc n ) have "(\<Sum> i =0.. Suc n . i ) = (\<Sum> i =0.. n . i ) + ( n + 1)" by simp also have "â = n * ( n + 1) div 2 + ( n + 1)" by ( simp add : Suc.hyps ) also have "â = ( n * ( n + 1) + 2 * ( n + 1)) div 2" by simp also have "â = ( Suc n * ( Suc n + 1)) div 2" by simp finally show ?case . qed On 21 October 2015 at 17:25, Rustom Mody <rustompmody at gmail.com> wrote: > Thanks Harry > > On Wed, Oct 21, 2015 at 2:11 PM, Harry Butterworth <heb1001 at gmail.com> > wrote: > >> Your star is the wrong star character. Maybe you have cut and pasted >> from a pdf document. That doesn't work. >> >> > Yeah I started with > https://www.lri.fr/~wenzel/Isabelle_Paris_2014/slides.pdf > And was looking for a source/thy version of that... > > >> With the version below... >> >> theory sum >> imports Main >> begin >> >> theorem >> fixes n::nat >> shows "(â i =0.. n . i ) = n * ( n + 1) div 2" >> >> ...I get the output >> >> proof (prove): depth 0 >> >> goal (1 subgoal): >> 1. â{0..n} = n * (n + 1) div 2 >> >> Harry >> > > > My current thy file is attached. > It has about a dozen 'red-marks' :-) > >

**Follow-Ups**:**Re: [isabelle] Sum of first n integers***From:*Rustom Mody

**References**:**[isabelle] Sum of first n integers***From:*Rustom Mody

**Re: [isabelle] Sum of first n integers***From:*Lars Noschinski

**Re: [isabelle] Sum of first n integers***From:*Rustom Mody

**Re: [isabelle] Sum of first n integers***From:*Harry Butterworth

**Re: [isabelle] Sum of first n integers***From:*Rustom Mody

- Previous by Date: Re: [isabelle] Sum of first n integers
- Next by Date: Re: [isabelle] Sum of first n integers
- Previous by Thread: Re: [isabelle] Sum of first n integers
- Next by Thread: Re: [isabelle] Sum of first n integers
- Cl-isabelle-users October 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