File: factorial.lisp

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (40 lines) | stat: -rwxr-xr-x 1,047 bytes parent folder | download | duplicates (4)
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
39
40
;;; Contributed by Ruben A. Gamboa

;;; This book includes many useful theorems about the factorial
;;; function.

(in-package "ACL2")

;;; We start with a definition of the factorial function.  This can be
;;; found in almost all LISP books!

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

;;; It is a (surprisingly) non-obvious fact that factorial returns a
;;; non-zero integer.  The default type heuristics of ACL2 simply
;;; conclude that it is a number!

(defthm factorial-positive-integer
  (and (integerp (factorial n))
       (< 0 (factorial n)))
  :rule-classes (:rewrite :type-prescription))

;;; Factorial is not just positive, it is at least 1.

(defthm factorial-non-negative
  (<= 1 (factorial n))
  :rule-classes (:rewrite :linear))

;;; Since it's always positive, |n!| = n!.

(defthm abs-factorial
  (equal (abs (factorial x))
	 (factorial x)))

;;; I prefer to disable the definition by default, and simply enable
;;; it where I need it.  This has worked well for me.
(in-theory (disable factorial))