# Theory Cantor_NF

```section ‹Cantor Normal Form›

theory Cantor_NF
imports Ordinal_Exp
begin

subsection ‹Cantor normal form›

text ‹Lemma 5.1›
lemma cnf_1:
assumes α: "α ∈ elts β" "Ord β" and "m > 0"
shows "ω↑α * ord_of_nat n < ω↑β * ord_of_nat m"
proof -
have †: "ω↑succ α ≤ ω↑β"
using Ord_mem_iff_less_TC assms oexp_mono succ_le_TC_iff by auto
have "ω↑α * ord_of_nat n < ω↑α * ω"
using Ord_in_Ord OrdmemD assms by auto
also have "… = ω↑succ α"
using Ord_in_Ord α by auto
also have "… ≤ ω↑β"
using "†" by blast
also have "… ≤ ω↑β * ord_of_nat m"
using ‹m > 0› le_mult by auto
finally show ?thesis .
qed

fun Cantor_sum  where
Cantor_sum_Nil: "Cantor_sum [] ms = 0"
| Cantor_sum_Nil2: "Cantor_sum (α#αs) [] = 0"
| Cantor_sum_Cons: "Cantor_sum (α#αs) (m#ms) = (ω↑α) * ord_of_nat m + Cantor_sum αs ms"

abbreviation Cantor_dec :: "V list ⇒ bool" where
"Cantor_dec ≡ sorted_wrt (>)"

lemma Ord_Cantor_sum:
assumes "List.set αs ⊆ ON"
shows "Ord (Cantor_sum αs ms)"
using assms
proof (induction αs arbitrary: ms)
case (Cons a αs ms)
then show ?case
by (cases ms) auto
qed auto

lemma Cantor_dec_Cons_iff [simp]: "Cantor_dec (α#β#βs) ⟷ β < α ∧ Cantor_dec (β#βs)"
by auto

text ‹Lemma 5.2. The second and third premises aren't really necessary, but their
removal requires quite a lot of work.›
lemma cnf_2:
assumes "List.set (α#αs) ⊆ ON" "list.set ms ⊆ {0<..}" "length αs = length ms"
and "Cantor_dec (α#αs)"
shows "ω↑α > Cantor_sum αs ms"
using assms
proof (induction ms arbitrary: α αs)
case Nil
then obtain α0 where α0: "(α#αs) = [α0]"
by (metis length_0_conv)
then have "Ord α0"
using Nil.prems(1) by auto
then show ?case
using α0 zero_less_Limit by auto
next
case (Cons m1 ms)
then obtain α0 α1 αs' where α01: "(α#αs) = α0#α1#αs'"
by (metis (no_types, lifting) Cons.prems(3) Suc_length_conv)
then have "Ord α0" "Ord α1"
using Cons.prems(1) α01 by auto
have *: "ω↑α0 * ord_of_nat 1 > ω↑α1 * ord_of_nat m1"
proof (rule cnf_1)
show "α1 ∈ elts α0"
using Cons.prems α01 by (simp add: Ord_mem_iff_lt ‹Ord α0› ‹Ord α1›)
qed (use ‹Ord α0› in auto)
show ?case
proof (cases ms)
case Nil
then show ?thesis
using * one_V_def Cons.prems(3) α01 by auto
next
case (Cons m2 ms')
then obtain α2 αs'' where α02: "(α#αs) = α0#α1#α2#αs''"
by (metis Cons.prems(3) Suc_length_conv α01 length_tl list.sel(3))
then have "Ord α2"
using Cons.prems(1) by auto
have "m1 > 0" "m2 > 0"
using Cons.prems Cons by auto
have "ω↑α1 * ord_of_nat m1 + ω↑α1 * ord_of_nat m1 = (ω↑α1 * ord_of_nat m1) * ord_of_nat 2"
by (simp add: mult_succ eval_nat_numeral)
also have "… < ω↑α0"
using cnf_1 [of concl: "α1" "m1 * 2" "α0" 1] Cons.prems α01 one_V_def
by (simp add: mult.assoc ord_of_nat_mult Ord_mem_iff_lt)
finally have II: "ω↑α1 * ord_of_nat m1 + ω↑α1 * ord_of_nat m1 < ω↑α0"
by simp
have "Cantor_sum (tl αs) ms < ω↑hd αs"
proof (rule Cons.IH)
show "Cantor_dec (hd αs # tl αs)"
using ‹Cantor_dec (α#αs)› α01 by auto
qed (use Cons.prems α01 in auto)
then have "Cantor_sum (α2 # αs'') ms < ω↑α1"
using α02 by auto
also have "… ≤ ω↑α1 * ord_of_nat m1"
by (simp add: ‹0 < m1› le_mult)
finally show ?thesis
using II α02 dual_order.strict_trans by fastforce
qed
qed

proposition Cantor_nf_exists:
assumes "Ord α"
obtains αs ms where "List.set αs ⊆ ON" "list.set ms ⊆ {0<..}" "length αs = length ms"
and "Cantor_dec αs"
and "α = Cantor_sum αs ms"
using assms
proof (induction α arbitrary: thesis rule: Ord_induct)
case (step α)
show ?case
proof (cases "α = 0")
case True
have "Cantor_sum [] [] = 0"
by simp
with True show ?thesis
using length_pos_if_in_set step.prems subset_eq
by (metis length_0_conv not_gr_zero sorted_wrt.simps(1))
next
case False
define αhat where "αhat ≡ Sup {γ ∈ ON. ω↑γ ≤ α}"
then have "Ord αhat"
using Ord_Sup assms by fastforce
have "⋀ξ. ⟦Ord ξ; ω↑ξ ≤ α⟧ ⟹ ξ ≤ ω↑α"
by (metis Ord_ω OrdmemD le_oexp' order_trans step.hyps one_V_def succ_in_omega zero_in_omega)
then have "{γ ∈ ON. ω↑γ ≤ α} ⊆ elts (succ (ω↑α))"
using Ord_mem_iff_lt step.hyps by force
then have sma: "small {γ ∈ ON. ω↑γ ≤ α}"
by (meson down)
have le: "ω↑αhat ≤ α"
proof (rule ccontr)
assume "¬ ω↑αhat ≤ α"
then have †: "α ∈ elts (ω↑αhat)"
by (meson Ord_ω Ord_linear2 Ord_mem_iff_lt Ord_oexp ‹Ord αhat› step.hyps)
obtain γ where "Ord γ" "ω↑γ ≤ α" "α < γ"
using ‹Ord αhat›
proof (cases αhat rule: Ord_cases)
case 0
with † show thesis
by (auto simp: False)
next
case (succ β)
have "succ β ∈ {γ ∈ ON. ω↑γ ≤ α}"
by (rule succ_in_Sup_Ord) (use succ αhat_def sma in auto)
then have "ω↑succ β ≤ α"
by blast
with † show thesis
using ‹¬ ω↑αhat ≤ α› succ by blast
next
case limit
with † show thesis
apply (clarsimp simp: oexp_Limit αhat_def)
by (meson Ord_ω Ord_in_Ord Ord_linear_le mem_not_refl oexp_mono_le omega_nonzero vsubsetD)
qed
then show False
by (metis Ord_ω OrdmemD leD le_less_trans le_oexp' one_V_def succ_in_omega zero_in_omega)
qed
have False if "∄M. α < ω↑αhat * ord_of_nat M"
proof -
have †: "ω↑αhat * ord_of_nat M ≤ α" for M
by (meson that Ord_ω Ord_linear2 Ord_mult Ord_oexp Ord_ord_of_nat ‹Ord αhat› step.hyps)
have "¬ ω↑succ αhat ≤ α"
using Ord_mem_iff_lt αhat_def ‹Ord αhat› sma elts_succ by blast
then have "α < ω↑succ αhat"
by (meson Ord_ω Ord_linear2 Ord_oexp Ord_succ ‹Ord αhat› step.hyps)
also have "… = ω↑αhat * ω"
using ‹Ord αhat› oexp_succ by blast
also have "… = Sup (range (λm. ω↑αhat * ord_of_nat m))"
by (simp add: mult_Limit) (auto simp: ω_def image_image)
also have "… ≤ α"
using † by blast
finally show False
by simp
qed
then obtain M where M: "ω↑αhat * ord_of_nat M > α"
by blast
have bound: "i ≤ M" if "ω↑αhat * ord_of_nat i ≤ α" for i
proof -
have "ω↑αhat * ord_of_nat i < ω↑αhat * ord_of_nat M"
using M dual_order.strict_trans2 that by blast
then show ?thesis
using ‹Ord αhat› less_V_def by auto
qed
define mhat where "mhat ≡ Greatest (λm. ω↑αhat * ord_of_nat m ≤ α)"
have mhat_ge: "m ≤ mhat" if "ω↑αhat * ord_of_nat m ≤ α" for m
unfolding mhat_def
by (metis (mono_tags, lifting) Greatest_le_nat bound that)
have mhat: "ω↑αhat * ord_of_nat mhat ≤ α"
unfolding mhat_def
by (rule GreatestI_nat [where k=0 and b=M]) (use bound in auto)
then obtain ξ where "Ord ξ" "ξ ≤ α" and ξ: "α = ω↑αhat * ord_of_nat mhat + ξ"
by (metis Ord_ω Ord_mult Ord_oexp Ord_ord_of_nat ‹Ord αhat› step.hyps le_Ord_diff)
have False if "ξ = α"
proof -
have "ξ ≥ ω↑αhat"
by (simp add: le that)
then obtain ζ where "Ord ζ" "ζ ≤ ξ" and ζ: "ξ = ω↑αhat + ζ"
by (metis Ord_ω Ord_oexp ‹Ord αhat› ‹Ord ξ› le_Ord_diff)
then have "α = ω↑αhat * ord_of_nat mhat + ω↑αhat + ζ"
by (simp add: ξ add.assoc)
then have "ω↑αhat * ord_of_nat (Suc mhat) ≤ α"
by (metis add_le_cancel_left add.right_neutral le_0 mult_succ ord_of_nat.simps(2))
then show False
using Suc_n_not_le_n mhat_ge by blast
qed
then have ξinα: "ξ ∈ elts α"
using Ord_mem_iff_lt ‹Ord ξ› ‹ξ ≤ α› less_V_def step.hyps by auto
show thesis
proof (cases "ξ = 0")
case True
show thesis
proof (rule step.prems)
show "α = Cantor_sum [αhat] [mhat]"
by (simp add: True ξ)
qed (use ξ True ‹α ≠ 0› ‹Ord αhat› in auto)
next
case False
obtain βs ns where sub: "List.set βs ⊆ ON" "list.set ns ⊆ {0<..}"
and len_eq: "length βs = length ns"
and dec: "Cantor_dec βs"
and ξeq: "ξ = Cantor_sum βs ns"
using step.IH [OF ξinα] by blast
then have "length βs > 0" "length ns > 0"
using False Cantor_sum.simps(1) ‹ξ = Cantor_sum βs ns› by auto
then obtain β0 n0 βs' ns' where β0: "βs = β0 # βs'" and "Ord β0"
and n0: "ns = n0 # ns'" and "n0 > 0"
using sub by (auto simp: neq_Nil_conv)
moreover have False if "β0 > αhat"
proof -
have "ω↑β0 ≤ ω↑β0 * ord_of_nat n0 + u" for u
using ‹n0 > 0›
by (metis add_le_cancel_left Ord_ord_of_nat add.right_neutral dual_order.trans gr_implies_not_zero le_0 le_mult ord_of_eq_0_iff)
moreover have "ω↑β0 > α"
using that ‹Ord β0›
by (metis (no_types, lifting) Ord_ω Ord_linear2 Ord_oexp Sup_upper αhat_def leD mem_Collect_eq sma step.hyps)
ultimately have "ξ ≥ ω↑β0"
by (simp add: ξeq β0 n0)
then show ?thesis
using ‹α < ω↑β0› ‹ξ ≤ α› by auto
qed
ultimately have "β0 ≤ αhat"
using Ord_linear2 ‹Ord αhat› by auto
then consider "β0 < αhat" | "β0 = αhat"
using dual_order.order_iff_strict by auto
then show ?thesis
proof cases
case 1
show ?thesis
proof (rule step.prems)
show "list.set (αhat#βs) ⊆ ON"
using sub by (auto simp: ‹Ord αhat›)
show "list.set (mhat#ns) ⊆ {0::nat<..}"
using sub using ‹ξ = α ⟹ False› ξ by fastforce
show "Cantor_dec (αhat#βs)"
using that ‹β0 < αhat› ‹Ord αhat› ‹Ord β0› Ord_mem_iff_lt β0 dec less_Suc_eq_0_disj
by (force simp: β0 n0)
show "length (αhat#βs) = length (mhat#ns)"
by (auto simp: len_eq)
show "α = Cantor_sum (αhat#βs) (mhat#ns)"
by (simp add: ξ ξeq β0 n0)
qed
next
case 2
show ?thesis
proof (rule step.prems)
show "list.set βs ⊆ ON"
by (simp add: sub(1))
show "list.set ((n0+mhat)#ns') ⊆ {0::nat<..}"
using n0 sub(2) by auto
show "length (βs::V list) = length ((n0+mhat)#ns')"
by (simp add: len_eq n0)
show "Cantor_dec βs"
using that β0 dec by auto
show "α = Cantor_sum βs ((n0+mhat)#ns')"
using 2
by (simp add: add_mult_distrib β0 ξ ξeq add.assoc add.commute n0 ord_of_nat_add)
qed
qed
qed
qed
qed

lemma Cantor_sum_0E:
assumes "Cantor_sum αs ms = 0" "List.set αs ⊆ ON" "list.set ms ⊆ {0<..}" "length αs = length ms"
shows "αs = []"
using assms
proof (induction αs arbitrary: ms)
case Nil
then show ?case
by auto
next
case (Cons a list)
then obtain m ms' where "ms = m#ms'" "m ≠ 0" "list.set ms' ⊆ {0<..}"
by simp (metis Suc_length_conv greaterThan_iff insert_subset list.set(2))
with Cons show ?case by auto
qed

lemma Cantor_nf_unique_aux:
assumes "Ord α"
and αsON: "List.set αs ⊆ ON"
and βsON: "List.set βs ⊆ ON"
and ms: "list.set ms ⊆ {0<..}"
and ns: "list.set ns ⊆ {0<..}"
and mseq: "length αs = length ms"
and nseq: "length βs = length ns"
and αsdec: "Cantor_dec αs"
and βsdec: "Cantor_dec βs"
and αseq: "α = Cantor_sum αs ms"
and βseq: "α = Cantor_sum βs ns"
shows "αs = βs ∧ ms = ns"
using assms
proof (induction α arbitrary: αs ms βs ns rule: Ord_induct)
case (step α)
show ?case
proof (cases "α = 0")
case True
then show ?thesis
using step.prems by (metis Cantor_sum_0E length_0_conv)
next
case False
then obtain α0 αs' β0 βs' where αs: "αs = α0 # αs'" and βs: "βs = β0 # βs'"
by (metis Cantor_sum.simps(1) min_list.cases step.prems(9,10))
then have ON: "Ord α0" "list.set αs' ⊆ ON" "Ord β0" "list.set βs' ⊆ ON"
using αs βs step.prems(1,2) by auto
then obtain m0 ms' n0 ns' where ms: "ms = m0 # ms'" and ns: "ns = n0 # ns'"
by (metis αs βs length_0_conv list.distinct(1) list.exhaust step.prems(5,6))
then have nz: "m0 ≠ 0" "list.set ms' ⊆ {0<..}" "n0 ≠ 0" "list.set ns' ⊆ {0<..}"
using ms ns step.prems(3,4) by auto
have False if "β0 < α0"
proof -
have Ordc: "Ord (Cantor_sum βs ns)" "Ord (ω↑α0)"
using Ord_oexp ‹Ord α0›  step.hyps step.prems(10) by blast+
have *: "Cantor_sum βs ns < ω↑α0"
using step.prems(2-6) ‹Ord α0› ‹Cantor_dec βs› that βs cnf_2
by (metis Cantor_dec_Cons_iff insert_subset list.set(2) mem_Collect_eq)
then show False
by (metis Cantor_sum_Cons Ord_mem_iff_lt Ord_ord_of_nat Ordc αs ‹m0 ≠ 0› * le_mult ms not_add_mem_right ord_of_eq_0 step.prems(9,10) vsubsetD)
qed
moreover
have False if "α0 < β0"
proof -
have Ordc: "Ord (Cantor_sum αs ms)" "Ord (ω↑β0)"
using Ord_oexp ‹Ord β0›  step.hyps step.prems(9) by blast+
have *: "Cantor_sum αs ms < ω↑β0"
using step.prems(1-5) ‹Ord β0› ‹Cantor_dec αs› that αs cnf_2
by (metis Cantor_dec_Cons_iff βs insert_subset list.set(2))
then show False
by (metis Cantor_sum_Cons Ord_mem_iff_lt Ord_ord_of_nat Ordc βs ‹n0 ≠ 0› * le_mult not_add_mem_right ns ord_of_eq_0 step.prems(9,10) vsubsetD)
qed
ultimately have 1: "α0 = β0"
using Ord_linear_lt ‹Ord α0› ‹Ord β0› by blast
have False if "m0 < n0"
proof -
have "ω↑α0 > Cantor_sum αs' ms'"
using αs ‹list.set ms' ⊆ {0<..}› cnf_2 ms step.prems(1,5,7) by auto
then have "α < ω↑α0 * ord_of_nat m0 + ω↑α0"
by (simp add: αs ms step.prems(9))
also have "… = ω↑α0 * ord_of_nat (Suc m0)"
by (simp add: mult_succ)
also have "… ≤ ω↑α0 * ord_of_nat n0"
by (meson Ord_ω Ord_oexp Ord_ord_of_nat Suc_leI ‹Ord α0› mult_cancel_le_iff ord_of_nat_mono_iff that)
also have "… ≤ α"
by (metis Cantor_sum_Cons add_le_cancel_left βs ‹α0 = β0› add.right_neutral le_0 ns step.prems(10))
finally show False
by blast
qed
moreover have False if "n0 < m0"
proof -
have "ω↑β0 > Cantor_sum βs' ns'"
using βs ‹list.set ns' ⊆ {0<..}› cnf_2 ns step.prems(2,6,8) by auto
then have "α < ω↑β0 * ord_of_nat n0 + ω↑β0"
by (simp add: βs ns step.prems(10))
also have "… = ω↑β0 * ord_of_nat (Suc n0)"
by (simp add: mult_succ)
also have "… ≤ ω↑β0 * ord_of_nat m0"
by (meson Ord_ω Ord_oexp Ord_ord_of_nat Suc_leI ‹Ord β0› mult_cancel_le_iff ord_of_nat_mono_iff that)
also have "… ≤ α"
by (metis Cantor_sum_Cons add_le_cancel_left αs ‹α0 = β0› add.right_neutral le_0 ms step.prems(9))
finally show False
by blast
qed
ultimately have 2: "m0 = n0"
using nat_neq_iff by blast
have "αs' = βs' ∧ ms' = ns'"
proof (rule step.IH)
have "Cantor_sum αs' ms' < ω↑α0"
using αs cnf_2 ms nz(2) step.prems(1) step.prems(5) step.prems(7) by auto
also have "… ≤ Cantor_sum αs ms"
apply (simp add: αs βs ms ns)
by (metis Cantor_sum_Cons add_less_cancel_left ON(1) Ord_ω Ord_linear2 Ord_oexp Ord_ord_of_nat αs add.right_neutral dual_order.strict_trans1 le_mult ms not_less_0 nz(1) ord_of_eq_0 step.hyps step.prems(9))
finally show "Cantor_sum αs' ms' ∈ elts α"
using ON(2) Ord_Cantor_sum Ord_mem_iff_lt step.hyps step.prems(9) by blast
show "length αs' = length ms'" "length βs' = length ns'"
using αs ms βs ns step.prems by auto
show "Cantor_dec αs'" "Cantor_dec βs'"
using αs βs step.prems(7,8) by auto
have "Cantor_sum αs ms = Cantor_sum βs ns"
using step.prems(9,10) by auto
then show "Cantor_sum αs' ms' = Cantor_sum βs' ns'"
using 1 2 by (simp add: αs βs ms ns)
qed (use ON nz in auto)
then show ?thesis
using 1 2 by (simp add: αs βs ms ns)
qed
qed

proposition Cantor_nf_unique:
assumes "Cantor_sum αs ms = Cantor_sum βs ns"
and αsON: "List.set αs ⊆ ON"
and βsON: "List.set βs ⊆ ON"
and ms: "list.set ms ⊆ {0<..}"
and ns: "list.set ns ⊆ {0<..}"
and mseq: "length αs = length ms"
and nseq: "length βs = length ns"
and αsdec: "Cantor_dec αs"
and βsdec: "Cantor_dec βs"
shows "αs = βs ∧ ms = ns"
using Cantor_nf_unique_aux Ord_Cantor_sum assms  by auto

lemma less_ω_power:
assumes "Ord α1" "Ord β"
and α2: "α2 ∈ elts α1" and β: "β < ω↑α2"
and "m1 > 0" "m2 > 0"
shows "ω↑α2 * ord_of_nat m2 + β < ω↑α1 * ord_of_nat m1 + (ω↑α2 * ord_of_nat m2 + β)"
(is "?lhs < ?rhs")
proof -
obtain oo: "Ord (ω↑α1)" "Ord (ω↑α2)"
using Ord_in_Ord Ord_oexp assms by blast
moreover obtain "ord_of_nat m2 ≠ 0"
using assms ord_of_eq_0 by blast
ultimately have "β < ω↑α2 * ord_of_nat m2"
by (meson Ord_ord_of_nat β dual_order.strict_trans1 le_mult)
with oo assms have "?lhs ≠ ?rhs"
by (metis Ord_mult Ord_ord_of_nat add_strict_mono add.assoc cnf_1 not_add_less_right oo)
then show ?thesis
by (simp add: add_le_left ‹Ord β› less_V_def oo)
qed

lemma Cantor_sum_ge:
assumes "List.set (α#αs) ⊆ ON" "list.set ms ⊆ {0<..}" "length ms > 0"
shows "ω ↑ α ≤ Cantor_sum (α#αs) ms"
proof -
obtain m ns where ms: "ms = Cons m ns"
by (meson assms(3) list.set_cases nth_mem)
then have "ω ↑ α ≤ ω ↑ α * ord_of_nat m"
using assms(2) le_mult by auto
then show ?thesis
using dual_order.trans ms by auto
qed

subsection ‹Simplified Cantor normal form›

text ‹No coefficients, and the exponents decreasing non-strictly›

fun ω_sum  where
ω_sum_Nil: "ω_sum [] = 0"
| ω_sum_Cons: "ω_sum (α#αs) = (ω↑α) + ω_sum αs"

abbreviation ω_dec :: "V list ⇒ bool" where
"ω_dec ≡ sorted_wrt (≥)"

lemma Ord_ω_sum [simp]: "List.set αs ⊆ ON ⟹ Ord (ω_sum αs)"
by (induction αs) auto

lemma ω_dec_Cons_iff [simp]: "ω_dec (α#β#βs) ⟷ β ≤ α ∧ ω_dec (β#βs)"
by auto

lemma ω_sum_0E:
assumes "ω_sum αs = 0" "List.set αs ⊆ ON"
shows "αs = []"
using assms
by (induction αs) auto

fun ω_of_Cantor where
ω_of_Cantor_Nil: "ω_of_Cantor [] ms = []"
| ω_of_Cantor_Nil2: "ω_of_Cantor (α#αs) [] = []"
| ω_of_Cantor_Cons: "ω_of_Cantor (α#αs) (m#ms) = replicate m α @ ω_of_Cantor αs ms"

lemma ω_sum_append [simp]: "ω_sum (xs @ ys) = ω_sum xs + ω_sum ys"
by (induction xs) (auto simp: add.assoc)

lemma ω_sum_replicate [simp]: "ω_sum (replicate m a) = ω ↑ a * ord_of_nat m"
by (induction m) (auto simp: mult_succ simp flip: replicate_append_same)

lemma ω_sum_of_Cantor [simp]: "ω_sum (ω_of_Cantor αs ms) = Cantor_sum αs ms"
proof (induction αs arbitrary: ms)
case (Cons a αs ms)
then show ?case
by (cases ms) auto
qed auto

lemma ω_of_Cantor_subset: "List.set (ω_of_Cantor αs ms) ⊆ List.set αs"
proof (induction αs arbitrary: ms)
case (Cons a αs ms)
then show ?case
by (cases ms) auto
qed auto

lemma ω_dec_replicate: "ω_dec (replicate m α @ αs) = (if m=0 then ω_dec αs else ω_dec (α#αs))"
by (induction m arbitrary: αs) (simp_all flip: replicate_append_same)

lemma ω_dec_of_Cantor_aux:
assumes "Cantor_dec (α#αs)" "length αs = length ms"
shows "ω_dec (ω_of_Cantor (α#αs) (m#ms))"
using assms
proof (induction αs arbitrary: ms)
case Nil
then show ?case
using sorted_wrt_iff_nth_less by fastforce
next
case (Cons a αs ms)
then obtain n ns where ns: "ms = n#ns"
by (metis length_Suc_conv)
then have "a ≤ α"
using Cons.prems(1) order.strict_implies_order by auto
moreover have "∀x∈list.set (ω_of_Cantor αs ns). x ≤ a"
using Cons ns ‹a ≤ α›
apply (simp add: ω_dec_replicate)
by (meson ω_of_Cantor_subset order.strict_implies_order subsetD)
ultimately show ?case
using Cons ns by (force simp: ω_dec_replicate)
qed

lemma ω_dec_of_Cantor:
assumes "Cantor_dec αs" "length αs = length ms"
shows "ω_dec (ω_of_Cantor αs ms)"
proof (cases αs)
case Nil
then have "ms = []"
using assms by auto
with Nil show ?thesis
by simp
next
case (Cons a list)
then show ?thesis
by (metis ω_dec_of_Cantor_aux assms length_Suc_conv)
qed

proposition ω_nf_exists:
assumes "Ord α"
obtains αs where "List.set αs ⊆ ON" and "ω_dec αs" and "α = ω_sum αs"
proof -
obtain αs ms where "List.set αs ⊆ ON" "list.set ms ⊆ {0<..}" and length: "length αs = length ms"
and "Cantor_dec αs"
and α: "α = Cantor_sum αs ms"
using Cantor_nf_exists assms by blast
then show thesis
by (metis ω_dec_of_Cantor ω_of_Cantor_subset ω_sum_of_Cantor order_trans that)
qed

lemma ω_sum_take_drop: "ω_sum αs = ω_sum (take k αs) + ω_sum (drop k αs)"
proof (induction k arbitrary: αs)
case 0
then show ?case
by simp
next
case (Suc k)
then show ?case
proof (cases "αs")
case Nil
then show ?thesis
by simp
next
case (Cons a list)
with Suc.prems show ?thesis
by (simp add: add.assoc flip: Suc.IH)
qed
qed

lemma in_elts_ω_sum:
assumes "δ ∈ elts (ω_sum αs)"
shows "∃k<length αs. ∃γ∈elts (ω ↑ (αs!k)). δ = ω_sum (take k αs) + γ"
using assms
proof (induction αs arbitrary: δ)
case (Cons α αs)
then have "δ ∈ elts (ω ↑ α + ω_sum αs)"
by simp
then show ?case
proof (rule mem_plus_V_E)
fix η
assume η: "η ∈ elts (ω_sum αs)" and δ: "δ = ω ↑ α + η"
then obtain k γ where "k<length αs" "γ ∈ elts (ω ↑ (αs!k))" "η = ω_sum (take k αs) + γ"
using Cons.IH by blast
then show ?case
by (rule_tac x="Suc k" in exI) (simp add: δ add.assoc)
qed auto
qed auto

lemma ω_le_ω_sum: "⟦k < length αs; List.set αs ⊆ ON⟧ ⟹ ω ↑ (αs!k) ≤ ω_sum αs"
proof (induction αs arbitrary: k)
case (Cons a αs)
then obtain "Ord a" "list.set αs ⊆ ON"
by simp
with Cons.IH have "⋀k x. k < length αs ⟹ ω ↑ αs ! k ≤ ω ↑ a + ω_sum αs"
by (meson Ord_ω Ord_ω_sum Ord_oexp add_le_left order_trans)
then show ?case
using Cons by (simp add: nth_Cons split: nat.split)
qed auto

lemma ω_sum_less_self:
assumes "List.set (α#αs) ⊆ ON" and "ω_dec (α#αs)"
shows "ω_sum αs < ω↑α + ω_sum αs"
using assms
proof (induction αs arbitrary: α)
case Nil
then show ?case
using ZFC_in_HOL.neq0_conv by fastforce
next
case (Cons α1 αs)
then show ?case
by (simp add: add_right_strict_mono oexp_mono_le)
qed

text ‹Something like Lemma 5.2 for @{term ω_sum}›
lemma ω_sum_less_ω_power:
assumes "ω_dec (α#αs)" "List.set (α#αs) ⊆ ON"
shows "ω_sum αs < ω↑α * ω"
using assms
proof (induction αs)
case Nil
then show ?case
by (simp add: ω_gt0)
next
case (Cons β αs)
then have "Ord α"
by auto
have "ω_sum αs < ω↑α * ω"
using Cons by force
then have "ω↑β + ω_sum αs < ω↑α + ω↑α * ω"
using Cons.prems add_right_strict_mono oexp_mono_le by auto
also have "… = ω↑α * ω"
by (metis Kirby.add_mult_distrib mult.right_neutral one_plus_ω_equals_ω)
finally show ?case
by simp
qed

lemma ω_sum_nf_unique_aux:
assumes "Ord α"
and αsON: "List.set αs ⊆ ON"
and βsON: "List.set βs ⊆ ON"
and αsdec: "ω_dec αs"
and βsdec: "ω_dec βs"
and αseq: "α = ω_sum αs"
and βseq: "α = ω_sum βs"
shows "αs = βs"
using assms
proof (induction α arbitrary: αs βs rule: Ord_induct)
case (step α)
show ?case
proof (cases "α = 0")
case True
then show ?thesis
using step.prems by (metis ω_sum_0E)
next
case False
then obtain α0 αs' β0 βs' where αs: "αs = α0 # αs'" and βs: "βs = β0 # βs'"
by (metis ω_sum.elims step.prems(5,6))
then have ON: "Ord α0" "list.set αs' ⊆ ON" "Ord β0" "list.set βs' ⊆ ON"
using αs βs step.prems(1,2) by auto
have False if "β0 < α0"
proof -
have Ordc: "Ord (ω_sum βs)" "Ord (ω↑α0)"
using Ord_oexp ‹Ord α0›  step.hyps step.prems(6) by blast+
have "ω_sum βs < ω↑β0 * ω"
by (rule ω_sum_less_ω_power) (use βs step.prems ON in auto)
also have "… ≤ ω↑α0"
using ON by (metis Ord_ω Ord_succ oexp_mono_le oexp_succ omega_nonzero succ_le_iff that)
finally show False
using αs leD step.prems(5,6) by auto
qed
moreover
have False if "α0 < β0"
proof -
have Ordc: "Ord (ω_sum αs)" "Ord (ω↑β0)"
using Ord_oexp ‹Ord β0›  step.hyps step.prems(5) by blast+
have "ω_sum αs < ω↑α0 * ω"
by (rule ω_sum_less_ω_power) (use αs step.prems ON in auto)
also have "… ≤ ω↑β0"
using ON by (metis Ord_ω Ord_succ oexp_mono_le oexp_succ omega_nonzero succ_le_iff that)
finally show False
using βs leD step.prems(5,6)
by (simp add: ‹α = ω_sum αs› leD)
qed
ultimately have †: "α0 = β0"
using Ord_linear_lt ‹Ord α0› ‹Ord β0› by blast
moreover have "αs' = βs'"
proof (rule step.IH)
show "ω_sum αs' ∈ elts α"
using step.prems αs
by (simp add: Ord_mem_iff_lt ω_sum_less_self)
show "ω_dec αs'" "ω_dec βs'"
using αs βs step.prems(3,4) by auto
have "ω_sum αs = ω_sum βs"
using step.prems(5,6) by auto
then show "ω_sum αs' = ω_sum βs'"
by (simp add: † αs βs)
qed (use ON in auto)
ultimately show ?thesis
by (simp add: αs βs)
qed
qed

subsection ‹Indecomposable ordinals›

text ‹Cf exercise 5 on page 43 of Kunen›

definition indecomposable
where "indecomposable α ≡ Ord α ∧ (∀β ∈ elts α. ∀γ ∈ elts α. β+γ ∈ elts α)"

lemma indecomposableD:
"⟦indecomposable α; β < α; γ < α; Ord β; Ord γ⟧ ⟹ β+γ < α"
by (meson Ord_mem_iff_lt OrdmemD indecomposable_def)

lemma indecomposable_imp_Ord:
"indecomposable α ⟹ Ord α"
using indecomposable_def by blast

lemma indecomposable_1: "indecomposable 1"
by (auto simp: indecomposable_def)

lemma indecomposable_0: "indecomposable 0"
by (auto simp: indecomposable_def)

lemma indecomposable_succ [simp]: "indecomposable (succ α) ⟷ α = 0"
using not_add_mem_right
apply (auto simp: indecomposable_def)
apply (metis add_right_cancel add.right_neutral)
done

lemma indecomposable_alt:
assumes ord: "Ord α" "Ord β" and β: "β < α" and minor: "⋀β γ. ⟦β < α; γ < α; Ord γ⟧ ⟹ β+γ < α"
shows "β+α = α"
proof -
have "¬ β+α < α"
by (simp add: add_le_left ord leD)
moreover have "¬ α < β+α"
by (metis assms le_Ord_diff less_V_def)
ultimately show ?thesis
by (simp add: add_le_left less_V_def ord)
qed

lemma indecomposable_imp_eq:
assumes "indecomposable α" "Ord β" "β < α"
shows "β+α = α"
by (metis assms indecomposableD indecomposable_def le_Ord_diff less_V_def less_irrefl)

lemma indecomposable2:
assumes y: "y < x" and z: "z < x" and minor: "⋀y::V. y < x ⟹ y+x = x"
shows "y+z < x"
by (metis add_less_cancel_left y z minor)

lemma indecomposable_imp_Limit:
assumes indec: "indecomposable α" and "α > 1"
shows "Limit α"
using indecomposable_imp_Ord [OF indec]
proof (cases rule: Ord_cases)
case (succ β)
then show ?thesis
using assms one_V_def by auto
qed (use assms in auto)

lemma eq_imp_indecomposable:
assumes "Ord α" "⋀β::V. β ∈ elts α ⟹ β+α = α"
shows "indecomposable α"
by (metis add_mem_right_cancel assms indecomposable_def)

lemma indecomposable_ω_power:
assumes "Ord δ"
shows "indecomposable (ω↑δ)"
unfolding indecomposable_def
proof (intro conjI ballI)
show "Ord (ω↑δ)"
by (simp add: ‹Ord δ›)
next
fix β γ
assume asm: "β ∈ elts (ω↑δ)" "γ ∈ elts (ω↑δ)"
then obtain ord: "Ord β" "Ord γ" and β: "β < ω↑δ" and γ: "γ < ω↑δ"
by (meson Ord_ω Ord_in_Ord Ord_oexp OrdmemD ‹Ord δ›)
show "β + γ ∈ elts (ω↑δ)"
using ‹Ord δ›
proof (cases δ rule: Ord_cases)
case 0
then show ?thesis
using ‹Ord δ› asm by auto
next
case (succ l)
have "∃x∈elts ω. β + γ ∈ elts (ω↑l * x)"
if x: "x ∈ elts ω" "β ∈ elts (ω↑l * x)" and y: "y ∈ elts ω" "γ ∈ elts (ω↑l * y)"
for x y
proof -
obtain "Ord x" "Ord y" "Ord (ω↑l * x)" "Ord (ω↑l * y)"
using Ord_ω Ord_mult Ord_oexp x y nat_into_Ord succ(1) by presburger
then have "β + γ ∈ elts (ω↑l * (x+y))"
using add_mult_distrib Ord_add Ord_mem_iff_lt add_strict_mono ord x y by presburger
then show ?thesis
using x y by blast
qed
then show ?thesis
using ‹Ord δ› succ ord β γ by (auto simp: mult_Limit simp flip: Ord_mem_iff_lt)
next
case limit
have "Ord (ω↑δ)"
by (simp add: ‹Ord δ›)
then obtain x y where x: "x ∈ elts δ" "Ord x" "β ∈ elts (ω↑x)"
and y: "y ∈ elts δ" "Ord y" "γ ∈ elts (ω↑y)"
using ‹Ord δ› limit ord β γ oexp_Limit
by (auto simp flip: Ord_mem_iff_lt intro: Ord_in_Ord)
then have "succ (x ⊔ y) ∈ elts δ"
by (metis Limit_def Ord_linear_le limit sup.absorb2 sup.orderE)
moreover have "β + γ ∈ elts (ω↑succ (x ⊔ y))"
proof -
have oxy: "Ord (x ⊔ y)"
using Ord_sup x y by blast
then obtain "ω↑x ≤ ω↑(x ⊔ y)" "ω↑y ≤ ω↑(x ⊔ y)"
by (metis Ord_ω Ord_linear_le Ord_mem_iff_less_TC Ord_mem_iff_lt le_TC_def less_le_not_le oexp_mono omega_nonzero sup.absorb2 sup.orderE x(2) y(2))
then have "β ∈ elts (ω↑(x ⊔ y))" "γ ∈ elts (ω↑(x ⊔ y))"
using x y by blast+
then have "β + γ ∈ elts (ω↑(x ⊔ y) * succ (succ 0))"
by (metis Ord_ω Ord_add Ord_mem_iff_lt Ord_oexp Ord_sup add_strict_mono mult.right_neutral mult_succ ord one_V_def x(2) y(2))
then show ?thesis
apply (simp add: oxy)
using Ord_ω Ord_mult Ord_oexp Ord_trans mem_0_Ord mult_add_mem_0 oexp_eq_0_iff omega_nonzero oxy succ_in_omega by presburger
qed
ultimately show ?thesis
using ord ‹Ord (ω↑δ)› limit oexp_Limit by auto
qed
qed

lemma ω_power_imp_eq:
assumes "β < ω↑δ" "Ord β" "Ord δ" "δ ≠ 0"
shows "β + ω↑δ = ω↑δ"
by (simp add: assms indecomposable_ω_power indecomposable_imp_eq)

lemma mult_oexp_indec: "⟦Ord α; Limit μ; indecomposable μ⟧ ⟹ α * (α ↑ μ) = (α ↑ μ)"
by (metis Limit_def Ord_1 OrdmemD indecomposable_imp_eq oexp_1_right oexp_add one_V_def)

lemma mult_oexp_ω: "Ord α ⟹ α * (α ↑ ω) = (α ↑ ω)"
by (metis Ord_1 Ord_ω oexp_1_right oexp_add one_plus_ω_equals_ω)

lemma type_imp_indecomposable:
assumes α: "Ord α"
and minor: "⋀X. X ⊆ elts α ⟹ ordertype X VWF = α ∨ ordertype (elts α - X) VWF = α"
shows "indecomposable α"
unfolding indecomposable_def
proof (intro conjI ballI)
fix β γ
assume β: "β ∈ elts α" and γ: "γ ∈ elts α"
then obtain βγ: "elts β ⊆ elts α" "elts γ ⊆ elts α" "Ord β" "Ord γ"
using α Ord_in_Ord Ord_trans by blast
then have oeq: "ordertype (elts β) VWF = β"
by auto
show "β + γ ∈ elts α"
proof (rule ccontr)
assume "β + γ ∉ elts α"
then obtain δ where δ: "Ord δ" "β + δ = α"
by (metis Ord_ordertype βγ(1) le_Ord_diff less_eq_V_def minor oeq)
then have "δ ∈ elts α"
using Ord_linear βγ γ ‹β + γ ∉ elts α› by blast
then have "ordertype (elts α - elts β) VWF = δ"
using δ ordertype_diff Limit_def α ‹Ord β› by blast
then show False
by (metis β ‹δ ∈ elts α› ‹elts β ⊆ elts α› oeq mem_not_refl minor)
qed
qed (use assms in auto)

text ‹This proof uses Cantor normal form, yet still is rather long›
proposition indecomposable_is_ω_power:
assumes inc: "indecomposable μ"
obtains "μ = 0" | δ where "Ord δ" "μ = ω↑δ"
proof (cases "μ = 0")
case True
then show thesis
by (simp add: that)
next
case False
obtain "Ord μ"
using Limit_def assms indecomposable_def by blast
then obtain αs ms where Cantor: "List.set αs ⊆ ON" "list.set ms ⊆ {0<..}"
"length αs = length ms" "Cantor_dec αs"
and μ: "μ = Cantor_sum αs ms"
using Cantor_nf_exists by blast
consider (0) "length αs = 0" | (1) "length αs = 1" | (2) "length αs ≥ 2"
by linarith
then show thesis
proof cases
case 0
then show ?thesis
using μ assms False indecomposable_def by auto
next
case 1
then obtain α m where αm: "αs = [α]" "ms = [m]"
by (metis One_nat_def ‹length αs = length ms› length_0_conv length_Suc_conv)
then obtain "Ord α" "m ≠ 0" "Ord (ω↑α)"
using ‹list.set αs ⊆ ON› ‹list.set ms ⊆ {0<..}› by auto
have μ: "μ = ω↑α * ord_of_nat m"
using αm by (simp add: μ)
moreover have "m = 1"
proof (rule ccontr)
assume "m ≠ 1"
then have 2: "m ≥ 2"
using ‹m ≠ 0› by linarith
then have "m = Suc 0 + Suc 0 + (m-2)"
by simp
then have "ord_of_nat m = 1 + 1 + ord_of_nat (m-2)"
by (metis add.left_neutral mult.left_neutral mult_succ ord_of_nat.simps ord_of_nat_add)
then have μeq: "μ = ω↑α + ω↑α + ω↑α * ord_of_nat (m-2)"
using μ by (simp add: add_mult_distrib)
moreover have less: "ω↑α < μ"
by (metis Ord_ω OrdmemD μeq ‹Ord α› add_le_cancel_left0 add_less_cancel_left0 le_less_trans less_V_def oexp_gt_0_iff zero_in_omega)
moreover have "ω↑α + ω↑α * ord_of_nat (m-2) < μ"
using "2" "μ" ‹Ord α› assms less indecomposableD less_V_def by auto
ultimately show False
using indecomposableD [OF inc, of "ω↑α" "ω↑α + ω↑α * ord_of_nat (m-2)"]
by (simp add: ‹Ord (ω↑α)› add.assoc)
qed
moreover have "Ord α"
using ‹List.set αs ⊆ ON› by (simp add: ‹αs = [α]›)
ultimately show ?thesis
by (metis One_nat_def mult.right_neutral ord_of_nat.simps one_V_def that(2))
next
case 2
then obtain α1 α2 αs' m1 m2 ms' where αm: "αs = α1#α2#αs'" "ms = m1#m2#ms'"
by (metis Cantor(3) One_nat_def Suc_1 impossible_Cons length_Cons list.size(3) not_numeral_le_zero remdups_adj.cases)
then obtain "Ord α1" "Ord α2" "m1 ≠ 0" "m2 ≠ 0" "Ord (ω↑α1)" "Ord (ω↑α2)"
"list.set αs' ⊆ ON" "list.set ms' ⊆ {0<..}"
using ‹list.set αs ⊆ ON› ‹list.set ms ⊆ {0<..}› by auto
have oCs: "Ord (Cantor_sum αs' ms')"
by (simp add: Ord_Cantor_sum ‹list.set αs' ⊆ ON›)
have α21: "α2 ∈ elts α1"
using Cantor_dec_Cons_iff αm(1) ‹Cantor_dec αs›
by (simp add: Ord_mem_iff_lt ‹Ord α1› ‹Ord α2›)
have "ω↑α2 ≠ 0"
by (simp add: ‹Ord α2›)
then have *: "(ω↑α2 * ord_of_nat m2 + Cantor_sum αs' ms') > 0"
by (simp add: OrdmemD ‹Ord (ω↑α2)› ‹m2 ≠ 0› mem_0_Ord oCs)
have μ: "μ = ω↑α1 * ord_of_nat m1 + (ω↑α2 * ord_of_nat m2 + Cantor_sum αs' ms')"
(is "μ = ?α + ?β")
using αm by (simp add: μ)
moreover
have "ω↑α2 * ord_of_nat m2 + Cantor_sum αs' ms' < ω↑α1 * ord_of_nat m1 + (ω↑α2 * ord_of_nat m2 + Cantor_sum αs' ms')"
if "α2 ∈ elts α1"
proof (rule less_ω_power)
show "Cantor_sum αs' ms' < ω↑α2"
using αm Cantor cnf_2 by auto
qed (use oCs ‹Ord α1› ‹m1 ≠ 0› ‹m2 ≠ 0› that in auto)
then have "?β < μ"
using α21 by (simp add: μ αm)
moreover have less: "?α < μ"
using oCs by (metis μ "*" add_less_cancel_left add.right_neutral)
ultimately have False
using indecomposableD [OF inc, of "?α" "?β"]
by (simp add: ‹Ord (ω↑α1)› ‹Ord (ω↑α2)› oCs)
then show ?thesis ..
qed
qed

corollary indecomposable_iff_ω_power:
"indecomposable μ ⟷ μ = 0 ∨ (∃δ. μ = ω↑δ ∧ Ord δ)"
by (meson indecomposable_0 indecomposable_ω_power indecomposable_is_ω_power)

theorem indecomposable_imp_type:
fixes X :: "bool ⇒ V set"
assumes γ: "indecomposable γ"
and "⋀b. ordertype (X b) VWF ≤ γ" "⋀b. small (X b)" "⋀b. X b ⊆ ON"
and "elts γ ⊆ (UN b. X b)"
shows "∃b. ordertype (X b) VWF = γ"
using γ [THEN indecomposable_imp_Ord] assms
proof (induction arbitrary: X)
case (succ β)
show ?case
proof (cases "β = 0")
case True
then have "∃b. 0 ∈ X b"
using succ.prems(5) by blast
then have "∃b. ordertype (X b) VWF ≠ 0"
using succ.prems(3) by auto
then have "∃b. ordertype (X b) VWF ≥ succ 0"
by (meson Ord_0 Ord_linear2 Ord_ordertype less_eq_V_0_iff succ_le_iff)
then show ?thesis
using True succ.prems(2) by blast
next
case False
then show ?thesis
using succ.prems by auto
qed
next
case (Limit γ)
then obtain δ where δ: "γ = ω↑δ" and "δ ≠ 0" "Ord δ"
by (metis Limit_eq_Sup_self image_ident indecomposable_is_ω_power not_succ_Limit oexp_0_right one_V_def zero_not_Limit)
show ?case
proof (cases "Limit δ")
case True
have ot: "∃b. ordertype (X b ∩ elts (ω↑α)) VWF = ω↑α"
if "α ∈ elts δ" for α
proof (rule Limit.IH)
have "Ord α"
using Ord_in_Ord ‹Ord δ› that by blast
then show "ω↑α ∈ elts γ"
by (simp add: Ord_mem_iff_lt δ ω_gt1 ‹Ord δ› oexp_less that)
show "indecomposable (ω↑α)"
using ‹Ord α› indecomposable_1 indecomposable_ω_power by fastforce
show "small (X b ∩ elts (ω↑α))" for b
by (meson down inf_le2)
show "ordertype (X b ∩ elts (ω ↑ α)) VWF ≤ ω ↑ α" for b
by (simp add: ‹Ord α› ordertype_le_Ord)
show "X b ∩ elts (ω ↑ α) ⊆ ON" for b
by (simp add: Limit.prems inf.coboundedI1)
show "elts (ω ↑ α) ⊆ (⋃b. X b ∩ elts (ω ↑ α))"
using Limit.prems Limit.hyps ‹ω ↑ α ∈ elts γ›
by clarsimp (metis Ord_trans UN_E indecomposable_imp_Ord subset_eq)
qed
define A where "A ≡ λb. {α ∈ elts δ. ordertype (X b ∩ elts (ω↑α)) VWF ≥ ω↑α}"
have Asmall: "small (A b)" for b
by (simp add: A_def)
have AON: "A b ⊆ ON" for b
using A_def ‹Ord δ› elts_subset_ON by blast
have eq: "elts δ = (⋃ b. A b)"
by (auto simp: A_def) (metis ot eq_refl)
then obtain b where b: "Sup (A b) = δ"
using ‹Limit δ›
apply (auto simp: UN_bool_eq)
by (metis AON ON_imp_Ord Ord_Sup Ord_linear_le Limit_eq_Sup_self Sup_Un_distrib Asmall sup.absorb2 sup.orderE)
have "ω↑α ≤ ordertype (X b) VWF" if "α ∈ A b" for α
proof -
have "(ω↑α) = ordertype ((X b) ∩ elts (ω↑α)) VWF"
using ‹Ord δ› that by (simp add: A_def Ord_in_Ord dual_order.antisym ordertype_le_Ord)
also have "… ≤ ordertype (X b) VWF"
by (simp add: Limit.prems ordertype_VWF_mono)
finally show ?thesis .
qed
then have "ordertype (X b) VWF ≥ Sup ((λα. ω↑α) ` A b)"
by blast
moreover have "Sup ((λα. ω↑α) ` A b) = ω ↑ Sup (A b)"
by (metis b Ord_ω ZFC_in_HOL.Sup_empty AON ‹δ ≠ 0› Asmall oexp_Sup omega_nonzero)
ultimately show ?thesis
using Limit.hyps Limit.prems δ b by auto
next
case False
then obtain β where β: "δ = succ β" "Ord β"
using Ord_cases ‹δ ≠ 0› ‹Ord δ› by auto
then have Ordωβ: "Ord (ω↑β)"
using Ord_oexp by blast
have subX12: "elts (ω↑β * ω) ⊆ (⋃b. X b)"
using Limit β δ by auto
define E where "E ≡ λn. {ω↑β * ord_of_nat n ..< ω↑β * ord_of_nat (Suc n)} ∩ ON"
have EON: "E n ⊆ ON" for n
using E_def by blast
have E_imp_less: "x < y" if "i < j" "x ∈ E i" "y ∈ E j" for x y i j
proof -
have "succ (i) ≤ ord_of_nat j"
using that(1) by force
then have "¬ y ≤ x"
using that
apply (auto simp: E_def)
by (metis Ordωβ Ord_ord_of_nat leD mult_cancel_le_iff ord_of_nat.simps(2) order_trans)
with that show ?thesis
by (meson EON ON_imp_Ord Ord_linear2)
qed
then have djE: "disjnt (E i) (E j)" if "i ≠ j" for i j
using that nat_neq_iff unfolding disjnt_def by auto
have less_imp_E: "i ≤ j" if "x < y" "x ∈ E i" "y ∈ E j" for x y i j
using that E_imp_less [OF _ ‹y ∈ E j› ‹x ∈ E i›] leI less_asym by blast
have inc: "indecomposable (ω↑β)"
using β indecomposable_1 indecomposable_ω_power by fastforce
have in_En: "ω↑β * ord_of_nat n + x ∈ E n" if "x ∈ elts (ω↑β)" for x n
using that Ordωβ Ord_in_Ord [OF Ordωβ] by (auto simp: E_def Ordωβ OrdmemD mult_succ)
have *: "elts γ = ⋃(range E)"
proof
have "∃m. ω↑β * m ≤ x ∧ x < ω↑β * succ (ord_of_nat m)"
if "x ∈ elts (ω↑β * ord_of_nat n)" for x n
using that
apply (clarsimp simp add: mult [of _ "ord_of_nat n"] lift_def)
by (metis add_less_cancel_left OrdmemD inc indecomposable_imp_Ord mult_succ plus sup_ge1)
moreover have "Ord x" if "x ∈ elts (ω↑β * ord_of_nat n)" for x n
by (meson Ordωβ Ord_in_Ord Ord_mult Ord_ord_of_nat that)
ultimately show "elts γ ⊆ ⋃(range E)"
by (auto simp: δ β E_def mult_Limit elts_ω)
have "x ∈ elts (ω↑β * succ(ord_of_nat n))"
if "Ord x" "x < ω↑β * succ (n)" for x n
by (metis that Ord_mem_iff_lt Ord_mult Ord_ord_of_nat inc indecomposable_imp_Ord ord_of_nat.simps(2))
then show "⋃(range E) ⊆ elts γ"
by (force simp: δ β E_def Limit.prems mult_Limit)
qed
have smE: "small (E n)" for n
by (metis "*" complete_lattice_class.Sup_upper down rangeI)
have otE: "ordertype (E n) VWF = ω↑β" for n
by (simp add: E_def inc indecomposable_imp_Ord mult_succ ordertype_interval_eq)

define cut where "cut ≡ λn x. odiff x (ω↑β * ord_of_nat n)"
have cutON: "cut n ` X ⊆ ON" if "X ⊆ ON" for n X
using that by (simp add: image_subset_iff cut_def ON_imp_Ord Ordωβ Ord_odiff)
have cut [simp]: "cut n (ω ↑ β * ord_of_nat n + x) = x" for x n
by (auto simp: cut_def)
have cuteq: "x ∈ cut n ` (X ∩ E n) ⟷ ω↑β * ord_of_nat n + x ∈ X"
if x: "x ∈ elts (ω↑β)" for x X n
proof
show "ω↑β * ord_of_nat n + x ∈ X" if "x ∈ cut n ` (X ∩ E n)"
using E_def Ordωβ Ord_odiff_eq image_iff local.cut_def that by auto
show "x ∈ cut n ` (X ∩ E n)"
if "ω↑β * ord_of_nat n + x ∈ X"
by (metis (full_types) IntI cut image_iff in_En that x)
qed
have ot_cuteq: "ordertype (cut n ` (X ∩ E n)) VWF = ordertype (X ∩ E n) VWF" for n X
proof (rule ordertype_VWF_inc_eq)
show "X ∩ E n ⊆ ON"
using E_def by blast
then show "cut n ` (X ∩ E n) ⊆ ON"
by (simp add: cutON)
show "small (X ∩ E n)"
by (meson Int_lower2 smE smaller_than_small)
show "cut n x < cut n y"
if "x ∈ X ∩ E n" "y ∈ X ∩ E n" "x < y" for x y
using that ‹X ∩ E n ⊆ ON› by(simp add: E_def Ordωβ Ord_odiff_less_odiff local.cut_def)
qed

define N where "N ≡ λb. {n. ordertype (X b ∩ E n) VWF = ω↑β}"
have "∃b. infinite (N b)"
proof (rule ccontr)
assume "∄b. infinite (N b)"
then obtain n where "⋀b. n ∉ N b"
apply (simp add: ex_bool_eq)
by (metis (full_types) finite_nat_set_iff_bounded not_less_iff_gr_or_eq)
moreover
have "∃b. ordertype (cut n ` (X b ∩ E n)) VWF = ω↑β"
proof (rule Limit.IH)
show "ω↑β ∈ elts γ"
by (metis Limit.hyps Limit_def Limit_omega Ord_mem_iff_less_TC β δ mult_le2 not_succ_Limit oexp_succ omega_nonzero one_V_def)
show "indecomposable (ω↑β)"
by (simp add: inc)
show "ordertype (cut n ` (X b ∩ E n)) VWF ≤ ω↑β" for b
by (metis "otE" inf_le2 ordertype_VWF_mono ot_cuteq smE)
show "small (cut n ` (X b ∩ E n))" for b
using smE subset_iff_less_eq_V
by (meson inf_le2 replacement)
show "cut n ` (X b ∩ E n) ⊆ ON" for b
using E_def cutON by auto
have "elts (ω↑β * succ n) ⊆ ⋃(range X)"
by (metis Ordωβ Ord_ω Ord_ord_of_nat less_eq_V_def mult_cancel_le_iff ord_of_nat.simps(2) ord_of_nat_le_omega order_trans subX12)
then show "elts (ω↑β) ⊆ (⋃b. cut n ` (X b ∩ E n))"
by (auto simp: mult_succ mult_Limit UN_subset_iff cuteq UN_bool_eq)
qed
then have "∃b. ordertype (X b ∩ E n) VWF = ω↑β"
by (simp add: ot_cuteq)
ultimately show False
by (simp add: N_def)
qed
then obtain b where b: "infinite (N b)"
by blast
then obtain φ :: "nat ⇒ nat" where φ: "bij_betw φ UNIV (N b)" and mono: "strict_mono φ"
by (meson bij_enumerate enumerate_mono strict_mono_def)
then have "ordertype (X b ∩ E (φ n)) VWF = ω↑β" for n
using N_def bij_betw_imp_surj_on by blast
moreover have "small (X b ∩ E (φ n))" for n
by (meson inf_le2 smE subset_iff_less_eq_V)
ultimately have "∃f. bij_betw f (X b ∩ E (φ n)) (elts (ω↑β)) ∧ (∀x ∈ X b ∩ E (φ n). ∀y ∈ X b ∩ E (φ n). f x < f y ⟷ (x,y) ∈ VWF)"
for n by (metis Ord_ordertype ordertype_VWF_eq_iff)
then obtain F where bijF: "⋀n. bij_betw (F n) (X b ∩ E (φ n)) (elts (ω↑β))"
and F: "⋀n. ∀x ∈ X b ∩ E (φ n). ∀y ∈ X b ∩ E (φ n). F n x < F n y ⟷ (x,y) ∈ VWF"
by metis
then have F_bound: "⋀n. ∀x ∈ X b ∩ E (φ n). F n x < ω↑β"
by (metis Ord_ω Ord_oexp OrdmemD β(2) bij_betw_imp_surj_on image_eqI)
have F_Ord: "⋀n. ∀x ∈ X b ∩ E (φ n). Ord (F n x)"
by (metis otE ON_imp_Ord Ord_ordertype bijF bij_betw_def elts_subset_ON imageI)

have inc: "φ n ≥ n" for n
by (simp add: mono strict_mono_imp_increasing)

have djφ: "disjnt (E (φ i)) (E (φ j))" if "i ≠ j" for i j
by (rule djE) (use φ that in ‹auto simp: bij_betw_def inj_def›)
define Y where "Y ≡ (⋃n. E (φ n))"
have "∃n. y ∈ E (φ n)" if "y ∈ Y" for y
using Y_def that by blast
then obtain ι where ι: "⋀y. y ∈ Y ⟹ y ∈ E (φ (ι y))"
by metis
have "Y ⊆ ON"
by (auto simp: Y_def E_def)
have ιle: "ι x ≤ ι y" if "x < y" "x ∈ Y" "y ∈ Y" for x y
using less_imp_E strict_mono_less_eq that ι [OF ‹x ∈ Y›] ι [OF ‹y ∈ Y›] mono
unfolding Y_def by blast
have eqι: "x ∈ E (φ k) ⟹ ι x = k" for x k
using ι unfolding Y_def
by (meson UN_I disjnt_iff djφ iso_tuple_UNIV_I)

have upper: "ω↑β * ord_of_nat (ι x) ≤ x" if "x ∈ Y" for x
using that
proof (clarsimp simp add: Y_def eqι)
fix u v
assume u: "u ∈ elts (ω↑β * ord_of_nat v)" and v: "x ∈ E (φ v)"
then have "u < ω↑β * ord_of_nat v"
by (simp add: OrdmemD β(2))
also have "… ≤ ω↑β * ord_of_nat (φ v)"
by (simp add: β(2) inc)
also have "… ≤ x"
using v by (simp add: E_def)
finally show "u ∈ elts x"
using ‹Y ⊆ ON›
by (meson ON_imp_Ord Ord_ω Ord_in_Ord Ord_mem_iff_lt Ord_mult Ord_oexp Ord_ord_of_nat β(2) that u)
qed

define G where "G ≡ λx. ω↑β * ord_of_nat (ι x) + F (ι x) x"
have G_strict_mono: "G x < G y" if "x < y" "x ∈ X b ∩ Y" "y ∈ X b ∩ Y" for x y
proof (cases "ι x = ι y")
case True
then show ?thesis
using that unfolding G_def
by (metis F Int_iff add_less_cancel_left Limit.prems(4) ON_imp_Ord VWF_iff_Ord_less ι)
next
case False
then have "ι x < ι y"
by (meson IntE ιle le_less that)
then show ?thesis
using that by (simp add: G_def F_Ord F_bound Ordωβ ι mult_nat_less_add_less)
qed

have "ordertype (X b ∩ Y) VWF = (ω↑β) * ω"
proof (rule ordertype_VWF_eq_iff [THEN iffD2])
show "Ord (ω↑β * ω)"
by (simp add: β)
show "small (X b ∩ Y)"
by (meson Limit.prems(3) inf_le1 subset_iff_less_eq_V)
have "bij_betw G (X b ∩ Y) (elts (ω↑β * ω))"
proof (rule bij_betw_imageI)
show "inj_on G (X b ∩ Y)"
proof (rule linorder_inj_onI)
fix x y
assume xy: "x < y" "x ∈ (X b ∩ Y)" "y ∈ (X b ∩ Y)"
show "G x ≠ G y"
using G_strict_mono xy by force
next
show "x ≤ y ∨ y ≤ x"
if "x ∈ (X b ∩ Y)" "y ∈ (X b ∩ Y)" for x y
using that ‹X b ⊆ ON› by (clarsimp simp: Y_def) (metis ON_imp_Ord Ord_linear Ord_trans)
qed
show "G ` (X b ∩ Y) = elts (ω↑β * ω)"
proof
show "G ` (X b ∩ Y) ⊆ elts (ω↑β * ω)"
using ‹X b ⊆ ON›
apply (clarsimp simp: G_def mult_Limit Y_def eqι)
by (metis IntI add_mem_right_cancel bijF bij_betw_imp_surj_on image_eqI mult_succ ord_of_nat_ω succ_in_omega)
show "elts (ω↑β * ω) ⊆ G ` (X b ∩ Y)"
proof
fix x
assume x: "x ∈ elts (ω↑β * ω)"
then obtain k where n: "x ∈ elts (ω↑β * ord_of_nat (Suc k))"
and minim: "⋀m. m < Suc k ⟹ x ∉ elts (ω↑β * ord_of_nat m)"
using elts_mult_ωE
by (metis old.nat.exhaust)
then obtain y where y: "y ∈ elts (ω↑β)" and xeq: "x = ω↑β * ord_of_nat k + y"
using x by (auto simp: mult_succ elim: mem_plus_V_E)
then have 1: "inv_into (X b ∩ E (φ k)) (F k) y ∈ (X b ∩ E (φ k))"
by (metis bijF bij_betw_def inv_into_into)
then have "(inv_into (X b ∩ E (φ k)) (F k) y) ∈ X b ∩ Y"
by (force simp: Y_def)
moreover have "G (inv_into (X b ∩ E (φ k)) (F k) y) = x"
by (metis "1" G_def Int_iff bijF bij_betw_inv_into_right eqι xeq y)
ultimately show "x ∈ G ` (X b ∩ Y)"
by blast
qed
qed
qed
moreover have "(x,y) ∈ VWF"
if "x ∈ X b" "x ∈ Y" "y ∈ X b" "y ∈ Y" "G x < G y" for x y
proof -
have "x < y"
using that by (metis G_strict_mono Int_iff Limit.prems(4) ON_imp_Ord Ord_linear_lt less_asym)
then show ?thesis
using ON_imp_Ord ‹Y ⊆ ON› that by auto
qed
moreover have "G x < G y"
if "x ∈ X b" "x ∈ Y" "y ∈ X b" "y ∈ Y" "(x, y) ∈ VWF" for x y
proof -
have "x < y"
using that ON_imp_Ord ‹Y ⊆ ON› by auto
then show ?thesis
by (simp add: G_strict_mono that)
qed
ultimately show "∃f. bij_betw f (X b ∩ Y) (elts (ω↑β * ω)) ∧ (∀x∈(X b ∩ Y). ∀y∈(X b ∩ Y). f x < f y ⟷ ((x, y) ∈ VWF))"
by blast
qed
moreover have "ordertype (⋃n. X b ∩ E (φ n)) VWF ≤ ordertype (X b) VWF"
using Limit.prems(3) ordertype_VWF_mono by auto
ultimately have "ordertype (X b) VWF = (ω↑β) * ω"
using Limit.hyps Limit.prems(2) β δ
using Y_def by auto
then show ?thesis
using Limit.hyps β δ by auto
qed
qed auto

corollary indecomposable_imp_type2:
assumes α: "indecomposable γ" "X ⊆ elts γ"
shows "ordertype X VWF = γ ∨ ordertype (elts γ - X) VWF = γ"
proof -
have "Ord γ"
using assms indecomposable_imp_Ord by blast
have "∃b. ordertype (if b then X else elts γ - X) VWF = γ"
proof (rule indecomposable_imp_type)
show "ordertype (if b then X else elts γ - X) VWF ≤ γ" for b
by (simp add: ‹Ord γ› assms ordertype_le_Ord)
show "(if b then X else elts γ - X) ⊆ ON" for b
using ‹Ord γ› assms elts_subset_ON by auto
qed (use assms down in auto)
then show ?thesis
by (metis (full_types))
qed

subsection ‹From ordinals to order types›

lemma indecomposable_ordertype_eq:
assumes indec: "indecomposable α" and α: "ordertype A VWF = α" and A: "B ⊆ A" "small A"
shows "ordertype B VWF = α ∨ ordertype (A-B) VWF = α"
proof (rule ccontr)
assume "¬ (ordertype B VWF = α ∨ ordertype (A - B) VWF = α)"
moreover have "ordertype (ordermap A VWF ` B) VWF = ordertype B VWF"
using ‹B ⊆ A› by (auto intro: ordertype_image_ordermap [OF ‹small A›])
moreover have "ordertype (elts α - ordermap A VWF ` B) VWF = ordertype (A - B) VWF"
by (metis ordertype_map_image α A elts_of_set ordertype_def replacement)
moreover have "ordermap A VWF ` B ⊆ elts α"
using α A by blast
ultimately show False
using indecomposable_imp_type2 [OF ‹indecomposable α›]  ‹small A› by metis
qed

lemma indecomposable_ordertype_ge:
assumes indec: "indecomposable α" and α: "ordertype A VWF ≥ α" and small: "small A" "small B"
shows "ordertype B VWF ≥ α ∨ ordertype (A-B) VWF ≥ α"
proof -
obtain A' where "A' ⊆ A" "ordertype A' VWF = α"
by (meson α ‹small A› indec indecomposable_def le_ordertype_obtains_subset)
then have "ordertype (B ∩ A') VWF = α ∨ ordertype (A'-B) VWF = α"
by (metis Diff_Diff_Int Diff_subset Int_commute ‹small A› indecomposable_ordertype_eq indec smaller_than_small)
moreover have "ordertype (B ∩ A') VWF ≤ ordertype B VWF"
by (meson Int_lower1 small ordertype_VWF_mono smaller_than_small)
moreover have "ordertype (A'-B) VWF ≤ ordertype (A-B) VWF"
by (meson Diff_mono Diff_subset ‹A' ⊆ A› ‹small A› order_refl ordertype_VWF_mono smaller_than_small)
ultimately show ?thesis
by blast
qed

text ‹now for finite partitions›
lemma indecomposable_ordertype_finite_eq:
assumes "indecomposable α"
and 𝒜: "finite 𝒜" "pairwise disjnt 𝒜" "⋃𝒜 = A" "𝒜 ≠ {}" "ordertype A VWF = α" "small A"
shows "∃X ∈ 𝒜. ordertype X VWF = α"
using 𝒜
proof (induction arbitrary: A)
case (insert X 𝒜)
show ?case
proof (cases "𝒜 = {}")
case True
then show ?thesis
using insert.prems by blast
next
case False
have smA: "small (⋃𝒜)"
using insert.prems by auto
show ?thesis
proof (cases "∃X ∈ 𝒜. ordertype X VWF = α")
case True
then show ?thesis
using insert.prems by blast
next
case False
have "X = A - ⋃𝒜"
using insert.hyps insert.prems by (auto simp: pairwise_insert disjnt_iff)
then have "ordertype X VWF = α"
using indecomposable_ordertype_eq assms insert False
by (metis Union_mono cSup_singleton pairwise_insert smA subset_insertI)
then show ?thesis
using insert.prems by blast
qed
qed
qed auto

lemma indecomposable_ordertype_finite_ge:
assumes indec: "indecomposable α"
and 𝒜: "finite 𝒜" "A ⊆ ⋃𝒜" "𝒜 ≠ {}" "ordertype A VWF ≥ α" "small (⋃𝒜)"
shows "```