Re: [isabelle] Difficulties with "setsum"

Hi Alfio,

Your sorry can be proved by:

  also have "... = (â k=l..i+1. k)"
    proof -
      have "{l..i + 1} = insert (i+1) {l..i}" using hip02 by auto
      thus ?thesis by simp

Also note, goals like this:

lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3"

if both sides can be evaluated to the same value, you can discharge the goal by "eval".


On 2015-04-22 17:24, Alfio Martini wrote:

I think that the main problem is that the automatic methods cannot cope
with following trivial
lemmas, although both sides evaluate correctly with the command 'value',

value "(setsum id {1::int..2}) + (3::int)"
value "(setsum id {1::int..3})"
lemma "(setsum id {1::int..3}) = (setsum id {1..2}) + 3" oops
value "(setsum id {-3::int..3})"
value "(setsum id {-3::int..2}) + 3"
lemma "(setsum id {-3::int..3}) = (setsum id {-3..2}) + 3" oops

I tried sledgehammer but it does not find anything. Anyway, the last time
sledgehammer worked
fine for me was with Isabelle 2012.


On Wed, Apr 22, 2015 at 12:00 PM, Manuel Eberl <eberlm at> wrote:

The problem is that in order to "unroll" the setsum, you first have to
bring the numerals (e.g. 2, 3, 4) into successor notation. One way to do
this is to add eval_nat_numeral to your simpset, e.g.

apply (auto simp: eval_nat_numeral)

Most of your example work automatically with these, but you will have to massage expressions like "(â k::nat â {j. 1âj â jâ3}. k)" by hand a bit
first, e.g. by proving that "{j. 1âj â jâ3} = {1..3}".

One could easily write simplification rules that unroll setsums over
constant intervals like these automatically or even write a simproc that
does that, but I don't think that would be very helpful in practice.



On 22/04/15 16:46, Alfio Martini wrote:

Dear Isabelle Users,

While trying to prove the correctness of a simple function that returns
the sum of the values between integers  l and u, I stumbled upon
an unexpected problem: I was ano able to prove that

(Sum k=l..(u+1). k) = (u+1) + (Sum k=l...u) if l<u+1, which should
hold by the  definition of an indexed sum.

My thy file is attached and, in the proof, is the only line with "sorry".
I would very grateful if anyone could take a quick look at that.

To get a better feeling of what are the underlying simplification rules, I performed some tests with setsum, but the results were disappointing.
(see below).

Besides, acoording to "What is is Main", setsum is defined in
but in Isabelle 2014 it is defined  in "Groups_Big".

(* Testing the setsum function                            *)
fun i2n::"int â nat" where
"i2n x = (if x â 0 then 0 else Suc (i2n (x - 1)))"

value  "int (setsum id {1::nat..5})" (* this works *)
lemma  "setsum id {1::nat..2} = (Suc (Suc (Suc 0)))"
    apply (auto) oops
lemma "setsum id {1::nat..5}= i2n 15"
     apply (auto) oops
lemma  "(setsum id {1::nat..2})= Suc (Suc (Suc 0))"
     apply (auto) oops
lemma  "(â k::nat â {j. 1âj â jâ3}. k) = 6"
      apply  oops
lemma  "(â k::nat | kâ1 â kâ2 . k) = Suc (Suc (Suc 0))"
    apply (auto) oops
lemma "(â k::nat=1..3. k)= (â k=1..2. k) + 3" oops
term "â k=1..n. k"
value "â k::nat = 2 ..1. k" (* this works *)
(*  end of test                                            *)

All the Best!

Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

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