*To*: Amine Chaieb <chaieb at in.tum.de>*Subject*: Re: [isabelle] Congruence rules for modular arithmetic*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Mon, 07 Apr 2008 10:18:24 +1000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, John Matthews <matthews at galois.com>*In-reply-to*: <47F8AED5.9040406@in.tum.de>*References*: <B4AE463E-E0ED-433D-945E-46D1735591BD@galois.com> <47DEA2B0.9000306@in.tum.de> <5198AD0B-C1A2-4D74-8ED0-6E4DFA2F154B@galois.com> <47F8AED5.9040406@in.tum.de>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Amine Chaieb wrote:

For e.g. (x mod 256 + 8) mod 256 = (x + 8) mod 256one would need more than simple rewriting with zmod_simps (maybe aspecial simproc or tactic to convert 8 into 8 mod 256 or generally yinto y mod m provided we can prove y < m and m >= 0 for the integers).

Jeremy Dawson

**References**:**Re: [isabelle] Congruence rules for modular arithmetic***From:*John Matthews

**Re: [isabelle] Congruence rules for modular arithmetic***From:*Amine Chaieb

- Previous by Date: Re: [isabelle] Program verification
- Next by Date: [isabelle] Can I assume an interpretation
- Previous by Thread: Re: [isabelle] Congruence rules for modular arithmetic
- Next by Thread: Re: [isabelle] Program verification
- Cl-isabelle-users April 2008 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