Structure veblenTheory

signature veblenTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val closed_def : thm
    val club_def : thm
    val continuous_def : thm
    val strict_mono_def : thm
    val unbounded_def : thm
  
  (*  Theorems  *)
    val better_induction : thm
    val club_INTER : thm
    val clubs_exist : thm
    val increasing : thm
    val mono_natI : thm
    val nrange_IN_Uinf : thm
    val oleast_leq : thm
    val sup_mem_INTER : thm
  
  val veblen_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [ordinal] Parent theory of "veblen"
   
   [closed_def]  Definition
      
      ⊢ ∀A. closed A ⇔ ∀g. (∀n. g n ∈ A) ⇒ sup {g n | n | T} ∈ A
   
   [club_def]  Definition
      
      ⊢ ∀A. club A ⇔ closed A ∧ unbounded A
   
   [continuous_def]  Definition
      
      ⊢ ∀f. continuous f ⇔
            ∀A. A ≼ 𝕌(:num + α) ⇒ f (sup A) = sup (IMAGE f A)
   
   [strict_mono_def]  Definition
      
      ⊢ ∀f. strict_mono f ⇔ ∀x y. x < y ⇒ f x < f y
   
   [unbounded_def]  Definition
      
      ⊢ ∀A. unbounded A ⇔ ∀a. ∃b. b ∈ A ∧ a < b
   
   [better_induction]  Theorem
      
      ⊢ ∀P. P 0 ∧ (∀a. P a ⇒ P a⁺) ∧
            (∀a. 0 < a ∧ (∀b. b < a ⇒ P b) ⇒ P (sup (preds a))) ⇒
            ∀a. P a
   
   [club_INTER]  Theorem
      
      ⊢ (∀n. club (A n)) ∧ (∀n. A (SUC n) ⊆ A n) ⇒
        club (BIGINTER {A n | n | T})
   
   [clubs_exist]  Theorem
      
      ⊢ strict_mono f ∧ continuous f ⇒ club (IMAGE f 𝕌(:α ordinal))
   
   [increasing]  Theorem
      
      ⊢ ∀f x. strict_mono f ∧ continuous f ⇒ x ≤ f x
   
   [mono_natI]  Theorem
      
      ⊢ (∀n. f n ≤ f (SUC n)) ⇒ ∀m n. m ≤ n ⇒ f m ≤ f n
   
   [nrange_IN_Uinf]  Theorem
      
      ⊢ {f n | n | T} ≼ 𝕌(:num + α)
   
   [oleast_leq]  Theorem
      
      ⊢ ∀P a. P a ⇒ $oleast P ≤ a
   
   [sup_mem_INTER]  Theorem
      
      ⊢ (∀n. club (A n)) ∧ (∀n. A (SUC n) ⊆ A n) ∧ (∀n. f n ∈ A n) ∧
        (∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
        sup {f n | n | T} ∈ BIGINTER {A n | n | T}
   
   
*)
end

HOL 4, Kananaskis-14