# Re: [isabelle] Integer Division

Dear Jens,
A test with presburger will show that such an i does not always exist:
lemma " EX (i::int). r - 2*i = 1" apply presburger (* Fails *)

`There was a feature on how to get an equivalent formula for that (now
``only available from ML). You can let Isabelle prove automatically for you:
`
"(EX (i::int). r - 2*i = 1) == 2 dvd (r - 1)"

`which means that such an i exists if and only if r is odd. From there
``it is easy to define a solution.
`
Hope it helps,
Amine.
Jens Doll wrote:

`I have a little problem with the integer division. When solving the
``equation
` r-2*i=1

`for integers i and r my algorithm gives
`i=(1/2*r+r mod 2)-1/2,

which does not seem right.
Could someone tell me, how to calculate the result?
Thanks, Jens

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