Re: [isabelle] power2_sum outside of rings

Thanks for the suggestion.

First a general point: we have not tried hard to keep nat and the algebraic type class hierarchy in sync. Additions are always welcome. But
- can you figure out the most general class the lemma can be proved in?
- are there other related lemmas that ought to be transfered? (certainly power2_diff)

There is no process. Typically the developer of the original theory has an opinion on it and adds the theorem if it appears useful.


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


---------- Forwarded message ----------
From: Tjark Weber<tw333 at>
Date: Mon, May 16, 2011 at 3:09 PM
Subject: Re: power2_sum
To: Ramana Kumar<ramana.kumar at>

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.