# Theory CZH_Sets_Ordinals

```(* Copyright 2021 (C) Mihails Milehins *)

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 (α * ξ) ⊆⇩∘ α * ξ + α"
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: "α ∈⇩∘ γ"
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))
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```