*To*: Michael Norrish <Michael.Norrish at nicta.com.au>*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Fri, 11 Nov 2005 11:14:52 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <17268.8955.736580.622575@raceme.rsise.anu.edu.au>*References*: <2034DB73-17B2-4337-B25B-047C9328BF87@galois.com> <20051110043029.7216F293AA@atbroy30.informatik.tu-muenchen.de> <Pine.GSO.4.60.0511100814040.21354@sunbroy2.informatik.tu-muenchen.de> <17268.8955.736580.622575@raceme.rsise.anu.edu.au>

Surely the elimination only produces two quantifiers. The relevant theorem is P (n mod c) = EX q r. n = q * c + r /\ r < c /\ P r

"?P (?n mod ?k) = ((?k = 0 --> ?P ?n) &

If you use integer modulus, you get a more complicated body because you allow for negative arguments, but you don't have the 0 <= constraints.

..... Cheers Amine

**Follow-Ups**:**Re: [isabelle] Modular arithmetic theory?***From:*Michael Norrish

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

**Re: [isabelle] Modular arithmetic theory?***From:*nipkow

**Re: [isabelle] Modular arithmetic theory?***From:*Amine Chaieb

**Re: [isabelle] Modular arithmetic theory?***From:*Michael Norrish

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