/usr/share/acl2-7.2dfsg/books/arithmetic/idiv.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 | ;;; Contributed by Ruben A. Gamboa
; Copyright (C) 2014, University of Wyoming
; All rights reserved.
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
#|
This file contains some obvious theorems about the integer division and
related functions. This should be developed into a significant library,
but for now, we're just keeping the theorems that we need.
|#
(in-package "ACL2")
(include-book "top")
(defthm quotient-cancellation
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y)
(integerp z) (< 0 z))
(equal (nonnegative-integer-quotient (* z x) (* z y))
(nonnegative-integer-quotient x y))))
(defthm quotient-numer-denom-lemma
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(equal (nonnegative-integer-quotient (* (numerator (/ x y))
(denominator (/ x y))
x)
(* (numerator (/ x y))
(denominator (/ x y))
y))
(nonnegative-integer-quotient x y)))
:hints (("Goal"
:use (:instance quotient-cancellation
(z (* (numerator (/ x y)) (denominator (/ x y)))))
:in-theory (disable quotient-cancellation))))
(defthm numer-denom-lemma-silly
(implies (and (acl2-numberp x) (acl2-numberp y) (not (equal 0 y)))
(equal (* x d)
(* y x (/ y) d)))
:rule-classes nil)
(defthm numer-denom-lemma
(implies (and (integerp x) (integerp y) (not (equal 0 y)))
(and (equal (* (denominator (/ x y)) x)
(* (numerator (/ x y)) y))))
:hints (("Goal" :use (:instance Rational-implies2 (x (/ x y)))
:in-theory (disable Rational-implies2 equal-*-/-2))
("Goal'4'" :use (:instance numer-denom-lemma-silly
(d (denominator (* x (/ y))))))))
(defthm quotient-numer-denom-lemma2-silly
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y)
(acl2-numberp d) (acl2-numberp n) (not (= 0 d))
(equal (* d x) (* n y)))
(equal (* X d d)
(* Y d n)))
:rule-classes nil)
(defthm quotient-numer-denom-lemma2
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(equal (* X (DENOMINATOR (* X (/ Y)))
(DENOMINATOR (* X (/ Y))))
(* Y (DENOMINATOR (* X (/ Y)))
(NUMERATOR (* X (/ Y))))))
:hints (("Goal" :use (:instance quotient-numer-denom-lemma2-silly
(d (DENOMINATOR (* X (/ Y))))
(n (NUMERATOR (* X (/ Y))))))))
(defthm quotient-numer-denom-lemma3
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(equal (nonnegative-integer-quotient (* (numerator (/ x y))
(denominator (/ x y))
x)
(* (numerator (/ x y))
(denominator (/ x y))
y))
(nonnegative-integer-quotient (numerator (/ x y))
(denominator (/ x y)))))
:hints (("Goal"
:use ((:instance quotient-cancellation
(x (numerator (/ x y)))
(y (denominator (/ x y)))
(z (* (denominator (/ x y)) x)))
(:instance numer-denom-lemma))
:in-theory (disable quotient-cancellation numer-denom-lemma))))
(defthm quotient-numer-denom
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(equal (nonnegative-integer-quotient (numerator (/ x y))
(denominator (/ x y)))
(nonnegative-integer-quotient x y)))
:hints (("Goal" :use ((:instance quotient-numer-denom-lemma)
(:instance quotient-numer-denom-lemma3))
:in-theory (disable quotient-numer-denom-lemma
quotient-numer-denom-lemma3))))
(defthm remainder-theorem-1
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(equal (+ (* (truncate x y) y) (rem x y)) x)))
(defthm remainder-lemma
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(< (- x (* y (nonnegative-integer-quotient x y))) y))
:rule-classes (:rewrite :linear))
(defthm remainder-theorem-2
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(< (rem x y) y)))
(defthm quotient-lower-bound
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(<= (nonnegative-integer-quotient x y)
(/ x y)))
:rule-classes (:linear :rewrite))
(defthm quotient-upper-bound
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(< (/ x y)
(1+ (nonnegative-integer-quotient x y))))
:hints (("Goal" :use (:instance remainder-lemma)
:in-theory (disable remainder-lemma)))
:rule-classes (:rewrite :linear))
(defthm truncate-lower-bound
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(<= (truncate x y) (/ x y)))
:rule-classes (:linear :rewrite))
(defthm truncate-upper-bound
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(< (/ x y) (1+ (truncate x y))))
:rule-classes (:linear :rewrite))
(defthm rem-lower-bound
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(<= 0 (rem x y)))
:rule-classes (:linear :rewrite))
(defthm rem-upper-bound
(implies (and (integerp x) (< 0 x) (integerp y) (< 0 y))
(< (rem x y) y))
:rule-classes (:linear :rewrite))
|