factorial: THEORY
%----------------------------------------------------------------------------
%
%  Factorial function:  factorial(n) = n!
%  
%  Author: Rick Butler                   NASA Langley Research Center
%
%----------------------------------------------------------------------------
BEGIN
 
   n,k: VAR nat

   factorial(n): recursive posnat =
          (if n = 0 then 1 else n*factorial(n-1) endif) MEASURE n

   factorial_0: LEMMA factorial(0) = 1
   factorial_1: LEMMA factorial(1) = 1
   factorial_2: LEMMA factorial(2) = 2
   factorial_3: LEMMA factorial(3) = 6

   factorial_def: LEMMA factorial(n) = IF n = 0 THEN 1 ELSE 
                                       n*factorial(n-1) ENDIF

   factorial_n:   LEMMA n > 0 IMPLIES
                          factorial(n) = n*factorial(n-1)

   factorial_plus1: LEMMA factorial(n+1) = (n+1)*factorial(n)

   factorial_gt: LEMMA n > k IMPLIES factorial(n) > k^(n-k)*factorial(k)

   factorial_ge: LEMMA n >= k IMPLIES factorial(n) >= k^(n-k)*factorial(k)

   factorial_incr: LEMMA k <= n IMPLIES factorial(k) <= factorial(n)

   factorial_strict_incr: LEMMA k /= 0 AND k < n 
                                IMPLIES factorial(k) < factorial(n)


   factorial_lt_n2n: LEMMA factorial(n) <= n^n

   AUTO_REWRITE+ factorial_0
   AUTO_REWRITE+ factorial_1

END factorial