← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2013/van-gastel-schmaltz/books/perm.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2013/van-gastel-schmaltz/books/perm.lisp
 
1
#|$ACL2s-Preamble$;
 
2
(begin-book t :ttags :all);$ACL2s-Preamble$|#
 
3
 
 
4
(in-package "ACL2")
 
5
 
 
6
;; The following book contains the defintion of del.
 
7
;; We load this book, to prevent mutliple defintions,
 
8
;; of the same function.
 
9
(include-book "meta/term-defuns" :dir :system)
 
10
 
 
11
 
 
12
(defun permp (left right)
 
13
  (or (and (endp left) (endp right))
 
14
      (and (consp left)
 
15
           (member-equal (car left) right)
 
16
           (permp (cdr left) (del (car left) right)))))
 
17
 
 
18
 
 
19
 
 
20
 
 
21
(defthm permp-reflexive
 
22
  (permp x x))
 
23
(defthm del-different-element-preserves-member
 
24
  (implies (not (equal a b))
 
25
           (iff (member-equal a (del b x))
 
26
                (member-equal a x))))
 
27
(defthm permp-implies-member-iff
 
28
  (implies (permp x y)
 
29
           (iff (member-equal a x)
 
30
                (member-equal a y))))
 
31
(defthm del-commutes
 
32
  (equal (del a (del b c)) (del b (del a c))))
 
33
(defthm del-same-member-preserves-permp
 
34
  (implies (and (member-equal x a)
 
35
                (member-equal x b)
 
36
                (permp a b))
 
37
           (permp (del x a)
 
38
                  (del x b))))
 
39
(defthm permp-transitive
 
40
  (implies (and (permp x y)
 
41
                (permp y z))
 
42
           (permp x z)))
 
43
(in-theory (disable permp-implies-member-iff))
 
44
(defthm cons-del-permutation-of-original
 
45
  (implies (and (member-equal a y)
 
46
        (permp (cons a (del a y)) x))
 
47
       (permp y x)))
 
48
(defthm permp-symmetric
 
49
  (implies (permp x y)
 
50
       (permp y x)))
 
51
(defthm member-of-append-iff-member-of-operand
 
52
  (iff (member-equal a (append x y))
 
53
       (or (member-equal a x)
 
54
           (member-equal a y))))
 
55
(defequiv permp)
 
56
(defcong permp permp (append x y) 2)
 
57
(defcong permp permp (append x y) 1)
 
58
(defcong permp permp (del a x) 2)
 
59
(defcong permp permp (cons a x) 2)
 
60
(defcong permp iff (member-equal a x) 2)
 
61
 
 
62
(defthm permp-append-cons
 
63
  (permp (append x (cons a y))
 
64
         (cons a (append x y))))
 
65
(local (defthm member-remove-equal
 
66
         (iff (member-equal a (remove-equal b x))
 
67
              (and (member-equal a x)
 
68
                   (not (equal a b))))))
 
69
(defcong permp permp (remove-equal a x) 2)
 
70
(defcong permp equal (subsetp x y) 1)
 
71
(defcong permp equal (subsetp x y) 2)
 
72
(defthm succesful-del-preserves-permp
 
73
  (implies (and (member c ch1)
 
74
                  (member c ch2))
 
75
           (equal (permp (del c ch1)
 
76
                         (del c ch2))
 
77
                  (permp ch1 ch2))))
 
78
(defthm unsuccesful-del-preserves-set
 
79
  (implies (not (member c ch1))
 
80
           (equal (del c ch1)
 
81
                  ch1)))
 
82
(defthm del-preserves-permp
 
83
  (implies (equal (member c ch1)
 
84
                  (member c ch2))
 
85
           (equal (permp (del c ch1)
 
86
                         (del c ch2))
 
87
                  (permp ch1 ch2)))
 
88
  :hints (("Goal"
 
89
           :cases ((and (member c ch1) (member c ch2)) (and (not (member c ch1)) (not (member c ch2))))
 
90
           ))
 
91
  )#|ACL2s-ToDo-Line|#
 
92
 
 
93