; ACL2 Proofs -- Lesson 1.
; 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.

;; This lesson contains the example used in class about the factorial 
;; function.

;; I suggest that you use emacs to interface with ACL2. 

;; Start ACL2. Submitt each event below, one at a time, to ACL2.
;; ===================================================
;; Events to be submitted to ACL2:
;;  Note: The 3rd and 5th events are identical.
;; ---------------------------------------------------

; ACL2 will accept the first two events which are definitions.

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

; Event 2.
(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)))))

; The third event is a proposed theorem which ACL2 has trouble
; proving because it does not know enough facts about addition.
; Look for `******** FAILED ********'.

; Event 3.
(defthm
   Equal-sum-of-fact
   (equal (sum-of-fact n)
          (- (fact (+ n 1)) 1)))

; The fourth event tells ACL2 enough about addition so that it 
; can now prove the proposed theorem, which is the fifth (and 
; last) event.

; Event 4.
(defthm
   Associate-constants-left-+
   (implies (and (syntaxp (and (consp x)
			       (eq (car x) 'quote)))
		 (syntaxp (and (consp y)
			       (eq (car y) 'quote))))
	    (equal (+ x y z)
		   (+ (+ x y) z))))

; Event 5.
(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.

;; Look up SYNTAXP in the documentation. The index to the ACL2
;; documentation is a good place to start looking. The index can 
;; be found by following the link on the ACL2 web page to the
;; The User's Manual. The expression 
;;           `(syntaxp (and (consp x)(eq (car x) 'quote)))' 
;; is mentioned in the documentation for SYNTAXP-EXAMPLES.