*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Proving with Indexed Sums*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 11 Dec 2012 14:34:12 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAPnxw0ZVYBKGC_nmqi5U6yO5VmKqERErEqvsZqWERSR4H_rJA@mail.gmail.com>*Organization*: Technische Universität München*References*: <CAAPnxw0ZVYBKGC_nmqi5U6yO5VmKqERErEqvsZqWERSR4H_rJA@mail.gmail.com>

Am Dienstag, den 11.12.2012, 10:49 -0200 schrieb Alfio Martini: > 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). I assume you want to try different ways to write down your lemma. If you just need Gauss summation there are a couple of lemmas in Set_Interval (gauss_sum and arith_sums_general), just use find_theorems setsum "_ * _" . > 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. First "∑j=0..n. 2*j" is just a different syntax for "∑j∈{0..n}. 2*j" the proof methods in Isabelle do not see any difference. So sum_pattern01 and sum_pattern02 are exactly the same theorems. What is the difference between sum_pattern02 and sum_pattern03: Isabelle applies eta normalization before it stores/displays terms "%x. f x" is rewritten to f so "SUM j : A. 2 * j" -display-> "setsum A (%j. 2 * j)" -eta-> "setsum A (op * 2)" there is no syntax defined for the last term so it is displayed as is. For sum_pattern03 eta normalization does not change the term. > Especially, I > don´t see any "relevant" difference > between sum_patter02 e sum_pattern03. %j. 2 * j -eta-> op * 2 whereas %j. 2 * j + 1 is not eta reducible. > 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? Isabelle does not automatically unfold "t^2" as t might be a quite big term. Use simp add: power2_eq_square to solve this. > 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

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

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