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
> add_commute ;
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.