;;; divisor-list.lisp: 約数に関する証明
(in-package "ACL2")

;; e が x の約数であるかどうかを調べる述語
(defmacro divisorp (e x)
  `(integerp (/ ,x ,e)))

;; n の約数のリストを作る
(defun divisors-1 (n i)
  (cond
    ((zp i) nil)
    ((divisorp i n)
     (cons i (divisors-1 n (1- i))))
    (t
     (divisors-1 n (1- i)))))

(defmacro divisors (n)
  `(divisors-1 ,n ,n))

;; x が n の約数のリストかどうかを調べる述語
(defun divisor-listp (x n)
  (cond
    ((endp x) (null x))
    (t (and (divisorp (car x) n)
            (divisor-listp (cdr x) n)))))

;; 約数リストは真リストであることを示す定理
(defthm divisor-listp-to-true-listp
  (implies (divisor-listp x n)
           (true-listp x))
  :rule-classes :forward-chaining)

;; divisors の結果は約数リストである
(defthm divisor-listp-divisors-1
  (implies (and (natp n)
                (posp m))
           (divisor-listp (divisors-1 n m) n)))

(defthm divisor-listp-divisors
  (implies (posp n)
           (divisor-listp (divisors n) n)))

;; 正数 x について x - 1 が正数でないとき x は 1
(defthm posp-and-not-posp-n-1
  (implies (posp n)
           (iff (not (posp (+ -1 n)))
                (equal n 1))))

;; divisorp-implies-member-divisors-1 の補助定理
(defthm divisorp-implies-member-divisors-1-lemma
  (implies (and (natp n)
                (posp m)
                (not (posp (+ -1 m))))
           (integerp (* (/ m) n)))
  :hints (("Goal" :in-theory (disable posp-and-not-posp-n-1)
                  :use (:instance posp-and-not-posp-n-1
                                  (n m)))))

;; e (e <= n) が n の約数のとき (divisors n) に
;; e が含まれている
(defthm divisorp-implies-member-divisors-1
  (implies (and (natp n)
                (posp m)
                (posp e)
                (<= e m))
           (implies (divisorp e n)
                    (member e (divisors-1 n m))))
  :hints (("Goal" :in-theory (disable posp-and-not-posp-n-1)
                  :use (:instance posp-and-not-posp-n-1
                                  (n m)))))

(defthm divisorp-implies-member-divisors
  (implies (and (posp n)
                (posp e)
                (<= e n))
           (implies (divisorp e n)
                    (member e (divisors n)))))

;; (divisors n) に e が含まれているとき、
;; e は n の約数
(defthm member-divisors-1-implies-divisorp
  (implies (and (natp n)
                (posp m)
                (posp e)
                (member e (divisors-1 n m)))
           (divisorp e n)))

(defthm member-divisors-implies-divisorp
  (implies (and (posp n)
                (posp e))
           (implies (member e (divisors n))
                    (divisorp e n)))
  :hints (("Goal" :in-theory (disable
                              member-divisors-1-implies-divisorp)
                  :use ((:instance member-divisors-1-implies-divisorp
                                   (n n)
                                   (m n)
                                   (e e))))))

;; (divisors n) に e (<= n) が含まれていることは
;; e が n の約数であることの
;; 必要十分条件である
(defthm member-divisors-iff-divisorp
  (implies (and (posp n)
                (posp e)
                (<= e n))
           (iff (member e (divisors n))
                (divisorp e n)))
  :hints (("Goal" :in-theory (disable member-divisors-implies-divisorp)
                  :use ((:instance member-divisors-implies-divisorp
                                   (n n)
                                   (e e))))))