*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] power2_sum outside of rings*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 22 Jun 2011 10:57:36 +0200*In-reply-to*: <BANLkTimFP-L3SOXhs_uSQS9Kiejz822n-A@mail.gmail.com>*References*: <BANLkTikJfja7Tfzr0cYDEYjK9-ZKOBOH3g@mail.gmail.com> <BANLkTimFP-L3SOXhs_uSQS9Kiejz822n-A@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; de; rv:1.9.2.18) Gecko/20110616 Thunderbird/3.1.11

Thanks for the suggestion.

- can you figure out the most general class the lemma can be proved in?

Tobias Am 21/06/2011 16:52, schrieb Ramana Kumar:

May I suggest that a version of power2_sum for a less specific type class be added to Main (more details below)? What is the usual process (if any) for contributing such very minor improvements? Thanks, Ramana ---------- Forwarded message ---------- From: Tjark Weber<tw333 at cam.ac.uk> Date: Mon, May 16, 2011 at 3:09 PM Subject: Re: power2_sum To: Ramana Kumar<ramana.kumar at gmail.com> On Fri, 2011-05-13 at 16:36 +0100, Ramana Kumar wrote:I think the theorem called power2_sum in Main only works in a ring, and natural numbers don't form a ring under plus and times. But the theorem is still true for natural numbers! (I just proved it using algebra_simps in place of ring_distribs and mult2.) Is this a deficiency in Main or in my ability to search for the correct lemmas to use?I believe that is a deficiency in Main. The whole type class hierarchy is a bit complex, and not every lemma has been proved in every possible context. One could consider adding the corresponding variant of power2_sum for nat (or whatever the most general sort may be) to Main. Kind regards, Tjark

**Follow-Ups**:**Re: [isabelle] power2_sum outside of rings***From:*Brian Huffman

**References**:**[isabelle] power2_sum outside of rings***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] structured induction again?
- Next by Date: Re: [isabelle] jedit interface with openjdk
- Previous by Thread: [isabelle] power2_sum outside of rings
- Next by Thread: Re: [isabelle] power2_sum outside of rings
- Cl-isabelle-users June 2011 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