[isabelle-dev] [isabelle] power2_sum outside of rings

[Brian Huffman]

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.

- Brian

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.
> Larry
>
> 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 ;-)
>>
>>       Florian
>>
>> --
>>
>> Home:
>> http://www.in.tum.de/~haftmann
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>