Numerals

Overview

The patch is now merged into the main Isabelle development version:

http://isabelle.in.tum.de/repos/isabelle/rev/2a1953f0d20d

For more revision history, see the patched Isabelle repo:

http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals

The initial big changeset:

http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/c98c478ed65d

The design

A type of positive binary numbers

datatype num = One | Bit0 num | Bit1 num

Note that this type is isomorphic to the strictly-positive natural numbers, with Bit0 interpreted as 2n and Bit1 as 2n+1.

A type class and constructor function for positive numerals

class numeral = semigroup_add + one

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

To represent positive numerals, we only require a "1" and an associative addition operator. Associativity means that it doesn't really matter how the additions are grouped in the definition of the "numeral" constant.

A type class and constructor function for negative numerals

class neg_numeral = group_add + one

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

It may be desirable to relax the group_add class constraint a bit. We might like to support negative numerals on the extended reals, which aren't actually a group (although they do have a subset that forms a group).

Syntax translations for numerals

 2 <==> numeral (Bit0 One)
 5 <==> numeral (Bit1 (Bit0 One))
-1 <==> neg_numeral One
-3 <==> neg_numeral (Bit1 One)

There is no special numeral representation for zero, so the syntax "0" just maps to the existing constant "zero".

Advantages

What are the advantages of this new numeral representation?

Rewrite rules for arithmetic on unsigned types are much simpler. The old rules in Nat_Numeral.thy involved all sorts of conditionals and special cases for negative values; the new ones are much more straightforward.

Rewrite rules for arithmetic on unsigned types are uniform. Formerly, Nat_Numeral.thy contained lots of rules that worked only on type nat. Setting up the simplifier to work in the same way for other unsigned types (e.g. extended naturals) meant writing a similar quantity of other type-specific rules. Now all those rules are available automatically for any semiring.

You can't write negative numerals on types (like nat) that don't have negation. So users won't get confused by writing things like "10 ^ -3"; this produces a type error instead.

Generic theorems about rings and fields can now use numerals. Formerly, users had two choices for such theorems: a) Add a "number_ring" class constraint, or b) use non-canonical forms for numerals, i.e., "- 1" for "-1" or "(1 + 1)" for "2". Numerals are also available in the locale context of these same type classes.

Cancellation simprocs are now available for arbitrary rings and fields; no extra "number_ring" class constraint is needed.

The numeral "2" always means "1 + 1", "3" always means "1 + 1 + 1", etc. Because there is a single, fixed definition for the meaning of numerals, we can now prove theorems like "1 + 2 = 3" without needing any additional type annotations.

Since numerals are always strictly positive, many rewrite rules for numerals can now be stated without side conditions. For example:
- "(x = y / #nn) = (x * #nn = y)"
- (and related theorems for <, <=, and symmetric versions)
- "numeral v = Suc (numeral v - 1)"
- various cancellation rules

The sign-magnitude representation of numerals makes many new rewrite rules possible. For example:
- "abs (#nn) = #nn"
- "abs (-#nn) = #nn"
- "even k ==> (-#nn) ^ k = #nn ^ k"
- "odd k ==> (-#nn) ^ k = - (#nn ^ k)"
- "x dvd -#nn <--> x dvd #nn"
- "-#nn dvd y <--> #nn dvd y"
- "x - (-#nn) = x + #nn"

Adapting to the new representation

What kinds of modifications are necessary to adapt theories?

Theorems with "number_ring" class constraints: Replace with "comm_ring_1" class constraint.

Theories that define numeric types: Remove all "number", "number_semiring", and "number_ring" instances. Theories with "number" instances must defer all theorems about numerals until after the "one" and "semigroup_add" classes have been instantiated.

Simp rules that are syntactically restricted to numerals: Replace foo[of "number_of v", standard] with two copies, one for "numeral" and one for "neg_numeral".

Generic theorems about subclasses of "semiring_1" or "ring_1": These types automatically support numerals now, so more simp rules and simprocs may now apply within the proof. Proofs must be adapted to work as if a "number_ring" constraint was also present. (Might need, e.g., simp del: minus_one)

Proofs that rely on the results of permutative rewriting: There is a small chance that such proofs may break, because the new numeral representation yields a slightly different term ordering. Affected proof scripts must be rewritten to be more robust (relying on the term ordering is considered poor practice anyway).

Status

Broken proof methods

~~sos_cert~~: ~~some uses in Library/Sum_of_Squares.thy~~
~~quickcheck~~: ~~some uses in ex/Quickcheck_Examples.thy that use finite_types = false~~ (thanks to Lukas Bulwahn)
~~algebra~~: ~~some uses in ex/Groebner_Examples.thy~~
~~normalization~~: ~~all uses in ex/Efficient_Nat_examples.thy~~ (thanks to Florian Haftmann)
nitpick: one use in Nitpick_Examples/Integer_Nits.thy
~~linarith~~: ~~some uses in ex/Arith_Examples.thy~~

Sessions that fail

None

Sessions adapted to work partially

HOL-Library
HOL-Nitpick_Examples

Sessions adapted to work 100%

HOL
HOL-ex
HOL-Algebra
HOL-Multivariate_Analysis
HOL-NSA
HOL-Nominal
HOL-SPARK
HOL-Library-Codegenerator_Test (thanks to Florian Haftmann)
HOL-Matrix (thanks to Florian Haftmann)
HOL-Metis_Examples
HOL-Mutabelle
HOL-Number_Theory
HOL-Decision_Procs
HOL-Word
HOL-Word-SMT_Examples (thanks to Sascha Böhme)

Sessions that work unmodified

HOL4
HOL-Auth
HOL-Bali
HOL-Boogie
HOL-Boogie-Examples
HOL-Hahn_Banach
HOL-Hoare
HOL-Hoare_Parallel
HOLCF
HOLCF-FOCUS
HOLCF-IMP
HOLCF-Library
HOLCF-Tutorial
HOLCF-ex
IOA
HOL-IMP
HOL-IMPP
HOL-IOA
IOA-ABP
IOA-NTP
IOA-Storage
IOA-ex
HOL-Imperative_HOL
HOL-Import
HOL-Induct
HOL-Isar_Examples
HOL-Lattice
HOL-MicroJava
HOL-Mirabelle
HOL-NanoJava
HOL-Old_Number_Theory
HOL-Quotient_Examples
HOL-Predicate_Compile_Examples
HOL-Prolog
HOL-SET_Protocol
HOL-SPARK-Examples
HOL-SPARK-Manual
HOL-Statespace
TLA
TLA-Buffer
TLA-Inc
TLA-Memory
HOL-TPTP
HOL-UNITY
HOL-Unix
HOL-Probability
HOL-Quickcheck_Examples
HOL-Word-Examples
HOL-ZF
HOL-Nominal-Examples

Possible perspectives

Preliminary: datatypes with exactly one type constructor (or newtype in Haskell) are optimized away on compilation (checked with Flyspeck-Tame already).
- Provide only one type Target_Numeral.int which always mapped to target language numerals; optional theories refine types nat or int respectively on type Target_Numeral.int. See also theory Library/Target_Numeral.thy for a quite complete demonstration. Use quotient for this.
- With this, get rid of types Code_Numeral.nat, Quickcheck_Narrowing.code_int', theories Library/Code_Natural.thy, Library/Code_Integer.thy, Library/Code_Numeral_Nat.thy.
Turn binary representation of nat into default…
- by means of a preprocessor which turns every equation f … (Suc n) … = … n … into f … (Num k) … = … decr k ……
- where decr :: num => nat with decr k = numeral k - 1.
- Note that this transformation does always work since it does not need a corresponding f … 0 … = … equation.
- See also theory Library/Code_Nat.thy.
- Technical note: need defined order on preprocessors then, in case the existing preprocessor (after Berghofer) is added later on, which is still necessary if nat is implemented (by which means ever) by target language numerals.
Optimize div and mod on binary numerals in case where second operand is divisible by 2 (important special case, e.g. for word library).