Structure finite_setTheory

signature finite_setTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val FSET_def : thm
    val fBIGUNION_def : thm
    val fCARD_def : thm
    val fDELETE_def : thm
    val fDIFF_def : thm
    val fEMPTY_def : thm
    val fIMAGE_def : thm
    val fINSERT_def : thm
    val fINTER_def : thm
    val fIN_def : thm
    val fITSET_def : thm
    val fMAX_SET_def : thm
    val fSUM_IMAGE_def : thm
    val fUNION_def : thm
    val fromSet_def : thm
    val fsequiv_def : thm
    val fset_ABS_def : thm
    val fset_REL_def : thm
    val fset_REP_def : thm
    val fset_TY_DEF : thm
    val fset_bijections : thm
    val rel_set_def : thm
    val sfSETREL_def : thm
    val toSet_def : thm
  
  (*  Theorems  *)
    val ABS_CLASS_onto : thm
    val BIGUNION_relates : thm
    val DECOMPOSITION : thm
    val DELETE_EMPTY : thm
    val EXTENSION : thm
    val FINITE_toSet : thm
    val FLAT_relates : thm
    val FSETEQ : thm
    val FSET_AB_eqn : thm
    val FSET_right_unique : thm
    val FSET_surj : thm
    val FUN_REL_O : thm
    val FUN_REL_RSUBSET : thm
    val INSERT_DELETE : thm
    val IN_BIGUNION : thm
    val IN_DELETE : thm
    val IN_DIFF : thm
    val IN_IMAGE : thm
    val IN_INSERT : thm
    val IN_INTER : thm
    val IN_UNION : thm
    val IN_fromSet : thm
    val LIST_REL_FSET0 : thm
    val LIST_REL_FSET0_Abs : thm
    val LIST_TO_SET_rel_set : thm
    val LIST_TO_SET_transfer : thm
    val MAP_relates : thm
    val MEM_FSET0 : thm
    val MEM_transfers : thm
    val NOT_EMPTY_INSERT : thm
    val NOT_IN_EMPTY : thm
    val Qt_composes : thm
    val RDOM_FSET0 : thm
    val RDOM_FSET0set : thm
    val REP_ABS_equiv : thm
    val REP_CLASS_11 : thm
    val REP_CLASS_NONEMPTY : thm
    val RSUBSET_I : thm
    val RSUBSET_REFL : thm
    val RSUBSET_rel_set : thm
    val bijection2 : thm
    val equalityp_relset : thm
    val fABSORPTION : thm
    val fBIGUNION_relates : thm
    val fCARD_EQ0 : thm
    val fCARD_THM : thm
    val fCARD_relates : thm
    val fDELETE_INSERT : thm
    val fDELETE_UNION : thm
    val fDELETE_nonelement : thm
    val fDELETE_relates : thm
    val fDIFF_relates : thm
    val fEMPTY_relates : thm
    val fIMAGE_11 : thm
    val fIMAGE_COMPOSE : thm
    val fIMAGE_ID : thm
    val fIMAGE_relates : thm
    val fIMAGE_thm : thm
    val fINSERT_commutes : thm
    val fINSERT_duplicates : thm
    val fINSERT_relates : thm
    val fINSERT_sfSETREL : thm
    val fINTER_COMM : thm
    val fINTER_EMPTY : thm
    val fINTER_IDEMPOT : thm
    val fINTER_INSERT : thm
    val fINTER_relates : thm
    val fIN_IN : thm
    val fIN_fMAX_SET : thm
    val fIN_relates : thm
    val fIN_sfSETREL : thm
    val fITSET_EMPTY : thm
    val fITSET_INSERT : thm
    val fITSET_INSERT_tail : thm
    val fITSETr_cases : thm
    val fITSETr_functional : thm
    val fITSETr_ind : thm
    val fITSETr_rules : thm
    val fITSETr_strongind : thm
    val fITSETr_total : thm
    val fMAX_SET_SUBSET : thm
    val fMAX_SET_THM : thm
    val fMAX_SET_fIN : thm
    val fSUM_IMAGE_SUBSET : thm
    val fSUM_IMAGE_THM : thm
    val fSUM_IMAGE_UNION : thm
    val fUNION_ASSOC : thm
    val fUNION_COMM : thm
    val fUNION_EMPTY : thm
    val fUNION_EQ_EMPTY : thm
    val fUNION_IDEMPOT : thm
    val fUNION_INSERT : thm
    val fUNION_relates : thm
    val fUNION_sfSETREL : thm
    val fromSet_EMPTY : thm
    val fromSet_INSERT : thm
    val fromSet_toSet : thm
    val fsequiv_equiv : thm
    val fsequiv_refl : thm
    val fset0Q : thm
    val fset_ABS_11 : thm
    val fset_ABS_REP : thm
    val fset_ABS_REP_CLASS : thm
    val fset_ABS_onto : thm
    val fset_QUOTIENT : thm
    val fset_REP_11 : thm
    val fset_cases : thm
    val fset_induction : thm
    val left_unique_rel_set : thm
    val rel_setEQ : thm
    val rel_set_RSUBSET : thm
    val rel_set_empty : thm
    val right_unique_FSET0 : thm
    val right_unique_rel_set : thm
    val set_BIGUNION : thm
    val set_IMAGE : thm
    val surj_FSET0 : thm
    val surjfns : thm
    val toSet_11 : thm
    val toSet_Qt : thm
    val toSet_fromSet : thm
    val toSet_rel_set_relates : thm
    val toSet_relates : thm
    val total_FSET : thm
  
  val finite_set_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [lifting] Parent theory of "finite_set"
   
   [FSET_def]  Definition
      
      ⊢ ∀AB al bfs.
          FSET AB al bfs ⇔ ∃bl. LIST_REL AB al bl ∧ bfs = fset_ABS bl
   
   [fBIGUNION_def]  Definition
      
      ⊢ fBIGUNION = (MAP fset_REP ∘ fset_REP ---> fset_ABS) FLAT
   
   [fCARD_def]  Definition
      
      ⊢ fCARD = (fset_REP ---> I) (LENGTH ∘ nub)
   
   [fDELETE_def]  Definition
      
      ⊢ fDELETE = (I ---> fset_REP ---> fset_ABS) (λe. FILTER ($¬ ∘ $= e))
   
   [fDIFF_def]  Definition
      
      ⊢ fDIFF =
        (fset_REP ---> fset_REP ---> fset_ABS)
          (λl1 l2. FILTER (λx. ¬MEM x l2) l1)
   
   [fEMPTY_def]  Definition
      
      ⊢ fEMPTY = fset_ABS []
   
   [fIMAGE_def]  Definition
      
      ⊢ fIMAGE = ((I ---> I) ---> fset_REP ---> fset_ABS) MAP
   
   [fINSERT_def]  Definition
      
      ⊢ fINSERT = (I ---> fset_REP ---> fset_ABS) CONS
   
   [fINTER_def]  Definition
      
      ⊢ fINTER =
        (fset_REP ---> fset_REP ---> fset_ABS) (FILTER ∘ flip $IN ∘ set)
   
   [fIN_def]  Definition
      
      ⊢ fIN = (I ---> fset_REP ---> I) (λx l. MEM x l)
   
   [fITSET_def]  Definition
      
      ⊢ ∀f s a0. fITSET f s a0 = @a. fITSETr f s a0 a
   
   [fMAX_SET_def]  Definition
      
      ⊢ ∀s. fMAX_SET s = fITSET MAX s 0
   
   [fSUM_IMAGE_def]  Definition
      
      ⊢ ∀f s. fSUM_IMAGE f s = fITSET (λe a. f e + a) s 0
   
   [fUNION_def]  Definition
      
      ⊢ fUNION = (fset_REP ---> fset_REP ---> fset_ABS) $++
   
   [fromSet_def]  Definition
      
      ⊢ ∀s. fromSet s = ITSET fINSERT s fEMPTY
   
   [fsequiv_def]  Definition
      
      ⊢ ∀l1 l2. fsequiv l1 l2 ⇔ set l1 = set l2
   
   [fset_ABS_def]  Definition
      
      ⊢ ∀r. fset_ABS r = fset_ABS_CLASS (fsequiv r)
   
   [fset_REL_def]  Definition
      
      ⊢ ∀AB fs1 fs2.
          fset_REL AB fs1 fs2 ⇔ ∀a b. AB a b ⇒ (fIN a fs1 ⇔ fIN b fs2)
   
   [fset_REP_def]  Definition
      
      ⊢ ∀a. fset_REP a = $@ (fset_REP_CLASS a)
   
   [fset_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. fsequiv r r ∧ c = fsequiv r) rep
   
   [fset_bijections]  Definition
      
      ⊢ (∀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]  Definition
      
      ⊢ ∀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
   
   [sfSETREL_def]  Definition
      
      ⊢ ∀AB s fs.
          sfSETREL AB s fs ⇔
          (∀a. a ∈ s ⇒ ∃b. fIN b fs ∧ AB a b) ∧
          ∀b. fIN b fs ⇒ ∃a. a ∈ s ∧ AB a b
   
   [toSet_def]  Definition
      
      ⊢ ∀fs. toSet fs = {x | fIN x fs}
   
   [ABS_CLASS_onto]  Theorem
      
      ⊢ ∀fs. ∃r. fs = fset_ABS_CLASS (fsequiv r)
   
   [BIGUNION_relates]  Theorem
      
      ⊢ (rel_set (rel_set AB) |==> rel_set AB) BIGUNION BIGUNION
   
   [DECOMPOSITION]  Theorem
      
      ⊢ fIN e s ⇔ ∃s0. s = fINSERT e s0 ∧ ¬fIN e s0
   
   [DELETE_EMPTY]  Theorem
      
      ⊢ ∀e. fDELETE e fEMPTY = fEMPTY
   
   [EXTENSION]  Theorem
      
      ⊢ ∀s1 s2. s1 = s2 ⇔ ∀e. fIN e s1 ⇔ fIN e s2
   
   [FINITE_toSet]  Theorem
      
      ⊢ ∀s. FINITE (toSet s)
   
   [FLAT_relates]  Theorem
      
      ⊢ (LIST_REL (LIST_REL AB) |==> LIST_REL AB) FLAT FLAT
   
   [FSETEQ]  Theorem
      
      ⊢ (FSET0 |==> FSET0 |==> $<=>) fsequiv $=
   
   [FSET_AB_eqn]  Theorem
      
      ⊢ FSET AB = FSET0 ∘ᵣ LIST_REL AB
   
   [FSET_right_unique]  Theorem
      
      ⊢ right_unique AB ⇒ right_unique (FSET AB)
   
   [FSET_surj]  Theorem
      
      ⊢ surj AB ⇒ surj (FSET AB)
   
   [FUN_REL_O]  Theorem
      
      ⊢ (D1 |==> R1) ∘ᵣ (D2 |==> R2) ⊆ᵣ D1 ∘ᵣ D2 |==> R1 ∘ᵣ R2
   
   [FUN_REL_RSUBSET]  Theorem
      
      ⊢ D2 ⊆ᵣ D1 ∧ R1 ⊆ᵣ R2 ⇒ D1 |==> R1 ⊆ᵣ D2 |==> R2
   
   [INSERT_DELETE]  Theorem
      
      ⊢ ∀e s. fINSERT e (fDELETE e s) = fINSERT e s
   
   [IN_BIGUNION]  Theorem
      
      ⊢ fIN e (fBIGUNION fss) ⇔ ∃fs. fIN fs fss ∧ fIN e fs
   
   [IN_DELETE]  Theorem
      
      ⊢ ∀a b s. fIN a (fDELETE b s) ⇔ a ≠ b ∧ fIN a s
   
   [IN_DIFF]  Theorem
      
      ⊢ ∀e s1 s2. fIN e (fDIFF s1 s2) ⇔ fIN e s1 ∧ ¬fIN e s2
   
   [IN_IMAGE]  Theorem
      
      ⊢ ∀f x s. fIN x (fIMAGE f s) ⇔ ∃y. fIN y s ∧ x = f y
   
   [IN_INSERT]  Theorem
      
      ⊢ ∀e1 e2 s. fIN e1 (fINSERT e2 s) ⇔ e1 = e2 ∨ fIN e1 s
   
   [IN_INTER]  Theorem
      
      ⊢ ∀e s1 s2. fIN e (fINTER s1 s2) ⇔ fIN e s1 ∧ fIN e s2
   
   [IN_UNION]  Theorem
      
      ⊢ ∀e s1 s2. fIN e (fUNION s1 s2) ⇔ fIN e s1 ∨ fIN e s2
   
   [IN_fromSet]  Theorem
      
      ⊢ FINITE s ⇒ (fIN e (fromSet s) ⇔ e ∈ s)
   
   [LIST_REL_FSET0]  Theorem
      
      ⊢ Qt (LIST_REL fsequiv) (MAP fset_ABS) (MAP fset_REP)
          (LIST_REL FSET0)
   
   [LIST_REL_FSET0_Abs]  Theorem
      
      ⊢ LIST_REL FSET0 ll lfs ⇒ lfs = MAP fset_ABS ll
   
   [LIST_TO_SET_rel_set]  Theorem
      
      ⊢ (LIST_REL AB |==> rel_set AB) set set
   
   [LIST_TO_SET_transfer]  Theorem
      
      ⊢ (LIST_REL AB |==> rel_set AB) set set
   
   [MAP_relates]  Theorem
      
      ⊢ ((AB |==> CD) |==> LIST_REL AB |==> LIST_REL CD) MAP MAP
   
   [MEM_FSET0]  Theorem
      
      ⊢ FSET0 l fs ⇒ ∀a. MEM a l ⇔ fIN a fs
   
   [MEM_transfers]  Theorem
      
      ⊢ bi_unique AB ⇒
        (AB |==> LIST_REL AB |==> $<=>) (λx l. MEM x l) (λx l. MEM x l)
   
   [NOT_EMPTY_INSERT]  Theorem
      
      ⊢ ∀h t. fEMPTY ≠ fINSERT h t
   
   [NOT_IN_EMPTY]  Theorem
      
      ⊢ ∀e. ¬fIN e fEMPTY
   
   [Qt_composes]  Theorem
      
      ⊢ Qt R1 Abs1 Rep1 Tf1 ∧ Qt R2 Abs2 Rep2 Tf2 ⇒
        Qt (Tf1ᵀ ∘ᵣ R2 ∘ᵣ Tf1) (Abs2 ∘ Abs1) (Rep1 ∘ Rep2) (Tf2 ∘ᵣ Tf1)
   
   [RDOM_FSET0]  Theorem
      
      ⊢ RDOM (FSET AB) = (λal. ∀x. MEM x al ⇒ RDOM AB x)
   
   [RDOM_FSET0set]  Theorem
      
      ⊢ RDOM (FSET0 |==> $<=>) =
        (λlP. ∀l1 l2. lP l1 ∧ fsequiv l1 l2 ⇒ lP l2)
   
   [REP_ABS_equiv]  Theorem
      
      ⊢ fset_REP_CLASS (fset_ABS_CLASS (fsequiv r)) = fsequiv r
   
   [REP_CLASS_11]  Theorem
      
      ⊢ fset_REP_CLASS fs1 = fset_REP_CLASS fs2 ⇔ fs1 = fs2
   
   [REP_CLASS_NONEMPTY]  Theorem
      
      ⊢ ∀fs. ∃x. fset_REP_CLASS fs x
   
   [RSUBSET_I]  Theorem
      
      ⊢ R1 ⊆ᵣ R2 ⇒ R1 x y ⇒ R2 x y
   
   [RSUBSET_REFL]  Theorem
      
      ⊢ R ⊆ᵣ R
   
   [RSUBSET_rel_set]  Theorem
      
      ⊢ bitotal AB ⇒ AB |==> $<=> ⊆ᵣ rel_set AB
   
   [bijection2]  Theorem
      
      ⊢ ∀r. fset_REP_CLASS (fset_ABS_CLASS (fsequiv r)) = fsequiv r
   
   [equalityp_relset]  Theorem
      
      ⊢ equalityp AB ⇒ equalityp (rel_set AB)
   
   [fABSORPTION]  Theorem
      
      ⊢ ∀a A. fIN a A ⇔ fINSERT a A = A
   
   [fBIGUNION_relates]  Theorem
      
      ⊢ (FSET (FSET AB) |==> FSET AB) FLAT fBIGUNION
   
   [fCARD_EQ0]  Theorem
      
      ⊢ ∀s. fCARD s = 0 ⇔ s = fEMPTY
   
   [fCARD_THM]  Theorem
      
      ⊢ fCARD fEMPTY = 0 ∧
        ∀e s. fCARD (fINSERT e s) = 1 + fCARD (fDELETE e s)
   
   [fCARD_relates]  Theorem
      
      ⊢ (FSET0 |==> $=) (LENGTH ∘ nub) fCARD
   
   [fDELETE_INSERT]  Theorem
      
      ⊢ fDELETE a (fINSERT a A) = fDELETE a A
   
   [fDELETE_UNION]  Theorem
      
      ⊢ fDELETE e (fUNION A B) = fUNION (fDELETE e A) (fDELETE e B)
   
   [fDELETE_nonelement]  Theorem
      
      ⊢ ∀e s. ¬fIN e s ⇒ fDELETE e s = s
   
   [fDELETE_relates]  Theorem
      
      ⊢ ($= |==> FSET0 |==> FSET0) (λe. FILTER ($¬ ∘ $= e)) fDELETE
   
   [fDIFF_relates]  Theorem
      
      ⊢ (FSET0 |==> FSET0 |==> FSET0) (λl1 l2. FILTER (λx. ¬MEM x l2) l1)
          fDIFF
   
   [fEMPTY_relates]  Theorem
      
      ⊢ FSET0 [] fEMPTY
   
   [fIMAGE_11]  Theorem
      
      ⊢ (∀x y. f x = f y ⇔ x = y) ⇒ (fIMAGE f x = fIMAGE f y ⇔ x = y)
   
   [fIMAGE_COMPOSE]  Theorem
      
      ⊢ fIMAGE (f ∘ g) s = fIMAGE f (fIMAGE g s)
   
   [fIMAGE_ID]  Theorem
      
      ⊢ fIMAGE (λx. x) s = s ∧ fIMAGE I s = s
   
   [fIMAGE_relates]  Theorem
      
      ⊢ ((AB |==> CD) |==> FSET AB |==> FSET CD) MAP fIMAGE
   
   [fIMAGE_thm]  Theorem
      
      ⊢ (∀f. fIMAGE f fEMPTY = fEMPTY) ∧
        ∀f e s. fIMAGE f (fINSERT e s) = fINSERT (f e) (fIMAGE f s)
   
   [fINSERT_commutes]  Theorem
      
      ⊢ ∀e1 e2 s. fINSERT e1 (fINSERT e2 s) = fINSERT e2 (fINSERT e1 s)
   
   [fINSERT_duplicates]  Theorem
      
      ⊢ ∀e s. fINSERT e (fINSERT e s) = fINSERT e s
   
   [fINSERT_relates]  Theorem
      
      ⊢ ($= |==> FSET0 |==> FSET0) CONS fINSERT
   
   [fINSERT_sfSETREL]  Theorem
      
      ⊢ (AB |==> sfSETREL AB |==> sfSETREL AB) $INSERT fINSERT
   
   [fINTER_COMM]  Theorem
      
      ⊢ fINTER a b = fINTER b a
   
   [fINTER_EMPTY]  Theorem
      
      ⊢ ∀x. fINTER x fEMPTY = fEMPTY ∧ fINTER fEMPTY x = fEMPTY
   
   [fINTER_IDEMPOT]  Theorem
      
      ⊢ ∀x. fINTER x x = x
   
   [fINTER_INSERT]  Theorem
      
      ⊢ fINTER (fINSERT a A) B =
        (if fIN a B then fINSERT a (fINTER A B) else fINTER A B) ∧
        fINTER A (fINSERT b B) =
        if fIN b A then fINSERT b (fINTER A B) else fINTER A B
   
   [fINTER_relates]  Theorem
      
      ⊢ (FSET0 |==> FSET0 |==> FSET0) (FILTER ∘ flip $IN ∘ set) fINTER
   
   [fIN_IN]  Theorem
      
      ⊢ ∀e fs. fIN e fs ⇔ e ∈ toSet fs
   
   [fIN_fMAX_SET]  Theorem
      
      ⊢ ∀A e. fIN e A ⇒ e ≤ fMAX_SET A
   
   [fIN_relates]  Theorem
      
      ⊢ bi_unique AB ⇒ (AB |==> FSET AB |==> $<=>) (λx l. MEM x l) fIN
   
   [fIN_sfSETREL]  Theorem
      
      ⊢ bi_unique AB ⇒ (AB |==> sfSETREL AB |==> $<=>) $IN fIN
   
   [fITSET_EMPTY]  Theorem
      
      ⊢ fITSET f fEMPTY a = a
   
   [fITSET_INSERT]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀s f a0. ∃a. fITSETr f s a0 a
   
   [fMAX_SET_SUBSET]  Theorem
      
      ⊢ ∀A B. (∀e. fIN e A ⇒ fIN e B) ⇒ fMAX_SET A ≤ fMAX_SET B
   
   [fMAX_SET_THM]  Theorem
      
      ⊢ fMAX_SET fEMPTY = 0 ∧ fMAX_SET (fINSERT e A) = MAX e (fMAX_SET A)
   
   [fMAX_SET_fIN]  Theorem
      
      ⊢ A ≠ fEMPTY ⇒ fIN (fMAX_SET A) A
   
   [fSUM_IMAGE_SUBSET]  Theorem
      
      ⊢ ∀A B. (∀a. fIN a A ⇒ fIN a B) ⇒ fSUM_IMAGE f A ≤ fSUM_IMAGE f B
   
   [fSUM_IMAGE_THM]  Theorem
      
      ⊢ fSUM_IMAGE f fEMPTY = 0 ∧
        fSUM_IMAGE f (fINSERT e A) = f e + fSUM_IMAGE f (fDELETE e A)
   
   [fSUM_IMAGE_UNION]  Theorem
      
      ⊢ ∀A B.
          fSUM_IMAGE f (fUNION A B) =
          fSUM_IMAGE f A + fSUM_IMAGE f B − fSUM_IMAGE f (fINTER A B)
   
   [fUNION_ASSOC]  Theorem
      
      ⊢ ∀s1 s2 s3. fUNION s1 (fUNION s2 s3) = fUNION (fUNION s1 s2) s3
   
   [fUNION_COMM]  Theorem
      
      ⊢ ∀s1 s2. fUNION s1 s2 = fUNION s2 s1
   
   [fUNION_EMPTY]  Theorem
      
      ⊢ ∀s. fUNION fEMPTY s = s ∧ fUNION s fEMPTY = s
   
   [fUNION_EQ_EMPTY]  Theorem
      
      ⊢ ∀s1 s2. fUNION s1 s2 = fEMPTY ⇔ s1 = fEMPTY ∧ s2 = fEMPTY
   
   [fUNION_IDEMPOT]  Theorem
      
      ⊢ ∀s. fUNION s s = s
   
   [fUNION_INSERT]  Theorem
      
      ⊢ fUNION (fINSERT a A) B = fINSERT a (fUNION A B)
   
   [fUNION_relates]  Theorem
      
      ⊢ (FSET0 |==> FSET0 |==> FSET0) $++ fUNION
   
   [fUNION_sfSETREL]  Theorem
      
      ⊢ (sfSETREL AB |==> sfSETREL AB |==> sfSETREL AB) $UNION fUNION
   
   [fromSet_EMPTY]  Theorem
      
      ⊢ fromSet ∅ = fEMPTY
   
   [fromSet_INSERT]  Theorem
      
      ⊢ FINITE s ⇒ fromSet (e INSERT s) = fINSERT e (fromSet s)
   
   [fromSet_toSet]  Theorem
      
      ⊢ fromSet (toSet s) = s
   
   [fsequiv_equiv]  Theorem
      
      ⊢ EQUIV fsequiv
   
   [fsequiv_refl]  Theorem
      
      ⊢ fsequiv l l
   
   [fset0Q]  Theorem
      
      ⊢ Qt fsequiv fset_ABS fset_REP FSET0
   
   [fset_ABS_11]  Theorem
      
      ⊢ fset_ABS l1 = fset_ABS l2 ⇔ fsequiv l1 l2
   
   [fset_ABS_REP]  Theorem
      
      ⊢ fset_ABS (fset_REP s) = s
   
   [fset_ABS_REP_CLASS]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀fs. ∃l. fset_ABS l = fs
   
   [fset_QUOTIENT]  Theorem
      
      ⊢ QUOTIENT fsequiv fset_ABS fset_REP
   
   [fset_REP_11]  Theorem
      
      ⊢ fset_REP fs1 = fset_REP fs2 ⇔ fs1 = fs2
   
   [fset_cases]  Theorem
      
      ⊢ ∀s. s = fEMPTY ∨ ∃e s0. s = fINSERT e s0 ∧ ¬fIN e s0
   
   [fset_induction]  Theorem
      
      ⊢ ∀P. P fEMPTY ∧ (∀e s. P s ∧ ¬fIN e s ⇒ P (fINSERT e s)) ⇒ ∀s. P s
   
   [left_unique_rel_set]  Theorem
      
      ⊢ left_unique AB ⇒ left_unique (rel_set AB)
   
   [rel_setEQ]  Theorem
      
      ⊢ rel_set $= = $=
   
   [rel_set_RSUBSET]  Theorem
      
      ⊢ bi_unique AB ⇒ rel_set AB ⊆ᵣ AB |==> $<=>
   
   [rel_set_empty]  Theorem
      
      ⊢ rel_set AB ∅ ∅
   
   [right_unique_FSET0]  Theorem
      
      ⊢ right_unique FSET0
   
   [right_unique_rel_set]  Theorem
      
      ⊢ right_unique AB ⇒ right_unique (rel_set AB)
   
   [set_BIGUNION]  Theorem
      
      ⊢ ∀fss. toSet (fBIGUNION fss) = BIGUNION (toSet (fIMAGE toSet fss))
   
   [set_IMAGE]  Theorem
      
      ⊢ ∀f fs. toSet (fIMAGE f fs) = IMAGE f (toSet fs)
   
   [surj_FSET0]  Theorem
      
      ⊢ surj FSET0
   
   [surjfns]  Theorem
      
      ⊢ surj AB ∧ right_unique AB ∧ surj CD ⇒ surj (AB |==> CD)
   
   [toSet_11]  Theorem
      
      ⊢ ∀fs1 fs2. toSet fs1 = toSet fs2 ⇔ fs1 = fs2
   
   [toSet_Qt]  Theorem
      
      ⊢ Qt (λx y. FINITE x ∧ x = y) fromSet toSet (λs fs. s = toSet fs)
   
   [toSet_fromSet]  Theorem
      
      ⊢ FINITE s ⇒ toSet (fromSet s) = s
   
   [toSet_rel_set_relates]  Theorem
      
      ⊢ (FSET AB |==> rel_set AB) set toSet
   
   [toSet_relates]  Theorem
      
      ⊢ bi_unique AB ⇒ (FSET AB |==> AB |==> $<=>) set toSet
   
   [total_FSET]  Theorem
      
      ⊢ total AB ⇒ total (FSET AB)
   
   
*)
end

HOL 4, Trindemossen-1