*To*: Amine Chaieb <chaieb at in.tum.de>*Subject*: Re: [isabelle] Modular arithmetic theory?*From*: Michael Norrish <Michael.Norrish at nicta.com.au>*Date*: Mon, 14 Nov 2005 09:57:37 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <67d4b68db126b59efbfd7d42725a33cc@in.tum.de>*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> <67d4b68db126b59efbfd7d42725a33cc@in.tum.de>*Reply-to*: Michael Norrish <Michael.Norrish at nicta.com.au>

Amine Chaieb writes: > > 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 > Yes, if you use the split rules over natural numbers. The current > implementation unfortunately uses the split rule over integers :-( > "?P (?n mod ?k) = > ((?k = 0 --> ?P ?n) & > (0 < ?k --> (ALL i j. 0 <= j & j < ?k & ?n = ?k * i + j --> ?P > j)) & > (?k < 0 --> (ALL i j. ?k < j & j <= 0 & ?n = ?k * i + j --> ?P > j)))" Give that k is a constant, all you need to do is calculate the k = 0, 0 < k and k < 0 sub-formulas to turn this into a formula with just two or fewer quantifiers. At the least, you could use ~(c = 0) ==> (P (x mod c) = EX k r. (x = k * c + r) /\ (c < 0 /\ c < r /\ r <= 0 \/ ~(c < 0) /\ 0 <= r /\ r < c) /\ P r) which doesn't involve having two instances of P on the RHS. (You could separately rewrite (n MOD 0) to n. I'd forgotten that Isabelle/HOL did this, ugh.) Michael.

**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

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

- Previous by Date: Re: [isabelle] novice problem
- Next by Date: RE: [isabelle] Questions about using Isabelle
- 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