Modulus
Theorem:
(defthm mod-def (implies (case-split (acl2-numberp x)) (equal (mod x y) (- x (* y (fl (/ x y)))))) :rule-classes nil)
Theorem:
(defthm mod-0 (and (equal (mod 0 y) 0) (equal (mod x 0) (fix x))))
Theorem:
(defthm rationalp-mod (implies (rationalp x) (rationalp (mod x y))) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm integerp-mod (implies (and (integerp m) (integerp n)) (integerp (mod m n))) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm natp-mod (implies (and (natp m) (natp n)) (natp (mod m n))) :rule-classes ((:type-prescription :typed-term (mod m n))))
Theorem:
(defthm natp-mod-2 (implies (and (integerp m) (integerp n) (> n 0)) (natp (mod m n))) :rule-classes ((:type-prescription :typed-term (mod m n))))
Theorem:
(defthm mod-bnd-1 (implies (and (case-split (< 0 n)) (case-split (not (complex-rationalp m))) (case-split (not (complex-rationalp n)))) (< (mod m n) n)) :rule-classes :linear)
Theorem:
(defthm mod-by-1 (implies (integerp m) (equal (mod m 1) 0)))
Theorem:
(defthm mod-bnd-2 (implies (and (<= 0 m) (case-split (rationalp m))) (<= (mod m n) m)) :rule-classes :linear)
Theorem:
(defthm mod-does-nothing (implies (and (< m n) (<= 0 m) (case-split (rationalp m))) (equal (mod m n) m)))
Theorem:
(defthm mod-0-fl (implies (acl2-numberp m) (iff (= (mod m n) 0) (= m (* (fl (/ m n)) n)))) :rule-classes nil)
Theorem:
(defthm mod-0-int (implies (and (integerp m) (integerp n) (not (= n 0))) (iff (= (mod m n) 0) (integerp (/ m n)))) :rule-classes nil)
Theorem:
(defthm mod-mult-n (equal (mod (* a n) n) (* n (mod a 1))))
Theorem:
(defthm mod-mult-n-alt (equal (mod (* n a) n) (* n (mod a 1))))
Theorem:
(defthm mod-squeeze (implies (and (= (mod m n) 0) (< m (* (1+ a) n)) (< (* (1- a) n) m) (integerp a) (integerp m) (integerp n)) (= m (* a n))) :rule-classes nil)
Theorem:
(defthm mod-must-be-n (implies (and (= (mod m n) 0) (< m (* 2 n)) (< 0 m) (rationalp m) (rationalp n)) (= m n)) :rule-classes nil)
Theorem:
(defthm fl-mod (implies (not (zp m)) (equal (fl (/ (mod a (* m n)) n)) (mod (fl (/ a n)) m))))
Theorem:
(defthm mod-0-0 (implies (and (integerp p) (rationalp m) (rationalp n)) (iff (= (mod m (* n p)) 0) (and (= (mod m n) 0) (= (mod (fl (/ m n)) p) 0)))) :rule-classes nil)
Theorem:
(defthm mod-equal-int (implies (and (= (mod a n) (mod b n)) (rationalp a) (rationalp b)) (integerp (/ (- a b) n))) :rule-classes nil)
Theorem:
(defthm mod-equal-int-reverse (implies (and (integerp (/ (- a b) n)) (rationalp a) (rationalp b) (rationalp n) (< 0 n)) (= (mod a n) (mod b n))) :rule-classes nil)
Theorem:
(defthm mod-force-equal (implies (and (< (abs (- a b)) n) (rationalp a) (rationalp b) (integerp n)) (iff (= (mod a n) (mod b n)) (= a b))) :rule-classes nil)
Function:
(defun congruent (a b n) (declare (xargs :guard (and (real/rationalp a) (real/rationalp b) (real/rationalp n) (not (= n 0))))) (equal (mod a n) (mod b n)))
Theorem:
(defthm mod-mult (implies (and (integerp a) (rationalp m) (rationalp n)) (equal (mod (+ m (* a n)) n) (mod m n))))
Theorem:
(defthm mod-force (implies (and (<= (* a n) m) (< m (* (1+ a) n)) (integerp a) (rationalp m) (rationalp n)) (= (mod m n) (- m (* a n)))) :rule-classes nil)
Theorem:
(defthm mod-bnd-3 (implies (and (< m (+ (* a n) r)) (<= (* a n) m) (integerp a) (case-split (rationalp m)) (case-split (rationalp n))) (< (mod m n) r)) :rule-classes :linear)
Theorem:
(defthm mod-sum (implies (and (rationalp a) (rationalp b)) (equal (mod (+ a (mod b n)) n) (mod (+ a b) n))))
Theorem:
(defthm mod-diff (implies (and (case-split (rationalp a)) (case-split (rationalp b))) (equal (mod (- a (mod b n)) n) (mod (- a b) n))))
Theorem:
(defthm mod-of-mod (implies (and (case-split (natp k)) (case-split (natp n))) (equal (mod (mod x (* k n)) n) (mod x n))))
Theorem:
(defthm mod-of-mod-cor (implies (and (<= b a) (case-split (integerp b)) (case-split (integerp a))) (equal (mod (mod x (expt 2 a)) (expt 2 b)) (mod x (expt 2 b)))))
Theorem:
(defthm mod-prod (implies (and (rationalp m) (rationalp n) (rationalp k)) (equal (mod (* k m) (* k n)) (* k (mod m n)))))
Theorem:
(defthm mod-mod-times (implies (and (integerp a) (integerp b) (integerp n) (> n 0)) (= (mod (* (mod a n) b) n) (mod (* a b) n))) :rule-classes nil)
Theorem:
(defthm mod-plus-mod-iff (implies (and (integerp a) (integerp b) (integerp c) (not (zp n))) (iff (= (mod a n) (mod b n)) (= (mod (+ a c) n) (mod (+ b c) n)))) :rule-classes nil)
Theorem:
(defthm mod-times-mod (implies (and (integerp a) (integerp b) (integerp c) (not (zp n)) (= (mod a n) (mod b n))) (= (mod (* a c) n) (mod (* b c) n))) :rule-classes nil)
Theorem:
(defthm mod012 (implies (integerp m) (or (equal (mod m 2) 0) (equal (mod m 2) 1))) :rule-classes nil)
Theorem:
(defthm mod-plus-mod-2 (implies (and (integerp a) (integerp b)) (iff (= (mod (+ a b) 2) (mod a 2)) (= (mod b 2) 0))) :rule-classes nil)
Theorem:
(defthm mod-mod-2-not-equal (implies (acl2-numberp m) (not (= (mod m 2) (mod (1+ m) 2)))) :rule-classes nil)
Theorem:
(defthm mod-2*m+1-rewrite (implies (integerp m) (equal (mod (1+ (* 2 m)) 2) 1)))
Theorem:
(defthm mod-neg (implies (and (posp n) (integerp m)) (equal (mod (- m) n) (- (1- n) (mod (1- m) n)))))