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
My paper "Organizing Numerical Theories Using Axiomatic Type Classes"
may be relevant: http://www.cl.cam.ac.uk/~lp15/papers/Reports/
(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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and