Re: [isabelle] Sum of first n integers



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
>



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