*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proving with Indexed Sums*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 11 Dec 2012 14:28:20 +0100*In-reply-to*: <CAAPnxw0ZVYBKGC_nmqi5U6yO5VmKqERErEqvsZqWERSR4H_rJA@mail.gmail.com>*References*: <CAAPnxw0ZVYBKGC_nmqi5U6yO5VmKqERErEqvsZqWERSR4H_rJA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:15.0) Gecko/20120827 Thunderbird/15.0

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 >

**Follow-Ups**:**Re: [isabelle] Proving with Indexed Sums***From:*Alfio Martini

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

- Previous by Date: [isabelle] Proving with Indexed Sums
- Next by Date: Re: [isabelle] Proving with Indexed Sums
- Previous by Thread: [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