; ACL2 Proofs -- Lesson 2.
; Copyright (C) 2004  John R. Cowles, University of Wyoming

; This program is free software; you can redistribute it and/or 
; modify it under the terms of the GNU General Public License as
; published by the Free Software Foundation; either version 2 of
; the License, or (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free 
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
; USA.

; Written by: John R. Cowles
; email:      cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.

;; In its native state, ACL2 ``knows'' very little about arithmetic
;; and other commonly used mathematical theories. Such knowledge is 
;; imparted to ACL2 in the form of ``books'' written by users; books 
;; contain definitions and theorems that ACL2 interprets as rules to 
;; guide its search for a proof. One such book is the arithmetic book.

;; The events below illustrate how to use the arithmetic book on
;; the hives. 

;; First, recall from ACL2 Proofs -- Lesson 1 that ACL2 will accept the
;; first two events given below. The third event is a proposed theorem 
;; which ACL2 has trouble proving because it does not know enough facts 
;; about addition.

#|
(defun 
    fact (n)
    (declare (xargs :guard (and (integerp n) 
				(>= n 0))))
    (if (zp n) 
	1 
        (* n (fact (- n 1)))))

(defun
    sum-of-fact ( n )
    (declare (xargs :guard (and (integerp n) 
				(>= n 0))))
    (if (zp n)
	0	
        (+ (sum-of-fact (- n 1))
	   (* n (fact n)))))

(defthm
   Equal-sum-of-fact
   (equal (sum-of-fact n)
          (- (fact (+ n 1)) 1)))
|#

;; We now provide ACL2 with enough information to prove the
;; last event by first including the arithmetic book.

;; ===================================================
;; Events to be submitted to ACL2:
;; ---------------------------------------------------
; Start a fresh ACL2.

; Tell ACL2 the location of the arithmetic book on the hives:

:set-cbd "/home/acl2/acl2-2.7/acl2-sources/books/arithmetic/"

(include-book "top")

(defun 
    fact (n)
    (declare (xargs :guard (and (integerp n) 
				(>= n 0))))
    (if (zp n) 
	1 
        (* n (fact (- n 1)))))

(defun
    sum-of-fact ( n )
    (declare (xargs :guard (and (integerp n) 
				(>= n 0))))
    (if (zp n)
	0	
        (+ (sum-of-fact (- n 1))
	   (* n (fact n)))))

(defthm
   Equal-sum-of-fact
   (equal (sum-of-fact n)
          (- (fact (+ n 1)) 1)))
;; -----------------------------------------------------
;; Don't forget to `quit' from ACL2 and return to the operating
;; system.