*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] how to proof some lemmas containing "\<Sum>"?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 09 Oct 2008 10:01:13 -0700*In-reply-to*: <6626508.600271223456498425.JavaMail.coremail@bj163app138.163.com>*References*: <6626508.600271223456498425.JavaMail.coremail@bj163app138.163.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Quoting 游珍 <yucy0405 at 163.com>:

consts setn::"nat \<Rightarrow> nat set" primrec "setn 0 = {}" "setn (Suc n) = insert (Suc n) (setn n)" lemma f: " (\<Sum>i\<in>(setn (Suc j)). i)=(Suc j)+(\<Sum>i\<in>(setn j). i)" apply auto apply ????? 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 andrules? I don't known any lemmas and themorems about \<Sum>.How can iget some informations about \<Sum>?need help! thanks in advance! yucy

If you type: apply (subst setsum_insert) you get the following subgoals: goal (3 subgoals): 1. finite (setn j) 2. Suc j \<notin> setn j 3. Suc j + \<Sum>(setn j) = Suc (j + \<Sum>(setn j))

Hope this helps, - Brian

**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: Re: [isabelle] how to proof some lemmas containing "\<Sum>"?
- Next by Thread: [isabelle] New AFP entry: Arrow's Impossibility Theorem
- 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