*To*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: John Matthews <matthews at galois.com>*Date*: Wed, 9 Nov 2005 16:34:52 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <437292A7.40104@rsise.anu.edu.au>*References*: <2034DB73-17B2-4337-B25B-047C9328BF87@galois.com> <437292A7.40104@rsise.anu.edu.au>

Thanks Jeremy, I'll take a look. -john On Nov 9, 2005, at 4:21 PM, Jeremy Dawson wrote:

John Matthews wrote:Hi,Does the Isabelle distribution contain efficient decisionprocedures or a comprehensive simpset for linear arithmetic onnumbers modulo a fixed constant N, but where N can be large, suchas 2^32? These kinds of verification conditions show up all thetime when you want to reason about the safety of C or machine code.The arith method doesn't seem to handle these kinds of subgoalswell. For example, applying arith to the following lemma hastaken over five minutes so far without returning.lemma "(((n::nat) mod 4294967296) + (m mod 4294967296)) mod4294967296= (m + n) mod 4294967296" apply arith Thanks, -johnJohn, 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 inhttp://userXs.rsise.anXu.edu.au/X~jeremy/iXsabelle/lX4_Isar/ (omitthe '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 versionGoal "(((n::int) mod 4294967296) + (m mod 4294967296)) mod4294967296 \\ = (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

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

**Re: [isabelle] Modular arithmetic theory?***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] Modular arithmetic theory?
- Next by Date: Re: [isabelle] Modular arithmetic theory?
- Previous by Thread: Re: [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