Structure cardinalTheory

signature cardinalTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val bijns_def : thm
    val cardeq_def : thm
    val cardleq_def : thm
    val list_def : thm
    val set_exp_def : thm
  
  (*  Theorems  *)
    val BIJ_functions_agree : thm
    val CANTOR : thm
    val CARDEQ_0 : thm
    val CARDEQ_CARD : thm
    val CARDEQ_CARDLEQ : thm
    val CARDEQ_CARD_EQN : thm
    val CARDEQ_CROSS : thm
    val CARDEQ_CROSS_SYM : thm
    val CARDEQ_FINITE : thm
    val CARDEQ_INSERT_RWT : thm
    val CARDEQ_SUBSET_CARDLEQ : thm
    val CARDLEQ_CARD : thm
    val CARDLEQ_CROSS_CONG : thm
    val CARDLEQ_FINITE : thm
    val CARD_BIGUNION : thm
    val CARD_CARDEQ_I : thm
    val CARD_LT_CARD : thm
    val CARD_MUL_ABSORB_LE : thm
    val CARD_MUL_LT_INFINITE : thm
    val CARD_MUL_LT_LEMMA : thm
    val COUNT_EQ_EMPTY : thm
    val EMPTY_CARDLEQ : thm
    val EMPTY_set_exp : thm
    val EMPTY_set_exp_CARD : thm
    val FINITE_CLE_INFINITE : thm
    val FINITE_IMAGE_INJ' : thm
    val IMAGE_cardleq : thm
    val IMAGE_cardleq_rwt : thm
    val INFINITE_A_list_BIJ_A : thm
    val INFINITE_UNIV_INF : thm
    val INFINITE_Unum : thm
    val INFINITE_cardleq_INSERT : thm
    val POW_EQ_X_EXP_X : thm
    val POW_TWO_set_exp : thm
    val SET_SQUARED_CARDEQ_SET : thm
    val SET_SUM_CARDEQ_SET : thm
    val SING_set_exp : thm
    val SING_set_exp_CARD : thm
    val SUBSET_CARDLEQ : thm
    val UNIV_list : thm
    val bijections_cardeq : thm
    val cardeq_INSERT : thm
    val cardeq_REFL : thm
    val cardeq_SYM : thm
    val cardeq_TRANS : thm
    val cardeq_bijns_cong : thm
    val cardleq_ANTISYM : thm
    val cardleq_REFL : thm
    val cardleq_SURJ : thm
    val cardleq_TRANS : thm
    val cardleq_dichotomy : thm
    val cardleq_empty : thm
    val cardleq_lt_trans : thm
    val cardleq_lteq : thm
    val cardlt_REFL : thm
    val cardlt_TRANS : thm
    val cardlt_cardle : thm
    val cardlt_lenoteq : thm
    val cardlt_leq_trans : thm
    val count_cardle : thm
    val countable_cardeq : thm
    val countable_decomposition : thm
    val countable_thm : thm
    val disjoint_countable_decomposition : thm
    val exp_INSERT_cardeq : thm
    val exp_count_cardeq : thm
    val finite_subsets_bijection : thm
    val list_BIGUNION_EXP : thm
    val list_EMPTY : thm
    val list_SING : thm
    val set_binomial2 : thm
    val set_exp_card_cong : thm
    val set_exp_cardle_cong : thm
    val set_exp_count : thm
    val set_exp_product : thm
  
  val cardinal_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [wellorder] Parent theory of "cardinal"
   
   [bijns_def]  Definition
      
      ⊢ ∀A.
            bijns A =
            {f | THE ∘ f PERMUTES A ∧ ∀a. a ∈ A ⇔ ∃b. f a = SOME b}
   
   [cardeq_def]  Definition
      
      ⊢ ∀s1 s2. s1 ≈ s2 ⇔ ∃f. BIJ f s1 s2
   
   [cardleq_def]  Definition
      
      ⊢ ∀s1 s2. s1 ≼ s2 ⇔ ∃f. INJ f s1 s2
   
   [list_def]  Definition
      
      ⊢ ∀A. list A = {l | ∀e. MEM e l ⇒ e ∈ A}
   
   [set_exp_def]  Definition
      
      ⊢ ∀A B.
            A ** B =
            {f |
            (∀b. b ∈ B ⇒ ∃a. a ∈ A ∧ (f b = SOME a)) ∧
            ∀b. b ∉ B ⇒ (f b = NONE)}
   
   [BIJ_functions_agree]  Theorem
      
      ⊢ ∀f g s t. BIJ f s t ∧ (∀x. x ∈ s ⇒ (f x = g x)) ⇒ BIJ g s t
   
   [CANTOR]  Theorem
      
      ⊢ A <</= POW A
   
   [CARDEQ_0]  Theorem
      
      ⊢ (x ≈ ∅ ⇔ (x = ∅)) ∧ (∅ ≈ x ⇔ (x = ∅))
   
   [CARDEQ_CARD]  Theorem
      
      ⊢ s1 ≈ s2 ∧ FINITE s1 ⇒ (CARD s1 = CARD s2)
   
   [CARDEQ_CARDLEQ]  Theorem
      
      ⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ (s1 ≼ t1 ⇔ s2 ≼ t2)
   
   [CARDEQ_CARD_EQN]  Theorem
      
      ⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≈ s2 ⇔ (CARD s1 = CARD s2))
   
   [CARDEQ_CROSS]  Theorem
      
      ⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ s1 × t1 ≈ s2 × t2
   
   [CARDEQ_CROSS_SYM]  Theorem
      
      ⊢ s × t ≈ t × s
   
   [CARDEQ_FINITE]  Theorem
      
      ⊢ s1 ≈ s2 ⇒ (FINITE s1 ⇔ FINITE s2)
   
   [CARDEQ_INSERT_RWT]  Theorem
      
      ⊢ ∀s. INFINITE s ⇒ x INSERT s ≈ s
   
   [CARDEQ_SUBSET_CARDLEQ]  Theorem
      
      ⊢ s ≈ t ⇒ s ≼ t
   
   [CARDLEQ_CARD]  Theorem
      
      ⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≼ s2 ⇔ CARD s1 ≤ CARD s2)
   
   [CARDLEQ_CROSS_CONG]  Theorem
      
      ⊢ x1 ≼ x2 ∧ y1 ≼ y2 ⇒ x1 × y1 ≼ x2 × y2
   
   [CARDLEQ_FINITE]  Theorem
      
      ⊢ ∀s1 s2. FINITE s2 ∧ s1 ≼ s2 ⇒ FINITE s1
   
   [CARD_BIGUNION]  Theorem
      
      ⊢ INFINITE k ∧ s1 ≼ k ∧ (∀e. e ∈ s1 ⇒ e ≼ k) ⇒ BIGUNION s1 ≼ k
   
   [CARD_CARDEQ_I]  Theorem
      
      ⊢ FINITE s1 ∧ FINITE s2 ∧ (CARD s1 = CARD s2) ⇒ s1 ≈ s2
   
   [CARD_LT_CARD]  Theorem
      
      ⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 <</= s2 ⇔ CARD s1 < CARD s2)
   
   [CARD_MUL_ABSORB_LE]  Theorem
      
      ⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s × t ≼ t
   
   [CARD_MUL_LT_INFINITE]  Theorem
      
      ⊢ ∀s t. s <</= t ∧ t <</= u ∧ INFINITE u ⇒ s × t <</= u
   
   [CARD_MUL_LT_LEMMA]  Theorem
      
      ⊢ ∀s t. s ≼ t ∧ t <</= u ∧ INFINITE u ⇒ s × t <</= u
   
   [COUNT_EQ_EMPTY]  Theorem
      
      ⊢ (count n = ∅) ⇔ (n = 0)
   
   [EMPTY_CARDLEQ]  Theorem
      
      ⊢ ∅ ≼ t
   
   [EMPTY_set_exp]  Theorem
      
      ⊢ (A ** ∅ = {K NONE}) ∧ (B ≠ ∅ ⇒ (∅ ** B = ∅))
   
   [EMPTY_set_exp_CARD]  Theorem
      
      ⊢ A ** ∅ ≈ count 1
   
   [FINITE_CLE_INFINITE]  Theorem
      
      ⊢ FINITE s ∧ INFINITE t ⇒ s ≼ t
   
   [FINITE_IMAGE_INJ']  Theorem
      
      ⊢ (∀x y. x ∈ s ∧ y ∈ s ⇒ ((f x = f y) ⇔ (x = y))) ⇒
        (FINITE (IMAGE f s) ⇔ FINITE s)
   
   [IMAGE_cardleq]  Theorem
      
      ⊢ IMAGE f s ≼ s
   
   [IMAGE_cardleq_rwt]  Theorem
      
      ⊢ s ≼ t ⇒ IMAGE f s ≼ t
   
   [INFINITE_A_list_BIJ_A]  Theorem
      
      ⊢ INFINITE A ⇒ list A ≈ A
   
   [INFINITE_UNIV_INF]  Theorem
      
      ⊢ INFINITE 𝕌(:α inf)
   
   [INFINITE_Unum]  Theorem
      
      ⊢ INFINITE A ⇔ 𝕌(:num) ≼ A
   
   [INFINITE_cardleq_INSERT]  Theorem
      
      ⊢ INFINITE A ⇒ (x INSERT s ≼ A ⇔ s ≼ A)
   
   [POW_EQ_X_EXP_X]  Theorem
      
      ⊢ INFINITE A ⇒ POW A ≈ A ** A
   
   [POW_TWO_set_exp]  Theorem
      
      ⊢ POW A ≈ count 2 ** A
   
   [SET_SQUARED_CARDEQ_SET]  Theorem
      
      ⊢ INFINITE s ⇒ s × s ≈ s
   
   [SET_SUM_CARDEQ_SET]  Theorem
      
      ⊢ INFINITE s ⇒
        s ≈ {T; F} × s ∧ ∀A B. DISJOINT A B ∧ A ≈ s ∧ B ≈ s ⇒ A ∪ B ≈ s
   
   [SING_set_exp]  Theorem
      
      ⊢ ({x} ** B = {(λb. if b ∈ B then SOME x else NONE)}) ∧
        (A ** {x} = {(λb. if b = x then SOME a else NONE) | a ∈ A})
   
   [SING_set_exp_CARD]  Theorem
      
      ⊢ {x} ** B ≈ count 1 ∧ A ** {x} ≈ A
   
   [SUBSET_CARDLEQ]  Theorem
      
      ⊢ x ⊆ y ⇒ x ≼ y
   
   [UNIV_list]  Theorem
      
      ⊢ 𝕌(:α list) = list 𝕌(:α)
   
   [bijections_cardeq]  Theorem
      
      ⊢ INFINITE s ⇒ bijns s ≈ POW s
   
   [cardeq_INSERT]  Theorem
      
      ⊢ x INSERT s ≈ s ⇔ x ∈ s ∨ INFINITE s
   
   [cardeq_REFL]  Theorem
      
      ⊢ ∀s. s ≈ s
   
   [cardeq_SYM]  Theorem
      
      ⊢ ∀s t. s ≈ t ⇔ t ≈ s
   
   [cardeq_TRANS]  Theorem
      
      ⊢ ∀s t u. s ≈ t ∧ t ≈ u ⇒ s ≈ u
   
   [cardeq_bijns_cong]  Theorem
      
      ⊢ A ≈ B ⇒ bijns A ≈ bijns B
   
   [cardleq_ANTISYM]  Theorem
      
      ⊢ ∀s t. s ≼ t ∧ t ≼ s ⇒ s ≈ t
   
   [cardleq_REFL]  Theorem
      
      ⊢ ∀s. s ≼ s
   
   [cardleq_SURJ]  Theorem
      
      ⊢ A ≼ B ⇔ (∃f. SURJ f B A) ∨ (A = ∅)
   
   [cardleq_TRANS]  Theorem
      
      ⊢ ∀s t u. s ≼ t ∧ t ≼ u ⇒ s ≼ u
   
   [cardleq_dichotomy]  Theorem
      
      ⊢ s ≼ t ∨ t ≼ s
   
   [cardleq_empty]  Theorem
      
      ⊢ x ≼ ∅ ⇔ (x = ∅)
   
   [cardleq_lt_trans]  Theorem
      
      ⊢ ∀r s t. r ≼ s ∧ s <</= t ⇒ r <</= t
   
   [cardleq_lteq]  Theorem
      
      ⊢ s1 ≼ s2 ⇔ s1 <</= s2 ∨ s1 ≈ s2
   
   [cardlt_REFL]  Theorem
      
      ⊢ ¬(s <</= s)
   
   [cardlt_TRANS]  Theorem
      
      ⊢ ∀s t u. s <</= t ∧ t <</= u ⇒ s <</= u
   
   [cardlt_cardle]  Theorem
      
      ⊢ A <</= B ⇒ A ≼ B
   
   [cardlt_lenoteq]  Theorem
      
      ⊢ s <</= t ⇔ s ≼ t ∧ ¬(s ≈ t)
   
   [cardlt_leq_trans]  Theorem
      
      ⊢ ∀r s t. r <</= s ∧ s ≼ t ⇒ r <</= t
   
   [count_cardle]  Theorem
      
      ⊢ count n ≼ A ⇔ FINITE A ⇒ n ≤ CARD A
   
   [countable_cardeq]  Theorem
      
      ⊢ s ≈ t ⇒ (countable s ⇔ countable t)
   
   [countable_decomposition]  Theorem
      
      ⊢ ∀s.
            INFINITE s ⇒
            ∃A. (BIGUNION A = s) ∧ ∀a. a ∈ A ⇒ INFINITE a ∧ countable a
   
   [countable_thm]  Theorem
      
      ⊢ countable s ⇔ s ≼ 𝕌(:num)
   
   [disjoint_countable_decomposition]  Theorem
      
      ⊢ ∀s.
            INFINITE s ⇒
            ∃A.
                (BIGUNION A = s) ∧ (∀a. a ∈ A ⇒ INFINITE a ∧ countable a) ∧
                ∀a1 a2. a1 ∈ A ∧ a2 ∈ A ∧ a1 ≠ a2 ⇒ DISJOINT a1 a2
   
   [exp_INSERT_cardeq]  Theorem
      
      ⊢ e ∉ s ⇒ A ** (e INSERT s) ≈ A × A ** s
   
   [exp_count_cardeq]  Theorem
      
      ⊢ INFINITE A ∧ 0 < n ⇒ A ** count n ≈ A
   
   [finite_subsets_bijection]  Theorem
      
      ⊢ INFINITE A ⇒ A ≈ {s | FINITE s ∧ s ⊆ A}
   
   [list_BIGUNION_EXP]  Theorem
      
      ⊢ list A ≈ BIGUNION (IMAGE (λn. A ** count n) 𝕌(:num))
   
   [list_EMPTY]  Theorem
      
      ⊢ list ∅ = {[]}
   
   [list_SING]  Theorem
      
      ⊢ list {e} ≈ 𝕌(:num)
   
   [set_binomial2]  Theorem
      
      ⊢ (A ∪ B) × (A ∪ B) = A × A ∪ A × B ∪ B × A ∪ B × B
   
   [set_exp_card_cong]  Theorem
      
      ⊢ a1 ≈ a2 ⇒ b1 ≈ b2 ⇒ a1 ** b1 ≈ a2 ** b2
   
   [set_exp_cardle_cong]  Theorem
      
      ⊢ ((b = ∅) ⇒ (d = ∅)) ⇒ a ≼ b ∧ c ≼ d ⇒ a ** c ≼ b ** d
   
   [set_exp_count]  Theorem
      
      ⊢ A ** count n ≈ {l | (LENGTH l = n) ∧ ∀e. MEM e l ⇒ e ∈ A}
   
   [set_exp_product]  Theorem
      
      ⊢ (A ** B1) ** B2 ≈ A ** (B1 × B2)
   
   
*)
end

HOL 4, Kananaskis-11