Re: [isabelle] power2_sum outside of rings

Theorems power2_sum and power2_diff are both proved in class
number_ring, which is defined in Int.thy:

class number_ring = number + comm_ring_1 +
  assumes number_of_eq: "number_of k = of_int k"

This class constraint is necessary because this is (currently) the
most general type class in which you can prove that 1 + 1 = 2.
Unfortunately nat cannot be made an instance of number_ring because it
is not a ring; in consequence every theorem that mentions numerals
needs to have a separate, specialized version for type nat.

I would propose adding a new number_semiring class, defined something like this:

class number_semiring = number + semiring_1 +
  assumes number_of_int_eq: "number_of (int n) = of_nat n"

It would be possible to prove 1 + 1 = 2 in class number_semiring, so
power2_sum and power2_diff (along with probably every theorem in
Nat_Numeral.thy) could be generalized to number_semiring. Types like
nat and inat (from Library/Nat_Infinity.thy) would be instances.

A more drastic solution would be to just get rid of the "number" class
altogether (its sole purpose seems to be so that you can have types
where numerals have a non-standard meaning) and have a single
definition of number_of that works uniformly for all types.

- Brian

On Wed, Jun 22, 2011 at 1:57 AM, Tobias Nipkow <nipkow at> wrote:
> 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.
> 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>
>> 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
>> 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

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