*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Date*: Thu, 10 Nov 2005 11:21:59 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <2034DB73-17B2-4337-B25B-047C9328BF87@galois.com>*Organization*: Australian National University*References*: <2034DB73-17B2-4337-B25B-047C9328BF87@galois.com>*User-agent*: Mozilla Thunderbird 0.9 (X11/20041124)

John Matthews wrote:

Hi,Does the Isabelle distribution contain efficient decision procedures ora comprehensive simpset for linear arithmetic on numbers modulo a fixedconstant N, but where N can be large, such as 2^32? These kinds ofverification conditions show up all the time when you want to reasonabout 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 fiveminutes 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

**Follow-Ups**:**Re: [isabelle] Modular arithmetic theory?***From:*John Matthews

**References**:**[isabelle] Modular arithmetic theory?***From:*John Matthews

- Previous by Date: [isabelle] Modular arithmetic theory?
- Next by Date: Re: [isabelle] Modular arithmetic theory?
- Previous by Thread: [isabelle] Modular arithmetic theory?
- Next by Thread: Re: [isabelle] Modular arithmetic theory?
- Cl-isabelle-users November 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list