[isabelle-dev] proposal for new numeral representation
huffman at in.tum.de
Thu Nov 24 16:12:20 CET 2011
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 ; a patched
version of the Isabelle hg repo is also available .
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
* 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.
More information about the isabelle-dev