Casting int to nat in Isabelle

Question

How can I cast an int to nat in Isabelle when I'm sure that it is positive?

value "((-10)::int) mod 3"

for example gives 2 and if I'm correct any application of modulo on an int should result in a nat.

Unfortunately the type signature of modulo is 'a => 'a => 'a so I cannot fix 3 to a nat beforehand and the result will be an int.

Answer 1

You can use value "nat (((-10)::int) mod 3)".