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