[isabelle] power2_sum outside of rings

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


---------- 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

One could consider adding the corresponding variant of power2_sum for
nat (or whatever the most general sort may be) to Main.

Kind regards,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.