Re: [isabelle] Questions about number representation in Isabelle

> (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?

Indeed, HOL contains a rich theory of abstract algebra: see theories
Orderings.thy, Lattices.thy, OrderedGroup.thy and Ring_and_Field.thy.
However, internal representation of numerals is implemented completely
independent from that.

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

Concerning code generation, the default HOL setup for code generator
framework leaves nats as datatypes and maps ints to machine ints.
Technically, it is hard to change without patching the HOL/Main theories
themselves.  In any case, you will have to reprove theorems on
fundamental operations in order to get it really working.  Though this
demands some effort, there are no fundamental issues to prevent somebody
from doing this.  Can you provide me with a little more context, i.e.
which particular representation you want to use for with numeric
datatype for what particular reason etc.?

fn:Florian Haftmann
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =

Attachment: signature.asc
Description: OpenPGP digital signature

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