Re: [isabelle] Questions about number representation in Isabelle



On 15 Jan 2007, at 12:07, Yevgeniy Makarov wrote:
(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?

My paper "Organizing Numerical Theories Using Axiomatic Type Classes" may be relevant: http://www.cl.cam.ac.uk/~lp15/papers/Reports/ TypeClasses.pdf

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

Can't you just prove that the old and new representations are isomorphic? Properties should then be easy to transfer from the old representation to the new one.

Larry Paulson








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