# Re: [isabelle] Modular arithmetic theory?

```John Matthews wrote:
```
```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

```
```
John,

I've had to do more-or-less this recently, and
I wrote a tactic called mod_tac based on conversions,
(which are very much based on the conversions of HOL)

It doesn't work for naturals - only for integers, but that's
just because of the theorems I've used to write it.

Find it in Num_lemmas.ML in
http://userXs.rsise.anXu.edu.au/X~jeremy/iXsabelle/lX4_Isar/ (omit the 'X's)

the code for conversions is in ../gen05/{conv,eq_conv}.ML

I'm afraid the example below is run on a recent development version of
Isabelle (which I had to use for this work - sorry!)
- but there might not be too much trouble changing it back to the
latest release version

Goal "(((n::int) mod 4294967296) + (m mod 4294967296)) mod 4294967296 \
\ = (m + n) mod 4294967296"  ;

> # ### Obsolete goal command encountered
Level 0 (1 subgoal)
(n mod 4294967296 + m mod 4294967296) mod 4294967296 =
(m + n) mod 4294967296
1. (n mod 4294967296 + m mod 4294967296) mod 4294967296 =
(m + n) mod 4294967296
val it = [] : Thm.thm list
> >  by mod_tac ;
Level 1 (1 subgoal)
(n mod 4294967296 + m mod 4294967296) mod 4294967296 =
(m + n) mod 4294967296
1. (n + m) mod 4294967296 = (m + n) mod 4294967296
val it = () : unit
>  by (Simp_tac 1) ;
### Warning: same as previous level
Level 2 (1 subgoal)
(n mod 4294967296 + m mod 4294967296) mod 4294967296 =
(m + n) mod 4294967296
1. (n + m) mod 4294967296 = (m + n) mod 4294967296
val it = () : unit
val it = "?a + ?b = ?b + ?a" : Thm.thm
>  by (simp_tac (simpset () addsimps [add_commute]) 1) ;
Level 3
(n mod 4294967296 + m mod 4294967296) mod 4294967296 =
(m + n) mod 4294967296
No subgoals!
val it = () : unit

Regards,

Jeremy Dawson

```

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