(* 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