# Re: [isabelle] Modular arithmetic theory?

```Amine Chaieb writes:
> > 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)))"

Give that k is a constant, all you need to do is calculate the k = 0,
0 < k and k < 0 sub-formulas to turn this into a formula with just two
or fewer quantifiers.  At the least, you could use

~(c = 0) ==>
(P (x mod c) =
EX k r.
(x = k * c + r) /\
(c < 0 /\ c < r /\ r <= 0 \/ ~(c < 0) /\ 0 <= r /\ r < c) /\
P r)

which doesn't involve having two instances of P on the RHS.

(You could separately rewrite (n MOD 0) to n.  I'd forgotten that
Isabelle/HOL did this, ugh.)

Michael.

```

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