;; factorial.lisp -- 階乗を求める

(in-package "ACL2")

(defun factorial (n)
  (if (zp n)
      1
      (* n (factorial (- n 1)))))

;; factorial は常に正の整数
(defthm posp-factorial
  (posp (factorial n)))


;; 末尾再帰版の階乗関数
(defun factorial-tail (n a)
  (if (zp n)
      a
      (factorial-tail (- n 1)
                      (* n a))))

;; 積の交換の定理が必要なので
;; arithmetic books を使う
(local (include-book "arithmetic/top-with-meta" :dir :system))

;; 末尾再帰版と通常版の値は一致する
;; ただし、a は1以外の値も取れるとする
(defthm factorial-tail-factorial-generic
  (implies (integerp a)
           (equal (factorial-tail n a)
                  (* a (factorial n)))))

;; 末尾再帰版と通常版の値は一致する
(defthm factorial-tail-factorial
  (equal (factorial-tail n 1)
         (factorial n)))