1 files changed, 67 insertions, 0 deletions
diff --git a/lists/perm.lisp b/lists/perm.lisp
new file mode 100644
index 0000000..e1d8c77
--- /dev/null
+++ b/lists/perm.lisp
@@ -0,0 +1,67 @@
+(in-package "ACL2")
+
+(defun perm (x 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
+ (encapsulate
+   ()
+
+   (local
+    (defthm remove1-remove1
+      (equal (remove1 x (remove1 y z))
+             (remove1 y (remove1 x z)))))
+
+   (local
+    (defthm member-remove1
+      (implies (not (equal x y))
+               (iff (member x (remove1 y z))
+                    (member 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))))))
+
+   (defthm perm-transitive
+     (implies (and (perm x y)
+                   (perm y z))
+              (perm x z)))))
+
+(defequiv perm)