[isabelle] Modular arithmetic theory?
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and