Re: [isabelle] Modular arithmetic theory?



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.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.