[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.