[isabelle-dev] NEWS: numeral representation

[Brian Huffman]

As of 2a1953f0d20d, Isabelle now has a new representation for binary numerals:

*** HOL ***

* The representation of numerals has changed. We now have a datatype
"num" representing strictly positive binary numerals, along with
functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to
represent positive and negated numeric literals, respectively. (See
definitions in Num.thy.) Potential INCOMPATIBILITY; some user theories
may require adaptations:

  - Theorems with number_ring or number_semiring constraints: These
    classes are gone; use comm_ring_1 or comm_semiring_1 instead.

  - Theories defining numeric types: Remove number, number_semiring,
    and number_ring instances. Defer all theorems about numerals until
    after classes one and semigroup_add have been instantiated.

  - Numeral-only simp rules: Replace each rule having a "number_of v"
    pattern with two copies, one for numeral and one for neg_numeral.

  - Theorems about subclasses of semiring_1 or ring_1: These classes
    automatically support numerals now, so more simp rules and
    simprocs may now apply within the proof.

  - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
    Redefine using other integer operations.


There are still a couple of loose ends to take care of, which are
currently marked with "BROKEN" in the sources:

* Nitpick_Examples/Integer_Nits.thy: A call to nitpick on a goal with
negative numerals doesn't work. I expect the problem originates in
Tools/Nitpick/nitpick_hol.ML, which I have adapted to handle positive
numerals only; it needs a neg_numeral case.

* SMT_Examples/SMT_{Examples,Tests}.thy: Some smt proofs don't work,
because the .certs files need to be updated again.

* Library/Float.thy: There are some simp rules for a bit-length
operation expressed in terms of the old binary constructors.

I also tested most of the AFP entries, and RSAPSS/Word.thy seems to be
the only theory that breaks: It contains definitions that use the old
binary constructors.

- Brian