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.