*To*: Felix Breuer <felix at fbreuer.de>*Subject*: Re: [isabelle] newbie questions: theory for sums and Isar syntax*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 16 Jul 2014 11:51:31 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <D4D2F234-CE47-49BC-A145-B0D58B8E929E@fbreuer.de>*References*: <D4D2F234-CE47-49BC-A145-B0D58B8E929E@fbreuer.de>

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

**References**:**[isabelle] newbie questions: theory for sums and Isar syntax***From:*Felix Breuer

- Previous by Date: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Next by Date: Re: [isabelle] newbie questions: theory for sums and Isar syntax
- Previous by Thread: [isabelle] newbie questions: theory for sums and Isar syntax
- Next by Thread: Re: [isabelle] newbie questions: theory for sums and Isar syntax
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list