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

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.


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