# Re: [isabelle] Modular arithmetic theory?

Amine Chaieb writes:
> Every mod or div results into 4 universal quantifiers (nested into
> the formula).
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
In HOL4, my normalisation of the goal
``(n MOD 10 + m MOD 10) MOD 10 = (n + m) MOD 10``
gives (in 0.05s)
?k.
0 <= k /\
?r.
0 <= r /\ (& n + & m = k * 10 + r) /\ r < 10 /\
?k.
0 <= k /\
?r'.
0 <= r' /\ (& n = k * 10 + r') /\ r' < 10 /\
?k.
0 <= k /\
?r''.
0 <= r'' /\
?k'.
0 <= k' /\
?r'''.
0 <= r''' /\ (r' + r'' = k' * 10 + r''') /\
r''' < 10 /\ (& m = k * 10 + r'') /\ r'' < 10 /\
(r''' = r)
This is a natural number goal, so all of the existential variables
have picked up 0 <= constraints. Things go horribly after this step,
though the first three variables can be eliminated very cheaply
because of the equality constraints.
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.
Michael.

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