Theory CZH_Sets_Ordinals

(* Copyright 2021 (C) Mihails Milehins *)

section‹Further results about ordinal numbers›
theory CZH_Sets_Ordinals
  imports 
    CZH_Sets_Nat
    CZH_Sets_IF
    Complex_Main
begin



subsection‹Background›


text‹
The subsection presents several results about ordinal 
numbers. The primary general reference for this section 
is cite‹"takeuti_introduction_1971"›.
›

lemmas [intro] = Limit_is_Ord Ord_in_Ord



subsection‹Further ordinal arithmetic and inequalities›


lemma Ord_succ_mono:
  assumes "Ord β" and "α ∈∘ β"
  shows "succ α ∈∘ succ β"
proof-
  from assms have "Ord α" by blast
  from assms ‹Ord α› have "α < β" by (auto dest: Ord_mem_iff_lt)
  from assms(1,2) this have "succ α < succ β"
    by (meson assms ‹Ord α› Ord_linear2 Ord_succ leD le_succ_iff)
  with assms(1) ‹Ord α› Ord_mem_iff_lt show "succ α ∈∘ succ β" by blast
qed

lemma Limit_right_Limit_mult:
  ―‹Based on Theorem 8.23 in \cite{takeuti_introduction_1971}.›
  assumes "Ord α" and "Limit β" and "0 ∈∘ α" 
  shows "Limit (α * β)"
proof-
  have αβ: "α * β = (⋃∘ξ∈∘β. α * ξ)" by (rule mult_Limit[OF assms(2), of α])
  from assms(1,2) Ord_mult have "Ord (α * β)" by blast
  then show ?thesis 
  proof(cases rule: Ord_cases)
    case (succ γ)
    from succ(1) have "γ ∈∘ α * β" unfolding succ(2)[symmetric] by simp
    then obtain ξ where "ξ ∈∘ β" and "γ ∈∘ α * ξ" unfolding αβ by auto
    moreover with assms(2) have "Ord ξ" by auto
    ultimately have sγ_sαξ: "succ γ ∈∘ succ (α * ξ)"
      using assms(1) Ord_succ_mono by simp
    from assms(2,3) have "succ (α * ξ) ⊆∘ α * ξ + α" 
      unfolding succ_eq_add1 by force
    with sγ_sαξ have "succ γ ∈∘ α * succ ξ" 
      unfolding mult_succ[symmetric] by auto
    moreover have "succ ξ ∈∘ β" 
      by (simp add: succ_in_Limit_iff ‹ξ ∈∘ β› assms(2))
    ultimately have "succ γ ∈∘ α * β" unfolding αβ by force
    with succ(2) show ?thesis by simp
  qed (use assms(2,3) in auto)
qed

lemma Limit_left_Limit_mult:
  assumes "Limit α" and "Ord β" and "0 ∈∘ β" 
  shows "Limit (α * β)"
proof(cases ‹Limit β›)
  case False
  then obtain β' where "Ord β'" and β_def: "β = succ β'" 
    by (metis Ord_cases assms(2,3) eq0_iff)
  have α_sβ': "α * succ β' = α * β' + α" by (simp add: mult_succ)
  from assms(1) have "Limit (α * β' + α)" by (simp add: Limit_is_Ord ‹Ord β'›)
  then show "Limit (α * β)" unfolding β_def α_sβ' by simp
qed (use assms in ‹auto simp: Limit_def dest: Limit_right_Limit_mult›)

lemma zero_if_Limit_eq_Limit_plus_vnat:
  assumes "Limit α" and "Limit β" and "α = β + n" and "n ∈∘ ω"
  shows "n = 0"
proof(rule ccontr)
  assume prems: "n ≠ 0"
  from assms(1,2,4) have "Ord α" and "Ord β" and "Ord 0" and "Ord n" by auto
  have "0 ∈∘ n" by (simp add: mem_0_Ord prems assms(4)) 
  with assms(4) obtain m where n_def: "n = succ m" by (auto elim: omega_prev)
  from assms(1,3) show False by (simp add: n_def plus_V_succ_right)
qed

lemma Ord_vsubset_closed: 
  assumes "Ord α" and "Ord γ" and "α ⊆∘ β" and "β ∈∘ γ" 
  shows "α ∈∘ γ" 
proof-
  from assms have "Ord β" by auto
  with assms show ?thesis by (simp add: Ord_mem_iff_lt)
qed

lemma
  ―‹Based on Exercise 1, page 53 in \cite{takeuti_introduction_1971}.›
  assumes "Ord α" and "Ord γ" and "α + β ∈∘ γ" 
  shows Ord_plus_Ord_closed_augend: "α ∈∘ γ" 
    and Ord_plus_Ord_closed_addend: "β ∈∘ γ"
proof-
  from assms have "α + β ∈∘ α + γ" by (meson vsubsetD add_le_left)
  from add_mem_right_cancel[THEN iffD1, OF this] show "β ∈∘ γ" .
  from assms have "α ⊆∘ α + β" by simp
  from Ord_vsubset_closed[OF assms(1,2) this assms(3)] show "α ∈∘ γ" .
qed

lemma Ord_ex1_Limit_plus_in_omega:
  ―‹Based on Theorem 8.13 in \cite{takeuti_introduction_1971}.›
  assumes "Ord α" and "ω ⊆∘ α"
  shows "∃!β. ∃!n. n ∈∘ ω ∧ Limit β ∧ α = β + n"
proof-
  let ?A = ‹set {γ. Limit γ ∧ γ ⊆∘ α}›
  have small[simp]: "small {γ. Limit γ ∧ γ ⊆∘ α}"
  proof-
    from Ord_mem_iff_lt  have "{γ. Limit γ ∧ γ ⊆∘ α} ⊆ elts (succ α)"
      by (auto dest: order.not_eq_order_implies_strict intro: assms(1))
    then show "small {γ. Limit γ ∧ γ ⊆∘ α}" by (meson down)
  qed
  let ?β = ‹⋃∘?A›
  have "?β ⊆∘ α" by auto
  moreover have L_β: "Limit ?β"
  proof(subst Limit_def, intro conjI allI impI)
    show "Ord ?β" by (fastforce intro: Ord_Sup)
    from assms(2) show "0 ∈∘ ?β" by auto
    fix y assume "y ∈∘ ?β"
    then obtain γ where "y ∈∘ γ" and "γ ∈∘ ?A" by clarsimp
    then show "succ y ∈∘ ?β" by (auto simp: succ_in_Limit_iff)
  qed
  ultimately obtain γ where "Ord γ" and α_def: "α = ?β + γ"
    by (metis assms(1) le_Ord_diff Limit_is_Ord)
  from L_β have L_βω: "Limit (?β + ω)" by (blast intro: Limit_add_Limit)
  have "γ ⊂∘ ω"
  proof(rule ccontr)
    assume "~γ ⊂∘ ω"
    with ‹Ord γ› Ord_linear2 have "ω ⊆∘ γ" by auto
    then obtain δ where γ_def: "γ = ω + δ" 
      by (blast dest: Ord_odiff_eq intro: ‹Ord γ›)
    from α_def have "α = (?β + ω) + δ" by (simp add: add.assoc γ_def)
    then have "?β + ω ⊆∘ α" by (metis add_le_cancel_left0)
    with L_βω have "?β + ω ⊆∘ ?β" by auto
    with add_le_cancel_left[of ?β ω 0, THEN iffD1] show False by simp
  qed
  with α_def have "γ ∈∘ ω" by (auto simp: Ord_mem_iff_lt ‹Ord γ›)
  show ?thesis
  proof
    (
      intro ex1I conjI; 
      (elim conjE ex1E allE conjE impE | tactic‹all_tac›);
      (intro conjI | tactic‹all_tac›)
    )
    show "γ ∈∘ ω" by (rule ‹γ ∈∘ ω›)
    show "Limit ?β" by (rule ‹Limit ?β›)
    show "α = ?β + γ" by (rule α_def)
    from α_def show "α = ?β + n ⟹ n = γ" for n by auto
    show "n ∈∘ ω ⟹ Limit β ⟹ α = β + n ⟹ β = ?β" for n β
    proof-
      assume prems: "n ∈∘ ω" "Limit β" "α = β + n"
      from L_β prems(2,3) have "β ⊆∘ ?β" by auto
      then obtain η where β_def: "?β = β + η" and "Ord η" 
        by (metis (lifting) L_β Limit_is_Ord le_Ord_diff prems(2))
      moreover have "η ∈∘ ω"
      proof-
        from α_def β_def have "β + η + γ = β + n" by (simp add: prems(3))
        then have "η + γ = n" by (simp add: add.assoc)
        with ‹γ ∈∘ ω› ‹n ∈∘ ω› ‹Ord γ› show "η ∈∘ ω"
          by (blast intro: calculation(2) Ord_plus_Ord_closed_augend)
      qed
      ultimately show ?thesis 
        using prems(2) L_β by (force dest: zero_if_Limit_eq_Limit_plus_vnat)
    qed      
  qed 
qed

lemma not_Limit_if_in_Limit_plus_omega:
  assumes "Limit α" and "α ∈∘ β" and "β ∈∘ α + ω"
  shows "~Limit β"
proof-
  from assms Ord_add have "Ord β" by blast
  show ?thesis
    using assms(3)
  proof(cases rule: mem_plus_V_E)
    case 1 with mem_not_sym show ?thesis by (auto simp: assms(2,3))
  next
    case (2 z)
    from zero_if_Limit_eq_Limit_plus_vnat[OF _ assms(1) 2(2) 2(1)] 2(2) assms(2) 
    show ?thesis  
      by force
  qed
qed

lemma Limit_plus_omega_vsubset_Limit: 
  assumes "Limit α" and "Limit β" and "α ∈∘ β"
  shows "α + ω ⊆∘ β"
proof- 
  from assms(1) have Lαω: "Limit (α + ω)" by (simp add: Limit_is_Ord)
  from not_Limit_if_in_Limit_plus_omega[OF assms(1,3)] assms(2) have
    "β ∉∘ α + ω"
    by clarsimp
  with assms(2) have "~β ⊂∘ α + ω"
    by (blast intro: Lαω dest: Ord_mem_iff_lt Limit_is_Ord)
  then show "α + ω ⊆∘ β" by (meson assms Lαω Limit_is_Ord Ord_linear2)
qed

lemma Limit_plus_nat_in_Limit:
  assumes "Limit α" and "Limit β" and "α ∈∘ β"
  shows "α + aℕ ∈∘ β"
  using assms Limit_plus_omega_vsubset_Limit[OF assms] by auto

lemma omega2_vsubset_Limit:
  assumes "Limit α" and "ω ∈∘ α"
  shows "ω + ω ⊆∘ α"
  using assms by (simp add: Limit_plus_omega_vsubset_Limit)

text‹\newpage›

end