title: Casting int to nat in Isabelle
body: <p>How can I cast an int to nat in Isabelle when I'm sure that it is positive?</p>
  
  <pre><code>value "((-10)::int) mod 3"
  </code></pre>
  
  <p>for example gives 2 and if I'm correct any application of modulo on an int should result in a nat.</p>
  
  <p>Unfortunately the type signature of modulo is <code>'a =&gt; 'a =&gt; 'a</code> so I cannot fix 3 to a nat beforehand and the result will be an int.</p>