[isabelle] Difficulties with "setsum"

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 "Finite_Set",
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!

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil

Attachment: SumInt.thy
Description: Binary data

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