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
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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and