[isabelle-dev] Obsolete numeral experiments?

[Brian Huffman]

On Tue, May 28, 2013 at 6:53 AM, Makarius <makarius at sketis.net> wrote:
> What is the status of the following experiments wrt. the regular numerals in
> main HOL?
>
> http://isabelle.in.tum.de/repos/isabelle/file/6324f30e23b6/src/HOL/ex/Binary.thy
> http://isabelle.in.tum.de/repos/isabelle/file/6324f30e23b6/src/HOL/ex/Numeral_Representation.thy
>
> Can we delete that, and keep the history inside the history? Or are there
> remaining aspects that are not in the official numeral implementation (and
> reform) by Brian Huffman?

Numeral_Representation.thy defines a couple of type classes for
subtraction that were never added to the main libraries:
semiring_minus and semiring_1_minus. (I believe these were Florian's
work.) They would let us generalize some rules that are currently
specific to nat. We should discuss whether these (or some variation)
would be appropriate to add to Groups.thy before we delete
Numeral_Representation.thy.

As for Binary.thy, I believe that all the main ideas there have
already been incorporated into the HOL numerals library, so there's no
reason not to delete it.

- Brian