# [isabelle] Indexed Sum/Product Operator

Dear Isabelle Users,
I was playing with the exercise below, and I wanted to find the
theory where the indexed sum operator is defined.
I tried find_consts name: Sum, but this does not seem to
be the way.
Thanks for any help!
theorem sum02: "∑{0..n::nat} = n * (n+1) div 2" (is "?P n")
proof (induction n)
show "?P 0"
proof -
have "∑{0..0::nat} = 0" by simp
also have "...= 0 * 0" by simp
also have "... = 0 * (0 + 1)" by simp
also have "... = (0 * (0 + 1)) div 2" by simp
finally show ?thesis by this
qed
next
fix x0::nat
assume IH: "?P x0"
show "?P (Suc x0)"
proof -
have "∑{0..(Suc x0)} = ∑{0..x0} + Suc x0" by simp
also have "...= ∑{0..x0} + (x0 + 1)" by simp
also have "...= (x0 * (x0 + 1) div 2) + (x0 + 1)" by (simp
only: IH)
also have "...= (x0 * (x0 + 1) + 2 * x0 + 2) div 2" by simp
also have "...= (x0 * x0 + x0 + 2*x0 + 2) div 2" by simp
also have "...= (x0 * x0 + 3*x0 +2) div 2" by simp
also have "...= (x0 + 1) * (x0 + 2) div 2" by simp
also have "...= Suc x0 * (Suc x0 + 1) div 2" by simp
finally show ?thesis by this
qed
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.*