Re: [isabelle] Sum of first n integers



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



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