# [isabelle] Proving with Indexed Sums

```Dear  Isabelle Users,

I wonder if there is a better way to express the summations below in
Isabelle/HOL/Isar (I might think
there is).

In particular, I do not get why the first two theorems express the subgoals
in term of the "lowest" level
terms "setsum" and "op" while the third one thankfully not. Especially, I
don´t see any "relevant" difference
between sum_patter02 e sum_pattern03.

As a last unrelated question, in theorem sum_pattern04, I could not prove
the inductive step with either
simp or auto. When using exponentiations, what kind of proof method does
one has to usually use?

Thanks for any help!
---------
theorem sum_pattern01:
fixes n::nat
shows "(∑j∈{0..n}. 2*j)= n * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0::nat
assume "?P x0"
from this show "?P (Suc x0)" by simp
qed

theorem sum_pattern02:
fixes n::nat
shows "(∑j=0..n. 2*j)= n * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0::nat
assume "?P x0"
from this show "?P (Suc x0)" by simp
qed

theorem sum_pattern03:
fixes n::nat
shows "(∑j=0..n. 2*j+1) = (n+1) * (n+1)" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0
assume IH: "?P x0"
from this show "?P (Suc x0)" by simp
qed

theorem sum_pattern04:
fixes n::nat
shows "(∑j=0..n. 2*j+1) = (n+1)^2" (is "?P n")
proof (induction n)
show "?P 0" by simp
next
fix x0
assume IH: "?P x0"
from this show "?P (Suc x0)" by simp (* fails *)
qed
--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

```

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