Theory "setLemmas"

Signature

Definitions

PRIME_def

|- !s. PRIME s = STRCAT s "'"

Theorems

SET_SPEC

|- !P x. x IN {y | P y} = P x

DIFF_OVER_INTER

|- !s t u.
     s SUBSET u /\ t SUBSET u ==>
     (u DIFF s INTER t = u DIFF s UNION (u DIFF t))

DIFF_OVER_UNION

|- !s t u.
     s SUBSET u /\ t SUBSET u ==>
     (u DIFF (s UNION t) = (u DIFF s) INTER (u DIFF t))

DIFF_OVER_BIGUNION

|- !P.
     UNIV DIFF BIGUNION {s | ?n. s = P n} =
     BIGINTER {s | ?n. s = UNIV DIFF P n}

DIFF_OVER_BIGINTER

|- !P.
     UNIV DIFF BIGINTER {s | ?n. s = P n} =
     BIGUNION {s | ?n. s = UNIV DIFF P n}

SET_GSPEC

|- !P x. {x | P x} = (\x. P x)

UNIV_DIFF_EQ

|- !s t. (UNIV DIFF s = UNIV DIFF t) = (s = t)

BIGINTER_LEMMA1

|- !P Q.
     (!n. P n = Q n) ==>
     (BIGINTER {s | ?n. s = P n} = BIGINTER {s | ?n. s = Q n})

BIGUNION_LEMMA1

|- !P Q.
     (!n. P n = Q n) ==>
     (BIGUNION {s | ?n. s = P n} = BIGUNION {s | ?n. s = Q n})

UNIV_DIFF_SUBSET

|- !s t. UNIV DIFF s SUBSET UNIV DIFF t = t SUBSET s

SUBSET_DEST

|- !s t. s SUBSET t = s SUBSET t \/ (s = t)

EQ_IMP_SUBSET

|- !P Q. (P = Q) ==> P SUBSET Q

bus1

|- !Q n'.
     {P | ?n. P = Q n} =
     {P | ?n. ~(n > n') /\ (P = Q n) \/ (n > n' \/ (n = n')) /\ (P = Q n)}

bus2

|- !P Q. (P = Q) ==> (BIGUNION P = BIGUNION Q)

BIGUNION_PSPLIT

|- !Q n'.
     BIGUNION {P | ?n. ~(n = 0) /\ (P = Q n)} =
     BIGUNION {P | ?n. ~(n = 0) /\ n <= n' /\ (P = Q n)} UNION
     BIGUNION {P | ?n. n > n' /\ (P = Q n)}

BIGUNION_PSPLIT2

|- !Q n'.
     BIGUNION {P | ?n. P = Q n} =
     BIGUNION {P | ?n. n <= n' /\ (P = Q n)} UNION
     BIGUNION {P | ?n. n > n' /\ (P = Q n)}

BIGUNION_SPLIT

|- !Q n'.
     BIGUNION {P | ?n. P = Q n} =
     BIGUNION {P | ?n. n <= n' /\ (P = Q n)} UNION
     BIGUNION {P | ?n. n >= n' /\ (P = Q n)}

BIGUNION_SPLIT_EXISTS

|- ?n'.
     !Q.
       BIGUNION {P | ?n. P = Q n} =
       BIGUNION {P | ?n. n <= n' /\ (P = Q n)} UNION
       BIGUNION {P | ?n. n >= n' /\ (P = Q n)}

SUBSET_DEST2

|- !s t. s SUBSET t = s PSUBSET t \/ (s = t)

PSUBSET_CARD_LT

|- !s t. FINITE s /\ FINITE t ==> s PSUBSET t ==> CARD s < CARD t

SUBSET_CARD_LTE

|- !s t. FINITE s /\ FINITE t ==> s SUBSET t ==> CARD s <= CARD t

GEN_PCHAIN_CARD_NO_UB

|- !P. (!n. CARD (P n) < CARD (P (SUC n))) ==> !m. ?n. CARD (P n) > m

BIGUNION_LEM2

|- !P Q.
     (!n. P n SUBSET Q n) ==>
     BIGUNION {p | ?n. p = P n} SUBSET BIGUNION {p | ?n. p = Q n}

SUBSET_EQ

|- !s t. s SUBSET t /\ t SUBSET s = (s = t)

BIGUNION_SUBSET_IMP

|- !P Q.
     (!n. P n SUBSET Q n) ==>
     BIGUNION {P' | ?n. P' = P n} SUBSET BIGUNION {Q' | ?n. Q' = Q n}

LEFT_BIGUNION_SUBSET

|- !X P. (!n. P n SUBSET X) ==> BIGUNION {Q | ?n. Q = P n} SUBSET X

BIGINTER_SUBSET_IMP

|- !P Q.
     (!n. P n SUBSET Q n) ==>
     BIGINTER {P' | ?n. P' = P n} SUBSET BIGINTER {Q' | ?n. Q' = Q n}

LEFT_BIGINTER_SUBSET

|- !X P. (!n. X SUBSET P n) ==> X SUBSET BIGINTER {Q | ?n. Q = P n}

BIGINTER_SPLIT

|- !Q n'.
     BIGINTER {P | ?n. P = Q n} =
     BIGINTER {P | ?n. n <= n' /\ (P = Q n)} INTER
     BIGINTER {P | ?n. n >= n' /\ (P = Q n)}

BIGINTER_INTER

|- !s1 s2. BIGINTER (s1 UNION s2) = BIGINTER s1 INTER BIGINTER s2

BIGINTER_SUBSET

|- !P Q.
     (!n. P n SUBSET Q n) ==>
     BIGINTER {P' | ?n. P' = P n} SUBSET BIGINTER {Q' | ?n. Q' = Q n}

BOOL_UNIV_FINITE

|- FINITE UNIV

UNIV_CROSS_UNIV

|- UNIV CROSS UNIV = UNIV

IN_APPLY

|- !P x. x IN P = P x

INF_STRING_UNIV

|- INFINITE UNIV

NOT_IN_FIN_STRING_SET

|- !s. FINITE s ==> ?x. ~(x IN s)

PUSH_IMP_THM

|- !a b c. a ==> b ==> c = b ==> a ==> c