*To*: Manuel Eberl <eberlm at in.tum.de>, Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Proving with Indexed Sums*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 11 Dec 2012 14:36:30 -0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50C734F4.20901@in.tum.de>*References*: <CAAPnxw0ZVYBKGC_nmqi5U6yO5VmKqERErEqvsZqWERSR4H_rJA@mail.gmail.com> <50C734F4.20901@in.tum.de>*Sender*: alfio.martini at gmail.com

Thank you Manuel and Johannes, These explanations were very helpful and enlightening at the same time. Best! On Tue, Dec 11, 2012 at 11:28 AM, Manuel Eberl <eberlm at in.tum.de> wrote: > Hallo, > > This is the normal way of writing sums in Isabelle. > > I think the reason for the behaviour of the output is that in case of > the first two lemmas, you have the statement "setsum (λj. 2*j) {0..n}". > "∑j=0..n. 2*j" is merely an abbreviation for that. > > However, the term "(λj. 2*j)" is morally "(λj. (op*) 2 j)", which > η-reduces automatically to "(op* 2)", and my guess is that the pretty > printer cannot match this to the abbreviation for setsum anymore, so > that you get the "naked" output "setsum (op * 2) {0..n}". > > > In the other two lemmas, you have "setsum (λj. 2*j + 1) {0..n}". This > does not η- or β-reduce to anything, so Isabelle can show it in its > abbreviated form in the output. > > A quick workaround for the first two lemmas would be two write them in a > form in which they are not η-reducible anymore, e.g. with "(λj. j*2)", > which is morally "(λj. (op*) j 2)". If you write your sum as "∑j∈{0..n}. > j*2", you get the nice output without setsum. > > > Regarding your last question, simp does the trick, but it needs the > lemma power2_eq_square, which states that "?a² = ?a * ?a". If you use > "simp add: power2_eq_square", your proof goes through automatically. > Normally, sledgehammer is a very good tool to find theorems like that, > but in this case, it doesn't work for some reason. In any case, if you > are in a situation like that, it can often help to do "apply simp" or > "apply auto" and examine where they get stuck. In this case, you can see > that the problem is that they cannot simplify the squared terms any > further, which is because simp doesn't "know" what squaring means. > Therefore, you need power2_eq_square to allow it to simplify the terms > further. > > > Cheers, > Manuel > > > On 11/12/12 13:49, Alfio Martini wrote: > > 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

**References**:**[isabelle] Proving with Indexed Sums***From:*Alfio Martini

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

- Previous by Date: Re: [isabelle] Proving with Indexed Sums
- Next by Date: [isabelle] command "types" on Isabelle 2012
- Previous by Thread: Re: [isabelle] Proving with Indexed Sums
- 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