1(IN-PACKAGE "ACL2")
2
3(INCLUDE-BOOK "records")
4
5(DEFUN SUBSET (X Y)
6       (IF (ENDP X)
7           'T
8           (IF (MEMBERP (CAR X) Y)
9               (SUBSET (CDR X) Y)
10               'NIL)))
11
12(DEFUN SET-INTERSECT (X Y)
13       (IF (ENDP X)
14           'NIL
15           (IF (MEMBERP (CAR X) Y)
16               (CONS (CAR X) (SET-INTERSECT (CDR X) Y))
17               (SET-INTERSECT (CDR X) Y))))
18
19(DEFUN SET-UNION (X Y)
20       (IF (ENDP X)
21           Y
22           (IF (MEMBERP (CAR X) Y)
23               (SET-UNION (CDR X) Y)
24               (CONS (CAR X) (SET-UNION (CDR X) Y)))))
25
26(DEFUN SET-EQUAL (X Y) (IF (SUBSET X Y) (SUBSET Y X) 'NIL))
27
28(DEFTHM SUBSET-IS-REFLEXIVE (SUBSET X X))
29
30(DEFTHM SUBSET-IS-TRANSITIVE
31        (IMPLIES (IF (SUBSET X Y) (SUBSET Y Z) 'NIL)
32                 (SUBSET X Z)))
33
34(DEFTHM SUBSET-OF-EMPTY-IS-EMPTY
35        (IMPLIES (IF (NOT (CONSP X)) (SUBSET Y X) 'NIL)
36                 (NOT (CONSP Y))))
37
38(DEFTHM SET-EQUAL-IS-AN-EQUIVALENCE
39        (IF (BOOLEANP (SET-EQUAL X Y))
40            (IF (SET-EQUAL X X)
41                (IF (IMPLIES (SET-EQUAL X Y)
42                             (SET-EQUAL Y X))
43                    (IMPLIES (IF (SET-EQUAL X Y)
44                                 (SET-EQUAL Y Z)
45                                 'NIL)
46                             (SET-EQUAL X Z))
47                    'NIL)
48                'NIL)
49            'NIL))
50
51(DEFTHM SUBSET-IS-ANTISYMMETRIC
52        (IMPLIES (IF (SUBSET X Y) (SUBSET Y X) 'NIL)
53                 (SET-EQUAL X Y)))
54
55(DEFTHM INTERSECT-IS-A-SUBSET-1 (SUBSET (SET-INTERSECT X Y) X))
56
57(DEFTHM INTERSECT-IS-A-SUBSET-2 (SUBSET (SET-INTERSECT X Y) Y))
58
59(DEFTHM UNION-IS-A-SUBSET-1 (SUBSET X (SET-UNION X Y)))
60
61(DEFTHM UNION-IS-A-SUBSET-2 (SUBSET Y (SET-UNION X Y)))
62
63(DEFTHM SUPERSET-CONTAINS-EVERYTHING
64        (IMPLIES (IF (MEMBERP E X) (SUBSET X Y) 'NIL)
65                 (MEMBERP E Y)))
66
67(DEFTHM SUBSET-OF-NIL-IS-NIL
68        (IMPLIES (IF (NOT (CONSP Y)) (SUBSET X Y) 'NIL)
69                 (NOT (CONSP X))))
70
71(DEFUN PROPER-SUBSET (X Y) (IF (SUBSET X Y) (NOT (SUBSET Y X)) 'NIL))
72
73(DEFTHM PROPER-SUBSET-IS-IRREFLEXIVE (NOT (PROPER-SUBSET X X)))
74
75(DEFTHM PROPER-SUBSET-IS-TRANSITIVE
76        (IMPLIES (IF (PROPER-SUBSET X Y)
77                     (PROPER-SUBSET Y Z)
78                     'NIL)
79                 (PROPER-SUBSET X Z)))
80
81(DEFTHM PROPER-SUBSET-IS-STRONGER-THAN-SUBSET
82        (IMPLIES (PROPER-SUBSET X Y)
83                 (SUBSET X Y)))
84