*To*: Tobias Nipkow <nipkow at in.tum.de>, Ramana Kumar <ramana.kumar at gmail.com>*Subject*: Re: [isabelle] power2_sum outside of rings*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 22 Jun 2011 07:59:37 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4E01AE80.50307@in.tum.de>*References*: <BANLkTikJfja7Tfzr0cYDEYjK9-ZKOBOH3g@mail.gmail.com> <BANLkTimFP-L3SOXhs_uSQS9Kiejz822n-A@mail.gmail.com> <4E01AE80.50307@in.tum.de>*Sender*: huffman.brian.c at gmail.com

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 in.tum.de> 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 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 >> 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 > >

**References**:**[isabelle] power2_sum outside of rings***From:*Ramana Kumar

**Re: [isabelle] power2_sum outside of rings***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] jedit interface with openjdk
- Next by Date: [isabelle] VSTTE 2012 : Second Call for Papers
- Previous by Thread: Re: [isabelle] power2_sum outside of rings
- Next by Thread: [isabelle] jedit interface with openjdk
- Cl-isabelle-users June 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list