diff options
| -rw-r--r-- | lists/perm.lisp | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/lists/perm.lisp b/lists/perm.lisp index a5b5487..d93a0c5 100644 --- a/lists/perm.lisp +++ b/lists/perm.lisp @@ -68,3 +68,26 @@ :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 (defthm perm-rev + (perm (rev x) (double-rewrite 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) |