[isabelle-dev] [isabelle] power2_sum outside of rings
brianh at cs.pdx.edu
Wed Jun 22 22:23:05 CEST 2011
Obviously, the naturals assign a non-standard meaning to negative numerals.
But are there any types that assign a non-standard meaning to
*positive* numerals? (By "standard" I mean 2=1+1, 3=1+1+1, 4=1+1+1+1,
etc.) Is there any reason why anyone would ever want to define or use
such a type?
If not - and if at some point in the future we switch over to unsigned
numerals - then I think it might be useful to do to class "number"
what we did with class "power" a while back: Replace the overloaded
constant with a single, standard definition.
In any case, I think such a major change would require a bit of
planning, and probably won't happen for a while. But I think that
adding a number_semiring class would be a step in the right direction,
and it would be easy enough to make that change right now.
On Wed, Jun 22, 2011 at 12:21 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> As I recall, the number class is for all types where numerals have a meaning. Of course, it is a constituent of number_ring, to which many numeric types belong, but not the naturals.
> On 22 Jun 2011, at 19:55, Florian Haftmann wrote:
>>> 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.
>> This would indeed be helpful, but I guess the natural numbers are the
>> show stopper.
>> Of course we could also attempt to get rid of signed numerals ;-)
>> PGP available:
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev