perm - ACL2 Book

other

(in-package "ACL2")

rmfunction

(defun rm
  (e x)
  (if (consp x)
    (if (equal e (car x))
      (cdr x)
      (cons (car x) (rm e (cdr x))))
    nil))

membfunction

(defun memb
  (a x)
  (declare (xargs :guard t))
  (if (consp x)
    (or (equal a (car x)) (memb a (cdr x)))
    nil))

permfunction

(defun perm
  (x y)
  (if (consp x)
    (and (memb (car x) y) (perm (cdr x) (rm (car x) y)))
    (not (consp y))))

local

(local (defthm perm-cons
    (implies (memb a x)
      (equal (perm x (cons a y)) (perm (rm a x) y)))
    :hints (("Goal" :induct (perm x y)))))

local

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

local

(local (defthm memb-rm (implies (memb a (rm b x)) (memb a x))))

local

(local (defthm perm-memb
    (implies (and (perm x y) (memb a x)) (memb a y))))

local

(local (defthm comm-rm (equal (rm a (rm b x)) (rm b (rm a x)))))

local

(local (defthm perm-rm
    (implies (perm x y) (perm (rm a x) (rm a y)))))

local

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

other

(defequiv perm)