Theory "finite_set"

Signature

Definitions

FSET_def

⊢ ∀AB al bfs. FSET AB al bfs ⇔ ∃bl. LIST_REL AB al bl ∧ (bfs = fset_ABS bl)

fBIGUNION_def

⊢ fBIGUNION = (MAP fset_REP ∘ fset_REP ---> fset_ABS) FLAT

fCARD_def

⊢ fCARD = (fset_REP ---> I) (LENGTH ∘ nub)

fDELETE_def

⊢ fDELETE = (I ---> fset_REP ---> fset_ABS) (λe. FILTER ($¬ ∘ $= e))

fDIFF_def

⊢ fDIFF =
  (fset_REP ---> fset_REP ---> fset_ABS) (λl1 l2. FILTER (λx. ¬MEM x l2) l1)

fEMPTY_def

⊢ fEMPTY = fset_ABS []

fIMAGE_def

⊢ fIMAGE = ((I ---> I) ---> fset_REP ---> fset_ABS) MAP

fINSERT_def

⊢ fINSERT = (I ---> fset_REP ---> fset_ABS) CONS

fINTER_def

⊢ fINTER =
  (fset_REP ---> fset_REP ---> fset_ABS) (FILTER ∘ flip $IN ∘ LIST_TO_SET)

fIN_def

⊢ fIN = (I ---> fset_REP ---> I) (λx l. MEM x l)

fITSET_def

⊢ ∀f s a0. fITSET f s a0 = @a. fITSETr f s a0 a

fITSETr_def

⊢ fITSETr =
  (λf a0 a1 a2.
       ∀fITSETr'.
         (∀a0 a1 a2.
            (a0 = fEMPTY) ∧ (a2 = a1) ∨
            (∃e s A1.
               (a0 = fINSERT e s) ∧ (a2 = f e A1) ∧ fITSETr' s a1 A1 ∧
               ¬fIN e s) ⇒
            fITSETr' a0 a1 a2) ⇒
         fITSETr' a0 a1 a2)

fUNION_def

⊢ fUNION = (fset_REP ---> fset_REP ---> fset_ABS) $++

fsequiv_def

⊢ ∀l1 l2. fsequiv l1 l2 ⇔ (LIST_TO_SET l1 = LIST_TO_SET l2)

fset_ABS_def

⊢ ∀r. fset_ABS r = fset_ABS_CLASS (fsequiv r)

fset_REL_def

⊢ ∀AB fs1 fs2. fset_REL AB fs1 fs2 ⇔ ∀a b. AB a b ⇒ (fIN a fs1 ⇔ fIN b fs2)

fset_REP_def

⊢ ∀a. fset_REP a = $@ (fset_REP_CLASS a)

fset_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. fsequiv r r ∧ (c = fsequiv r)) rep

fset_bijections

⊢ (∀a. fset_ABS_CLASS (fset_REP_CLASS a) = a) ∧
  ∀r. (λc. ∃r. fsequiv r r ∧ (c = fsequiv r)) r ⇔
      (fset_REP_CLASS (fset_ABS_CLASS r) = r)

rel_set_def

⊢ ∀AB A B.
    rel_set AB A B ⇔
    (∀a. a ∈ A ⇒ ∃b. b ∈ B ∧ AB a b) ∧ ∀b. b ∈ B ⇒ ∃a. a ∈ A ∧ AB a b

toSet_def

⊢ ∀fs. toSet fs = {x | fIN x fs}

Theorems

ABS_CLASS_onto

⊢ ∀fs. ∃r. fs = fset_ABS_CLASS (fsequiv r)

BIGUNION_relates

⊢ (rel_set (rel_set AB) |==> rel_set AB) BIGUNION BIGUNION

DECOMPOSITION

⊢ fIN e s ⇔ ∃s0. (s = fINSERT e s0) ∧ ¬fIN e s0

DELETE_EMPTY

⊢ ∀e. fDELETE e fEMPTY = fEMPTY

EXTENSION

⊢ ∀s1 s2. (s1 = s2) ⇔ ∀e. fIN e s1 ⇔ fIN e s2

FINITE_toSet

⊢ ∀s. FINITE (toSet s)

FLAT_relates

⊢ (LIST_REL (LIST_REL AB) |==> LIST_REL AB) FLAT FLAT

FSETEQ

⊢ (FSET $= |==> FSET $= |==> $<=>) fsequiv $=

FSET_AB_eqn

⊢ FSET AB = FSET $= ∘ᵣ LIST_REL AB

FSET_right_unique

⊢ right_unique AB ⇒ right_unique (FSET AB)

FSET_surj

⊢ surj AB ⇒ surj (FSET AB)

FUN_REL_O

⊢ (D1 |==> R1) ∘ᵣ (D2 |==> R2) ⊆ᵣ D1 ∘ᵣ D2 |==> R1 ∘ᵣ R2

FUN_REL_RSUBSET

⊢ D2 ⊆ᵣ D1 ∧ R1 ⊆ᵣ R2 ⇒ D1 |==> R1 ⊆ᵣ D2 |==> R2

INSERT_DELETE

⊢ ∀e s. fINSERT e (fDELETE e s) = fINSERT e s

IN_BIGUNION

⊢ fIN e (fBIGUNION fss) ⇔ ∃fs. fIN fs fss ∧ fIN e fs

IN_DELETE

⊢ ∀a b s. fIN a (fDELETE b s) ⇔ a ≠ b ∧ fIN a s

IN_DIFF

⊢ ∀e s1 s2. fIN e (fDIFF s1 s2) ⇔ fIN e s1 ∧ ¬fIN e s2

IN_IMAGE

⊢ ∀f x s. fIN x (fIMAGE f s) ⇔ ∃y. fIN y s ∧ (x = f y)

IN_INSERT

⊢ ∀e1 e2 s. fIN e1 (fINSERT e2 s) ⇔ (e1 = e2) ∨ fIN e1 s

IN_INTER

⊢ ∀e s1 s2. fIN e (fINTER s1 s2) ⇔ fIN e s1 ∧ fIN e s2

IN_UNION

⊢ ∀e s1 s2. fIN e (fUNION s1 s2) ⇔ fIN e s1 ∨ fIN e s2

LIST_REL_FSET0

⊢ Qt (LIST_REL fsequiv) (MAP fset_ABS) (MAP fset_REP) (LIST_REL (FSET $=))

LIST_REL_FSET0_Abs

⊢ LIST_REL (FSET $=) ll lfs ⇒ (lfs = MAP fset_ABS ll)

LIST_TO_SET_rel_set

⊢ (LIST_REL AB |==> rel_set AB) LIST_TO_SET LIST_TO_SET

LIST_TO_SET_transfer

⊢ (LIST_REL AB |==> rel_set AB) LIST_TO_SET LIST_TO_SET

MAP_relates

⊢ ((AB |==> CD) |==> LIST_REL AB |==> LIST_REL CD) MAP MAP

MEM_FSET0

⊢ FSET $= l fs ⇒ ∀a. MEM a l ⇔ fIN a fs

MEM_transfers

⊢ bi_unique AB ⇒
  (AB |==> LIST_REL AB |==> $<=>) (λx l. MEM x l) (λx l. MEM x l)

NOT_EMPTY_INSERT

⊢ ∀h t. fEMPTY ≠ fINSERT h t

NOT_IN_EMPTY

⊢ ∀e. ¬fIN e fEMPTY

Qt_composes

⊢ Qt R1 Abs1 Rep1 Tf1 ∧ Qt R2 Abs2 Rep2 Tf2 ⇒
  Qt (Tf1ᵀ ∘ᵣ R2 ∘ᵣ Tf1) (Abs2 ∘ Abs1) (Rep1 ∘ Rep2) (Tf2 ∘ᵣ Tf1)

RDOM_FSET0

⊢ RDOM (FSET AB) = (λal. ∀x. MEM x al ⇒ RDOM AB x)

RDOM_FSET0set

⊢ RDOM (FSET $= |==> $<=>) = (λlP. ∀l1 l2. lP l1 ∧ fsequiv l1 l2 ⇒ lP l2)

REP_ABS_equiv

⊢ fset_REP_CLASS (fset_ABS_CLASS (fsequiv r)) = fsequiv r

REP_CLASS_11

⊢ (fset_REP_CLASS fs1 = fset_REP_CLASS fs2) ⇔ (fs1 = fs2)

REP_CLASS_NONEMPTY

⊢ ∀fs. ∃x. fset_REP_CLASS fs x

RSUBSET_I

⊢ R1 ⊆ᵣ R2 ⇒ R1 x y ⇒ R2 x y

RSUBSET_REFL

⊢ R ⊆ᵣ R

RSUBSET_rel_set

⊢ bitotal AB ⇒ AB |==> $<=> ⊆ᵣ rel_set AB

bijection2

⊢ ∀r. fset_REP_CLASS (fset_ABS_CLASS (fsequiv r)) = fsequiv r

equalityp_relset

⊢ equalityp AB ⇒ equalityp (rel_set AB)

fBIGUNION_relates

⊢ (FSET (FSET AB) |==> FSET AB) FLAT fBIGUNION

fCARD_EQ0

⊢ ∀s. (fCARD s = 0) ⇔ (s = fEMPTY)

fCARD_THM

⊢ (fCARD fEMPTY = 0) ∧ ∀e s. fCARD (fINSERT e s) = 1 + fCARD (fDELETE e s)

fCARD_relates

⊢ (FSET $= |==> $=) (LENGTH ∘ nub) fCARD

fDELETE_nonelement

⊢ ∀e s. ¬fIN e s ⇒ (fDELETE e s = s)

fDELETE_relates

⊢ ($= |==> FSET $= |==> FSET $=) (λe. FILTER ($¬ ∘ $= e)) fDELETE

fDIFF_relates

⊢ (FSET $= |==> FSET $= |==> FSET $=) (λl1 l2. FILTER (λx. ¬MEM x l2) l1)
    fDIFF

fEMPTY_relates

⊢ FSET $= [] fEMPTY

fIMAGE_relates

⊢ ((AB |==> CD) |==> FSET AB |==> FSET CD) MAP fIMAGE

fIMAGE_thm

⊢ (∀f. fIMAGE f fEMPTY = fEMPTY) ∧
  ∀f e s. fIMAGE f (fINSERT e s) = fINSERT (f e) (fIMAGE f s)

fINSERT_commutes

⊢ ∀e1 e2 s. fINSERT e1 (fINSERT e2 s) = fINSERT e2 (fINSERT e1 s)

fINSERT_duplicates

⊢ ∀e s. fINSERT e (fINSERT e s) = fINSERT e s

fINSERT_relates

⊢ ($= |==> FSET $= |==> FSET $=) CONS fINSERT

fINTER_EMPTY

⊢ ∀x. (fINTER x fEMPTY = fEMPTY) ∧ (fINTER fEMPTY x = fEMPTY)

fINTER_IDEMPOT

⊢ ∀x. fINTER x x = x

fINTER_relates

⊢ (FSET $= |==> FSET $= |==> FSET $=) (FILTER ∘ flip $IN ∘ LIST_TO_SET) fINTER

fIN_IN

⊢ ∀e fs. fIN e fs ⇔ e ∈ toSet fs

fIN_relates

⊢ bi_unique AB ⇒ (AB |==> FSET AB |==> $<=>) (λx l. MEM x l) fIN

fITSET_EMPTY

⊢ fITSET f fEMPTY a = a

fITSET_INSERT

⊢ (∀x y a. f x (f y a) = f y (f x a)) ⇒
  ∀e s a. fITSET f (fINSERT e s) a = f e (fITSET f (fDELETE e s) a)

fITSET_INSERT_tail

⊢ (∀x y a. f x (f y a) = f y (f x a)) ⇒
  ∀e s a. fITSET f (fINSERT e s) a = fITSET f (fDELETE e s) (f e a)

fITSETr_cases

⊢ ∀f a0 a1 a2.
    fITSETr f a0 a1 a2 ⇔
    (a0 = fEMPTY) ∧ (a2 = a1) ∨
    ∃e s A1. (a0 = fINSERT e s) ∧ (a2 = f e A1) ∧ fITSETr f s a1 A1 ∧ ¬fIN e s

fITSETr_functional

⊢ (∀x y a. f x (f y a) = f y (f x a)) ⇒
  ∀s a0 a1 a2. fITSETr f s a0 a1 ∧ fITSETr f s a0 a2 ⇒ (a1 = a2)

fITSETr_ind

⊢ ∀f fITSETr'.
    (∀A. fITSETr' fEMPTY A A) ∧
    (∀e s A0 A1.
       fITSETr' s A0 A1 ∧ ¬fIN e s ⇒ fITSETr' (fINSERT e s) A0 (f e A1)) ⇒
    ∀a0 a1 a2. fITSETr f a0 a1 a2 ⇒ fITSETr' a0 a1 a2

fITSETr_rules

⊢ ∀f. (∀A. fITSETr f fEMPTY A A) ∧
      ∀e s A0 A1.
        fITSETr f s A0 A1 ∧ ¬fIN e s ⇒ fITSETr f (fINSERT e s) A0 (f e A1)

fITSETr_strongind

⊢ ∀f fITSETr'.
    (∀A. fITSETr' fEMPTY A A) ∧
    (∀e s A0 A1.
       fITSETr f s A0 A1 ∧ fITSETr' s A0 A1 ∧ ¬fIN e s ⇒
       fITSETr' (fINSERT e s) A0 (f e A1)) ⇒
    ∀a0 a1 a2. fITSETr f a0 a1 a2 ⇒ fITSETr' a0 a1 a2

fITSETr_total

⊢ ∀s f a0. ∃a. fITSETr f s a0 a

fUNION_ASSOC

⊢ ∀s1 s2 s3. fUNION s1 (fUNION s2 s3) = fUNION (fUNION s1 s2) s3

fUNION_COMM

⊢ ∀s1 s2. fUNION s1 s2 = fUNION s2 s1

fUNION_EMPTY

⊢ ∀s. (fUNION fEMPTY s = s) ∧ (fUNION s fEMPTY = s)

fUNION_EQ_EMPTY

⊢ ∀s1 s2. (fUNION s1 s2 = fEMPTY) ⇔ (s1 = fEMPTY) ∧ (s2 = fEMPTY)

fUNION_IDEMPOT

⊢ ∀s. fUNION s s = s

fUNION_relates

⊢ (FSET $= |==> FSET $= |==> FSET $=) $++ fUNION

fsequiv_equiv

⊢ EQUIV fsequiv

fsequiv_refl

⊢ fsequiv l l

fset0Q

⊢ Qt fsequiv fset_ABS fset_REP (FSET $=)

fset_ABS_11

⊢ (fset_ABS l1 = fset_ABS l2) ⇔ fsequiv l1 l2

fset_ABS_REP

⊢ fset_ABS (fset_REP s) = s

fset_ABS_REP_CLASS

⊢ (∀a. fset_ABS_CLASS (fset_REP_CLASS a) = a) ∧
  ∀c. (∃r. fsequiv r r ∧ (c = fsequiv r)) ⇔
      (fset_REP_CLASS (fset_ABS_CLASS c) = c)

fset_ABS_onto

⊢ ∀fs. ∃l. fset_ABS l = fs

fset_QUOTIENT

⊢ QUOTIENT fsequiv fset_ABS fset_REP

fset_REP_11

⊢ (fset_REP fs1 = fset_REP fs2) ⇔ (fs1 = fs2)

fset_cases

⊢ ∀s. (s = fEMPTY) ∨ ∃e s0. (s = fINSERT e s0) ∧ ¬fIN e s0

fset_induction

⊢ ∀P. P fEMPTY ∧ (∀e s. P s ∧ ¬fIN e s ⇒ P (fINSERT e s)) ⇒ ∀s. P s

left_unique_rel_set

⊢ left_unique AB ⇒ left_unique (rel_set AB)

rel_setEQ

⊢ rel_set $= = $=

rel_set_RSUBSET

⊢ bi_unique AB ⇒ rel_set AB ⊆ᵣ AB |==> $<=>

rel_set_empty

⊢ rel_set AB ∅ ∅

right_unique_FSET0

⊢ right_unique (FSET $=)

right_unique_rel_set

⊢ right_unique AB ⇒ right_unique (rel_set AB)

set_BIGUNION

⊢ ∀fss. toSet (fBIGUNION fss) = BIGUNION (toSet (fIMAGE toSet fss))

set_IMAGE

⊢ ∀f fs. toSet (fIMAGE f fs) = IMAGE f (toSet fs)

surj_FSET0

⊢ surj (FSET $=)

surjfns

⊢ surj AB ∧ right_unique AB ∧ surj CD ⇒ surj (AB |==> CD)

toSet_11

⊢ ∀fs1 fs2. (toSet fs1 = toSet fs2) ⇔ (fs1 = fs2)

toSet_rel_set_relates

⊢ (FSET AB |==> rel_set AB) LIST_TO_SET toSet

toSet_relates

⊢ bi_unique AB ⇒ (FSET AB |==> AB |==> $<=>) LIST_TO_SET toSet

total_FSET

⊢ total AB ⇒ total (FSET AB)