On Tue, May 28, 2013 at 6:53 AM, Makarius <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
