Re: [isabelle] Modular arithmetic theory?



Surely the elimination only produces two quantifiers.  The relevant
theorem is

  P (n mod c) = EX q r. n = q * c + r /\ r < c /\ P r

Yes, if you use the split rules over natural numbers. The current implementation unfortunately uses the split rule over integers :-(

"?P (?n mod ?k) =
      ((?k = 0 --> ?P ?n) &
(0 < ?k --> (ALL i j. 0 <= j & j < ?k & ?n = ?k * i + j --> ?P j)) & (?k < 0 --> (ALL i j. ?k < j & j <= 0 & ?n = ?k * i + j --> ?P j)))"


If you use integer modulus, you get a more complicated body because
you allow for negative arguments, but you don't have the 0 <=
constraints.

.....

Cheers
Amine






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