#| ; Certification instructions: (certify-book "perm") JSM June, 2000 |# (in-package "ACL2") (defun del (x y) (if (consp y) (if (equal x (car y)) (cdr y) (cons (car y) (del x (cdr y)))) y)) (defun mem (e x) (if (consp x) (or (equal e (car x)) (mem e (cdr x))) nil)) (defun perm (x y) (if (consp x) (and (mem (car x) y) (perm (cdr x) (del (car x) y))) (not (consp y)))) ; The following could be proved right now. ; (local ; (defthm perm-reflexive ; (perm x x))) (local (defthm perm-cons (implies (mem a x) (equal (perm x (cons a y)) (perm (del a x) y))) :hints (("Goal" :induct (perm x y))))) (local (defthm perm-symmetric (implies (perm x y) (perm y x)))) (local (defthm mem-del (implies (mem a (del b x)) (mem a x)))) (local (defthm perm-mem (implies (and (perm x y) (mem a x)) (mem a y)))) (local (defthm comm-del (equal (del a (del b x)) (del b (del a x))))) (local (defthm perm-del (implies (perm x y) (perm (del a x) (del a y))))) ; We now prove this because we give a hint. (local (defthm perm-transitive (implies (and (perm x y) (perm y z)) (perm x z)) :hints (("Goal" :induct (and (perm x y) (perm x z)))))) (defequiv perm) (defcong perm perm (cons x y) 2) (defcong perm perm (append x y) 1) (defcong perm perm (append x y) 2)