*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Proving with Indexed Sums*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 11 Dec 2012 10:49:49 -0200*Sender*: alfio.martini at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Proving with Indexed Sums***From:*Manuel Eberl

**Re: [isabelle] Proving with Indexed Sums***From:*Johannes Hölzl

- Previous by Date: [isabelle] SCP Special Issue on Invariant Generation - Second Call for Papers [2 months to go]
- Next by Date: Re: [isabelle] Proving with Indexed Sums
- Previous by Thread: [isabelle] SCP Special Issue on Invariant Generation - Second Call for Papers [2 months to go]
- Next by Thread: Re: [isabelle] Proving with Indexed Sums
- Cl-isabelle-users December 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list