*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 16:41:10 +0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAJ+Teofw1L-vUOe0zU+etRrAopQp+rxUKYmM8FmHG3=-4EbRQg@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>

Your star is the wrong star character. Maybe you have cut and pasted from a pdf document. That doesn't work. 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 On 21 October 2015 at 14:55, Rustom Mody <rustompmody at gmail.com> wrote: > Thanks Lars! > > On Wed, Oct 21, 2015 at 11:14 AM, Lars Noschinski <noschinl at in.tum.de> > wrote: > > > On 21.10.2015 06:06, Rustom Mody wrote: > > > In paper https://www.lri.fr/~wenzel/Isabelle_Paris_2014/slides.pdf > > > there is the example of sum of first n integers. > > > > > > Quite stuck at 'outer/inner' syntax errors. > > > Is there somewhere I can find the full example so that I can study it? > > > > It is customary to omit the quotation marks ("), when type-setting > > Isabelle theories -- these need to surround every (non-atomic) > > expression of the inner syntax. > > > > Maybe so > But I think I am stuck on something much more preliminary > > The example starts with > > theorem > fixes "n :: nat" > shows "(â i =0.. n . i ) = n â ( n + 1) div 2" > etc > > [assuming that's how the quotes should be put > > But it looks that Isabelle (or should I be saying Isar?) wants some prefix > like > > theory sum > imports Main > begin > > which gives the following at theorem > > Outer syntax errorâ: proposition expected, > but keyword (â was found > > > > > Refering to slide 24 of the above document, "inner syntax" is everything > > printed in cursive, except the proofs (which are proceeded by "by"). > > > > For starting, I would recommend to look at "Programming and Proving in > > Isabelle/HOL". > > > > > > > > Also: > > > Spent some hours figuring out what is 'sorry' > > > Which manual answers such questions? > > > > The Isabelle/Isar Reference Manual (look at the index at the end of the > > document). Be warned that this is a reference manual -- if you do not > > already understand how the system works, many explanations are hard to > > understand. > > > > > Finally if there is a more noob-list than this one please let me know! > > > > No, this is the right list. > > > > Good to know! > > -- > http://www.the-magus.in > http://blog.languager.org >

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

- 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