; CSU290 Homework 5 - Fall 2008
; You must work in pairs on this assignment, but with a DIFFERENT partner
; than you have had on previous homeworks.
;
; Student name 1:  TODO: PUT ONE NAME HERE
; Student name 2:  TODO: PUT OTHER NAME HERE
;
; This assignment will NOT involve ACL2s, though you may use the .lisp editor
; in ACL2s to help with code/formula formatting.  You must construct proofs
; by hand in the style presented in class, and turn them in in a text file
; (.txt or .lisp is OK.  .doc or .docx or .rtf is NOT)


; Given these definitions:

; MEM: all true-list -> boolean
; Returns boolean indicating whether the first argument is a member
; of the second argument list.
(defun mem (x a)
  (if (endp a)
    nil
    (if (equal x (car a))
      t
      (mem x (cdr a)))))

; UN: true-list true-list -> true-list
; Set-theoretic UNION. Returns a list with all the elements of both
; the argument lists.
(defun un (a b)
  (if (endp a)
    b
    (cons (car a)
          (un (cdr a)
              b))))

; Using these definitions, AND axioms given in Hwk4, prove the
; following theorems.  You can use each as a lemma in later proofs
; in this assignment.

; 1. Prove this (using induction) and call it lemma Un-Cons-Element 
(mem x (un a (cons x b)))

; 2. Prove this (using induction) and call it lemma Un-Empty
(implies (endp b)
         (equal (mem x (un a b))
                (mem x a)))

; 3. Prove this (using induction) and call it lemma Un-Cons-Other
(implies (not (equal x y))
         (equal (mem x (un a (cons y b)))
                (mem x (un a b))))

; 4. Prove this (using induction) and call it lemma Mem-Un-Commutative
;    (Hint: Use lemmas!  (Here and for the rest...))
(equal (mem x (un a b))
       (mem x (un b a)))

; 5. Prove this (using induction) and call it lemma Mem-Un1
(implies (mem x a)
         (mem x (un a b)))

; 6. Prove this--without induction, just using lemmas--and call it Mem-Un2
(implies (mem x b)
         (mem x (un a b)))


; Now consider this definition:

; UN-TAIL: true-list true-list -> true-list
; Set-theoretic UNION using tail recursion. Returns a list with all the
; elements of both the argument lists.
(defun un-tail (a b)
  (if (endp a)
    b
    (un-tail (cdr a)
             (cons (car a)
                   b))))


; 7. Prove this using an a more complicated induction scheme, that based
;    on the function definition of UN-TAIL.  (Refer to the notes on deriving
;    an induction scheme from a function definition)

(implies (mem x (un-tail a b))
         (mem x (un a b)))




;;; ################# Begin extra practice (optional!) ################## ;;;

; INT: true-list true-list -> true-list
; Set-theoretic INTERSECTION. Returns a list with just the elements that are
; in *both* the argument lists.
(defun int (a b)
  (if (endp a)
    nil
    (if (mem (car a) b)
      (cons (car a)
            (int (cdr a) b))
      (int (cdr a) b))))

; Int-Empty
(implies (endp b)
         (equal (int a b)
                nil))

; Int-Cons-Element
(implies (mem x a)
         (mem x (int a (cons x b))))

; Int-Cons-Other1
(implies (not (equal x y))
         (equal (mem x (int a (cons y b)))
                (mem x (int a b))))

; Int-Cons-Other2
(implies (not (mem y a))
         (equal (mem x (int a (cons y b)))
                (mem x (int a b))))

; Mem-Int-Commutative
(equal (mem x (int a b))
       (mem x (int b a)))