*To*: 游珍 <yucy0405 at 163.com>*Subject*: Re: [isabelle] how to proof some lemmas containing "\<Sum>"?*From*: Simon Winwood <sjw at cse.unsw.edu.au>*Date*: Thu, 09 Oct 2008 20:04:49 +1100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <6626508.600271223456498425.JavaMail.coremail@bj163app138.163.com>*References*: <6626508.600271223456498425.JavaMail.coremail@bj163app138.163.com>*User-agent*: WanderLust

At Wed, 8 Oct 2008 17:01:38 +0800 (CST), =?gbk?B?087V5A==?= <yucy0405 at 163.com> wrote: > [...] > The reslut is displayed in the next window > proof (prove): step 1 > goal (1 subgoal): > 1. \<Sum>(insert (Suc j) (setn j)) = Suc (j + \<Sum>(setn j)) > > Which method or rule I can choose? How to use these methods and > rules? I don't known any lemmas and themorems about \<Sum>.How can i > get some informations about \<Sum>? It seems obvious that you need something about \<Sum> and insert. Isabelle has a very useful find-theorems command (I use it via C-c C-f in Emacs) --- in this case it is a little tricky as \<Sum> is a translation for setsum (which I found by greping for \<Sum> in isabelle/HOL). If you search for "\<Sum>_._" and insert (or setsum and insert), you get a number of lemmas from Finite_Set, of which setsum_insert is the one we want. This requires a few helper lemmas, but the proof is more or less straightforward (especially if you keep in mind that most lemmas to be proved about setn will be via induction): theory sumlist imports Main List begin consts setn::"nat \<Rightarrow> nat set" primrec "setn 0 = {}" "setn (Suc n) = insert (Suc n) (setn n)" lemma finite_setn: "finite (setn n)" apply (induct n) apply simp apply simp done lemma setn_n_le_n: "x \<in> setn n \<Longrightarrow> x \<le> n" apply (induct n) apply simp apply fastsimp done lemma f: " (\<Sum>i\<in>(setn (Suc j)). i)=(Suc j)+(\<Sum>i\<in>(setn j). i)" proof (subst setn.simps, rule setsum_insert) show "finite (setn j)" by (rule finite_setn) show "Suc j \<notin> setn j" proof assume "Suc j \<in> setn j" hence "Suc j \<le> j" by (rule setn_n_le_n) thus False by simp qed qed end Simon

**References**:

- Previous by Date: Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
- Next by Date: Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
- Previous by Thread: [isabelle] how to proof some lemmas containing "\<Sum>"?
- Next by Thread: Re: [isabelle] how to proof some lemmas containing "\<Sum>"?
- Cl-isabelle-users October 2008 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