*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Questions about number representation in Isabelle*From*: "Yevgeniy Makarov" <emakarov at gmail.com>*Date*: Mon, 15 Jan 2007 13:07:34 +0100

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

**Follow-Ups**:**Re: [isabelle] Questions about number representation in Isabelle***From:*Tobias Nipkow

**Re: [isabelle] Questions about number representation in Isabelle***From:*Lawrence Paulson

**Re: [isabelle] Questions about number representation in Isabelle***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] bug in application of intro rule for SOME P when its type is a function?
- Next by Date: [isabelle] LFMTP'07: Call For Papers
- Previous by Thread: Re: [isabelle] bug in application of intro rule for SOME P when its type is a function?
- Next by Thread: Re: [isabelle] Questions about number representation in Isabelle
- Cl-isabelle-users January 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list