Structure ucordTheory

signature ucordTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val omega1_def : thm
  
  (*  Theorems  *)
    val Unum_cardle_ucinf : thm
    val Unum_cardlt_ucinf : thm
    val omega1_not_countable : thm
    val ucinf_uncountable : thm
    val ucord_sup_exists_lemma : thm
    val x_lt_omega1_countable : thm
  
  val ucord_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [ordinal] Parent theory of "ucord"
   
   [omega1_def]  Definition
      
      ⊢ ω₁ = sup {a | countableOrd a}
   
   [Unum_cardle_ucinf]  Theorem
      
      ⊢ 𝕌(:num) ≼ 𝕌(:num + α + (num -> bool))
   
   [Unum_cardlt_ucinf]  Theorem
      
      ⊢ 𝕌(:num) ≺ 𝕌(:num + α + (num -> bool))
   
   [omega1_not_countable]  Theorem
      
      ⊢ ¬countableOrd ω₁
   
   [ucinf_uncountable]  Theorem
      
      ⊢ ¬COUNTABLE 𝕌(:num + α + (num -> bool))
   
   [ucord_sup_exists_lemma]  Theorem
      
      ⊢ {a | countableOrd a} ≼ 𝕌(:num + α + (num -> bool))
   
   [x_lt_omega1_countable]  Theorem
      
      ⊢ x < ω₁ ⇔ countableOrd x
   
   
*)
end

HOL 4, Kananaskis-13