[isabelle] Questions about number representation in Isabelle



Hello,

I am wondering how easy it is to change the representation of numbers
in Isabelle. If I understand correctly, currently natural numbers are
represented as a datatype that has zero and successor, integers are
represented as equivalence classes of pairs of natural numbers, and
rationals are equivalence classes of fractions. Moreover, when
Isabelle specifications are translated into ML, natural numbers are
again represented as a datatype, and integers are converted into the
type int of ML. As was pointed out in couple of days ago in this list,
rational numbers in the development snapshot may be represented as
triples (sign, enumerator, denominator). There is also a module that
maps natural numbers to ML's int. Of course, providing ML types as
counterparts for Isabelle ones raises efficiency and clarity of
programs; however, one has to trust that facts about types proved in
Isabelle hold for the implementation.

Changing number representation is important for code generation. For
example, one may want to produce a program that works with natural
numbers in binary representation or a representation based on an array
of digits instead of a datatype.  Of course, it is desirable that the
number of properties proved manually for the new representation is
minimal.

Isabelle library contains definitions and properties for semirings,
rings, and fields, and many lemmas are proved for those abstract
structures. However, there are dozens of statements proved
specifically for natural numbers as a datatype, such as statements
about the successor, order, and truncated subtraction. Some lemmas are
also proved specifically for integers, e.g., facts that the order on
int is not dense and properties of absolute value.

Isabelle also has internal binary representation of integers given by
numerals as well as simplification rules for operations on such
integers, but this seems unrelated to number representation in
Isabelle and extracted programs.

I'd like to ask the following questions:

(1) Was there any attempt to characterize different classes of numbers
(naturals, integers, rationals) purely axiomatically in order to
minimize the number of facts one has to prove for a new
representation?

(2) What is the best way in Isabelle to change the representation of
naturals or integers? I am not just talking about types_code
directive, which maps an Isabelle type into an unrelated ML type, but
a representation whose properties (like commutativity of addition) can
be proved in Isabelle.

Thank you,
Yevgeniy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.