1 files changed, 38 insertions, 0 deletions
diff --git a/factorial.lisp b/factorial.lisp
new file mode 100644
index 0000000..d51157a
--- /dev/null
+++ b/factorial.lisp
@@ -0,0 +1,38 @@
+;; 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)))
+
+