int-division

other

(in-package "ACL2")

include-book

(include-book "arithmetic/equalities" :dir :system)

include-book

(include-book "arithmetic/inequalities" :dir :system)

integer-quotientfunction

(defun integer-quotient
  (a b)
  (if (and (integerp a) (integerp b))
    (if (equal 0 a)
      (if (equal 0 b)
        1
        nil)
      (if (integerp (/ b a))
        (/ b a)
        nil))
    nil))

integer-quotient-typetheorem

(defthm integer-quotient-type
  (or (integerp (integer-quotient a b))
    (equal (integer-quotient a b) nil))
  :rule-classes :type-prescription)

integer-quotient-arg-1-typetheorem

(defthm integer-quotient-arg-1-type
  (implies (integerp (integer-quotient a b))
    (equal (integerp a) t))
  :rule-classes :type-prescription)

integer-quotient-arg-2-typetheorem

(defthm integer-quotient-arg-2-type
  (implies (integerp (integer-quotient a b))
    (equal (integerp b) t))
  :rule-classes :type-prescription)

integer-quotient-spec-0-0theorem

(defthm integer-quotient-spec-0-0
  (equal (integer-quotient 0 0) 1))

integer-quotient-spec-a-0theorem

(defthm integer-quotient-spec-a-0
  (implies (and (integerp a) (case-split (not (equal 0 a))))
    (equal (integer-quotient a 0) 0)))

integer-quotient-spec-0-btheorem

(defthm integer-quotient-spec-0-b
  (implies (integerp (integer-quotient 0 b)) (equal 0 b))
  :rule-classes :forward-chaining)

integer-quotient-spec-a-atheorem

(defthm integer-quotient-spec-a-a
  (equal (integer-quotient a a)
    (if (integerp a)
      1
      nil)))

local

(local (defthm inequality-lemma-1
    (implies (and (integerp a) (< 0 a) (not (equal 1 a)))
      (<= 2 a))
    :rule-classes :forward-chaining))

local

(local (defthm inequality-lemma-2
    (implies (and (integerp a) (< a 0) (not (equal -1 a)))
      (<= a -2))
    :rule-classes :forward-chaining))

local

(local (defthm inequality-lemma-3
    (implies (and (integerp (/ a))
        (integerp a)
        (case-split (not (equal 0 a))))
      (or (equal 1 a) (equal -1 a)))
    :rule-classes :forward-chaining :hints (("Goal" :use ((:instance inequality-lemma-1 (a (/ a))) (:instance inequality-lemma-2 (a (/ a))))))))

integer-quotient-spec-a-1theorem

(defthm integer-quotient-spec-a-1
  (implies (and (integerp (integer-quotient a 1)))
    (or (equal 1 a) (equal -1 a)))
  :rule-classes :forward-chaining)

integer-quotient-spec-1-btheorem

(defthm integer-quotient-spec-1-b
  (equal (integer-quotient 1 b)
    (if (integerp b)
      b
      nil)))

integer-quotient-commutes-with-+theorem

(defthm integer-quotient-commutes-with-+
  (implies (and (integerp (integer-quotient a b))
      (integerp (integer-quotient a c))
      (case-split (not (equal 0 a))))
    (equal (integer-quotient a (+ b c))
      (+ (integer-quotient a b) (integer-quotient a c)))))

integer-quotient-commutes-with-unary-minus-1theorem

(defthm integer-quotient-commutes-with-unary-minus-1
  (equal (integer-quotient a (- a))
    (if (integerp a)
      (if (equal 0 a)
        1
        (- 1))
      nil)))

integer-quotient-commutes-with-unary-minus-2theorem

(defthm integer-quotient-commutes-with-unary-minus-2
  (equal (integer-quotient (- a) a)
    (if (integerp a)
      (if (equal 0 a)
        1
        (- 1))
      nil)))

local

(local (defun ind-int-abs
    (n)
    (if (integerp n)
      (if (equal 0 n)
        t
        (if (< 0 n)
          (ind-int-abs (+ -1 n))
          (ind-int-abs (+ 1 n))))
      t)))

integer-quotient-commutes-with-*theorem

(defthm integer-quotient-commutes-with-*
  (implies (and (integerp (integer-quotient a b))
      (case-split (not (equal 0 b)))
      (integerp c))
    (equal (integer-quotient a (* b c))
      (* (integer-quotient a b) c)))
  :hints (("Goal" :induct (ind-int-abs c))))

in-theory

(in-theory (disable integer-quotient-commutes-with-*))

integer-quotient-commutes-with-*-alttheorem

(defthm integer-quotient-commutes-with-*-alt
  (equal (integer-quotient a (* b c))
    (if (and (integerp (integer-quotient a b))
        (case-split (not (equal 0 b)))
        (integerp c))
      (* (integer-quotient a b) c)
      (integer-quotient a (* b c))))
  :hints (("Goal" :induct (ind-int-abs c))))

integer-quotient-*-cancellationtheorem

(defthm integer-quotient-*-cancellation
  (implies (and (integerp a)
      (case-split (not (equal 0 a)))
      (integerp q))
    (equal (integer-quotient a (* a q)) q)))

local

(local (defthm crap001
    (implies (and (integerp a)
        (integerp b)
        (integerp c)
        (not (equal 0 a))
        (not (equal 0 b)))
      (equal (* (/ b a) (/ c b)) (/ c a)))
    :rule-classes nil))

local

(local (defthm crap002
    (implies (and (integerp a) (integerp b)) (integerp (* a b)))
    :rule-classes :type-prescription))

crap003theorem

(defthm crap003
  (implies (and (integerp (* (/ a) b))
      (integerp a)
      (integerp b)
      (integerp c)
      (not (equal 0 a))
      (not (equal 0 b))
      (integerp (/ c b)))
    (integerp (* (/ a) c)))
  :hints (("Goal" :use (crap001 (:instance crap002 (a (/ b a)) (b (/ c b)))))))

integer-quotient-factorizationtheorem

(defthm integer-quotient-factorization
  (implies (and (integerp a)
      (integerp b)
      (integerp c)
      (case-split (not (equal 0 a)))
      (case-split (not (equal 0 b)))
      (integerp (integer-quotient a b))
      (integerp (integer-quotient b c)))
    (equal (* (integer-quotient a b) (integer-quotient b c))
      (integer-quotient a c))))

dividesfunction

(defun divides
  (a b)
  (and (integerp a)
    (integerp b)
    (equal b (* a (integer-quotient a b)))))

divides-integer-quotient-equivalencetheorem

(defthm divides-integer-quotient-equivalence
  (equal (divides a b)
    (and (integerp a)
      (integerp b)
      (integerp (integer-quotient a b))
      (equal b (* a (integer-quotient a b))))))

in-theory

(in-theory (disable divides))

divides-spec-0-0theorem

(defthm divides-spec-0-0 (divides 0 0))

divides-spec-a-0theorem

(defthm divides-spec-a-0
  (implies (integerp a) (divides a 0)))

divides-spec-0-btheorem

(defthm divides-spec-0-b
  (implies (divides 0 b) (equal 0 b))
  :rule-classes :forward-chaining)

divides-spec-a-1theorem

(defthm divides-spec-a-1
  (implies (divides a 1) (or (equal 1 a) (equal -1 a)))
  :rule-classes :forward-chaining)

divides-spec-1-btheorem

(defthm divides-spec-1-b
  (implies (integerp b) (divides 1 b)))

divide-sumtheorem

(defthm divide-sum
  (implies (and (divides d a) (divides d b))
    (divides d (+ a b))))

divide-factortheorem

(defthm divide-factor
  (implies (and (equal b (* a q)) (integerp a) (integerp q))
    (divides a b)))

divides-reflexivitytheorem

(defthm divides-reflexivity
  (implies (integerp a) (divides a a)))

divide-producttheorem

(defthm divide-product
  (implies (and (integerp b) (divides d a))
    (divides d (* a b)))
  :hints (("Goal" :use ((:instance crap002 (a (* a (/ d))))))))

divide-factorizationtheorem

(defthm divide-factorization
  (implies (divides a b)
    (equal (* a (integer-quotient a b)) b)))

in-theory

(in-theory (disable divide-factorization))

local

(local (defthm inequality-lemma-4
    (implies (and (integerp a) (< 0 a) (integerp q) (< 0 q))
      (<= a (* a q)))
    :rule-classes :forward-chaining))

in-theory

(in-theory (disable integer-quotient))

divider-<theorem

(defthm divider-<
  (implies (and (divides a b)
      (integerp a)
      (<= 0 a)
      (integerp b)
      (< 0 b))
    (<= a b))
  :rule-classes :forward-chaining :hints (("Goal" :use ((:instance inequality-lemma-4 (q (integer-quotient a b)))))))

in-theory

(in-theory (enable integer-quotient))

divide-transitivitytheorem

(defthm divide-transitivity
  (implies (and (divides a b) (divides b c)) (divides a c))
  :hints (("Goal" :in-theory (enable integer-quotient) :use crap003)))

equality-from-divisiontheorem

(defthm equality-from-division
  (implies (and (divides a b)
      (divides b a)
      (integerp a)
      (< 0 a)
      (integerp b)
      (< 0 b))
    (equal a b))
  :rule-classes :forward-chaining :hints (("Goal" :in-theory (disable divider-<)
     :use (divider-< (:instance divider-< (a b) (b a))))))

divide-linear-combinationtheorem

(defthm divide-linear-combination
  (implies (and (integerp x) (integerp y))
    (implies (and (divides d a) (divides d b))
      (divides d (+ (* a x) (* b y))))))

in-theory

(in-theory (disable divides))

in-theory

(in-theory (disable integer-quotient))

Included Books