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