blob: d51157af43016d7101f032c33daeae83fba5b33d (
plain)
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
|
;; 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)))
|
