(in-package "ACL2")

(defun perm (x y)
  (declare (xargs :guard (and (true-listp x)
                              (true-listp y))))
  (cond
    ((atom x) (atom y))
    ((member-equal (car x) y)
     (perm (cdr x) (remove1-equal (car x) y)))
    (t nil)))

(local
 (defthm perm-reflexive
   (perm x x)))

(local
 (encapsulate
   ()
   (local
    (defthm perm-member
      (implies (and (consp y)
                    (perm x y))
               (member (car y) x))))

   (local
    (defthm perm-remove1
      (implies (and (consp y) (perm x y))
               (perm (remove1 (car y) x)
                     (cdr y)))))

   (defthm perm-symmetric
     (implies (perm x y)
              (perm y x))
     :hints (("Goal" :induct (perm y x))))))

(local
 (defthm member-remove1
   (implies (not (equal x y))
            (iff (member x (remove1 y z))
                 (member x z)))))
(local
 (encapsulate
   ()

   (local
    (defthm remove1-remove1
      (equal (remove1 x (remove1 y z))
             (remove1 y (remove1 x z)))))

   (local
    (defthm perm-remove1
      (implies (perm x y)
               (perm (remove1 e x)
                     (remove1 e y)))))

   (local
    (defthm perm-not-member
      (implies (and (member e x)
                    (not (member e y)))
               (not (perm x y)))
      :hints (("Subgoal *1/3" :cases ((equal (car x) e))))
      :rule-classes ((:rewrite :match-free :all))))

   (defthm perm-transitive
     (implies (and (perm x y)
                   (perm y z))
              (perm x z))
     :rule-classes ((:rewrite :match-free :all)))))

(defequiv perm)

(defcong perm perm (remove1 e x) 2)
(defcong perm iff (member e x) 2)


(local (include-book "std/lists/rev" :dir :system))

(local
 (encapsulate
   ()
   (local (defthm perm-rev
            (perm (rev x) (double-rewrite x))
            :hints (("Goal" :induct (perm x x)))))

   (defcong perm perm (rev x) 1)))

(local (defthm perm-rev
         (perm (rev x) x)
         :hints (("Goal" :induct (perm x x)))))

(defcong perm perm (append x y) 2)
(defcong perm perm (append x y) 1)
(defcong perm perm (cons x y) 2)
(defcong perm perm (revappend x y) 2)
(defcong perm perm (revappend x y) 1)

(local
 (defthm member-remove
   (implies (not (equal x y))
            (iff (member x (remove y z))
                 (member x (double-rewrite z))))))

(defcong perm perm (remove e x) 2)