From Isabelle Community Wiki
Jump to: navigation, search


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

For more revision history, see the patched Isabelle repo:

The initial big changeset:

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".


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).


Broken proof methods

some uses in Library/Sum_of_Squares.thy
some uses in ex/Quickcheck_Examples.thy that use finite_types = false (thanks to Lukas Bulwahn)
some uses in ex/Groebner_Examples.thy
all uses in ex/Efficient_Nat_examples.thy (thanks to Florian Haftmann)
one use in Nitpick_Examples/Integer_Nits.thy
some uses in ex/Arith_Examples.thy

Sessions that fail


Sessions adapted to work partially

  • HOL-Library
  • HOL-Nitpick_Examples

Sessions adapted to work 100%

  • HOL
  • HOL-ex
  • HOL-Algebra
  • HOL-Multivariate_Analysis
  • HOL-Nominal
  • 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-Library
  • HOLCF-Tutorial
  • HOLCF-ex
  • IOA
  • 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-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 which always mapped to target language numerals; optional theories refine types nat or int respectively on type 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).