; 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))))