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



Hello Felix,

> 1) Does Isabelle have a theory for finite sums of numbers?

indeed it does:

  term "∑i ∈ {0..n}. f i"

> 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?

The sum of all integers from 1 to n can be written like this:

  term "∑i ∈ {1..n}. i"

(although here, the types of "1", "n" and "i" are polymorphic; so they
can be "int" or "nat" or ...)

You can write the above even shorter:

  term "∑{1..n}"

The underlying constant for sums of sets is called "setsum", and by
analogy, there's also "listsum" to compute the sum of the elements in a
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

Let's state this more generally:

  lemma "k ≤ n ⟹ (∑i ∈ {k..n}. f i) = f k + (∑i ∈ {Suc k..n}. f i)"

Isabelle/jEdit tells us:

  Auto solve_direct: The current goal can be solved directly with
    Set_Interval.setsum_head_Suc:
    ?m ≤ ?n ⟹ setsum ?f {?m..?n} = ?f ?m + setsum ?f {Suc ?m..?n}

Your original rule can be proved like this:

  lemma "0 < (n::nat) ⟹ (∑i ∈ {0..n}. f i) = f 0 + (∑i ∈ {1..n}. f i)"
  by (auto simp: setsum_head_Suc)

For these kinds of things, you might want to try the "find_theorems"
command. For example, the query

  find_theorems "setsum ?f _ = ?f _ + setsum ?f _"

finds the relevant theorem and some more.

Cheers
Lars




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