factorial

(in-package "ACL2")

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

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

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

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

(in-theory (disable factorial))