Numerals
Contents
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/cgibin/repos.cgi/numerals
The initial big changeset:
http://www4.in.tum.de/~huffman/cgibin/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 strictlypositive 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 typespecific 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 noncanonical 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 signmagnitude 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
 HOLLibrary
 HOLNitpick_Examples
Sessions adapted to work 100%
 HOL
 HOLex
 HOLAlgebra
 HOLMultivariate_Analysis
 HOLNSA
 HOLNominal
 HOLSPARK
 HOLLibraryCodegenerator_Test (thanks to Florian Haftmann)
 HOLMatrix (thanks to Florian Haftmann)
 HOLMetis_Examples
 HOLMutabelle
 HOLNumber_Theory
 HOLDecision_Procs
 HOLWord
 HOLWordSMT_Examples (thanks to Sascha Böhme)
Sessions that work unmodified
 HOL4
 HOLAuth
 HOLBali
 HOLBoogie
 HOLBoogieExamples
 HOLHahn_Banach
 HOLHoare
 HOLHoare_Parallel
 HOLCF
 HOLCFFOCUS
 HOLCFIMP
 HOLCFLibrary
 HOLCFTutorial
 HOLCFex
 IOA
 HOLIMP
 HOLIMPP
 HOLIOA
 IOAABP
 IOANTP
 IOAStorage
 IOAex
 HOLImperative_HOL
 HOLImport
 HOLInduct
 HOLIsar_Examples
 HOLLattice
 HOLMicroJava
 HOLMirabelle
 HOLNanoJava
 HOLOld_Number_Theory
 HOLQuotient_Examples
 HOLPredicate_Compile_Examples
 HOLProlog
 HOLSET_Protocol
 HOLSPARKExamples
 HOLSPARKManual
 HOLStatespace
 TLA
 TLABuffer
 TLAInc
 TLAMemory
 HOLTPTP
 HOLUNITY
 HOLUnix
 HOLProbability
 HOLQuickcheck_Examples
 HOLWordExamples
 HOLZF
 HOLNominalExamples
Possible perspectives
 Preliminary: datatypes with exactly one type constructor (or newtype in Haskell) are optimized away on compilation (checked with FlyspeckTame 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
.
 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
 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).