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 "