Re: [isabelle] Integer Division
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,
Jens Doll wrote:
I have a little problem with the integer division. When solving the
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and