1(IN-PACKAGE "ACL2")
2
3(INCLUDE-BOOK "total-order")
4
5(DEFUN MEMBERP (A X)
6       (IF (CONSP X)
7           (IF (EQUAL A (CAR X))
8               (EQUAL A (CAR X))
9               (MEMBERP A (CDR X)))
10           'NIL))
11
12(DEFUN DROP (A X)
13       (IF (ENDP X)
14           'NIL
15           (IF (EQUAL A (CAR X))
16               (DROP A (CDR X))
17               (CONS (CAR X) (DROP A (CDR X))))))
18
19(DEFUN INSERT (A X)
20       (IF (ENDP X)
21           (CONS A 'NIL)
22           (IF (EQUAL A (CAR X))
23               X
24               (IF (<< A (CAR X))
25                   (CONS A X)
26                   (CONS (CAR X) (INSERT A (CDR X)))))))
27
28(DEFUN ORDEREDP (X)
29       (IF (ENDP (CDR X))
30           (ENDP (CDR X))
31           (IF (<< (CAR X) (CAR (CDR X)))
32               (ORDEREDP (CDR X))
33               'NIL)))
34
35(DEFUN UNIQUEP (X)
36       (IF (ENDP X)
37           (ENDP X)
38           (IF (NOT (MEMBERP (CAR X) (CDR X)))
39               (UNIQUEP (CDR X))
40               'NIL)))
41
42(DEFTHM MEMBERP-INSERT-SAME (EQUAL (MEMBERP A (INSERT A X)) 'T))
43
44(DEFTHM MEMBERP-INSERT-DIFF
45        (IMPLIES (NOT (EQUAL A B))
46                 (EQUAL (MEMBERP A (INSERT B X))
47                        (MEMBERP A X))))
48
49(DEFTHM MEMBERP-DROP-SAME (EQUAL (MEMBERP A (DROP A X)) 'NIL))
50
51(DEFTHM MEMBERP-DROP-DIFF
52        (IMPLIES (NOT (EQUAL A B))
53                 (EQUAL (MEMBERP A (DROP B X))
54                        (MEMBERP A X))))
55
56(DEFTHM ORDERED-IMPLIES-UNIQUE (IMPLIES (ORDEREDP X) (UNIQUEP X)))
57
58(DEFTHM MEMBERP-YES-REDUCE-INSERT
59        (IMPLIES (IF (ORDEREDP X) (MEMBERP A X) 'NIL)
60                 (EQUAL (INSERT A X) X)))
61
62(DEFTHM MEMBERP-NO-REDUCE-DROP
63        (IMPLIES (IF (TRUE-LISTP X)
64                     (NOT (MEMBERP A X))
65                     'NIL)
66                 (EQUAL (DROP A X) X)))
67
68(DEFTHM DROP-PRESERVES-ORDEREDP
69        (IMPLIES (ORDEREDP X)
70                 (ORDEREDP (DROP A X))))
71
72(DEFTHM INSERT-PRESERVES-ORDEREDP
73        (IMPLIES (ORDEREDP X)
74                 (ORDEREDP (INSERT A X))))
75
76(DEFTHM DROP-OF-INSERT-IS-SAME
77        (IMPLIES (IF (TRUE-LISTP X)
78                     (NOT (MEMBERP A X))
79                     'NIL)
80                 (EQUAL (DROP A (INSERT A X)) X)))
81
82(DEFTHM INSERT-OF-DROP-IS-SAME
83        (IMPLIES (IF (ORDEREDP X)
84                     (IF (TRUE-LISTP X) (MEMBERP A X) 'NIL)
85                     'NIL)
86                 (EQUAL (INSERT A (DROP A X)) X)))
87
88(DEFTHM INSERT-RETURNS-TRUE-LISTS
89        (IMPLIES (TRUE-LISTP X)
90                 (TRUE-LISTP (INSERT A X))))
91