; File: lemmas.lisp
; Author: Julien Schmaltz
; September 12th, 2001
; University of Texas at Austin, Texas, USA
; visitor of University Joseph Fourier, Grenoble, France

; content: 
; all the lemmas proved during the talk

(in-package "ACL2")

; Please adapt the ../../ to point to the right directory
(include-book "../../../books/Arithmetic-4/bind-free/top")
(set-non-linearp t)
(include-book "../../../books/Arithmetic-4/floor-mod/floor-mod")


(defthm mod-x-=-x
  (implies (and (rationalp x)
                (integerp n)
                (<= 0 x)
                (< 0 n)
                (< x n))
           (equal (mod x n) x)))

(defthm mod-x-=-x-+-n
  (implies (and (rationalp x) 
                (< x 0)
                (< (- x) n)
                (integerp n)
                (< 0 n))
           (equal (mod x n)
                  (+ x n)))
  :hints (("GOAL" :in-theory (enable mod))))

(defthm abs-<-1-imp-not-int
  (implies (and (< (abs x) 1)
                (not (equal x 0)))
           (not (integerp x))))

(defthm mod-x-=-minusx-pos
  (implies (and (rationalp x)
                (integerp n)
                (< 0 n)
                (<= n x)
                (< x (* 2 n)))
           (equal (mod x n)
                  (- x n))))

(defthm mod-+-n/2-pos
  (implies (and (< x n)
                (rationalp x)
                (integerp n)
                (<= (* 1/2 n) x)
                (< 2 n)
                )
           (< (mod (+ x (* 1/2 n)) n)
              (mod x n))))

(defthm mod-+-n/2-neg
  (implies (and (< x 0)
                (< (- x) n)
                (rationalp x)
                (<= (- x) (* 1/2 n))
                (integerp n)
                (< 0 n))
           (<  (mod (+ x (* 1/2 n)) n)
               (mod x n))))

(defthm mod-+-1/2-=-mod-minus-1/2
  (implies (and (integerp n)
                (< 0 n)
                (rationalp x)
                (< (abs x) n))
           (equal (mod (+ x (* -1/2 n)) n)
                  (mod (+ x (* 1/2 n)) n)))
  :hints (("GOAL" :in-theory (enable mod))))

(defthm mod-n/2-pos
  (implies (and (< 0 x)
                (< x n)
                (rationalp x)
                (integerp n)
                (<= (* 1/2 n) x)
                (< 0 n)
                )
           (< (mod (+ x (* -1/2 n)) n)
              (mod x n))))

(defthm mod-n/2-neg
  (implies (and (< x 0)
                (< (- x) n)
                (rationalp x)
                (<= (- x) (* 1/2 n))
                (integerp n)
                (< 0 n))
           (<  (mod (+ x (* -1/2 n)) n)
               (mod x n))))