; ACL2 Proofs -- Lesson 5
; 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 this lesson we continue with the study of Ackermann's function
;; that was studied in ACL2 Proofs -- Lesson 3 and ACL2 Proofs -- Lesson 4

;; ACL2 should readily accept the following events without error.

; 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
    ack ( x y )
    (declare (xargs :guard (and (integerp x)
				(integerp y)
				(>= x 0)
				(>= y 0))
		    :measure (cons (+ 1 (acl2-count x)) 
				   (acl2-count y))
                    :verify-guards nil))
    (if (zp x)
	(+ y 1)
        (if (zp y)
	    (ack (- x 1) 1)
	    (ack (- x 1) (ack x (- y 1))))))

(defthm
    non-neg-int-ack
    (implies (and (integerp y)
                  (>= y 0))
             (and (integerp (ack x y))
                  (>= (ack x y) 0)))
    :rule-classes :type-prescription)

(verify-guards ack)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Try to use ACL2 to prove the following event:
;; (It will FAIL.)

(defthm
    ack-at-x=1
    (implies (and (integerp y)
		  (>= y 0))
	     (equal (ack 1 y)
		    (+ 2 y))))

;; ACL2 wants to prove this event by induction, but has trouble
;; deciding on an induction scheme. Therefore, we suggest that ACL2
;; use the usual mathematical induction scheme on the nonnegative
;; integers. We do this in a slightly roundabout way because ACL2
;; always chooses induction schemes by looking at the recursive
;; definitions of the functions involved in the statement of the
;; proposed theorem.  The only recursively defined function in the
;; theorem is ACK and its recursive definition does not generate
;; an induction scheme that can be used in a proof of the theorem.
;; In order to tell ACL2 about other induction schemes, a recursive 
;; function must be defined using the recursion corresponding to
;; the inductive scheme: We need a function that is defined on the
;; nonnegative integers with a base step saying what to do with 0
;; and an induction step saying what to do with n based on what was
;; done to n-1. Any such function will do; one that we know about
;; is the factorial function.

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

;; We use HINTS to tell ACL2 to use the induction scheme suggested
;; by the definition of fact.

(defthm
    ack-at-x=1
    (implies (and (integerp y)
		  (>= y 0))
	     (equal (ack 1 y)
		    (+ 2 y)))
    :hints (("Goal"
	     :INDUCT (fact y))))

;; Here is another fact about ack for ACL2 to prove:

(defthm
    ack-at-x=2
    (implies (and (integerp y)
		  (>= y 0))
	     (equal (ack 2 y)
		    (+ 3 (* 2 y))))
    :hints (("Goal"
	     :induct (fact y))))

;; Read about the :INDUCT hint under the topic HINTS in the ACL2 
;; documentation.