Re: [isabelle] Sum of first n integers



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'  :-)

Attachment: sum.thy
Description: Binary data



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