# Re: [isabelle] newbie questions: theory for sums and Isar syntax

Isabelle supports sums and products over index sets very generally, via axiomatic type classes (allowing just about all kinds of numbers). Index sets can be anything, but there is particular support for intervals of various kinds (over naturals, integers and other ordered types).

For some proofs over summations, see Convex.thy and Formal_Power_Series.thy in HOL/Library/.

Larry Paulson

On 15 Jul 2014, at 14:49, Felix Breuer <felix at fbreuer.de> wrote:

> Hello Isabelle Community!
>
> On Sunday I took my first steps with Isabelle at the very nice and useful Isabelle Tutorial at the Vienna Summer of Logic. Having finished the exercises I am now working on porting a toy proof that I did some time ago using Freek Wiedijk’s miz3 (based on HOL Light) to Isabelle/Isar. In this context, two questions came up:
>
>
> 1) Does Isabelle have a theory for finite sums of numbers?
>
> What is the best way to represent in Isabelle/HOL the sum of all integers from 1 to n or the sum of all integers in a given list? Are there theorems for working with sums available? For example, is the rewrite rule (in mathematical/TeX notation):
>
>   \sum_{i=0}^n a_i = a_0 + \sum_{i=1}^n
>
> proved somewhere in Isabelle’s library? A naive search of the library did not turn up anything.
>
>
> 2) In Isar proofs, is there a way to omit the “by” clause at the end of each statement?
>
> I find that many steps in Isar proofs can be justified by one of the usual suspects (simp, auto, blast, force,…). Is there a way to omit the “by” clause and have Isabelle implicitly try the most common proof methods in some order? miz3 has this feature and it unclutters miz3 proofs considerably.
>
>
> Thanks,
> Felix



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