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