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