Email Gateway (Aug 18 2022 at 17:48): Email Gateway (Aug 18 2022 at 17:48):From: Ramana Kumar <rk436@cam.ac.uk>
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@cam.ac.uk>
Date: Mon, May 16, 2011 at 3:09 PM
Subject: Re: power2_sum
To: Ramana Kumar <ramana.kumar@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
Email Gateway (Aug 18 2022 at 17:48):From: Tobias Nipkow <nipkow@in.tum.de>
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
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
Email Gateway (Aug 18 2022 at 17:48):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Last updated: Apr 25 2024 at 20:15 UTC