#|
This lab session is a warm-up exercise for homework 9. We will prove that a
tail-recursive definition works and some theorems about the functions in the
homework.

Remember that we are working with the "intermediate" mode.
|#

;; Let's start with some definitions:

;; tlp : All -> Bool
;; Recognizer of true lists.
(defun tlp (x)
  (if (endp x)
    (equal x nil)
    (tlp (cdr x))))

;; app : tlp x tlp -> tlp
;; Append two lists
(defun app (x y)
  (if (endp x)
    y
    (cons (car x) (app (cdr x) y))))

;; rev : tlp -> tlp
;; Reverse a list
(defun rev (x)
  (if (endp x)
    nil
    (app (rev (cdr x)) (list (car x)))))

;; remove-all: All tlp -> tlp
;; signature: (a X)
;; removes all occurrences of a from X
(defun remove-all (a X)
  (cond ((endp X) nil)
        ((equal a (car X)) (remove-all a (cdr X)))
        (t (cons (car X) (remove-all a (cdr X))))))

;; remove-once: All tlp -> tlp
;; signature: (a X)
;; removes the first occurrence of a from X
(defun remove-once (a X)
  (cond ((endp X) nil)
        ((equal a (car X)) (cdr X))
        (t (cons (car X) (remove-once a (cdr X))))))

;; remove-multiple: tlp tlp -> tlp
;; signature: x y
;; removes all elements in x from y
(defun remove-multiple (x y)
  (if (endp x)
    y
    (remove-multiple (cdr x) (remove-all (car x) y))))

;; contains: All tlp -> boolean
;; signature: (a X)
;; returns true if X contains a, nil otherwise
(defun contains (a X)
 (cond ((endp X) nil)
       ((equal a (car X)) t)
       (t (contains a (cdr X)))))

;; perm: tlp tlp -> boolean
;; signature: (x y)
;; returns true if x is a permutation of y, i.e. they contain the same
;; elements in a different order (same number of occurrences for each)
(defun perm (x y)
  (if (endp x)
      (endp y)
    (and (contains (car x) y)
         (perm (cdr x) (remove-once (car x) y)))))

;; only-naturals: tlp -> LoNat
;; removes all non-natural elements from the list
(defun only-naturals (l)
  (if (endp l)
    nil
    (if (natp (car l))
      (cons (car l) (only-naturals (cdr l)))
      (only-naturals (cdr l)))))

;; only-naturals*-acc: tlp tlp -> LoNat
;; tail-recursive version of only-naturals (auxiliary function)
(defun only-naturals*-acc (l acc)
  (if (endp l)
    (rev acc)
    (if (natp (car l))
      (only-naturals*-acc (cdr l) (cons (car l) acc))
      (only-naturals*-acc (cdr l) acc))))

;; only-naturals*: tlp tlp -> LoNat
;; tail-recursive version of only-naturals
(defun only-naturals* (l)
  (only-naturals*-acc l nil))

;; For your convenience, here are some theorems we already know:

(defthm app-nil
  (implies (tlp x)
           (equal (app x nil) x)))

(defthm tlp-app
  (equal (tlp (app x y))
         (tlp y)))

(defthm tlp-rev
  (tlp (rev x)))

(defthm app-assoc
  (equal (app (app x y) z)
         (app x (app y z))))

;; Part A
;;
;; Prove the following theorem about only-naturals: 

(defthm only-naturals*-only-naturals
  (equal (only-naturals* l)
         (only-naturals l)))

;; Part B
;;
;; Prove the following theorem:

(defthm part-b
  (equal (remove-multiple A (remove-multiple B C))
         (remove-multiple B (remove-multiple A C))))

;; Part C (optional)
;;
;; If you have time, prove the following theorem:

(defthm part-c
  (implies (perm a b)
           (equal (remove-multiple a c)
                  (remove-multiple b c))))