theory Erdos_Milner imports Partitions begin subsection ‹Erdős-Milner theorem› text ‹P. Erdős and E. C. Milner, A Theorem in the Partition Calculus. Canadian Math. Bull. 15:4 (1972), 501-505. Corrigendum, Canadian Math. Bull. 17:2 (1974), 305.› text ‹The paper defines strong types as satisfying the criteria below. It remarks that ordinals satisfy those criteria. Here is a (too complicated) proof.› proposition strong_ordertype_eq: assumes D: "D ⊆ elts β" and "Ord β" obtains L where "⋃(List.set L) = D" "⋀X. X ∈ List.set L ⟹ indecomposable (tp X)" and "⋀M. ⟦M ⊆ D; ⋀X. X ∈ List.set L ⟹ tp (M ∩ X) ≥ tp X⟧ ⟹ tp M = tp D" proof - define φ where "φ ≡ inv_into D (ordermap D VWF)" then have bij_φ: "bij_betw φ (elts (tp D)) D" using D bij_betw_inv_into down ordermap_bij by blast have φ_cancel_left: "⋀d. d ∈ D ⟹ φ (ordermap D VWF d) = d" by (metis D φ_def bij_betw_inv_into_left down ordermap_bij total_on_VWF wf_VWF) have φ_cancel_right: "⋀γ. γ ∈ elts (tp D) ⟹ ordermap D VWF (φ γ) = γ" by (metis φ_def f_inv_into_f ordermap_surj subsetD) have "small D" "D ⊆ ON" using assms down elts_subset_ON [of β] by auto then have φ_less_iff: "⋀γ δ. ⟦γ ∈ elts (tp D); δ ∈ elts (tp D)⟧ ⟹ φ γ < φ δ ⟷ γ < δ" by (metis φ_def inv_ordermap_VWF_mono_iff inv_ordermap_mono_eq less_V_def) obtain αs where "List.set αs ⊆ ON" and "ω_dec αs" and tpD_eq: "tp D = ω_sum αs" using Ord_ordertype ω_nf_exists by blast ― ‹Cantor normal form of the ordertype› have ord [simp]: "Ord (αs ! k)" "Ord (ω_sum (take k αs))" if "k < length αs" for k using that ‹list.set αs ⊆ ON› by (auto simp: dual_order.trans set_take_subset elim: ON_imp_Ord) define E where "E ≡ λk. lift (ω_sum (take k αs)) (ω↑(αs!k))" define L where "L ≡ map (λk. φ ` (elts (E k))) [0..<length αs]" have lengthL [simp]: "length L = length αs" by (simp add: L_def) have in_elts_E_less: "elts (E k') ≪ elts (E k)" if "k'<k" "k < length αs" for k k' ― ‹The ordinals have been partitioned into disjoint intervals› proof - have ordω: "Ord (ω ↑ αs ! k')" using that by auto from that id_take_nth_drop [of k' "take k αs"] obtain l where "take k αs = take k' αs @ (αs!k') # l" by (simp add: min_def) then show ?thesis using that unfolding E_def lift_def less_sets_def by (auto dest!: OrdmemD [OF ordω] intro: less_le_trans) qed have elts_E: "elts (E k) ⊆ elts (ω_sum αs)" if "k < length αs" for k proof - have "ω ↑ (αs!k) ≤ ω_sum (drop k αs)" by (metis that Cons_nth_drop_Suc ω_sum_Cons add_le_cancel_left0) then have "(+) (ω_sum (take k αs)) ` elts (ω ↑ (αs!k)) ⊆ elts (ω_sum (take k αs) + ω_sum (drop k αs))" by blast also have "… = elts (ω_sum αs)" using ω_sum_take_drop by auto finally show ?thesis by (simp add: lift_def E_def) qed have ω_sum_in_tpD: "ω_sum (take k αs) + γ ∈ elts (tp D)" if "γ ∈ elts (ω ↑ αs!k)" "k < length αs" for γ k using elts_E lift_def that tpD_eq by (auto simp: E_def) have Ord_φ: "Ord (φ (ω_sum (take k αs) + γ))" if "γ ∈ elts (ω ↑ αs!k)" "k < length αs" for γ k using ω_sum_in_tpD ‹D ⊆ ON› bij_φ bij_betw_imp_surj_on that by fastforce define π where "π ≡ λk. ((λy. odiff y (ω_sum (take k αs))) ∘ ordermap D VWF)" ― ‹mapping the segments of @{term D} into some power of @{term ω}› have bij_π: "bij_betw (π k) (φ ` elts (E k)) (elts (ω ↑ (αs!k)))" if "k < length αs" for k using that by (auto simp: bij_betw_def π_def E_def inj_on_def lift_def image_comp ω_sum_in_tpD φ_cancel_right that) have π_iff: "π k x < π k y ⟷ (x,y) ∈ VWF" if "x ∈ φ ` elts (E k)" "y ∈ φ ` elts (E k)" "k < length αs" for k x y using that by (auto simp: π_def E_def lift_def ω_sum_in_tpD φ_cancel_right Ord_φ φ_less_iff) have tp_E_eq [simp]: "tp (φ ` elts (E k)) = ω↑(αs!k)" if k: "k < length αs" for k by (metis Ord_ω Ord_oexp π_iff bij_π ord(1) ordertype_VWF_eq_iff replacement small_elts that) have tp_L_eq [simp]: "tp (L!k) = ω↑(αs!k)" if "k < length αs" for k by (simp add: L_def that) have UL_eq_D: "⋃ (list.set L) = D" proof (rule antisym) show "⋃ (list.set L) ⊆ D" by (force simp: L_def tpD_eq bij_betw_apply [OF bij_φ] dest: elts_E) show "D ⊆ ⋃ (list.set L)" proof fix δ assume "δ ∈ D" then have "ordermap D VWF δ ∈ elts (ω_sum αs)" by (metis ‹small D› ordermap_in_ordertype tpD_eq) then show "δ ∈ ⋃ (list.set L)" using ‹δ ∈ D› φ_cancel_left in_elts_ω_sum by (fastforce simp: L_def E_def image_iff lift_def) qed qed show thesis proof show "indecomposable (tp X)" if "X ∈ list.set L" for X using that by (auto simp: L_def indecomposable_ω_power) next fix M assume "M ⊆ D" and *: "⋀X. X ∈ list.set L ⟹ tp X ≤ tp (M ∩ X)" show "tp M = tp D" proof (rule antisym) show "tp M ≤ tp D" by (simp add: ‹M ⊆ D› ‹small D› ordertype_VWF_mono) define σ where "σ ≡ λX. inv_into (M ∩ X) (ordermap (M ∩ X) VWF)" ― ‹The bijection from an @{term ω}-power into the appropriate segment of @{term M}› have bij_σ: "bij_betw (σ X) (elts (tp (M ∩ X))) (M ∩ X)" for X unfolding σ_def by (meson ‹M ⊆ D› ‹small D› bij_betw_inv_into inf_le1 ordermap_bij smaller_than_small total_on_VWF wf_VWF) have Ord_σ: "Ord (σ X α)" if "α ∈ elts (tp (M ∩ X))" for α X using ‹D ⊆ ON› ‹M ⊆ D› bij_betw_apply [OF bij_σ] that by blast have σ_cancel_right: "⋀γ X. γ ∈ elts (tp (M ∩ X)) ⟹ ordermap (M ∩ X) VWF (σ X γ) = γ" by (metis σ_def f_inv_into_f ordermap_surj subsetD) have smM: "small (M ∩ X)" for X by (meson ‹M ⊆ D› ‹small D› inf_le1 subset_iff_less_eq_V) have "∃k < length αs. γ ∈ elts (E k)" if γ: "γ ∈ elts (tp D)" for γ proof - obtain X where "X ∈ set L" and X: "φ γ ∈ X" by (metis UL_eq_D γ Union_iff φ_def in_mono inv_into_into ordermap_surj) then have "∃k < length αs. γ ∈ elts (E k) ∧ X = φ ` elts (E k)" apply (clarsimp simp: L_def) by (metis γ φ_cancel_right elts_E in_mono tpD_eq) then show ?thesis by blast qed then obtain K where K: "⋀γ. γ ∈ elts (tp D) ⟹ K γ < length αs ∧ γ ∈ elts (E (K γ))" by metis ― ‹The index from @{term "tp D"} to the appropriate segment number› define ψ where "ψ ≡ λd. σ (L ! K (ordermap D VWF d)) (π (K (ordermap D VWF d)) d)" show "tp D ≤ tp M" proof (rule ordertype_inc_le) show "small D" "small M" using ‹M ⊆ D› ‹small D› subset_iff_less_eq_V by auto next fix d' d assume xy: "d' ∈ D" "d ∈ D" and "(d',d) ∈ VWF" then have "d' < d" using ON_imp_Ord ‹D ⊆ ON› by auto let ?γ' = "ordermap D VWF d'" let ?γ = "ordermap D VWF d" have len': "K ?γ' < length αs" and elts': "?γ' ∈ elts (E (K ?γ'))" and len: "K ?γ < length αs" and elts: "?γ ∈ elts (E (K ?γ))" using K ‹d' ∈ D› ‹d ∈ D› by (auto simp: ‹small D› ordermap_in_ordertype) have Ord_σL: "Ord (σ (L!k) (π k d))" if "d ∈ φ ` elts (E k)" "k < length αs" for k d by (metis (mono_tags) "*" Ord_σ bij_π bij_betw_apply lengthL nth_mem that tp_L_eq vsubsetD) have "?γ' < ?γ" by (simp add: ‹(d', d) ∈ VWF› ‹small D› ordermap_mono_less xy) then have "K ?γ' ≤ K ?γ" using elts' elts in_elts_E_less by (meson leI len' less_asym less_sets_def) then consider (less) "K ?γ' < K ?γ" | (equal) "K ?γ' = K ?γ" by linarith then have "σ (L ! K ?γ') (π (K ?γ') d') < σ (L ! K ?γ) (π (K ?γ) d)" proof cases case less obtain †: "σ (L ! K ?γ') (π (K ?γ') d') ∈ M ∩ L ! K ?γ'" "σ (L ! K ?γ) (π (K ?γ) d) ∈ M ∩ L ! K ?γ" using elts' elts len' len * [THEN vsubsetD] by (metis lengthL φ_cancel_left bij_π bij_σ bij_betw_imp_surj_on imageI nth_mem tp_L_eq xy) then have "ordermap D VWF (σ (L ! K ?γ') (π (K ?γ') d')) ∈ elts (E (K ?γ'))" "ordermap D VWF (σ (L ! K ?γ) (π (K ?γ) d)) ∈ elts (E (K ?γ))" using len' len elts_E tpD_eq by (fastforce simp: L_def φ_cancel_right)+ then have "ordermap D VWF (σ (L ! K ?γ') (π (K ?γ') d')) < ordermap D VWF (σ (L ! K ?γ) (π (K ?γ) d))" using in_elts_E_less len less by (meson less_sets_def) moreover have "σ (L ! K ?γ') (π (K ?γ') d') ∈ D" "σ (L ! K ?γ) (π (K ?γ) d) ∈ D" using ‹M ⊆ D› † by auto ultimately show ?thesis by (metis ‹small D› φ_cancel_left φ_less_iff ordermap_in_ordertype) next case equal have σ_less: "⋀X γ δ. ⟦γ < δ; γ ∈ elts (tp (M ∩ X)); δ ∈ elts (tp (M ∩ X))⟧ ⟹ σ X γ < σ X δ" by (metis ‹D ⊆ ON› ‹M ⊆ D› σ_def dual_order.trans inv_ordermap_VWF_strict_mono_iff le_infI1 smM) have "π (K ?γ) d' < π (K ?γ) d" by (metis equal ‹(d', d) ∈ VWF› φ_cancel_left π_iff elts elts' imageI len xy) then show ?thesis unfolding equal by (metis * [THEN vsubsetD] lengthL φ_cancel_left σ_less bij_π bij_betw_imp_surj_on elts elts' image_eqI len local.equal nth_mem tp_L_eq xy) qed moreover have "Ord (σ (L ! K ?γ') (π (K ?γ') d'))" "Ord (σ (L ! K ?γ) (π (K ?γ) d))" using Ord_σL φ_cancel_left elts len elts' len' xy by fastforce+ ultimately show "(ψ d', ψ d) ∈ VWF" by (simp add: ψ_def) next show "ψ ` D ⊆ M" proof (clarsimp simp: ψ_def) fix d assume "d ∈ D" let ?γ = "ordermap D VWF d" have len: "K ?γ < length αs" and elts: "?γ ∈ elts (E (K ?γ))" using K ‹d ∈ D› by (auto simp: ‹small D› ordermap_in_ordertype) have "π (K ?γ) d ∈ elts (tp (L! (K ?γ)))" using bij_π [OF len] ‹d ∈ D› by (metis φ_cancel_left bij_betw_apply elts imageI len tp_L_eq) then show "σ (L ! K (ordermap D VWF d)) (π (K (ordermap D VWF d)) d) ∈ M" by (metis "*" lengthL Int_iff bij_σ bij_betw_apply len nth_mem vsubsetD) qed qed auto qed qed (simp add: UL_eq_D) qed text ‹The ``remark'' of Erdős and E. C. Milner, Canad. Math. Bull. Vol. 17 (2), 1974› proposition indecomposable_imp_Ex_less_sets: assumes indec: "indecomposable α" and "α ≥ ω" and A: "tp A = α" "small A" "A ⊆ ON" and "x ∈ A" and A1: "tp A1 = α" "A1 ⊆ A" obtains A2 where "tp A2 = α" "A2 ⊆ A1" "{x} ≪ A2" proof - have "Ord α" using indec indecomposable_imp_Ord by blast have "Limit α" by (meson ω_gt1 assms indec indecomposable_imp_Limit less_le_trans) define φ where "φ ≡ inv_into A (ordermap A VWF)" then have bij_φ: "bij_betw φ (elts α) A" using A bij_betw_inv_into down ordermap_bij by blast have bij_om: "bij_betw (ordermap A VWF) A (elts α)" using A down ordermap_bij by blast define γ where "γ ≡ ordermap A VWF x" have γ: "γ ∈ elts α" unfolding γ_def using A ‹x ∈ A› down by auto then have "Ord γ" using Ord_in_Ord ‹Ord α› by blast define B where "B ≡ φ ` (elts (succ γ))" have B: "{y ∈ A. ordermap A VWF y ≤ ordermap A VWF x} ⊆ B" apply (clarsimp simp add: B_def γ_def image_iff φ_def) by (metis Ord_linear Ord_ordermap OrdmemD bij_betw_inv_into_left bij_om leD) show thesis proof have "small A1" by (meson ‹small A› A1 smaller_than_small) then have "tp (A1 - B) ≤ tp A1" by (simp add: ordertype_VWF_mono) moreover have "tp (A1 - B) ≥ α" proof - have "¬ (α ≤ tp B)" unfolding B_def proof (subst ordertype_VWF_inc_eq) show "elts (succ γ) ⊆ ON" by (auto simp: γ_def ordertype_VWF_inc_eq intro: Ord_in_Ord) have sub: "elts (succ γ) ⊆ elts α" using Ord_trans γ ‹Ord α› by auto then show "φ ` elts (succ γ) ⊆ ON" using ‹A ⊆ ON› bij_φ bij_betw_imp_surj_on by blast have "succ γ ∈ elts α" using γ Limit_def ‹Limit α› by blast with A sub show "φ u < φ v" if "u ∈ elts (succ γ)" and "v ∈ elts (succ γ)" and "u < v" for u v by (metis φ_def inv_ordermap_VWF_strict_mono_iff subsetD that) show "¬ α ≤ tp (elts (succ γ))" by (metis Limit_def Ord_succ γ ‹Limit α› ‹Ord γ› mem_not_refl ordertype_eq_Ord vsubsetD) qed auto then show ?thesis using indecomposable_ordertype_ge [OF indec, of A1 B] ‹small A1› A1 by (auto simp: B_def) qed ultimately show "tp (A1 - B) = α" using A1 by blast have "{x} ≪ (A - B)" using assms B apply (clarsimp simp: less_sets_def φ_def subset_iff) by (metis Ord_not_le VWF_iff_Ord_less less_V_def order_refl ordermap_mono_less trans_VWF wf_VWF) with ‹A1 ⊆ A› show "{x} ≪ (A1 - B)" by auto qed auto qed text ‹the main theorem, from which they derive the headline result› theorem Erdos_Milner_aux: assumes part: "partn_lst_VWF α [k, γ] 2" and indec: "indecomposable α" and "k > 1" "Ord γ" and β: "β ∈ elts ω1" shows "partn_lst_VWF (α*β) [ord_of_nat (2*k), min γ (ω*β)] 2" proof (cases "α≤1 ∨ β=0") case True have "Ord α" using indec indecomposable_def by blast show ?thesis proof (cases "β=0") case True then show ?thesis by (simp add: partn_lst_triv0 [where i=1]) next case False then consider (0) "α=0" | (1) "α=1" by (metis Ord_0 OrdmemD True ‹Ord α› mem_0_Ord one_V_def order.antisym succ_le_iff) then show ?thesis proof cases case 0 with part show ?thesis by (force simp add: partn_lst_def nsets_empty_iff less_Suc_eq) next case 1 then obtain "Ord β" by (meson ON_imp_Ord Ord_ω1 True β elts_subset_ON) then obtain i where "i < Suc (Suc 0)" "[ord_of_nat k, γ] ! i ≤ α" using partn_lst_VWF_nontriv [OF part] 1 by auto then have "γ ≤ 1" using ‹α=1› ‹k > 1› by (fastforce simp: less_Suc_eq) then have "min γ (ω*β) ≤ 1" by (metis Ord_1 Ord_ω Ord_linear_le Ord_mult ‹Ord β› min_def order_trans) then show ?thesis using False by (auto simp: True ‹Ord β› ‹β≠0› ‹α=1› intro!: partn_lst_triv1 [where i=1]) qed qed next case False then have "α ≥ ω" by (meson Ord_1 Ord_not_less indec indecomposable_def indecomposable_imp_Limit omega_le_Limit) have "0 ∈ elts β" "β ≠ 0" using False Ord_ω1 Ord_in_Ord β mem_0_Ord by blast+ show ?thesis unfolding partn_lst_def proof clarsimp fix f assume "f ∈ [elts (α*β)]⇗2⇖ → {..<Suc (Suc 0)}" then have f: "f ∈ [elts (α*β)]⇗2⇖ → {..<2::nat}" by (simp add: eval_nat_numeral) obtain ord [iff]: "Ord α" "Ord β" "Ord (α*β)" using Ord_ω1 Ord_in_Ord β indec indecomposable_imp_Ord Ord_mult by blast have *: False if i [rule_format]: "∀H. tp H = ord_of_nat (2*k) ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {0}" and ii [rule_format]: "∀H. tp H = γ ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {1}" and iii [rule_format]: "∀H. tp H = (ω*β) ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {1}" proof - have Ak0: "∃X ∈ [A]⇗k⇖. f ` [X]⇗2⇖ ⊆ {0}" ―‹remark (8) about @{term"A ⊆ S"}› if A_αβ: "A ⊆ elts (α*β)" and ot: "tp A ≥ α" for A proof - let ?g = "inv_into A (ordermap A VWF)" have "small A" using down that by auto then have inj_g: "inj_on ?g (elts α)" by (meson inj_on_inv_into less_eq_V_def ordermap_surj ot subset_trans) have om_A_less: "⋀x y. ⟦x ∈ A; y ∈ A; x < y⟧ ⟹ ordermap A VWF x < ordermap A VWF y" using ord by (meson A_αβ Ord_in_Ord VWF_iff_Ord_less ‹small A› in_mono ordermap_mono_less trans_VWF wf_VWF) have α_sub: "elts α ⊆ ordermap A VWF ` A" by (metis ‹small A› elts_of_set less_eq_V_def ordertype_def ot replacement) have g: "?g ∈ elts α → elts (α*β)" by (meson A_αβ Pi_I' α_sub inv_into_into subset_eq) then have fg: "f ∘ (λX. ?g ` X) ∈ [elts α]⇗2⇖ → {..<2}" by (rule nsets_compose_image_funcset [OF f _ inj_g]) obtain i H where "i < 2" "H ⊆ elts α" and ot_eq: "tp H = [k,γ]!i" "(f ∘ (λX. ?g ` X)) ` (nsets H 2) ⊆ {i}" using ii partn_lst_E [OF part fg] by (auto simp: eval_nat_numeral) then consider (0) "i=0" | (1) "i=1" by linarith then show ?thesis proof cases case 0 then have "f ` [inv_into A (ordermap A VWF) ` H]⇗2⇖ ⊆ {0}" using ot_eq ‹H ⊆ elts α› α_sub by (auto simp: nsets_def [of _ k] inj_on_inv_into elim!: nset_image_obtains) moreover have "finite H ∧ card H = k" using 0 ot_eq ‹H ⊆ elts α› down by (simp add: finite_ordertype_eq_card) then have "inv_into A (ordermap A VWF) ` H ∈ [A]⇗k⇖" using ‹H ⊆ elts α› α_sub by (auto simp: nsets_def [of _ k] card_image inj_on_inv_into inv_into_into) ultimately show ?thesis by blast next case 1 have gH: "?g ` H ⊆ elts (α*β)" by (metis A_αβ α_sub ‹H ⊆ elts α› image_subsetI inv_into_into subset_eq) have g_less: "?g x < ?g y" if "x < y" "x ∈ elts α" "y ∈ elts α" for x y using Pi_mem [OF g] ord that by (meson A_αβ Ord_in_Ord Ord_not_le ‹small A› dual_order.trans elts_subset_ON inv_ordermap_VWF_mono_le ot vsubsetD) have [simp]: "tp (?g ` H) = tp H" by (meson ‹H ⊆ elts α› ord down dual_order.trans elts_subset_ON gH g_less ordertype_VWF_inc_eq subsetD) show ?thesis using ii [of "?g ` H"] subset_inj_on [OF inj_g ‹H ⊆ elts α›] ot_eq 1 by (auto simp: gH elim!: nset_image_obtains) qed qed define K where "K ≡ λi x. {y ∈ elts (α*β). x ≠ y ∧ f{x,y} = i}" have small_K: "small (K i x)" for i x by (simp add: K_def) define KI where "KI ≡ λi X. (⋂x∈X. K i x)" have KI_disj_self: "X ∩ KI i X = {}" for i X by (auto simp: KI_def K_def) define M where "M ≡ λD 𝔄 x. {ν::V. ν ∈ D ∧ tp (K 1 x ∩ 𝔄 ν) ≥ α}" have M_sub_D: "M D 𝔄 x ⊆ D" for D 𝔄 x by (auto simp: M_def) have small_M [simp]: "small (M D 𝔄 x)" if "small D" for D 𝔄 x by (simp add: M_def that) have 9: "tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D} ≥ α" (is "ordertype ?AD _ ≥ α") if inD: "indecomposable (tp D)" and D: "D ⊆ elts β" and A: "A ⊆ elts (α*β)" and tpA: "tp A = α" and 𝔄: "𝔄 ∈ D → {X. X ⊆ elts (α*β) ∧ tp X = α}" for D A 𝔄 ―‹remark (9), assuming an indecomposable order type› proof (rule ccontr) define A' where "A' ≡ {x ∈ A. ¬ tp (M D 𝔄 x) ≥ tp D}" have small [iff]: "small A" "small D" using A D down by (auto simp: M_def) have small_𝔄: "small (𝔄 δ)" if "δ ∈ D" for δ using that 𝔄 by (auto simp: Pi_iff subset_iff_less_eq_V) assume not_α_le: "¬ α ≤ tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D}" moreover obtain "small A" "small A'" "A' ⊆ A" and A'_sub: "A' ⊆ elts (α*β)" using A'_def A down by auto moreover have "A' = A - ?AD" by (force simp: A'_def) ultimately have A'_ge: "tp A' ≥ α" by (metis (no_types, lifting) dual_order.refl indec indecomposable_ordertype_eq mem_Collect_eq subsetI tpA) obtain X where "X ⊆ A'" "finite X" "card X = k" and fX0: "f ` [X]⇗2⇖ ⊆ {0}" using Ak0 [OF A'_sub A'_ge] by (auto simp: nsets_def [of _ k]) then have ‡: "¬ tp (M D 𝔄 x) ≥ tp D" if "x ∈ X" for x using that by (auto simp: A'_def) obtain x where "x ∈ X" using ‹card X = k› ‹k>1› by fastforce have "¬ D ⊆ (⋃ x∈X. M D 𝔄 x)" proof assume not: "D ⊆ (⋃x∈X. M D 𝔄 x)" have "∃X∈M D 𝔄 ` X. tp D ≤ tp X" proof (rule indecomposable_ordertype_finite_ge [OF inD]) show "M D 𝔄 ` X ≠ {}" using A'_def A'_ge not not_α_le by auto show "small (⋃ (M D 𝔄 ` X))" using ‹finite X› by (simp add: finite_imp_small) qed (use ‹finite X› not in auto) then show False by (simp add: ‡) qed then obtain ν where "ν ∈ D" and ν: "ν ∉ (⋃ x∈X. M D 𝔄 x)" by blast define 𝒜 where "𝒜 ≡ {KI 0 X ∩ 𝔄 ν, ⋃x∈X. K 1 x ∩ 𝔄 ν, X ∩ 𝔄 ν}" have αβ: "X ⊆ elts (α*β)" "𝔄 ν ⊆ elts (α*β)" using A'_sub ‹X ⊆ A'› 𝔄 ‹ν ∈ D› by auto then have "KI 0 X ∪ (⋃x∈X. K 1 x) ∪ X = elts (α*β)" using ‹x ∈ X› f by (force simp: K_def KI_def Pi_iff less_2_cases_iff) with αβ have 𝔄ν_𝒜: "finite 𝒜" "𝔄 ν ⊆ ⋃𝒜" by (auto simp: 𝒜_def) then have "¬ tp (K 1 x ∩ 𝔄 ν) ≥ α" if "x ∈ X" for x using that ‹ν ∈ D› ν ‹k > 1› ‹card X = k› by (fastforce simp: M_def) moreover have sm_K1: "small (⋃x∈X. K 1 x ∩ 𝔄 ν)" by (meson Finite_V Int_lower2 ‹ν ∈ D› ‹finite X› small_𝔄 small_UN smaller_than_small) ultimately have not1: "¬ tp (⋃x∈X. K 1 x ∩ 𝔄 ν) ≥ α" using ‹finite X› ‹x ∈ X› indecomposable_ordertype_finite_ge [OF indec, of "(λx. K 1 x ∩ 𝔄 ν) ` X"] by blast moreover have "¬ tp (X ∩ 𝔄 ν) ≥ α" using ‹finite X› ‹α ≥ ω› by (meson finite_Int mem_not_refl ordertype_VWF_ω vsubsetD) moreover have "α ≤ tp (𝔄 ν)" using 𝔄 ‹ν ∈ D› small_𝔄 by fastforce+ moreover have "small (⋃ 𝒜)" using ‹ν ∈ D› small_𝔄 by (fastforce simp: 𝒜_def intro: smaller_than_small sm_K1) ultimately have K0𝔄_ge: "tp (KI 0 X ∩ 𝔄 ν) ≥ α" using indecomposable_ordertype_finite_ge [OF indec 𝔄ν_𝒜] by (auto simp: 𝒜_def) have 𝔄ν: "𝔄 ν ⊆ elts (α*β)" "tp (𝔄 ν) = α" using ‹ν ∈ D› 𝔄 by blast+ then obtain Y where Ysub: "Y ⊆ KI 0 X ∩ 𝔄 ν" and "finite Y" "card Y = k" and fY0: "f ` [Y]⇗2⇖ ⊆ {0}" using Ak0 [OF _ K0𝔄_ge] by (auto simp: nsets_def [of _ k]) have †: "X ∩ Y = {}" using Ysub KI_disj_self by blast then have "card (X ∪ Y) = 2*k" by (simp add: ‹card X = k› ‹card Y = k› ‹finite X› ‹finite Y› card_Un_disjoint) moreover have "X ∪ Y ⊆ elts (α*β)" using A'_sub ‹X ⊆ A'› 𝔄ν(1) ‹Y ⊆ KI 0 X ∩ 𝔄 ν› by auto moreover have "f ` [X ∪ Y]⇗2⇖ ⊆ {0}" using fX0 fY0 Ysub by (auto simp: † nsets_disjoint_2 image_Un image_UN KI_def K_def) ultimately show False using i ‹finite X› ‹finite Y› ordertype_VWF_finite_nat by auto qed have IX: "tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D} ≥ α" if D: "D ⊆ elts β" and A: "A ⊆ elts (α*β)" and tpA: "tp A = α" and 𝔄: "𝔄 ∈ D → {X. X ⊆ elts (α*β) ∧ tp X = α}" for D A 𝔄 ―‹remark (9) for any order type› proof - obtain L where UL: "⋃(List.set L) ⊆ D" and indL: "⋀X. X ∈ List.set L ⟹ indecomposable (tp X)" and eqL: "⋀M. ⟦M ⊆ D; ⋀X. X ∈ List.set L ⟹ tp (M ∩ X) ≥ tp X⟧ ⟹ tp M = tp D" using ord by (metis strong_ordertype_eq D order_refl) obtain A'' where A'': "A'' ⊆ A" "tp A'' ≥ α" and "⋀x X. ⟦x ∈ A''; X ∈ List.set L⟧ ⟹ tp (M D 𝔄 x ∩ X) ≥ tp X" using UL indL proof (induction L arbitrary: thesis) case (Cons X L) then obtain A'' where A'': "A'' ⊆ A" "tp A'' ≥ α" and "X ⊆ D" and ge_X: "⋀x X. ⟦x ∈ A''; X ∈ List.set L⟧ ⟹ tp (M D 𝔄 x ∩ X) ≥ tp X" by auto then have tp_A'': "tp A'' = α" by (metis A antisym down ordertype_VWF_mono tpA) have ge_α: "tp {x ∈ A''. tp (M X 𝔄 x) ≥ tp X} ≥ α" by (rule 9) (use A A'' tp_A'' Cons.prems ‹D ⊆ elts β› ‹X ⊆ D› 𝔄 in auto) let ?A = "{x ∈ A''. tp (M D 𝔄 x ∩ X) ≥ tp X}" have M_eq: "M D 𝔄 x ∩ X = M X 𝔄 x" if "x ∈ A''" for x using that ‹X ⊆ D› by (auto simp: M_def) show thesis proof (rule Cons.prems) show "α ≤ tp ?A" using ge_α by (simp add: M_eq cong: conj_cong) show "tp Y ≤ tp (M D 𝔄 x ∩ Y)" if "x ∈ ?A" "Y ∈ list.set (X # L)" for x Y using that ge_X by force qed (use A'' in auto) qed (use tpA in auto) then have tp_M_ge: "tp (M D 𝔄 x) ≥ tp D" if "x ∈ A''" for x using eqL that by (auto simp: M_def) have "α ≤ tp A''" by (simp add: A'') also have "… ≤ tp {x ∈ A''. tp (M D 𝔄 x) ≥ tp D}" by (metis (mono_tags, lifting) tp_M_ge eq_iff mem_Collect_eq subsetI) also have "… ≤ tp {x ∈ A. tp D ≤ tp (M D 𝔄 x)}" by (rule ordertype_mono) (use A'' A down in auto) finally show ?thesis . qed have IX': "tp {x ∈ A'. tp (K 1 x ∩ A) ≥ α} ≥ α" if A: "A ⊆ elts (α*β)" "tp A = α" and A': "A' ⊆ elts (α*β)" "tp A' = α" for A A' proof - have ‡: "α ≤ tp (K 1 t ∩ A)" if "1 ≤ tp {ν. ν = 0 ∧ α ≤ tp (K 1 t ∩ A)}" for t using that by (metis Collect_empty_eq less_eq_V_0_iff ordertype_empty zero_neq_one) have "tp {x ∈ A'. 1 ≤ tp {ν. ν = 0 ∧ α ≤ tp (K 1 x ∩ A)}} ≤ tp {x ∈ A'. α ≤ tp (K 1 x ∩ A)}" by (rule ordertype_mono) (use "‡" A' in ‹auto simp: down›) then show ?thesis using IX [of "{0}" A' "λx. A"] that ‹0 ∈ elts β› by (force simp: M_def) qed have 10: "∃x0 ∈ A. ∃g ∈ elts β → elts β. strict_mono_on (elts β) g ∧ (∀ν ∈ F. g ν = ν) ∧ (∀ν ∈ elts β. tp (K 1 x0 ∩ 𝔄 (g ν)) ≥ α)" if F: "finite F" "F ⊆ elts β" and A: "A ⊆ elts (α*β)" "tp A = α" and 𝔄: "𝔄 ∈ elts β → {X. X ⊆ elts (α*β) ∧ tp X = α}" for F A 𝔄 proof - define p where "p ≡ card F" have "β ∉ F" using that by auto then obtain ι :: "nat ⇒ V" where bijι: "bij_betw ι {..p} (insert β F)" and monι: "strict_mono_on {..p} ι" using ZFC_Cardinals.ex_bij_betw_strict_mono_card [of "insert β F"] elts_subset_ON ‹Ord β› F by (simp add: p_def lessThan_Suc_atMost) blast have less_ι_I: "ι k < ι l" if "k < l" "l ≤ p" for k l using monι that by (auto simp: strict_mono_on_def) then have less_ι_D: "k < l" if "ι k < ι l" "k ≤ p" for k l by (metis less_asym linorder_neqE_nat that) have Ord_ι: "Ord (ι k)" if "k ≤ p" for k by (metis (no_types, lifting) ON_imp_Ord atMost_iff insert_subset mem_Collect_eq order_trans ‹F ⊆ elts β› bijι bij_betwE elts_subset_ON ‹Ord β› that) have le_ι0 [simp]: "⋀j. j ≤ p ⟹ ι 0 ≤ ι j" by (metis eq_refl leI le_0_eq less_ι_I less_imp_le) have le_ι: "ι i ≤ ι (j - Suc 0)" if "i < j" "j ≤ p" for i j proof (cases i) case 0 then show ?thesis using le_ι0 that by auto next case (Suc i') then show ?thesis by (metis (no_types, opaque_lifting) Suc_pred le_less less_Suc_eq less_Suc_eq_0_disj less_ι_I not_less_eq that) qed have [simp]: "ι p = β" proof - obtain k where k: "ι k = β" "k ≤ p" by (meson atMost_iff bijι bij_betw_iff_bijections insertI1) then have "k = p ∨ k < p" by linarith then show ?thesis using bijι ord k that(2) by (metis OrdmemD atMost_iff bij_betw_iff_bijections insert_iff leD less_ι_D order_refl subsetD) qed have F_imp_Ex: "∃k < p. ξ = ι k" if "ξ ∈ F" for ξ proof - obtain k where k: "k ≤ p" "ξ = ι k" by (metis ‹ξ ∈ F› atMost_iff bijι bij_betw_def imageE insert_iff) then show ?thesis using ‹β ∉ F› ‹ι p = β› le_imp_less_or_eq that by blast qed have F_imp_ge: "ξ ≥ ι 0" if "ξ ∈ F" for ξ using F_imp_Ex [OF that] by (metis dual_order.order_iff_strict le0 less_ι_I) define D where "D ≡ λk. (if k=0 then {..<ι 0} else {ι (k-1)<..<ι k}) ∩ elts β" have Dβ: "D k ⊆ elts β" for k by (auto simp: D_def) then have small_D [simp]: "small (D k)" for k by (meson down) have M_Int_D: "M (elts β) 𝔄 x ∩ D k = M (D k) 𝔄 x" if "k ≤ p" for x k using Dβ by (auto simp: M_def) have ι_le_if_D: "ι k ≤ μ" if "μ ∈ D (Suc k)" for μ k using that by (simp add: D_def order.order_iff_strict) have mono_D: "D i ≪ D j" if "i < j" "j ≤ p" for i j proof (cases j) case (Suc j') with that show ?thesis apply (simp add: less_sets_def D_def Ball_def) by (metis One_nat_def diff_Suc_1 le_ι less_le_trans less_trans) qed (use that in auto) then have disjnt_DD: "disjnt (D i) (D j)" if "i ≠ j" "i ≤ p" "j ≤ p" for i j by (meson disjnt_sym less_linear less_sets_imp_disjnt that) have UN_D_eq: "(⋃l ≤ k. D l) = {..<ι k} ∩ (elts β - F)" if "k ≤ p" for k using that proof (induction k) case 0 then show ?case by (auto simp: D_def F_imp_ge leD) next case (Suc k) have "D (Suc k) ∪ {..<ι k} ∩ (elts β - F) = {..<ι (Suc k)} ∩ (elts β - F)" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" using Suc.prems by (auto simp: D_def if_split_mem2 intro: less_ι_I less_trans dest!: less_ι_D F_imp_Ex) have "⋀x. ⟦x < ι (Suc k); x ∈ elts β; x ∉ F; ι k ≤ x⟧ ⟹ ι k < x" using Suc.prems ‹F ⊆ elts β› bijι le_imp_less_or_eq by (fastforce simp: bij_betw_iff_bijections) then show "?rhs ⊆ ?lhs" using Suc.prems by (auto simp: D_def Ord_not_less Ord_in_Ord [OF ‹Ord β›] Ord_ι if_split_mem2) qed then show ?case using Suc by (simp add: atMost_Suc) qed have β_decomp: "elts β = F ∪ (⋃k ≤ p. D k)" using ‹F ⊆ elts β› OrdmemD [OF ‹Ord β›] by (auto simp: UN_D_eq) define βidx where "βidx ≡ λν. @k. ν ∈ D k ∧ k ≤ p" have βidx: "ν ∈ D (βidx ν) ∧ βidx ν ≤ p" if "ν ∈ elts β - F" for ν using that by (force simp: βidx_def β_decomp intro: someI_ex del: conjI) have any_imp_βidx: "k = βidx ν" if "ν ∈ D k" "k ≤ p" for k ν proof (rule ccontr) assume non: "k ≠ βidx ν" have "ν ∉ F" using that UN_D_eq by auto then show False using disjnt_DD [OF non] by (metis Dβ Diff_iff βidx disjnt_iff subsetD that) qed have "∃A'. A' ⊆ A ∧ tp A' = α ∧ (∀x ∈ A'. F ⊆ M (elts β) 𝔄 x)" using F proof induction case (insert ν F) then obtain A' where "A' ⊆ A" and A': "A' ⊆ elts (α*β)" "tp A' = α" and FN: "⋀x. x ∈ A' ⟹ F ⊆ M (elts β) 𝔄 x" using A(1) by auto define A'' where "A'' ≡ {x ∈ A'. α ≤ tp (K 1 x ∩ 𝔄 ν)}" have "ν ∈ elts β" "F ⊆ elts β" using insert by auto note ordertype_eq_Ord [OF ‹Ord β›, simp] show ?case proof (intro exI conjI) show "A'' ⊆ A" using ‹A' ⊆ A› by (auto simp: A''_def) show "tp A'' = α" proof (rule antisym) show "tp A'' ≤ α" using ‹A'' ⊆ A› down ordertype_VWF_mono A by blast have "𝔄 ν ⊆ elts (α*β)" "tp (𝔄 ν) = α" using 𝔄 ‹ν ∈ elts β› by auto then show "α ≤ tp A''" using IX' [OF _ _ A'] by (simp add: A''_def) qed show "∀x∈A''. insert ν F ⊆ M (elts β) 𝔄 x" using A''_def FN M_def ‹ν ∈ elts β› by blast qed qed (use A in auto) then obtain A' where A': "A' ⊆ A" "tp A' = α" and FN: "⋀x. x ∈ A' ⟹ F ⊆ M (elts β) 𝔄 x" by metis have False if *: "⋀x0 g. ⟦x0 ∈ A; g ∈ elts β → elts β; strict_mono_on (elts β) g⟧ ⟹ (∃ν∈F. g ν ≠ ν) ∨ (∃ν∈elts β. tp (K 1 x0 ∩ 𝔄 (g ν)) < α)" proof - { fix x ― ‹construction of the monotone map @{term g} mentioned above› assume "x ∈ A'" with A' have "x ∈ A" by blast have "∃k. k ≤ p ∧ tp (M (D k) 𝔄 x) < tp (D k)" (is "?P") proof (rule ccontr) assume "¬ ?P" then have le: "tp (D k) ≤ tp (M (D k) 𝔄 x)" if "k ≤ p" for k by (meson Ord_linear2 Ord_ordertype that) have "∃f∈D k → M (D k) 𝔄 x. inj_on f (D k) ∧ (strict_mono_on (D k) f)" if "k ≤ p" for k using le [OF that] that VWF_iff_Ord_less apply (clarsimp simp: ordertype_le_ordertype strict_mono_on_def) by (metis (full_types) Dβ M_sub_D Ord_in_Ord PiE VWF_iff_Ord_less ord(2) subsetD) then obtain h where fun_h: "⋀k. k ≤ p ⟹ h k ∈ D k → M (D k) 𝔄 x" and inj_h: "⋀k. k ≤ p ⟹ inj_on (h k) (D k)" and mono_h: "⋀k x y. k ≤ p ⟹ strict_mono_on (D k) (h k)" by metis then have fun_hD: "⋀k. k ≤ p ⟹ h k ∈ D k → D k" by (auto simp: M_def) have h_increasing: "ν ≤ h k ν" if "k ≤ p" "ν ∈ D k" for k ν by (meson Dβ Ord_mono_imp_increasing ord dual_order.trans elts_subset_ON fun_hD mono_h that) define g where "g ≡ λν. if ν ∈ F then ν else h (βidx ν) ν" have [simp]: "g ν = ν" if "ν ∈ F" for ν using that by (auto simp: g_def) have fun_g: "g ∈ elts β → elts β" proof (rule Pi_I) fix x assume "x ∈ elts β" then have "x ∈ D (βidx x)" "βidx x ≤ p" if "x ∉ F" using that by (auto simp: βidx) then show "g x ∈ elts β" by (metis fun_h Dβ M_sub_D ‹x ∈ elts β› PiE g_def subsetD) qed have h_in_D: "h (βidx ν) ν ∈ D (βidx ν)" if "ν ∉ F" "ν ∈ elts β" for ν using βidx fun_hD that by fastforce have 1: "ι k < h (βidx ν) ν" if "k < p" and ν: "ν ∉ F" "ν ∈ elts β" and "ι k < ν" for k ν by (meson that h_in_D [OF ν] βidx DiffI h_increasing order_less_le_trans) moreover have 2: "h (βidx μ) μ < ι k" if μ: "μ ∉ F" "μ ∈ elts β" and "k < p" "μ < ι k" for μ k proof - have "βidx μ ≤ k" proof (rule ccontr) assume "¬ βidx μ ≤ k" then have "k < βidx μ" by linarith then show False using ι_le_if_D βidx that by (metis Diff_iff Suc_pred le0 leD le_ι le_less_trans) qed then show ?thesis using that h_in_D [OF μ] by (smt (verit, best) Int_lower1 UN_D_eq UN_I atMost_iff lessThan_iff less_imp_le subset_eq) qed moreover have "h (βidx μ) μ < h (βidx ν) ν" if μ: "μ ∉ F" "μ ∈ elts β" and ν: "ν ∉ F" "ν ∈ elts β" and "μ < ν" for μ ν proof - have le: "βidx μ ≤ βidx ν" if "ι (βidx μ - Suc 0) < h (βidx μ) μ" "h (βidx ν) ν < ι (βidx ν)" by (metis 2 DiffI βidx μ ν ‹μ < ν› order.strict_trans h_increasing leI le_ι order_less_asym order_less_le_trans that) have "h 0 μ < h 0 ν" if "βidx μ = 0" "βidx ν = 0" using that mono_h unfolding strict_mono_on_def by (metis Diff_iff βidx μ ν ‹μ < ν›) moreover have "h 0 μ < h (βidx ν) ν" if "0 < βidx ν" "h 0 μ < ι 0" and "ι (βidx ν - Suc 0) < h (βidx ν) ν" by (meson DiffI βidx ν le_ι le_less_trans less_le_not_le that) moreover have "βidx ν ≠ 0" if "0 < βidx μ" "h 0 ν < ι 0" "ι (βidx μ - Suc 0) < h (βidx μ) μ" using le le_0_eq that by fastforce moreover have "h (βidx μ) μ < h (βidx ν) ν" if "ι (βidx μ - Suc 0) < h (βidx μ) μ" "h (βidx ν) ν < ι (βidx ν)" "h (βidx μ) μ < ι (βidx μ)" "ι (βidx ν - Suc 0) < h (βidx ν) ν" using mono_h unfolding strict_mono_on_def by (metis le Diff_iff βidx μ ν ‹μ < ν› le_ι le_less le_less_trans that) ultimately show ?thesis using h_in_D [OF μ] h_in_D [OF ν] by (simp add: D_def split: if_split_asm) qed ultimately have sm_g: "strict_mono_on (elts β) g" by (auto simp: g_def strict_mono_on_def dest!: F_imp_Ex) have False if "ν ∈ elts β" and ν: "tp (K 1 x ∩ 𝔄 (g ν)) < α" for ν proof - have "F ⊆ M (elts β) 𝔄 x" by (meson FN ‹x ∈ A'›) then have False if "tp (K (Suc 0) x ∩ 𝔄 ν) < α" "ν ∈ F" using that by (auto simp: M_def) moreover have False if "tp (K (Suc 0) x ∩ 𝔄 (g ν)) < α" "ν ∈ D k" "k ≤ p" "ν ∉ F" for k proof - have "h (βidx ν) ν ∈ M (D (βidx ν)) 𝔄 x" using fun_h βidx ‹ν ∈ elts β› ‹ν ∉ F› by auto then show False using that by (simp add: M_def g_def leD) qed ultimately show False using ‹ν ∈ elts β› ν by (force simp: β_decomp) qed then show False using * [OF ‹x ∈ A› fun_g sm_g] by auto qed then have "∃l. l ≤ p ∧ tp (M (elts β) 𝔄 x ∩ D l) < tp (D l)" using M_Int_D by auto } then obtain l where lp: "⋀x. x ∈ A'⟹ l x ≤ p" and lless: "⋀x. x ∈ A'⟹ tp (M (elts β) 𝔄 x ∩ D (l x)) < tp (D (l x))" by metis obtain A'' L where "A'' ⊆ A'" and A'': "A'' ⊆ elts (α*β)" "tp A'' = α" and lL: "⋀x. x ∈ A'' ⟹ l x = L" proof - have eq: "A' = (⋃i≤p. {x ∈ A'. l x = i})" using lp by auto have "∃X∈(λi. {x ∈ A'. l x = i}) ` {..p}. α ≤ tp X" proof (rule indecomposable_ordertype_finite_ge [OF indec]) show "small (⋃i≤p. {x ∈ A'. l x = i})" by (metis A'(1) A(1) eq down smaller_than_small) qed (use A' eq in auto) then show thesis proof fix A'' assume A'': "A'' ∈ (λi. {x ∈ A'. l x = i}) ` {..p}" and "α ≤ tp A''" then obtain L where L: "⋀x. x ∈ A'' ⟹ l x = L" by auto have "A'' ⊆ A'" using A'' by force then have "tp A'' ≤ tp A'" by (meson A' A down order_trans ordertype_VWF_mono) with ‹α ≤ tp A''› have "tp A'' = α" using A'(2) by auto moreover have "A'' ⊆ elts (α*β)" using A' A ‹A'' ⊆ A'› by auto ultimately show thesis using L that [OF ‹A'' ⊆ A'›] by blast qed qed have 𝔄D: "𝔄 ∈ D L → {X. X ⊆ elts (α*β) ∧ tp X = α}" using 𝔄 Dβ by blast have α: "α ≤ tp {x ∈ A''. tp (D L) ≤ tp (M (D L) 𝔄 x)}" using IX [OF Dβ A'' 𝔄D] by simp have "M (elts β) 𝔄 x ∩ D L = M (D L) 𝔄 x" for x using Dβ by (auto simp: M_def) then have "tp (M (D L) 𝔄 x) < tp (D L)" if "x ∈ A''" for x using lless that ‹A'' ⊆ A'› lL by force then have [simp]: "{x ∈ A''. tp (D L) ≤ tp (M (D L) 𝔄 x)} = {}" using leD by blast show False using α ‹α ≥ ω› by simp qed then show ?thesis by (meson Ord_linear2 Ord_ordertype ‹Ord α›) qed let ?U = "UNIV :: nat set" define μ where "μ ≡ fst ∘ from_nat_into (elts β × ?U)" define q where "q ≡ to_nat_on (elts β × ?U)" have co_βU: "countable (elts β × ?U)" by (simp add: β less_ω1_imp_countable) moreover have "elts β × ?U ≠ {}" using ‹0 ∈ elts β› by blast ultimately have "range (from_nat_into (elts β × ?U)) = (elts β × ?U)" by (metis range_from_nat_into) then have μ_in_β [simp]: "μ i ∈ elts β" for i by (metis SigmaE μ_def comp_apply fst_conv range_eqI) then have Ord_μ [simp]: "Ord (μ i)" for i using Ord_in_Ord by blast have inf_βU: "infinite (elts β × ?U)" using ‹0 ∈ elts β› finite_cartesian_productD2 by auto have 11 [simp]: "μ (q (ν,n)) = ν" if "ν ∈ elts β" for ν n by (simp add: μ_def q_def that co_βU) have range_μ [simp]: "range μ = elts β" by (auto simp: image_iff) (metis 11) have [simp]: "KI i {} = UNIV" "KI i (insert a X) = K i a ∩ KI i X" for i a X by (auto simp: KI_def) define Φ where "Φ ≡ λn::nat. λ𝔄 x. (∀ν ∈ elts β. 𝔄 ν ⊆ elts (α*β) ∧ tp (𝔄 ν) = α) ∧ x ` {..<n} ⊆ elts (α*β) ∧ (⋃ν ∈ elts β. 𝔄 ν) ⊆ KI 1 (x ` {..<n}) ∧ strict_mono_sets (elts β) 𝔄" define Ψ where "Ψ ≡ λn::nat. λg 𝔄 𝔄' xn. g ∈ elts β → elts β ∧ strict_mono_on (elts β) g ∧ (∀i≤n. g (μ i) = μ i) ∧ (∀ν ∈ elts β. 𝔄' ν ⊆ K 1 xn ∩ 𝔄 (g ν)) ∧ {xn} ≪ (𝔄' (μ n)) ∧ xn ∈ 𝔄 (μ n)" let ?𝔄0 = "λν. plus (α * ν) ` elts α" have base: "Φ 0 ?𝔄0 x" for x by (auto simp: Φ_def add_mult_less add_mult_less_add_mult ordertype_image_plus strict_mono_sets_def less_sets_def) have step: "Ex (λ(g,𝔄',xn). Ψ n g 𝔄 𝔄' xn ∧ Φ (Suc n) 𝔄' (x(n:=xn)))" if "Φ n 𝔄 x" for n 𝔄 x proof - have 𝔄: "⋀ν. ν ∈ elts β ⟹ 𝔄 ν ⊆ elts (α*β) ∧ tp (𝔄 ν) = α" and x: "x ` {..<n} ⊆ elts (α*β)" and sub: "⋃ (𝔄 ` elts β) ⊆ KI (Suc 0) (x ` {..<n})" and sm: "strict_mono_sets (elts β) 𝔄" and μβ: "μ ` {..n} ⊆ elts β" and 𝔄sub: "𝔄 (μ n) ⊆ elts (α*β)" and 𝔄fun: "𝔄 ∈ elts β → {X. X ⊆ elts (α*β) ∧ tp X = α}" using that by (auto simp: Φ_def) then obtain xn g where xn: "xn ∈ 𝔄 (μ n)" and g: "g ∈ elts β → elts β" and sm_g: "strict_mono_on (elts β) g" and g_μ: "∀ν ∈ μ`{..n}. g ν = ν" and g_α: "∀ν ∈ elts β. α ≤ tp (K 1 xn ∩ 𝔄 (g ν))" using 10 [OF _ μβ 𝔄sub _ 𝔄fun] by (auto simp: 𝔄) have tp1: "tp (K 1 xn ∩ 𝔄 (g ν)) = α" if "ν ∈ elts β" for ν by (metis antisym Int_lower2 PiE 𝔄 down g g_α ordertype_VWF_mono that) have tp2: "tp (𝔄 (μ n)) = α" by (auto simp: 𝔄) obtain "small (𝔄 (μ n))" "𝔄 (μ n) ⊆ ON" by (meson 𝔄sub ord down elts_subset_ON subset_trans) then obtain A2 where A2: "tp A2 = α" "A2 ⊆ K 1 xn ∩ 𝔄 (μ n)" "{xn} ≪ A2" using indecomposable_imp_Ex_less_sets [OF indec ‹α ≥ ω› tp2] by (metis μ_in_β atMost_iff image_eqI inf_le2 le_refl xn tp1 g_μ) then have A2_sub: "A2 ⊆ 𝔄 (μ n)" by simp let ?𝔄 = "λν. if ν = μ n then A2 else K 1 xn ∩ 𝔄 (g ν)" have [simp]: "({..<Suc n} ∩ {x. x ≠ n}) = ({..<n})" by auto have "K (Suc 0) xn ∩ (⋃x∈elts β ∩ {ν. ν ≠ μ n}. 𝔄 (g x)) ⊆ KI (Suc 0) (x ` {..<n})" using sub g by (auto simp: KI_def) moreover have "A2 ⊆ KI (Suc 0) (x ` {..<n})" "A2 ⊆ elts (α*β)" "xn ∈ elts (α*β)" using 𝔄sub sub A2 xn by fastforce+ moreover have "strict_mono_sets (elts β) ?𝔄" using sm sm_g g g_μ A2_sub unfolding strict_mono_sets_def strict_mono_on_def less_sets_def Pi_iff subset_iff Ball_def Bex_def image_iff by (simp (no_asm_use) add: if_split_mem2) (smt order_refl) ultimately have "Φ (Suc n) ?𝔄 (x(n := xn))" using tp1 x A2 by (auto simp: Φ_def K_def) with A2 show ?thesis by (rule_tac x="(g,?𝔄,xn)" in exI) (simp add: Ψ_def g sm_g g_μ xn) qed define G where "G ≡ λn 𝔄 x. @(g,𝔄',x'). ∃xn. Ψ n g 𝔄 𝔄' xn ∧ x' = (x(n:=xn)) ∧ Φ (Suc n) 𝔄' x'" have GΦ: "(λ(g,𝔄',x'). Φ (Suc n) 𝔄' x') (G n 𝔄 x)" and GΨ: "(λ(g,𝔄',x'). Ψ n g 𝔄 𝔄' (x' n)) (G n 𝔄 x)" if "Φ n 𝔄 x" for n 𝔄 x using step [OF that] by (force simp: G_def dest: some_eq_imp)+ define H where "H ≡ rec_nat (id,?𝔄0,undefined) (λn (g0,𝔄,x0). G n 𝔄 x0)" have "(λ(g,𝔄,x). Φ n 𝔄 x) (H n)" for n unfolding H_def by (induction n) (use GΦ base in fastforce)+ then have H_imp_Φ: "Φ n 𝔄 x" if "H n = (g,𝔄,x)" for g 𝔄 x n by (metis case_prodD that) then have H_imp_Ψ: "(λ(g,𝔄',x'). let (g0,𝔄,x) = H n in Ψ n g 𝔄 𝔄' (x' n)) (H (Suc n))" for n using GΨ by (fastforce simp: H_def split: prod.split) define g where "g ≡ λn. (λ(g,𝔄,x). g) (H (Suc n))" have g: "g n ∈ elts β → elts β" and sm_g: "strict_mono_on (elts β) (g n)" and 13: "⋀i. i≤n ⟹ g n (μ i) = μ i" for n using H_imp_Ψ [of n] by (auto simp: g_def Ψ_def) define 𝔄 where "𝔄 ≡ λn. (λ(g,𝔄,x). 𝔄) (H n)" define x where "x ≡ λn. (λ(g,𝔄,x). x n) (H (Suc n))" have 14: "𝔄 (Suc n) ν ⊆ K 1 (x n) ∩ 𝔄 n (g n ν)" if "ν ∈ elts β" for ν n using H_imp_Ψ [of n] that by (force simp: Ψ_def 𝔄_def x_def g_def) then have x14: "𝔄 (Suc n) ν ⊆ 𝔄 n (g n ν)" if "ν ∈ elts β" for ν n using that by blast have 15: "x n ∈ 𝔄 n (μ n)" and 16: "{x n} ≪ (𝔄 (Suc n) (μ n))" for n using H_imp_Ψ [of n] by (force simp: Ψ_def 𝔄_def x_def)+ have 𝔄_αβ: "𝔄 n ν ⊆ elts (α*β)" if "ν ∈ elts β" for ν n using H_imp_Φ [of n] that by (auto simp: Φ_def 𝔄_def split: prod.split) have 12: "strict_mono_sets (elts β) (𝔄 n)" for n using H_imp_Φ [of n] that by (auto simp: Φ_def 𝔄_def split: prod.split) let ?Z = "range x" have S_dec: "⋃ (𝔄 (m+k) ` elts β) ⊆ ⋃ (𝔄 m ` elts β)" for k m by (induction k) (use 14 g in ‹fastforce+›) have "x n ∈ K 1 (x m)" if "m<n" for m n proof - have "x n ∈ (⋃ν ∈ elts β. 𝔄 n ν)" by (meson "15" UN_I μ_in_β) also have "… ⊆ (⋃ν ∈ elts β. 𝔄 (Suc m) ν)" using S_dec [of "Suc m"] less_iff_Suc_add that by auto also have "… ⊆ K 1 (x m)" using 14 by auto finally show ?thesis . qed then have "f{x m, x n} = 1" if "m<n" for m n using that by (auto simp: K_def) then have Z_K1: "f ` [?Z]⇗2⇖ ⊆ {1}" by (clarsimp simp: nsets_2_eq) (metis insert_commute less_linear) moreover have Z_sub: "?Z ⊆ elts (α*β)" using "15" 𝔄_αβ μ_in_β by blast moreover have "tp ?Z ≥ ω * β" proof - define 𝔤 where "𝔤 ≡ λi j x. wfrec (measure (λk. j-k)) (λ𝔤 k. if k<j then g k (𝔤 (Suc k)) else x) i" have 𝔤: "𝔤 i j x = (if i<j then g i (𝔤 (Suc i) j x) else x)" for i j x by (simp add: 𝔤_def wfrec cut_apply) have 17: "𝔤 k j (μ i) = μ i" if "i ≤ k" for i j k using wf_measure [of "λk. j-k"] that by (induction k rule: wf_induct_rule) (simp add: "13" 𝔤 le_imp_less_Suc) have 𝔤_in_β: "𝔤 i j ν ∈ elts β" if "ν ∈ elts β" for i j ν using wf_measure [of "λk. j-k"] that proof (induction i rule: wf_induct_rule) case (less i) with g show ?case by (force simp: 𝔤 [of i]) qed then have 𝔤_fun: "𝔤 i j ∈ elts β → elts β" for i j by simp have sm_𝔤: "strict_mono_on (elts β) (𝔤 i j)" for i j using wf_measure [of "λk. j-k"] proof (induction i rule: wf_induct_rule) case (less i) with sm_g show ?case by (auto simp: 𝔤 [of i] strict_mono_on_def 𝔤_in_β) qed have *: "𝔄 j (μ j) ⊆ 𝔄 i (𝔤 i j (μ j))" if "i < j" for i j using wf_measure [of "λk. j-k"] that proof (induction i rule: wf_induct_rule) case (less i) then have "j - Suc i < j - i" by (metis (no_types) Suc_diff_Suc lessI) with less 𝔤_in_β show ?case by (simp add: 𝔤 [of i]) (metis 17 Suc_lessI μ_in_β order_refl order_trans x14) qed have le_iff: "𝔤 i j (μ j) ≤ μ i ⟷ μ j ≤ μ i" for i j using sm_𝔤 unfolding strict_mono_on_def by (metis "17" Ord_in_Ord Ord_linear2 μ_in_β leD le_refl less_V_def ‹Ord β›) then have less_iff: "𝔤 i j (μ j) < μ i ⟷ μ j < μ i" for i j by (metis (no_types, lifting) "17" μ_in_β less_V_def order_refl sm_𝔤 strict_mono_on_def) have eq_iff: "𝔤 i j (μ j) = μ i ⟷ μ j = μ i" for i j by (metis eq_refl le_iff less_iff less_le) have μ_if_ne: "μ m < μ n" if mn: "𝔄 m (μ m) ≪ 𝔄 n (μ n)" "m ≠ n" for m n proof - have xmn: "x m < x n" using "15" less_setsD that(1) by blast have Ord𝔤: "Ord (𝔤 n m (μ m))" using Ord_in_Ord 𝔤_in_β μ_in_β ord(2) by presburger have "¬ 𝔄 m (μ m) ≪ 𝔄 n (μ n)" if "μ n = μ m" using "*" "15" eq_iff that unfolding less_sets_def by (metis in_mono less_irrefl not_less_iff_gr_or_eq) moreover have "𝔄 n (μ n) ⊆ 𝔄 m (𝔤 m n (μ n)) ∨ 𝔄 m (μ m) ⊆ 𝔄 n (𝔤 n m (μ m))" using * mn by (meson antisym_conv3) then have False if "μ n < μ m" using strict_mono_setsD [OF 12] 15 xmn 𝔤_in_β μ_in_β that by (smt (verit, best) Ord𝔤 Ord_μ Ord_linear2 leD le_iff less_asym less_iff less_setsD subset_iff) ultimately show "μ m < μ n" by (meson that(1) Ord_μ Ord_linear_lt) qed have 18: "𝔄 m (μ m) ≪ 𝔄 n (μ n) ⟷ μ m < μ n" for m n proof (cases n m rule: linorder_cases) case less show ?thesis proof (intro iffI) assume "μ m < μ n" then have "𝔄 n (𝔤 n m (μ m)) ≪ 𝔄 n (μ n)" by (metis "12" 𝔤_in_β μ_in_β eq_iff le_iff less_V_def strict_mono_sets_def) then show "𝔄 m (μ m) ≪ 𝔄 n (μ n)" by (meson "*" less less_sets_weaken1) qed (use μ_if_ne less in blast) next case equal with 15 show ?thesis by auto next case greater show ?thesis proof (intro iffI) assume "μ m < μ n" then have "𝔄 m (μ m) ≪ (𝔄 m (𝔤 m n (μ n)))" by (meson 12 Ord_in_Ord Ord_linear2 𝔤_in_β μ_in_β le_iff leD ord(2) strict_mono_sets_def) then show "𝔄 m (μ m) ≪ 𝔄 n (μ n)" by (meson "*" greater less_sets_weaken2) qed (use μ_if_ne greater in blast) qed have 𝔄_increasing_μ: "𝔄 n (μ n) ⊆ 𝔄 m (μ m)" if "m ≤ n" "μ m = μ n" for m n by (metis "*" "17" dual_order.order_iff_strict that) moreover have INF: "infinite {n. n ≥ m ∧ μ m = μ n}" for m proof - have "infinite (range (λn. q (μ m, n)))" unfolding q_def using to_nat_on_infinite [OF co_βU inf_βU] finite_image_iff by (simp add: finite_image_iff inj_on_def) moreover have "(range (λn. q (μ m, n))) ⊆ {n. μ m = μ n}" using 11 [of "μ m"] by auto ultimately have "infinite {n. μ m = μ n}" using finite_subset by auto then have "infinite ({n. μ m = μ n} - {..<m})" by simp then show ?thesis by (auto simp: finite_nat_set_iff_bounded Bex_def not_less) qed let ?eqv = "λm. {n. m ≤ n ∧ μ m = μ n}" have sm_x: "strict_mono_on (?eqv m) x" for m proof (clarsimp simp: strict_mono_on_def) fix n p assume "m ≤ n" "μ p = μ n" "μ m = μ n" "n < p" with 16 [of n] show "x n < x p" by (metis "*" "15" "17" Suc_lessI insert_absorb insert_subset le_SucI less_sets_singleton1) qed then have inj_x: "inj_on x (?eqv m)" for m using strict_mono_on_imp_inj_on by blast define ZA where "ZA ≡ λm. ?Z ∩ 𝔄 m (μ m)" have small_ZA [simp]: "small (ZA m)" for m by (metis ZA_def inf_le1 small_image_nat smaller_than_small) have 19: "tp (ZA m) ≥ ω" for m proof - have "x ` {n. m ≤ n ∧ μ m = μ n} ⊆ ZA m" unfolding ZA_def using "15" 𝔄_increasing_μ by blast then have "infinite (ZA m)" using INF [of m] finite_image_iff [OF inj_x] by (meson finite_subset) then show ?thesis by (simp add: ordertype_infinite_ge_ω) qed have "∃f ∈ elts ω → ZA m. strict_mono_on (elts ω) f" for m proof - obtain Z where "Z ⊆ ZA m" "tp Z = ω" by (meson 19 Ord_ω le_ordertype_obtains_subset small_ZA) moreover have "ZA m ⊆ ON" using Ord_in_Ord 𝔄_αβ μ_in_β unfolding ZA_def by blast ultimately show ?thesis by (metis strict_mono_on_ordertype Pi_mono small_ZA smaller_than_small subset_iff) qed then obtain φ where φ: "⋀m. φ m ∈ elts ω → ZA m" and sm_φ: "⋀m. strict_mono_on (elts ω) (φ m)" by metis have "Ex(λ(m,ν). ν ∈ elts β ∧ γ = ω * ν + ord_of_nat m)" if "γ ∈ elts (ω * β)" for γ using that by (auto simp: mult [of ω β] lift_def elts_ω) then obtain split where split: "⋀γ. γ ∈