Re: [isabelle] Sum of first n integers



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.