; ACL2 Proofs -- Lesson 4
; 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 the function ack (for
;; Ackermann's function) studied in ACL2 Proofs -- Lesson 3. 

;; By the way DO NOT try to evaluate ack for any but very small values of
;; x and y. The integer value of (ack 4 4) is estimated to have more
;; decimal digits than there are protons, neutrons, and electrons in the
;; universe.

;; 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)

(defthm
    Theorem
    (implies (and (integerp y)
                  (>= y 0))
             (< y (ack x y))))

;; ACL2 uses induction to prove the following.

(thm
 (implies (and (integerp y)
	       (>= y 0))
	  (< (ack x y)
	     (ack x (+ 1 y)))))

;; Read about THM.

;; A simple human proof, not using induction, can be based on an instance 
;; of Theorem.

;; Theorem:              y  < (ack x    y)
;; Instance:      (ack x y) < (ack x-1 (ack x y)) = (ack x y+1)

;; That is, in Theorem, replace y with (ack x y) and replace x with x-1.

;; Try to get ACL2 to ``discover'' this simple proof. 
;; First we use a HINT to tell ACL2 NOT to use induction.

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

(defthm
    monotony-2nd-arg-ack
    (implies (and (integerp y)
		  (>= y 0))
	     (< (ack x y)
		(ack x (+ 1 y))))
    :HINTS (("Goal"
	     :DO-NOT-INDUCT T)))

;; ACL2 completely misses the simple instance of Theorem, so we add to
;; the HINTS to draw ACL2's attention to the instance. Try this in ACL2:

(defthm
    monotony-2nd-arg-ack
    (implies (and (integerp y)
		  (>= y 0))
	     (< (ack x y)
		(ack x (+ 1 y))))
   :HINTS (("Goal"
	    :do-not-induct t
            :USE ((:INSTANCE
                   Theorem
                   (x (- x 1))
                   (y (ack x y))))
            :IN-THEORY (DISABLE Theorem))))           

;; Read about DEFTHM, HINTS, and DISABLE in the ACL2 documentation.