===============================================================
; JVM Problem Set 1
; Copyright (C) 2004  J Strother Moore,
;               University of Texas at Austin

; 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: J Strother Moore
; email:      Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

; Modified by: John Cowles
; email:       cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
; ===============================================================
; Below you are asked to define some functions.  You may use only the
; primitives defun, if, equal, consp, car, cdr, binary-+, cons, and,
; or, and integerp, constants such as 1, 2, 3, t, and nil, and macros,
; such as cond, endp, and +, that expand into these primitives.  After
; each informal description is a proposed defthm event that
; illustrates evaluations of the definition.  Make sure your defuns
; satisfy these defthms.

#|
; Here is a simple example.
; Define (app x y) so that it concatenates the lists x and y, 
; i.e., copies x to replace the terminal marker in x with y.

(defthm app-examples
  (and (equal (app '(1 2 3) '(4 5 6)) '(1 2 3 4 5 6))
       (equal (app '(1 2 3 . 7) '(4 5 6)) '(1 2 3 4 5 6))
       (equal (app '(A P P . 7) '(E N D . 8)) '(A P P E N D . 8))
       (equal (app '((A)(B)(C)) '((D)(E))) '((A) (B) (C) (D) (E)))
       (equal (app (list 'M 'O 'N) (cons 'D '(A Y)))
              '(M O N D A Y)))
  :rule-classes nil)

; A correct solution would be to add the event:

(defun app (x y)
  (if (endp x)
      y
      (cons (car x)
	    (app (cdr x) y))))

; You would be wise to submit this event to ACL2, make sure it is
; accepted, and then try the defthm event above to make sure it is
; accepted.

; The last definition is equivalent to this one.

(defun app (x y)
  (if (consp x)
      (cons (car x)
            (app (cdr x) y))
      y))

; The definitions above are equivalent to this one.

(defun app (x y)
  (cond ((endp x) y)
        (t (cons (car x)
                 (app (cdr x) y)))))

; If you are not sure how a macro expands, use :trans.  
; For example, after defining app, you might try:

ACL2 !>:trans (cond ((endp x) y)
                    (t (cons (car x)
                             (app (cdr x) y))))

; and see that the expansion involves only the allowed primitives.

; Question: What would happen if the :trans command were tried
; before defining app?
|#

; Problem 1.1:
; Define (mem e x) so that it returns t if e is an element of the
; list x and returns nil otherwise.

(defthm mem-examples
  (and (mem 1 '(1 2 3))
       (mem 2 '(1 2 3))
       (not (mem '(1) '(1 2 3)))
       (not (mem 1 '(2 3 . 1)))
       (mem '(3) '(2 (3) . 1))
       (mem 'd '(M O N D A Y)))
  :rule-classes nil)

; Problem 1.2:
; Define (ln x) so that it returns the length of the list. 
; Make sure the following defthms are successful.

(defthm ln-examples
  (and (equal (ln '(1 2 3)) 3)
       (equal (ln '(a b c d e)) 5)
       (equal (ln '((1) (2) (3) . 7)) 3))
  :rule-classes nil)

; Problem 1.3 
; Define (sum x) so that it returns the sum of the elements of the
; list x.  You may assume that every element of x is a number.

(defthm sum-examples
  (and (equal (sum '(1 2 3)) 6)
       (equal (sum '(3 -3 3 3 -3 -3)) 0)
       (equal (sum '(1 2 3 . -6)) 6))
  :rule-classes nil)

; What happens if you evaluate (sum '(1 2 T NIL))?  You don't have
; to answer, but think about and try it.  Be ready to discuss it.

; Problem 1.4
; Define (tmark x) so that it returns the terminal mark of the 
; list x.

(defthm tmark-examples
  (and (equal (tmark '(1 2 3)) nil)
       (equal (tmark '(a b c d . nil)) nil)
       (equal (tmark '(1 2 3 . 7)) 7))
  :rule-classes nil)

; Problem 1.5
; Define (all-ints x) so that it returns t if each element, e, 
; of x satisfies (integerp e), and nil otherwise.

(defthm all-ints-examples
  (and (equal (all-ints '(1 2 3)) t)
       (equal (all-ints '(1 2 t 4)) nil)
       (equal (all-ints '(1 2 3 . ABC)) t))
  :rule-classes nil)

; Problem 1.6
; Define (some-int x) so that it returns t if some element, e, 
; of x satisfies (integerp e), and nil otherwise.

(defthm some-int-examples
  (and (equal (some-int '(nil t 1/2)) nil)
       (equal (some-int '(nil 1/2 -3 . ABD)) t)
       (equal (some-int '(1/2 1/3 1/4 . 7)) nil))
  :rule-classes nil)

; Problem 1.7
; Define (all-ints-counterexample x) so that if (all-ints x) is
; false, (all-ints-counterexample x) is a non-integer element of 
; x.  Note that the spec above does not say what the function 
; returns when every element of x is an integer.  To complete the
; spec (arbitrarily), I'll say: If (all-ints x) is t, then
; (all-ints-counterexample x) should return 23.

(defthm all-ints-counterexample-examples
  (and (equal (all-ints-counterexample '(1 2 3)) 23)
       (equal (all-ints-counterexample '(1 2 t 4)) t)
       (equal (all-ints-counterexample '(nil 2 t 4)) nil)
       (equal (all-ints-counterexample '(1 2 3 . ABC)) 23))
  :rule-classes nil)

; Note that the spec does not specify which non-integer in x 
; should be returned, but that the example suggests a convention.

; Informal challenge (no credit): Can you specify
; all-ints-counterexample formally, i.e., with a formula?

; Problem 1.8
; Define (cp x) so that it copies the spine of the list x, i.e.,
; ``re-conses'' x's elements together.

(defthm cp-examples
  (and (equal (cp '(1 2 3)) '(1 2 3))
       (equal (cp '(1 2 3 . 7)) '(1 2 3 . 7))
       (equal (cp '(a b c . nil)) '(A B C)))
  :rule-classes nil)

; Problem 1.9
; Define (rep e x) so that it replaces each element of x by e.

(defthm rep-examples
  (and (equal (rep 3 '(1 2 3 4)) '(3 3 3 3))
       (equal (rep nil '(1 2 3)) '(() () ()))
       (equal (rep 'a '(a b c . 7)) '(A A A . 7))
       (equal (rep '(A) '(1 2 3)) '((A) (A) (A))))
  :rule-classes nil)

; Problem 1.10
; Using, at most, only the functions defined above, mem, ln, sum,
; tmark, all-ints, some-int, all-ints-counterexample, cp, and rep,
; define the function (sq x) to return the square of the length 
; of the list x.

(defthm sq-examples
  (and (equal (sq '(1 2 3 4 5)) 25)
       (equal (sq '(a b c)) 9)
       (equal (sq '(1 -1 1 -1)) 16))
  :rule-classes nil)