Structure ordNotationSemanticsTheory

signature ordNotationSemanticsTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ordModel_def : thm
  
  (*  Theorems  *)
    val WF_ord_less : thm
    val addL_disappears : thm
    val add_disappears_kexp : thm
    val add_nat1_disappears : thm
    val add_nat1_disappears_kexp : thm
    val better_ord_mult_def : thm
    val better_pmult_def : thm
    val is_ord_expt : thm
    val kexp_lt : thm
    val kexp_mult : thm
    val kexp_sum_times_nat : thm
    val model_expt : thm
    val mvjar_lemma3 : thm
    val mvjar_lemma4 : thm
    val mvjar_lemma5 : thm
    val mvjar_theorem10 : thm
    val nat_times_omega : thm
    val notation_exists : thm
    val oless_0 : thm
    val oless_0a : thm
    val oless_modelled : thm
    val oless_total : thm
    val oless_x_End : thm
    val ordModel_11 : thm
    val ordModel_BIJ : thm
    val ordModel_lt_epsilon0 : thm
    val ord_add_correct : thm
    val ord_less_expt_monotone : thm
    val ord_less_modelled : thm
    val ord_less_models_ordlt : thm
    val ord_mult_correct : thm
    val osyntax_EQ_0 : thm
    val tail_dominated : thm
  
  val ordNotationSemantics_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [ordinal] Parent theory of "ordNotationSemantics"
   
   [ordinalNotation] Parent theory of "ordNotationSemantics"
   
   [ordModel_def]  Definition
      
      ⊢ (∀n. ⟦End n⟧ = &n) ∧ ∀e c t. ⟦Plus e c t⟧ = ω ** ⟦e⟧ * &c + ⟦t⟧
   
   [WF_ord_less]  Theorem
      
      ⊢ WF ord_less
   
   [addL_disappears]  Theorem
      
      ⊢ ∀e a. a < ω ** e ⇒ (a + ω ** e = ω ** e)
   
   [add_disappears_kexp]  Theorem
      
      ⊢ e ≠ 0 ∧ 0 < k ∧ a < ω ** e ⇒ (a + ω ** e * &k = ω ** e * &k)
   
   [add_nat1_disappears]  Theorem
      
      ⊢ ω ≤ a ⇒ (&n + a = a)
   
   [add_nat1_disappears_kexp]  Theorem
      
      ⊢ e ≠ 0 ∧ 0 < k ⇒ (&n + ω ** e * &k = ω ** e * &k)
   
   [better_ord_mult_def]  Theorem
      
      ⊢ ord_mult a (Plus be bc bt) =
        if a = End 0 then End 0
        else Plus (ord_add (expt a) be) bc (ord_mult a bt)
   
   [better_pmult_def]  Theorem
      
      ⊢ pmult a (Plus be bc bt) n =
        if a = End 0 then End 0
        else
          (let
             m = cf2 (expt a) be n
           in
             Plus (padd (expt a) be m) bc (pmult a bt m))
   
   [is_ord_expt]  Theorem
      
      ⊢ is_ord e ⇒ is_ord (expt e)
   
   [kexp_lt]  Theorem
      
      ⊢ e1 < e2 ⇒ ω ** e1 * &k < ω ** e2
   
   [kexp_mult]  Theorem
      
      ⊢ ∀e2 e1 c t.
            0 < e2 ∧ t < ω ** e1 ∧ 0 < c ⇒
            ((ω ** e1 * &c + t) * ω ** e2 = ω ** (e1 + e2))
   
   [kexp_sum_times_nat]  Theorem
      
      ⊢ ∀c2 c t e.
            0 < c2 ∧ 0 < c ∧ t < ω ** e ⇒
            ((ω ** e * &c + t) * &c2 = ω ** e * &(c * c2) + t)
   
   [model_expt]  Theorem
      
      ⊢ is_ord a ⇒ (⟦expt a⟧ = if a = End 0 then 0 else olog ⟦a⟧)
   
   [mvjar_lemma3]  Theorem
      
      ⊢ ord_less d b ⇒ cf1 a b ≤ cf1 a d
   
   [mvjar_lemma4]  Theorem
      
      ⊢ ∀a n b. n ≤ cf1 a b ⇒ (cf1 a b = cf2 a b n)
   
   [mvjar_lemma5]  Theorem
      
      ⊢ padd a b (cf1 a b) = ord_add a b
   
   [mvjar_theorem10]  Theorem
      
      ⊢ ∀n a b.
            is_ord a ∧ is_ord b ∧ n ≤ cf1 (expt a) (expt b) ⇒
            (⟦pmult a b n⟧ = ⟦a⟧ * ⟦b⟧)
   
   [nat_times_omega]  Theorem
      
      ⊢ ∀e m. 0 < m ∧ 0 < e ⇒ (&m * ω ** e = ω ** e)
   
   [notation_exists]  Theorem
      
      ⊢ ∀a.
            a < ε₀ ⇒
            ∃n. is_ord n ∧ (⟦n⟧ = a) ∧ (0 < a ⇒ (⟦expt n⟧ = olog a))
   
   [oless_0]  Theorem
      
      ⊢ ∀n. oless n (End 0) ⇔ F
   
   [oless_0a]  Theorem
      
      ⊢ oless (End 0) n ⇔ n ≠ End 0
   
   [oless_modelled]  Theorem
      
      ⊢ is_ord x ∧ is_ord y ⇒ (oless x y ⇔ ⟦x⟧ < ⟦y⟧)
   
   [oless_total]  Theorem
      
      ⊢ ∀m n. oless m n ∨ oless n m ∨ (m = n)
   
   [oless_x_End]  Theorem
      
      ⊢ oless x (End n) ⇔ ∃m. (x = End m) ∧ m < n
   
   [ordModel_11]  Theorem
      
      ⊢ is_ord n1 ∧ is_ord n2 ⇒ ((⟦n1⟧ = ⟦n2⟧) ⇔ (n1 = n2))
   
   [ordModel_BIJ]  Theorem
      
      ⊢ BIJ ordModel {n | is_ord n} {a | a < ε₀}
   
   [ordModel_lt_epsilon0]  Theorem
      
      ⊢ ∀a. ⟦a⟧ < ε₀
   
   [ord_add_correct]  Theorem
      
      ⊢ ∀x y. is_ord x ∧ is_ord y ⇒ (⟦ord_add x y⟧ = ⟦x⟧ + ⟦y⟧)
   
   [ord_less_expt_monotone]  Theorem
      
      ⊢ ord_less x y ⇒ (expt x = expt y) ∨ ord_less (expt x) (expt y)
   
   [ord_less_modelled]  Theorem
      
      ⊢ ord_less x y ⇔ is_ord x ∧ is_ord y ∧ ⟦x⟧ < ⟦y⟧
   
   [ord_less_models_ordlt]  Theorem
      
      ⊢ ∀x.
            is_ord x ⇒
            (∀y. oless x y ∧ is_ord y ⇒ ⟦x⟧ < ⟦y⟧) ∧
            (¬finp x ⇒ ⟦tail x⟧ < ω ** ⟦expt x⟧)
   
   [ord_mult_correct]  Theorem
      
      ⊢ ∀x y. is_ord x ∧ is_ord y ⇒ (⟦ord_mult x y⟧ = ⟦x⟧ * ⟦y⟧)
   
   [osyntax_EQ_0]  Theorem
      
      ⊢ ∀a. is_ord a ⇒ ((⟦a⟧ = 0) ⇔ (a = End 0))
   
   [tail_dominated]  Theorem
      
      ⊢ ⟦expt t⟧ < ⟦e⟧ ∧ is_ord e ∧ is_ord t ⇒ ⟦t⟧ < ω ** ⟦e⟧
   
   
*)
end

HOL 4, Kananaskis-13