# [isabelle] Modular arithmetic theory?

Hi,

`Does the Isabelle distribution contain efficient decision procedures
``or a comprehensive simpset for linear arithmetic on numbers modulo a
``fixed constant N, but where N can be large, such as 2^32? These kinds
``of verification conditions show up all the time when you want to
``reason about the safety of C or machine code.
`

`The arith method doesn't seem to handle these kinds of subgoals well.
``For example, applying arith to the following lemma has taken over
``five minutes so far without returning.
`
lemma "(((n::nat) mod 4294967296) + (m mod 4294967296)) mod 4294967296
= (m + n) mod 4294967296"
apply arith
Thanks,
-john

`
``
`

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