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 "xlist.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 "xelts ω. β + γ  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