[isabelle-dev] proposal for new numeral representation

[Brian Huffman]

Hi all,

I have been working on a new numeral representation for Isabelle
recently, and I would like to share it with everyone. An overview of
the design is now available on the Isanotes wiki [1]; a patched
version of the Isabelle hg repo is also available [2].

[1] https://isabelle.in.tum.de/isanotes/index.php/Numerals
[2] http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals

The design is based on the one in HOL/ex/Numeral.thy by Florian
Haftmann. The main definitions are as follows:

datatype bin = One | Bit0 bin | Bit1 bin

class numeral = semigroup_add + one

primrec (in numeral) numeral :: "bin => 'a" where
  "numeral One = 1" |
  "numeral (Bit0 k) = numeral k + numeral k" |
  "numeral (Bit1 k) = numeral k + numeral k + 1"

class neg_numeral = group_add + one

definition (in neg_numeral) neg_numeral :: "bin => 'a" where
  "neg_numeral k = - numeral k"

Some of the advantages of the design:
* No more number_ring class; numerals are available on any ring type.
* Nonsense like "10^-3" is not allowed; using negative numerals on
type nat causes a type error.
* Arithmetic simp rules on type nat are *much* simpler.
* Arithmetic rules are easier to configure for other semirings, like
extended nat.
* It is no longer ever necessary to use "1+1" in place of "2".

Adapting theories to work with the new numerals is usually not a
problem: Of all the AFP entries I tested, all but three worked without
modification. Two required small one-line changes; only RSAPSS (which
has several theorems that explicitly depend on the numeral
representation) will need deeper changes.

I would welcome any suggestions, criticism, or other feedback.

- Brian