Theory DilworthCountable

(* Dilworth's Theorem for countable finite Graphs version
   Fabian Fernando Serrano Suárez  UNAL Manizales
   Thaynara Arielly de Lima        Universidade Federal de Goiás 
   Mauricio Ayala-Rincón           Universidade Federal de Goiás and Universidade de Brasília
   Last modified: 16 June, 2026
*)

section ‹Dilworth Countable Theorem›

theory DilworthCountable
  imports 
    Dilworth_Finite 
    Prop_Compactness.k_coloring
begin
text‹The countable infinite version of Dilworth's theorem for partially ordered sets states that, 
whenever the "width" of the partial order is finite, i.e., whenever there exists a finite upper 
bound on the size of anti-chains, there exists a finite minimal chain decomposition with size equal
to the size of the largest anti-chain.› 

definition incomparability_graph :: "'a rel ⇒ 'a set ⇒'a digraph"
  where 
    "incomparability_graph r A  ≡  (A,{(x, y)|x y. x ∈ A ∧ y ∈ A ∧ (x,y) ∉ r ∧ (y,x) ∉ r ∧ x≠y})"

lemma chain_decomposition_colorable:
  assumes  "partition_on A P" and "finite P" and "(∀B∈P.(total_on B r))"
  shows "(colorable (incomparability_graph r A) (card P))"  
proof-
  let ?k = "(card P)"
  have  "∃f. P = f ` {i. i < ?k} ∧ inj_on f {i. i < ?k}" using assms(2)
    by (metis card_Collect_less_nat card_image finite_imp_nat_seg_image_inj_on) 
  then obtain f where f1: "P = f ` {i::nat. i < ?k}" and f2: "inj_on f {i. i < ?k}" by auto
  let ?G = "incomparability_graph r A"
  let ?c = "λv. THE i. i < ?k ∧ (∃p ∈ P. v ∈ p ∧ f i = p)"
  have *: "∀u. u∈V[?G]⟶ (∃!i. i < ?k ∧ (∃p. p ∈ P ∧ u ∈ p ∧ f i = p ) ∧ ?c(u) = i)"
  proof(intro allI impI)
    fix u
    assume hip: "u∈V[?G]"
    show "(∃!i. i < ?k ∧ (∃p. p ∈ P ∧ u ∈ p ∧ f i = p ) ∧ ?c(u) = i)"
    proof-
      have 1:"∃i. i < ?k ∧ (∃p. p∈P ∧ u ∈ p ∧ f i = p)" using hip assms f1 
        by(metis (no_types, lifting) UN_E image_eqI
            incomparability_graph_def mem_Collect_eq partition_onD1 prod.sel(1))
      then obtain p i where p: " p ∈ P ∧ u ∈ p" and i1: "f i = p"  and i2:  "i < ?k" by blast
      hence "i < ?k ∧ (∃p. p∈P ∧ u ∈ p ∧ f i = p)" by auto 
      have 2: "∀x. x < ?k ∧ (∃p ∈ P. u ∈ p ∧ f x = p) ⟶ x = i"
      proof(intro allI impI)
        fix x
        assume hip: "x < ?k ∧ (∃p ∈ P. u ∈ p ∧ f x = p)"
        show "x = i"
        proof-
          from hip obtain q  where q: "q ∈ P ∧ u ∈ q" and q1: "f x = q" by auto
          hence 1:  "f x ∈ f ` {i::nat. i < ?k}" using f1 by auto   
          have  2: "f i ∈ f ` {i::nat. i < ?k}" using i2 by auto
          have "p = q" using q p  assms(1) using disjointD partition_on_def by fastforce
          hence "f x = f i" using q1 i1 by auto
          hence "x = i" using hip i2  1 2 f2 by(simp add: inj_onD)
          thus ?thesis by auto
        qed
      qed
      from 1 and 2 show ?thesis by auto
      have 3: "?c(u) = i" using 1 2 p by auto
    qed
  qed
  have c1: "(∀u. u∈V[?G]⟶ ?c(u) < ?k)" using * by blast 
  have c2: "(∀u v.(u,v)∈E[?G] ⟶ ?c(u)≠?c(v))" 
  proof(intro allI impI)
    fix u v 
    assume hip:  "(u,v)∈E[?G]"   
    hence a: "u∈V[?G]" and b:  "v∈V[?G]" by(unfold incomparability_graph_def, auto) 
    have "∃i.∃p. p∈P ∧ u ∈ p ∧ f i = p ∧ i <  ?k " using * a by auto
    then obtain p i where p: "p ∈ P ∧ u ∈ p" and i1: "f i = p"  and i2: "i < ?k"
      and i3: "?c(u) = i" using * a by auto
    have  "∃j.∃q. q∈P ∧ v ∈ q ∧ f j = q ∧ j <  ?k" using * b by auto
    then obtain q j where q: "q ∈ P ∧ v ∈ q" and j1: "f j = q"  and j2: "j < ?k"
      and j3: "?c(v) = j" using * b by auto 
    show "?c(u)≠?c(v)" 
    proof(rule notI)
      assume "?c(u) = ?c(v)"        
      hence 3:  "p = q" using i1 i3 j1 j3 by auto  
      have 4: "u∈A" and "v∈A" using hip by(unfold incomparability_graph_def, auto)
      hence "(u,v) ∈ r ∨ (v,u)∈ r" using p q 3 assms(3)
        by (smt (verit, best) CollectD Pair_inject hip incomparability_graph_def sndI total_on_def)  
      thus False using hip by(unfold incomparability_graph_def, auto)
    qed
  qed
  hence "coloring ?c ?k (incomparability_graph r A)" 
    using c1 c2 by(unfold coloring_def,auto) 
  thus ?thesis using c1 c2 by (unfold colorable_def,auto) 
qed

lemma non_empty_set_color: assumes "coloring c k (incomparability_graph r A)" and "j∈ c`A"
  shows "{x ∈ A. c x = j} ≠ {}"
proof-
  have "V[incomparability_graph r A] = A" 
    using incomparability_graph_def[of r A] by auto  
  have  "∃x ∈ A. c(x) = j" 
    using assms incomparability_graph_def[of r A] by auto 
  thus ?thesis by auto
qed

lemma coloring_particion: 
  assumes  "coloring c k (incomparability_graph r A)" 
  shows  "partition_on A {{x ∈ A. c(x) = j}|j. j ∈ c`A}"
proof-
  let ?G = "incomparability_graph r A"
  have 1:  "⋃{{x ∈ A. c x = j} |j. j ∈  c`(V[?G])} = A" 
  proof-
    have "⋃ {{x ∈ A. c x = j} |j. j ∈  c`(V[?G])} ⊆ A" by auto
    moreover 
    have  "A ⊆ ⋃ {{x ∈ A. c x = j} |j. j ∈  c`(V[?G])}"
    proof
      fix x
      assume h: "x ∈ A"
      hence "x∈V[?G]" using incomparability_graph_def
        by (metis (lifting) fst_conv) 
      hence "∃j. c(x) = j" using assms coloring_def
        by metis
      then obtain j where j: "c(x) = j" by auto
      hence "x∈{x ∈ A. c x = j |j ∈  c`(V[?G])}" using h by auto
      thus "x∈⋃ {{x ∈ A. c x = j} |j. j ∈ c`(V[?G])}" using j
        using ‹x ∈ V[incomparability_graph r A]› by blast
    qed  
    finally 
    show  "⋃ {{x ∈ A. c x = j} |j. j ∈ c`(V[?G]) } = A" by auto
  qed
  have 2:  "disjoint {{x ∈ A. c x = j} |j. j ∈ c`(V[?G])}" 
    using assms coloring_def
    by (smt (verit, best) disjnt_iff mem_Collect_eq pairwiseI)    
  have 3: "{} ∉ {{x ∈ A. c x = j} |j. j ∈ c`(V[?G])}"  
    using assms coloring_def non_empty_set_color
    by (smt (verit, best) Collect_empty_eq fst_conv incomparability_graph_def mem_Collect_eq)   
  show ?thesis using 1 2 3
    by (simp add: incomparability_graph_def partition_on_def)
qed

lemma (in part_order) coloring_total:
  assumes "coloring c k (incomparability_graph r A)" and "j ∈ c`A"
  shows "total_on {x ∈ A. c x = j} r"
proof-
  {
    fix x y
    assume h1: "x∈{x ∈ A. c x = j}" and h2: "y∈{x ∈ A. c x = j}" 
    have "x ≠ y ⟶ (x, y) ∈ r ∨ (y, x) ∈ r" 
    proof
      assume "x ≠ y" 
      thus  "(x, y) ∈ r ∨ (y, x) ∈ r" using h1 h2 assms incomparability_graph_def[of r A]
        by (smt (verit, best) coloring_def mem_Collect_eq snd_conv)  
    qed
  }
  thus ?thesis using total_on_def
    by blast 
qed 

lemma partition_card_le_colors:
  assumes col: "coloring c k G" 
  shows "card ({{x ∈ A. c x = j} | j. j ∈ c`(V[G])}) ≤ k"
proof(cases "k = 0")
  assume "k = 0" 
  hence "V[G] = {}" using assms coloring_def
    by (meson coloring_nonemptygraph colorable_def dual_order.irrefl)
  thus ?thesis
    by simp
next 
  assume "k ≠ 0" 
  hence "k > 0" by auto
  let ?P = "{{x ∈ A. c x = j} | j. j ∈ c`(V[G])}"
  have P_image: "?P = (λj. {x ∈ A. c x = j})`(c`(V[G]))"
    by auto
  have fin_colors: "finite (c`(V[G]))"
  proof -
    have "card (c`(V[G])) ≤ k"
      using coloring_card_image[OF col] by simp 
    thus ?thesis
      by (metis (no_types, lifting) bounded_nat_set_is_finite col coloring_def imageE)
  qed
  have "card ?P ≤ card (c ` (V[G]))"
    unfolding P_image  using fin_colors 
    by (rule card_image_le)
  also have "... ≤ k"
    using coloring_card_image[OF col] by simp
  finally show ?thesis by simp
qed

lemma (in part_order) coloring_chain_decomposition1:
  assumes "coloring c k (incomparability_graph r A)"
  shows  "chain_decomposition A r {{x ∈ A. c x = j} |j. j ∈ c`A} ∧ 
          card ({{x ∈ A. c x = j} |j. j ∈ c`A})≤ k "
proof-
  have "chain_decomposition A r {{x ∈ A. c x = j} |j. j ∈ c`A}"
    using coloring_particion[of c k r A] coloring_total[of c k] 
    by (smt (verit, best) Dilworth_Finite.chain_def Sup_upper assms(1) 
        chain_decomposition_def mem_Collect_eq  p_o_translation partition_onD1) 
  moreover
  have "card ({{x ∈ A. c x = j} |j. j ∈ c`A}) ≤ k" using assms partition_card_le_colors
      coloring_def[of c k "(incomparability_graph r A)"]  
      coloring_card_image[of c k "(incomparability_graph r A)"]
    using incomparability_graph_def[of r A] by fastforce
  ultimately show ?thesis by auto
qed

lemma coloring_chain_decomposition_finite:
  assumes "coloring c k (incomparability_graph r A)"
  shows "finite ({{x ∈ A. c x = j} | j. j ∈ c`A})"
proof -
  let ?CD = "{{x ∈ A. c x = j} | j. j ∈ c`A}"
  have "?CD = (λj. {x ∈ A. c x = j}) ` (c`A)"
    by auto
  moreover have "finite (c`A)"
  proof -
    have "c`A ⊆ {0..<k}"
      using assms
      unfolding coloring_def incomparability_graph_def
      by auto
    thus ?thesis
      using finite_lessThan finite_subset
      by blast
  qed
  ultimately show ?thesis
    by simp
qed

lemma (in part_order) coloring_chain_decomposition:
  assumes "coloring c k (incomparability_graph r A)" 
  shows "(∃CD. chain_decomposition A r CD ∧  card CD ≤ k ∧ finite CD)"
  using coloring_chain_decomposition1  coloring_chain_decomposition_finite assms
  by blast 

lemma (in part_order_countable) width_coloring_finite:
  assumes "(∀AC. anti_chain A r AC ⟶ card AC ≤ m)" and "finite A"
  shows "(∃c. ∃k. coloring c k (incomparability_graph r A) ∧ k ≤ m)"
proof-
  have  "∃sCD. chain_decomposition A r sCD ∧ card sCD ≤ m" 
    by (metis assms(2) assms(1) smallest_chain_decomposition_def largest_antichain_def 
        Dilworth_Finite)  
  then obtain sCD where sCD:  "chain_decomposition A r sCD ∧ card sCD ≤ m" by auto
  hence 1:"(colorable (incomparability_graph r A) (card sCD))"
    using  chain_decomposition_def chain_decomposition_colorable
    by (metis Dilworth_Finite.chain_def assms(2) finite_elements)
  have "∃c. coloring c (card sCD) (incomparability_graph r A) ∧ card sCD ≤ m"
    using colorable_def 1 sCD 
    by blast 
  thus ?thesis 
    using colorable_def coloring_def sCD
    by (smt (verit, best) ‹chain_decomposition A r sCD ∧ card sCD ≤ m› coloring_def order_trans) 
qed

lemma (in part_order_countable) partial_order_restrc:
  assumes "B⊆A"
  shows "partial_order_on B (Restr r B)" 
  using partial_order_on_def[of B "(Restr r B)"]
  by (smt (verit, best) Int_iff Sigma_cong antisym_Restr assms mem_Sigma_iff p_o_translation 
      partial_order_on_def preorder_on_def refl_on_def subsetD subsetI trans_Restr)

lemma (in part_order_countable) antichain_restrc:
  assumes "anti_chain A r AC" and "B⊆A"
  shows "anti_chain B (Restr r B) (AC ∩ B)" 
  using partial_order_restrc[of B] anti_chain_def[of B "(Restr r B)" "(AC ∩ B)"]
  by (meson IntE anti_chain_def anti_total_def assms(1,2) inf_le2)   

lemma (in part_order_countable) width_induced_subgraph:
  assumes "∀AC. anti_chain A r AC ⟶ card AC ≤ w" and "finite B"
  shows  "∀ACB. anti_chain B (Restr r B) ACB ⟶ card ACB ≤ w" using assms
  by (smt (verit, del_insts) Int_iff anti_chain_def anti_total_def mem_Sigma_iff 
      p_o_translation partial_order_onD(1,4) refl_on_def subset_iff)

lemma graph_incomparability:
  "is_graph (incomparability_graph r A)" 
  using is_graph_def incomparability_graph_def
  by (smt (verit, ccfv_SIG) mem_Collect_eq split_pairs2) 

lemma induced_subgraph_incomparability:  
  assumes "is_induced_subgraph H (incomparability_graph r A) ∧ finite_graph H"
  shows "∃B. (finite B) ∧ B = V[H] ∧ (E[H] = E[(incomparability_graph r A)] ∩ (B×B)) ∧ B ⊆ A"        
  using assms is_induced_subgraph_def incomparability_graph_def
  by (metis (mono_tags, lifting) finite_graph_def fst_conv)

lemma  incomparability_subgraph: 
  assumes "is_graph (incomparability_graph r A)"    
    and "is_subgraph H (incomparability_graph r A) ∧ finite_graph H"
  shows "∃B. (finite B) ∧ B = V[H] ∧ (E[H] ⊆ E[(incomparability_graph r A)] ∩ (B×B)) ∧ B ⊆ A"
  using assms is_subgraph_def incomparability_graph_def
  by (metis (no_types, lifting) Sigma_cong finite_graph_def fst_conv)

lemma (in part_order_countable) colorable_induced_subgraph:
  assumes "∀AC. anti_chain A r AC ⟶ card AC ≤ m" 
  shows "(∀H. is_induced_subgraph H (incomparability_graph r A) ∧  finite_graph H ⟶ colorable H m)" 
proof-  
  have "∀H. is_induced_subgraph H (incomparability_graph r A) ∧ finite_graph H ⟶ colorable H m"
  proof (rule allI, rule impI)
    fix H  
    assume H_assms: "is_induced_subgraph H (incomparability_graph r A) ∧ finite_graph H"     
    have "∃B. (finite B) ∧ B = V[H] ∧ (E[H] = E[(incomparability_graph r A)] ∩ (B×B)) ∧ B ⊆ A"
      using incomparability_subgraph assms(1)
      by (simp add: H_assms graph_incomparability induced_subgraph_incomparability)
    then obtain B where B: "(finite B) ∧ B = V[H] ∧ (E[H] = E[(incomparability_graph r A)] ∩ (B×B)) ∧ B ⊆ A" 
      by auto
    have AC_B: "∀AC. anti_chain B (Restr r B) AC ⟶ card AC ≤ m"
      using B antichain_restrc
      by (smt (verit, ccfv_threshold) Int_iff anti_chain_def anti_total_def assms mem_Sigma_iff 
          p_o_translation subset_iff)
    have poB: "partial_order_on B (Restr r B)"
      using partial_order_restrc B p_o_translation  
      by auto
    have "∃c.∃k. coloring c k (incomparability_graph (Restr r B) B) ∧ k ≤ m"
      using AC_B B part_order_countable.width_coloring_finite part_order_countable_def part_order_def poB by blast
    then obtain  c k where c: "coloring c k (incomparability_graph (Restr r B) B) ∧ k ≤ m" by auto    
    hence "coloring c k H"
      using B induced_subgraph_incomparability 
      by (simp add: coloring_def incomparability_graph_def)
    hence "coloring c m H" using coloring_def
      by (metis c inf.absorb_iff2 inf.strict_boundedE) 
    thus "colorable H m"
      using colorable_def by blast
  qed
  thus ?thesis
    by blast
qed

lemma exists_smallest_chain_decomposition:
  assumes "∃C. chain_decomposition A r C"
  shows "∃C. smallest_chain_decomposition A r C"
proof-
  let ?Q = "λn. ∃C. chain_decomposition A r C ∧ card C = n"
  obtain k where k1: "?Q k" and k2: "∀m<k. ¬ ?Q m"
    using assms ex_least_nat_le[of ?Q ]  by blast
  obtain C where CD1: "chain_decomposition A r C" and CD2: "card C = k"
    using k1 by blast 
  have minC: "∀P. chain_decomposition A r P ⟶ card C ≤ card P"
  proof(rule allI)
    fix P
    show  "chain_decomposition A r P ⟶ card C ≤ card P"
    proof
      assume PCD: "chain_decomposition A r P"
      show "card C ≤ card P"
      proof-
        have 1: "¬ card P < k"
        proof
          assume "card P < k"
          hence "?Q (card P)"
            using PCD by blast      
          with k2 show False
            by (metis k2 ‹∃C. chain_decomposition A r C ∧ card C = card P› ‹card P < k›) 
        qed 
        thus "card C ≤ card P"  using CD2 1 not_le_imp_less by blast 
      qed
    qed
  qed
  have "smallest_chain_decomposition A r C"
    unfolding smallest_chain_decomposition_def
    using CD1 minC by blast
  thus ?thesis by blast
qed

lemma (in part_order_countable) exists_largest_antichain:
  assumes "∀AC. anti_chain A r AC ⟶ card AC ≤ m" 
  shows "∃lgAC. largest_antichain A r lgAC"
proof-
  let ?P = "{card B | B. anti_chain A r B}"
  have 1:"?P ⊆ {0..m}"
    using assms(1) atLeastAtMost_iff by blast
  moreover
  have "anti_chain A r {}" 
    using anti_chain_def  anti_total_def p_o_translation 
    by blast
  hence 2: "?P ≠ {}"
    by blast
  ultimately 
  have "∃k. k = Max ?P"
    by blast 
  then obtain k where  "k = Max ?P" by auto
  moreover 
  have finP: "finite ?P" 
    using 1 by (meson finite_atLeastAtMost finite_subset)
  hence  k_in: "k ∈ ?P" 
    using Max_in calculation 2 by auto  
  then obtain lgAC where
    lgAC_antichain: "anti_chain A r lgAC" and lgAC_card: "card lgAC = k"
    by blast
  have largest: "largest_antichain A r lgAC"
  proof(unfold largest_antichain_def, intro conjI allI impI)
    show "anti_chain A r lgAC"
      by (rule lgAC_antichain)
  next
    fix C
    assume Canti: "anti_chain A r C"
    have "card C ∈ ?P" 
      using Canti by blast
    hence "card C ≤ k"
      using finP calculation by auto
    hence "card C ≤ card lgAC"
      using lgAC_card  by simp
    thus "card C ≤ card lgAC" 
      by metis 
  qed  
  thus "∃lgAC. largest_antichain A r lgAC" by auto
qed

theorem (in part_order_countable) Dilworth_countable_aux:
  assumes "largest_antichain A r lgAC" 
  shows "(∃CD. (chain_decomposition A r CD ∧ finite CD) ∧ card CD ≤ card lgAC)" 
proof- 
  have 1: "is_graph (incomparability_graph r A)" 
    using  graph_incomparability by auto
  have "(colorable (incomparability_graph r A) (card lgAC))"
  proof-
    have "∀H. is_induced_subgraph H (incomparability_graph r A) ∧ finite_graph H ⟶  
          colorable H (card lgAC)" 
      using colorable_induced_subgraph assms
      by (metis largest_antichain_def)
    thus ?thesis
      using "1"  deBruijn_Erdos_coloring_for_finite_induced_subgraphs 
      by metis
  qed  
  thus ?thesis 
    using  colorable_def coloring_chain_decomposition         
    by metis
qed

definition largest_finite_antichain :: "'a set ⇒ 'a rel ⇒ 'a set ⇒ bool"
  where "largest_finite_antichain A r B ≡
      anti_chain A r B ∧ finite B ∧ (∀C. anti_chain A r C ∧ finite C ⟶ card C ≤ card B)"

lemma (in part_order_countable) exists_largest_finite_antichain:
  assumes H: "∀AC. anti_chain A r AC ∧ finite AC ⟶ card AC ≤ m"
  shows "∃lgAC. largest_finite_antichain A r lgAC"
proof -
  let ?P = "{card B | B. anti_chain A r B ∧ finite B}"
  have subsetP: "?P ⊆ {0..m}"
  proof
    fix n
    assume "n ∈ ?P"
    then obtain B where
      B: "anti_chain A r B ∧ finite B" and n: "n = card B"
      by blast
    have "card B ≤ m" 
      using H B by blast
    thus "n ∈ {0..m}"
      using n by auto
  qed
  have anti_empty: "anti_chain A r {}"
    unfolding anti_chain_def anti_total_def
    using p_o_translation by auto
  hence 2: "?P ≠ {}"
    by auto
  have finP: "finite ?P"
    using subsetP finite_atLeastAtMost
    by (rule finite_subset)
  let ?k = "Max ?P"
  have k_in: "?k ∈ ?P"
    using "2" Max_eq_iff finP by blast
  then obtain lgAC where
    lgAC1: "anti_chain A r lgAC ∧ finite lgAC" and lgAC2: "card lgAC = ?k"
    by fastforce
  have largest:
    "largest_finite_antichain A r lgAC"
  proof (unfold largest_finite_antichain_def, intro conjI allI impI)
    show "anti_chain A r lgAC"
      using lgAC1 by blast
    show "finite lgAC"
      using lgAC1 by blast
    fix C
    assume C: "anti_chain A r C ∧ finite C"
    have "card C ∈ ?P"
      using C by blast
    hence "card C ≤ ?k"
      using finP k_in by simp
    thus "card C ≤ card lgAC"
      using lgAC2 by simp
  qed
  show ?thesis
    using largest by blast
qed

(*Since the partition in singletons of any partial order is always a chain decomposition, 
  and in Isabelle the Cardinal of infinite sets is defined as zero, in the countable case, 
  it is necessary to distinguish the smallest Cardinal of finite chain decompositions to 
  have a correct notion of smallest chain decomposition *)

definition finite_smallest_chain_decomposition :: "'a set ⇒ 'a rel ⇒'a set set ⇒ bool" where
  "finite_smallest_chain_decomposition A r CD ≡ 
  chain_decomposition A r CD  ∧ 
  finite CD ∧ 
  (∀P. chain_decomposition A r P ∧ finite P  ⟶ card CD ≤ card P)"

lemma exists_smallest_finite_chain_decomposition:
  assumes "∃CD. chain_decomposition A r CD ∧ finite CD"
  shows "∃sCD. finite_smallest_chain_decomposition A r sCD"
proof-
  let ?Q = "λn. ∃C. chain_decomposition A r C ∧ finite C ∧ card C = n"
  obtain k where k1: "?Q k" and k2: "∀m<k. ¬ ?Q m"
    using assms ex_least_nat_le[of ?Q ]  by blast
  obtain sC where CD1: "chain_decomposition A r sC ∧ finite sC" and CD2: "card sC = k"
    using k1 by blast 
  have minC: "∀P. chain_decomposition A r P ∧ finite P ⟶ card sC ≤ card P"
  proof(intro allI impI)
    fix P
    assume PCD: "chain_decomposition A r P ∧ finite P"
    show "card sC ≤ card P"
    proof-
      have 1: "¬ card P < k"
      proof
        assume "card P < k"
        hence "?Q (card P)"
          using PCD by blast      
        with k2 show False
          by (metis ‹∃C. chain_decomposition A r C ∧ finite C ∧ card C = card P› k2 ‹card P < k›)
      qed 
      thus "card sC ≤ card P"  using CD2 1 not_le_imp_less by blast 
    qed
  qed
  have "finite_smallest_chain_decomposition A r sC"
    unfolding finite_smallest_chain_decomposition_def
    using CD1 minC by blast
  thus ?thesis by blast
qed

theorem (in part_order_countable) Dilworth_countable:
  assumes "∃m.∀AC. anti_chain A r AC ∧ finite AC  ⟶ card AC ≤ m"
  shows "∃smD. ∃lgAC. finite_smallest_chain_decomposition A r smD ∧ largest_finite_antichain A r lgAC ∧
        card smD = card lgAC"
proof-
  obtain lgAC where lgAC1: "largest_finite_antichain A r lgAC" 
    using assms exists_largest_finite_antichain 
    by auto 
  hence lgAC: "largest_antichain A r lgAC ∧ finite lgAC" 
    using largest_finite_antichain_def
    by (metis bot_nat_0.extremum card_eq_0_iff largest_antichain_def) 
  then obtain sCD  where sCD: "(chain_decomposition A r sCD ∧ finite sCD) ∧ card sCD ≤ card lgAC" 
    by (meson Dilworth_countable_aux)
  then obtain C where C: "finite_smallest_chain_decomposition A r C " 
    using exists_smallest_finite_chain_decomposition  finite_smallest_chain_decomposition_def 
    by blast
  hence "card lgAC ≤ card C" 
    using lgAC sCD antichain_le_chain_decomposition[of C lgAC]
      largest_antichain_def finite_smallest_chain_decomposition_def
    by blast
  moreover
  have "card C ≤ card lgAC" using C finite_smallest_chain_decomposition_def sCD
    using le_trans by blast
  ultimately
  have "card lgAC = card C" by auto
  thus  ?thesis using C lgAC1
    by metis 
qed

end