Theory ZFC_in_HOL.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 "∃X ∈ 𝒜. ordertype X VWF ≥ α"
  using 𝒜
proof (induction arbitrary: A)
  case (insert X 𝒜)
  show ?case
  proof (cases "𝒜 = {}")
    case True
    then have "α ≤ ordertype X VWF"
      using insert.prems
      by (simp add: order.trans ordertype_VWF_mono)
    then show ?thesis
      using insert.prems by blast
  next
    case False
    show ?thesis
    proof (cases "∃X ∈ 𝒜. ordertype X VWF ≥ α")
      case True
      then show ?thesis
        using insert.prems by blast
    next
      case False
      moreover have "small (X ∪ ⋃𝒜)"
        using insert.prems by auto
      moreover have "ordertype (⋃(insert X 𝒜)) VWF ≥ α"
        using insert.prems ordertype_VWF_mono by blast
      ultimately have "ordertype X VWF ≥ α"
        using indecomposable_ordertype_ge [OF indec]
        by (metis Diff_subset_conv Sup_insert cSup_singleton insert.IH small_sup_iff subset_refl)
      then show ?thesis
        using insert.prems by blast
    qed
  qed
qed auto

end