; Exercise:

; Given the definitions below, prove the indicated theorems.  Most
; will require you to prove other theorems first.

; At the end, do what is necessary in order to run certify-book
; successfully on your file.

(defun del (a lst)
; Delete the first occurrence of a (if any) in the list, lst.
  (cond ((atom lst)
         nil)
        ((equal a (car lst))
         (cdr lst))
        (t
         (cons (car lst)
               (del a (cdr lst))))))

(defun mem (a lst)
; Return t if a is a member of the list, lst, else return nil.
  (cond ((atom lst)
         nil)
        ((equal a (car lst))
         t)
        (t
         (mem a (cdr lst)))))

(defun perm (lst1 lst2)
; Given two lists, return t if lst1 is a permutation of lst2.
  (cond ((atom lst1)
         (atom lst2))
        ((mem (car lst1) lst2)
         (perm (cdr lst1)
               (del (car lst1) lst2)))
        (t
         nil)))

(defthm perm-reflexive
  (perm x x))

(defthm perm-symmetric
  (implies (perm x y)
           (perm y x)))

(defthm perm-transitive
  (implies (and (perm x y) (perm y z))
           (perm x z)))

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

(defun rev (x)
  (if (consp x)
      (app (rev (cdr x)) (cons (car x) nil))
    nil))

; Use the hint shown in the following -- otherwise it proves
; automatically, and what's the fun in that?
(defthm rev-is-id
  (perm (rev x) x)
  :hints (("Goal" :do-not '(generalize))))