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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev