[isabelle-dev] New handling of int/nat

[René Neumann]

Dear all,

in Isabelle2012 (and 2013?), the types "nat" and "int" where (using
Efficient_Nat) directly translated into SML's IntInf.int on code_export.

This does not happen anymore in Isabelle-dev -- here they are now mapped
to types in Arith.

The new behavior yields problems when interfacing with the exported code
to other SML-code (type mismatch). What is the proposed "new" way here?
Port all definitions to use type "integer" instead of "nat" ("natural"
also maps to something in Arith)? Or add a 'wrapper' to each definition?:

definition foo :: "nat => nat" where "foo x = x + 1"
definition foo_wrap :: "integer => integer"
  where "foo_wrap x = x + 1"

lemma [code]:
  "foo x = nat_of_integer (foo_wrap (integer_of_nat x))"

Or am I using the new theories in a wrong fashion / there is automation
I could use?

Thanks,
René

P.S.: Hopefully, this is the right mailinglist.

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4782 bytes
Desc: S/MIME Kryptografische Unterschrift
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130910/10e6d563/attachment-0001.p7s>