Quellcode-Bibliothek Dilworth.thy

(*   Title:      Formal Proof of Dilworth's Theorem
     Author:  Vivek Soorya Maadoori, Syed Mohammad Meesum, Shiv Pillai, T.V.H. Prathamesh, Aditya Swami,  2025
     Maintainer:  Vivek Soorya Maadoori, Syed Mohammad Meesum, Shiv Pillai, T.V.H. Prathamesh, Aditya Swami
 *)



theory Dilworth
imports Main HOL.Complete_Partial_Order HOL.Relation HOL.Order_Relation 
        "Min_Max_Least_Greatest.Min_Max_Least_Greatest_Set"
begin


text ‹Note: The Dilworth's theorem for chain cover is labelled Dilworth and the
  to chain decomposition is labelled Dilworth\_Decomposition.›

context order
begin

section "Definitions"

definition chain_on :: "_ set ==> _ set ==> bool" where
"chain_on A S ⟷ ((A ⊆ S) ∧ (Complete_Partial_Order.chain (≤) A))"

definition antichain :: " _ set ==> bool" where
"antichain S ⟷ (∀x ∈ S. ∀y ∈ S. ( x ≤ y ∨ y ≤ x) ⟶ x = y)"

definition antichain_on :: "_ set ==> _ set ==> bool" where
"(antichain_on A S) ⟷
  (partial_order_on A (relation_of (≤) A)) ∧ (S ⊆ A) ∧ (antichain S)"

definition largest_antichain_on:: "_ set ==> _ set ==> bool" where
"largest_antichain_on P lac ⟷
  (antichain_on P lac ∧ (∀ ac. antichain_on P ac ⟶ card ac ≤ card lac))"

definition chain_cover_on:: "_ set ==> _ set set ==> bool" where
"chain_cover_on S cv ⟷ (∪ cv = S) ∧ (∀ x ∈ cv . chain_on x S)"

definition antichain_cover_on:: "_ set ==> _ set set ==> bool" where
"antichain_cover_on S cv ⟷ (∪ cv = S) ∧ (∀ x ∈ cv . antichain_on S x)"

definition smallest_chain_cover_on:: "_ set ==> _ set set ==> bool" where
"smallest_chain_cover_on S cv ≡
  (chain_cover_on S cv ∧
  (∀ cv2. (chain_cover_on S cv2 ∧ card cv2 ≤ card cv) ⟶ card cv = card cv2))"

definition chain_decomposition where  
"chain_decomposition S cd ≡ ((chain_cover_on S cd) ∧
                             (∀ x ∈ cd. ∀ y ∈ cd. x ≠ y ⟶ (x ∩ y = {})))"

definition smallest_chain_decomposition:: "_ set ==> _ set set ==> bool" where
"smallest_chain_decomposition S cd
  ≡ (chain_decomposition S cd
      ∧ (∀ cd2. (chain_decomposition S cd2 ∧ card cd2 ≤ card cd)
                                          ⟶ card cd = card cd2))"

section "Preliminary Lemmas"

text ‹ The following lemma shows that given a chain and an antichain, if the cardinality of their
 intersection is equal to 0, then their intersection is empty..›


lemma inter_nInf: 
  assumes a1: "Complete_Partial_Order.chain (⊆) X" 
      and a2: "antichain Y"
  and asmInf: "card (X ∩ Y) = 0"
        shows "X ∩ Y = {}"
proof (rule ccontr)
  assume "X ∩ Y ≠ {}"
  then obtain a b where 1:"a ∈ (X ∩ Y)" "b ∈ (X ∩ Y)" using asmInf by blast
  then have in_chain: "a ∈ X ∧ b ∈ X" using 1 by simp
  then have 3: "(a ≤ b) ∨ (b ≤ a)" using  a1 
    by (simp add: chain_def) 
  have in_antichain: "a ∈ Y ∧ b ∈ Y" using 1 by blast
  then have "a = b" using antichain_def a2 3 
    by (metis order_class.antichain_def)
  then have "∀ a ∈ (X ∩ Y). ∀ b ∈ (X ∩ Y). a = b" 
    using 1 a1 a2 order_class.antichain_def
    by (smt (verit, best) IntE chain_def)
  then have "card (X ∩ Y) = 1" using 1 a1 a2 card_def
    by (smt (verit, best) all_not_in_conv asmInf card_0_eq card_le_Suc0_iff_eq 
        finite_if_finite_subsets_card_bdd subset_eq subset_iff)
  then show False using asmInf by presburger
qed

text ‹ The following lemma shows that given a chain X and an antichain Y that both are subsets of S, their intersection
  either empty or has cardinality one..›

lemma chain_antichain_inter: 
  assumes a1: "Complete_Partial_Order.chain (⊆) X"  
      and a2: "antichain Y"
      and a3: "X ⊆ S ∧ Y ⊆ S"
        shows "(card (X ∩ Y) = 1) ∨ ((X ∩ Y) = {})"
proof (cases "card (X ∩ Y) ≥ 1")
  case True
  then obtain a b where 1:"a ∈ (X ∩ Y)" "b ∈ (X ∩ Y)"
    by (metis card_1_singletonE insert_subset obtain_subset_with_card_n)
  then have "a ∈ X ∧ b ∈ X" using 1 by blast
  then have 3: "(a ≤ b) ∨ (b ≤ a)" using Complete_Partial_Order.chain_def a1 
    by (smt (verit, best)) 
  have "a ∈ Y ∧ b ∈ Y" using 1 by blast
  then have "a = b" using a2 order_class.antichain_def 3 
    by (metis)
  then have "∀ a ∈ (X ∩ Y). ∀ b ∈ (X ∩ Y). a = b" 
    using 1 a1 a2 order_class.antichain_def
    by (smt (verit, best) Int_iff chainD)
  then have "card (X ∩ Y) = 1" using 1 a1 a2
    by (metis One_nat_def True card.infinite card_le_Suc0_iff_eq 
              order_class.order_antisym zero_less_one_class.zero_le_one)
  then show ?thesis by presburger
next
  case False
  then have "card (X ∩ Y) < 1" by linarith
  then have "card (X ∩ Y) = 0" by blast
  then have "X ∩ Y = {}" using assms inter_nInf by blast
  then show ?thesis by force
qed

text ‹Following lemmas show that given a finite set S, there exists a chain decomposition of S.›

lemma po_restr: assumes "partial_order_on B r" 
                    and "A ⊆ B" 
                  shows "partial_order_on A (r ∩ (A × A))"
  using assms 
  unfolding partial_order_on_def preorder_on_def antisym_def refl_on_def trans_def
  by (metis (no_types, lifting) IntD1 IntD2 IntI Int_lower2 inf.orderE mem_Sigma_iff)


lemma eq_restr: "(Restr (relation_of (≤) (insert a A)) A) = (relation_of (≤) A)" 
  (is "?P = ?Q")
proof
  show "?P ⊆ ?Q"
  proof
    fix z
    assume "z ∈ ?P"
    then obtain x y where tuple: "(x, y) = z" using relation_of_def by blast
    then have 1: "(x, y) ∈ ((relation_of (≤) (insert a A)) ∩ (A × A))" 
      using relation_of_def
      using ‹z ∈ Restr (relation_of (≤) (insert a A)) A› by blast
    then have 2: "(x, y) ∈ (relation_of (≤) (insert a A))" by simp
    then have 3: "(x, y) ∈ (A × A)" using 1 by simp
    then have "(x, y) ∈ (A × A) ∧ (x ≤ y)" using relation_of_def 2
      by (metis (no_types, lifting) case_prodD mem_Collect_eq)
    then have "(x, y) ∈ (relation_of (≤) A)" using relation_of_def by blast
    then show "z ∈ ?Q" using tuple by fast
  qed
next
  show "?Q ⊆ ?P"
  proof
    fix z
    assume asm1: "z ∈ ?Q"
    then obtain x y where tuple: "(x, y) = z" by (metis prod.collapse)
    then have 0: "(x, y) ∈ (A × A) ∧ (x ≤ y)" using asm1 relation_of_def
      by (metis (mono_tags, lifting) case_prod_conv mem_Collect_eq)
    then have 1: "(x, y) ∈ (A × A)" by fast
    have rel: "x ≤ y" using 0 by blast
    have "(A × A) ⊆ ((insert a A) × (insert a A))" by blast
    then have "(x, y) ∈ ((insert a A) × (insert a A))" using 1 by blast
    then have "(x, y) ∈ (relation_of (≤) (insert a A))" 
      using rel relation_of_def by blast
    then have "(x, y) ∈ ((relation_of (≤) (insert a A)) ∩ (A × A))" using 1 by fast
    then show "z ∈ ?P" using tuple by fast
  qed
qed

lemma part_ord:"partial_order_on S (relation_of (≤) S)" 
  by (smt (verit, ccfv_SIG) local.dual_order.eq_iff local.dual_order.trans 
      partial_order_on_relation_ofI)

text ‹The following lemma shows that a chain decomposition exists for any finite set S.›

lemma exists_cd: assumes "finite S"
                   shows "∃ cd. chain_decomposition S cd" 
   using assms
proof(induction rule: finite.induct)
  case emptyI
  then show ?case using assms unfolding chain_decomposition_def chain_cover_on_def
    by (metis Sup_empty empty_iff)
next
  case (insertI A a)
  show ?case using assms
  proof (cases "a ∈ A")
    case True
    then have 1: "(insert a A) = A" by fast
    then have "∃ X. chain_decomposition A X" using insertI by simp
    then show ?thesis using 1 by auto
  next
    case False
    have subset_a: "{a} ⊆ (insert a A)" by simp
    have chain_a: "Complete_Partial_Order.chain (≤) {a}" 
      using chain_singleton chain_def by auto
    have subset_A: "A ⊆ (insert a A)" by blast
    have partial_a: "partial_order_on A ((relation_of (≤) (insert a A)) ∩ (A × A))"
      using po_restr insertI subset_A part_ord by blast
    then have chain_on_A: "chain_on {a} (insert a A)" 
      unfolding order_class.chain_on_def using chain_a partial_a 
                insertI.prems chain_on_def by simp 
    then  obtain X where chain_set: "chain_decomposition A X" 
      using insertI partial_a eq_restr 
      by auto 
    have chains_X: "∀ x ∈ (insert {a} X). chain_on x (insert a A)" 
      using subset_A chain_set chain_on_def 
            chain_decomposition_def chain_cover_on_def chain_on_A
      by auto
    have subsets_X: "∀ x ∈ (insert {a} X). x ⊆ (insert a A)" 
      using chain_set chain_decomposition_def subset_a chain_cover_on_def
      by auto
    have null_inter_X: "∀ x ∈ X. ∀ y ∈ X. x ≠ y ⟶ x ∩ y = {}"
      using chain_set chain_decomposition_def 
      by (simp add: order_class.chain_decomposition_def)
    have "{a} ∉ X" using False chain_set chain_decomposition_def chain_cover_on_def
      by (metis UnionI insertCI)
    then have null_inter_a: "∀ x ∈ X. {a} ∩ x = {}"
      using False chain_set order_class.chain_decomposition_def 
      using chain_decomposition_def chain_cover_on_def by auto
    then have null_inter: "∀ x ∈ (insert {a} X). ∀ y ∈ (insert {a} X). x ≠ y ⟶ x ∩ y = {}" 
      using null_inter_X by simp
    have union: "∪ (insert {a} X) = (insert a A)" using chain_set
      by (simp add: chain_decomposition_def chain_cover_on_def)
    have "chain_decomposition (insert a A) (insert {a} X)"
      using subsets_X chains_X union null_inter unfolding chain_decomposition_def 
            chain_cover_on_def  
      by simp
    then show ?thesis by blast
  qed
qed

text ‹The following lemma shows that the chain decomposition of a set is a chain cover.›

lemma cd_cv: 
  assumes "chain_decomposition P cd"
  shows "chain_cover_on P cd"
  using assms unfolding chain_decomposition_def by argo

text ‹The following lemma shows that for any finite partially ordered set, there exists a chain cover on that set.›

lemma exists_chain_cover: assumes "finite P"
                   shows "∃ cv. chain_cover_on P cv"
proof-
  show ?thesis using assms exists_cd cd_cv by blast
qed

lemma finite_cv_set: assumes "finite P"
                         and "S = {x. chain_cover_on P x}"
                       shows "finite S"
proof-
  have 1: "∀ cv. chain_cover_on P cv ⟶ (∀ c ∈ cv. finite c)" 
    unfolding chain_cover_on_def chain_on_def chain_def
    using assms(1) rev_finite_subset by auto 
  have 2: "∀ cv. chain_cover_on P cv ⟶ finite cv" 
    unfolding chain_cover_on_def
    using assms(1) finite_UnionD by auto
  have "∀ cv. chain_cover_on P cv ⟶ (∀ c ∈ cv. c ⊆ P)" 
    unfolding chain_cover_on_def by blast
  then have "∀ cv. chain_cover_on P cv ⟶ cv ⊆ Fpow P" using Fpow_def 1 by fast
  then have "∀ cv. chain_cover_on P cv ⟶ cv ∈ Fpow (Fpow P)" 
    using Fpow_def 2 by fast
  then have "S ⊆ Fpow (Fpow P)" using assms(2) by blast
  then show ?thesis 
    using assms(1) by (meson Fpow_subset_Pow finite_Pow_iff finite_subset)
qed


text ‹The following lemma shows that for every element of an antichain in a set, there exists a chain in the
  cover of that set, such that the element of the antichain belongs to the chain.›

lemma elem_ac_in_c: assumes a1: "antichain_on P ac" 
                        and "chain_cover_on P cv"
                      shows "∀ a ∈ ac. ∃ c ∈ cv. a ∈ c"
proof-
  have "∪ cv = P" using assms(2) chain_cover_on_def by simp
  then have "ac ⊆ ∪ cv" using a1 antichain_on_def by simp
  then show "∀ a ∈ ac. ∃ c ∈ cv. a ∈ c" by blast
qed

text ‹ For a function f that maps every element of an antichain to
  chain it belongs to in a chain cover, we show that, the co-domain of f is a subset of
  chain cover.›

lemma f_image: fixes f :: "_ ==> _ set"
             assumes a1: "(antichain_on P ac)"
                 and a2: "(chain_cover_on P cv)"
                 and a3: "∀a ∈ ac. ∃ c ∈ cv. a ∈ c ∧ f a = c"
               shows "(f ` ac) ⊆ cv"
proof
  have 1: "∀a ∈ ac. ∃ c ∈ cv. a ∈ c" using elem_ac_in_c a1 a2 by presburger
  fix y
  assume "y ∈ (f ` ac)"
  then obtain x where "f x = y" " x ∈ ac" using a1 a2 by auto
  then have "x ∈ y" using a3 by blast
  then show "y ∈ cv" using a3 using ‹f x = y› ‹x ∈ ac› by blast
qed

section "Size of an antichain is less than or equal to the
size of a chain cover"

text ‹The following lemma shows that given an antichain ac and chain cover cv on a finite set, the
  of ac will be less than or equal to the cardinality of cv.›

lemma antichain_card_leq: 
           assumes "(antichain_on P ac)"
               and "(chain_cover_on P cv)"
               and "finite P"
             shows "card ac ≤ card cv"
proof (rule ccontr)
  assume a_contr: "¬ card ac ≤ card cv"
  then have 1: "card cv < card ac" by simp
  have finite_cv: "finite cv" using assms(2,3) chain_cover_on_def
    by (simp add: finite_UnionD)
  have 2: "∀ a ∈ ac. ∃ c ∈ cv. a ∈ c" using assms(1,2) elem_ac_in_c by simp
  then obtain f where f_def: "∀a ∈ ac. ∃ c ∈ cv. a ∈ c ∧ f a = c" by metis
  then have "(f ` ac) ⊆ cv" using f_image assms by blast
  then have 3: "card (f ` ac) ≤ card cv" using f_def finite_cv card_mono by metis
  then have "card (f ` ac) < card ac" using 1 by auto
  then have "¬ inj_on f ac" using pigeonhole by blast
  then obtain a b where p1: "f a = f b" "a ≠ b" "a ∈ ac" "b ∈ ac" 
    using inj_def f_def by (meson inj_on_def)
  then have antichain_elem: "a ∈ ac ∧ b ∈ ac" using f_def by blast
  then have "∃ c ∈ cv. f a = c ∧ f b = c" using f_def 2 1 ‹f ` ac ⊆ cv› p1(1) by auto
  then have chain_elem: "∃ c ∈ cv. a ∈ c ∧ b ∈ c" 
    using f_def p1(1) p1(3) p1(4) by blast
  then have "a ≤ b ∨ b ≤ a" using chain_elem chain_cover_on_def chain_on_def 
    by (metis assms(2) chainD) 
  then have "a = b" 
    using antichain_elem assms(1) antichain_on_def antichain_def by auto
  then show False using p1(2) by blast
qed

section "Existence of a chain cover whose cardinality is the cardinality of the
largest antichain"

subsection "Preliminary lemmas"

text ‹The following lemma shows that the maximal set is an antichain.›

lemma maxset_ac: "antichain ({x . is_maximal_in_set P x})" 
  using antichain_def local.is_maximal_in_set_iff by auto

text ‹ The following lemma shows that the minimal set is an antichain.›

lemma minset_ac: "antichain ({x . is_minimal_in_set P x})" 
  using antichain_def is_minimal_in_set_iff by force


text ‹ The following lemma shows that the null set is both an antichain and a chain cover.›

lemma antichain_null: "antichain {}"
proof-
  show ?thesis using antichain_def by simp
qed

lemma chain_cover_null: assumes "P = {}" shows "chain_cover_on P {}"
proof-
  show ?thesis using chain_cover_on_def
    by (simp add: assms)
qed

text ‹ The following lemma shows that for any arbitrary x that does not belong to the largest antichain of
 a set, there exists an element y in the antichain such that x is related to y or y is
 related to x.›

lemma x_not_in_ac_rel: assumes "largest_antichain_on P ac"
                           and "x ∈ P" 
                           and "x ∉ ac"
                           and "finite P"
                         shows "∃ y ∈ ac. (x ≤ y) ∨ (y ≤ x)"
proof (rule ccontr)
  assume "¬ (∃y∈ac. x ≤ y ∨ y ≤ x)"
  then have 1: "∀ y ∈ ac. (¬(x ≤ y) ∧ ¬(y ≤ x))" by simp
  then have 2: "∀ y ∈ ac. x ≠ y" by auto
  then obtain S where S_def: "S = {x} ∪ ac" by blast
  then have S_fin: "finite S" 
    using assms(4) assms(1) assms(2) largest_antichain_on_def antichain_on_def
    by (meson Un_least bot.extremum insert_subset rev_finite_subset)
  have S_on_P: "antichain_on P S" 
    using S_def largest_antichain_on_def antichain_on_def assms(1,2) 1 2 antichain_def 
    by auto
  then have "ac ⊂ S" using S_def assms(3) by auto
  then have "card ac < card S" using psubset_card_mono S_fin by blast
  then show False using assms(1) largest_antichain_on_def S_on_P by fastforce
qed


text ‹The following lemma shows that for any subset Q of the partially ordered P, if the minimal set of P is a subset
  Q, then it is a subset of the minimal set of Q as well.›

lemma minset_subset_minset:
  assumes "finite P"
      and "Q ⊆ P"
      and "∀ x. (is_minimal_in_set P x ⟶ x ∈ Q)"
    shows "{x . is_minimal_in_set P x} ⊆ {x. is_minimal_in_set Q x}" 
proof
  fix x
  assume asm1: "x ∈ {z. is_minimal_in_set P z}"
  have 1: "x ∈ Q" using asm1 assms(3)  
    by blast 
  have partial_Q: "partial_order_on Q (relation_of (≤) Q)" 
    using assms(1) assms(3) partial_order_on_def
    by (simp add: partial_order_on_relation_ofI)
  have "∀ q ∈ Q. q ∈ P" using assms(2) by blast
  then have "is_minimal_in_set Q x" using is_minimal_in_set_iff 1 partial_Q 
    using asm1 by force
  then show "x ∈ {z. is_minimal_in_set Q z}" by blast
qed

text ‹ The following lemma show that if P is not empty,
  minimal set of P is not empty.›

lemma non_empty_minset: assumes "finite P"
                            and "P ≠ {}"
                          shows "{x . is_minimal_in_set P x} ≠ {}"
  by (simp add: assms ex_minimal_in_set)


text ‹ The following lemma shows that for all elements m of the minimal set, there exists a
  c in the chain cover such that m belongs to c.›

lemma elem_minset_in_chain: assumes "finite P"
                                and "chain_cover_on P cv"
                              shows "is_minimal_in_set P a ⟶ (∃ c ∈ cv. a ∈ c)" 
  using assms(2) chain_cover_on_def is_minimal_in_set_iff by auto


text ‹ The following lemma shows that for all elements m of the maximal set, there exists a chain c
  the chain cover such that m belongs to c.›

lemma elem_maxset_in_chain: assumes "finite P"
                                and "chain_cover_on P cv"
                              shows "is_maximal_in_set P a ⟶ (∃ c ∈ cv. a ∈ c)" 
  using chain_cover_on_def assms is_maximal_in_set_iff by auto


text ‹The following lemma shows that for a given chain cover and antichain on P,
  the cardinality of the chain cover is equal to the cardinality of the antichain
  for all chains c of the chain cover, there exists an element a of the antichain
  that a belongs to c.›

lemma card_ac_cv_eq: assumes "finite P"
                         and "chain_cover_on P cv"
                         and "antichain_on P ac"
                         and "card cv = card ac"
                       shows "∀ c ∈ cv. ∃ a ∈ ac. a ∈ c"
proof (rule ccontr)
  assume "¬ (∀c∈cv. ∃a∈ac. a ∈ c)"
  then obtain c where "c ∈ cv" "∀ a ∈ ac. a ∉ c" by blast
  then have "∀ a ∈ ac. a ∈ ∪ (cv - {c})" (is "∀ a ∈ ac. a ∈ ?cv_c")
    using assms(2,3) unfolding chain_cover_on_def antichain_on_def by blast
  then have 1: "ac ⊆ ?cv_c" by blast
  have 2: "partial_order_on ?cv_c (relation_of (≤) ?cv_c)" 
    using assms(1) assms(3) partial_order_on_def
    by (simp add: partial_order_on_relation_ofI)
  then have ac_on_cv_v: "antichain_on ?cv_c ac" 
    using 1 assms(3) antichain_on_def unfolding antichain_on_def by blast
  have 3: "∀ a ∈ (cv - {c}). a ⊆ ?cv_c" by auto
  have 4: "∀ a ∈ (cv - {c}). Complete_Partial_Order.chain (≤) a" using assms(2) 
    unfolding chain_cover_on_def chain_on_def 
    by (meson DiffD1 Union_upper chain_subset)  
  have 5: "∀ a ∈ (cv - {c}). chain_on a ?cv_c" using chain_on_def 2 3 4 
    by metis
  have "∪ (cv - {c}) = ?cv_c" by simp
  then have cv_on_cv_v: "chain_cover_on ?cv_c (cv - {c})" 
    using 5 chain_cover_on_def by simp
  have "card (cv - {c}) < card cv"
    by (metis ‹c ∈ cv› assms(1) assms(2) card_Diff1_less 
        chain_cover_on_def finite_UnionD)
  then have "card (cv - {c}) < card ac" using assms(4) by simp
  then show False using ac_on_cv_v cv_on_cv_v antichain_card_leq assms part_ord
    by (metis Diff_insert_absorb Diff_subset Set.set_insert Union_mono assms(2,4) 
        card_Diff1_less_iff card_seteq chain_cover_on_def rev_finite_subset)
qed

text ‹ The following lemma shows that if an element m from the minimal set is in a chain, it is less
  or equal to all elements in the chain.›

lemma e_minset_lesseq_e_chain: assumes "chain_on c P" 
                                   and "is_minimal_in_set P m" 
                                   and "m ∈ c"
                                 shows "∀ a ∈ c. m ≤ a"
proof-
  have 1: "c ⊆ P" using assms(1) unfolding chain_on_def  by simp
  then have "is_minimal_in_set c m" using 1 assms(2,3) is_minimal_in_set_iff by auto

  then have 3: "∀ a ∈ c. (a ≤ m) ⟶ a = m" unfolding is_minimal_in_set_iff by auto
  have "∀ a ∈ c. ∀ b ∈ c. (a ≤ b) ∨ (b ≤ a)" using assms(1) 
    unfolding chain_on_def chain_def by blast
  then show ?thesis using 3 assms(3) by blast
qed

text ‹The following lemma shows that if an element m from the maximal set is in a chain, it is greater
  or equal to all elements in the chain.›

lemma e_chain_lesseq_e_maxset: assumes "chain_on c P" 
                                   and "is_maximal_in_set P m" 
                                   and "m ∈ c"
                                 shows "∀ a ∈ c. a ≤ m"
  using assms chainE chain_on_def is_maximal_in_set_iff local.less_le_not_le subsetD 
  by metis 

text ‹The following lemma shows that for any two elements of an antichain, if they both belong to the same chain in
  chain cover, they must be the same element.›

lemma ac_to_c : assumes "finite P"
                    and "chain_cover_on P cv"
                    and "antichain_on P ac"
                  shows "∀ a ∈ ac. ∀ b ∈ ac. ∃ c ∈ cv. a ∈ c ∧ b ∈ c ⟶ a = b"
proof-
  show ?thesis 
    using assms chain_cover_on_def antichain_on_def
    unfolding chain_cover_on_def chain_on_def chain_def antichain_on_def antichain_def 
    by (meson assms(2,3) elem_ac_in_c subsetD)
qed

text ‹The following lemma shows that for two finite sets, if their cardinalities are equal, then their
  would remain equal after removing a single element from both sets.›

lemma card_Diff1_eq: assumes "finite A"
                         and "finite B"
                         and "card A = card B"
                       shows "∀ a ∈ A. ∀ b ∈ B. card (A - {a}) = card (B - {b})"
proof-
  show ?thesis using assms(3) by auto
qed

text ‹The following lemma shows that for two finite sets A and B of equal cardinality, removing two unique elements
  A and one element from B will ensure the cardinality of A is less than B.›

lemma card_Diff2_1_less: assumes "finite A"
                             and "finite B"
                             and "card A = card B"
                             and "a ∈ A"
                             and "b ∈ A"
                             and "a ≠ b"
                           shows "∀ x ∈ B. card ((A - {a}) - {b}) < card (B - {x})"
proof-
  show ?thesis
    by (metis DiffI assms card_Diff1_eq card_Diff1_less_iff finite_Diff singletonD)
qed

text ‹The following lemma shows that for all elements of a partially ordered set, there exists an element in the
  set that will be less than or equal to it.›

lemma min_elem_for_P: assumes "finite P"
                        shows "∀ p ∈ P. ∃ m. is_minimal_in_set P m ∧ m ≤ p" 
proof
  fix p
  assume asm:"p ∈ P"
  obtain m where m: "m ∈ P"  "m ≤ p" "∀a ∈ P. a ≤ m ⟶ a = m"
    using finite_has_minimal2[OF assms(1) asm] by metis 
  hence "is_minimal_in_set P m" unfolding  is_minimal_in_set_iff 
    using part_ord by force
  then show "∃m. is_minimal_in_set P m ∧ m ≤ p" using m 
    by blast
qed

text ‹ The following lemma shows that for all elements of a partially ordered set, there exists an element
  the maximal set that will be greater than or equal to it.›

lemma max_elem_for_P: assumes "finite P"
  shows "∀ p ∈ P. ∃ m. is_maximal_in_set P m ∧ p ≤ m" 
  using assms finite_has_maximal2
  by (metis dual_order.strict_implies_order  is_maximal_in_set_iff)

text ‹ The following lemma shows that if the minimal set is not considered as the largest antichain on a set,
  there exists an element a in the minimal set such that a does not belong to the
 largest antichain.›

lemma min_e_nIn_lac: assumes "largest_antichain_on P ac"
                         and "{x. is_minimal_in_set P x} ≠ ac"
                         and "finite P"
                       shows "∃m. (is_minimal_in_set P m) ∧ (m ∉ ac)"
                          (is "∃m. (?ms m) ∧ (m ∉ ac)")
proof (rule ccontr)
  assume asm:"¬ (∃ m. (?ms m) ∧ (m ∉ ac))"
  then have "∀ m. ¬(?ms m) ∨ m ∈ ac" by blast
  then have 1: "{m . ?ms m} ⊆ ac" by blast
  then show False
  proof cases
    assume "{m . ?ms m} = ac"
    then show ?thesis using assms(2) by blast
  next
    assume "¬ ({m . ?ms m} = ac)"
    then have 1:"{m . ?ms m} ⊂ ac" using 1 by simp
    then obtain y where y_def: "y ∈ ac" "?ms y" using asm assms(1,3)
      by (metis chain_cover_null elem_ac_in_c empty_subsetI ex_in_conv 
                largest_antichain_on_def local.ex_minimal_in_set psubsetE)
    then have y_in_P: "y ∈ P"
      using y_def(1) assms(1) largest_antichain_on_def antichain_on_def by blast
    then have 2: "∀ x. (?ms x ⟶ x ≠ y)" using y_def(2) 1 assms(1,3)
      using asm min_elem_for_P  DiffE mem_Collect_eq psubset_imp_ex_mem subset_iff
      unfolding largest_antichain_on_def antichain_def antichain_on_def
      by (smt (verit)) 
    have partial_P: "partial_order_on P (relation_of (≤) P)"
      using assms(1) largest_antichain_on_def antichain_on_def by simp
    then have "∀ x. ?ms x ⟶ ¬ (y ≤ x)" using 2 unfolding  is_minimal_in_set_iff
      using ‹y ∈ P›
      using "2" y_def(2) by blast
    then show False using y_def(2) by blast
  qed
qed

text ‹ The following lemma shows that if the maximal set is not considered as the largest antichain on a set,
  there exists an element a in the maximal set such that a does not belong to the
  antichain.›

lemma max_e_nIn_lac: assumes "largest_antichain_on P ac"
                         and "{x . is_maximal_in_set P x} ≠ ac"
                         and "finite P"
                       shows "∃ m . is_maximal_in_set P m ∧ m ∉ ac"
                         (is "∃ m. ?ms m ∧ m ∉ ac")
proof (rule ccontr)
  assume asm:"¬ (∃ m. ?ms m ∧ m ∉ ac)"
  then have "∀ m . ¬ ?ms m ∨ m ∈ ac" by blast
  then have 1: "{x . ?ms x} ⊆ ac" by blast
  then show False
  proof cases
    assume asm: "{x . ?ms x} = ac"
    then show ?thesis using assms(2) by blast
  next
    assume "¬ ({x . ?ms x} = ac)"
    then have "{x . ?ms x} ⊂ ac" using 1 by simp
    then obtain y where y_def: "y ∈ ac" "¬ (?ms y)" using assms asm
      by blast
    then have y_in_P: "y ∈ P"
      using y_def(1) assms(1) largest_antichain_on_def antichain_on_def by blast
    then have 2: "∀ x . ?ms x ⟶ x ≠ y" using y_def(2) by auto
    have partial_P: "partial_order_on P (relation_of (≤) P)"
      using assms(1) largest_antichain_on_def antichain_on_def by simp
    then have "∀ x . ?ms x ⟶ ¬ (x ≤ y)" using 2 unfolding  is_maximal_in_set_iff
      using ‹y ∈ P›
      using local.dual_order.order_iff_strict by auto
    then have 3: "∀ x . ?ms x ⟶ (x > y) ∨ ¬ (x ≤ y)" by blast
    then show False
    proof cases
      assume asm1: "∃ x. ?ms x ∧ (x > y)"
      have "∀ x ∈ ac. (x ≤ y) ∨ (y ≤ x) ⟶ x = y" using assms(1) y_def(1)
        unfolding largest_antichain_on_def antichain_on_def antichain_def by simp
      then have "∀ x . ?ms x ⟶ (x > y) ⟶ x = y" using 1 by auto
      then have "∃ x. ?ms x ∧ y = x" using asm1 by auto
      then show ?thesis using 2 by blast
    next
      assume "¬ (∃ x. ?ms x ∧ (x > y))"
      then have "∀ x. ?ms x ⟶ ¬ (x ≤ y)" using 3 by simp
      have a: "∃ z . ?ms z ∧ y ≤ z" 
        using max_elem_for_P[OF assms(3)] y_in_P  partial_P 
        by fastforce
        
      have "∀ a. ?ms a ⟶ (a ≤ y) ∨ (y ≤ a) ⟶ a = y" using assms(1) y_def(1) 1
        unfolding largest_antichain_on_def antichain_on_def antichain_def by blast
      then have "∃ z .?ms z ∧ z = y" using a by blast
      then show ?thesis using 2 by blast
    qed
  qed
qed

subsection "Statement and Proof"

text ‹ Proves theorem for the empty set.›

lemma largest_antichain_card_eq_empty: 
  assumes "largest_antichain_on P lac"
      and "P = {}"
    shows "∃ cv. (chain_cover_on P cv) ∧ (card cv = card lac)"
proof-
  have "lac = {}" using assms(1) assms(2) 
    unfolding largest_antichain_on_def antichain_on_def by simp
  then show ?thesis using assms(2) chain_cover_null by auto
qed


text ‹ Proves theorem for the non-empty set.›

lemma largest_antichard_card_eq: 
           assumes asm1: "largest_antichain_on P lac"
               and asm2: "finite P"
               and asm3: "P ≠ {}"
             shows "∃ cv. (chain_cover_on P cv) ∧ (card cv = card lac)"
  using assms
―‹Proof by induction on the cardinality of P›
proof (induction "card P" arbitrary: P lac rule: less_induct)
  case less
  let ?max = "{x . is_maximal_in_set P x}"
  let ?min = "{x . is_minimal_in_set P x}"
  have partial_P: "partial_order_on P (relation_of (≤) P)" 
    using assms partial_order_on_def antichain_on_def largest_antichain_on_def 
          less.prems(1) by presburger
  show ?case ―‹the largest antichain is not the maximal set or the minimal set›
  proof (cases "∃ ac. (antichain_on P ac ∧ ac ≠ ?min ∧ ac ≠ ?max) ∧ card ac = card lac")
    case True
    obtain ac where ac:"antichain_on P ac" "ac ≠ ?min" "ac ≠ ?max" "card ac = card lac"
      using True by force
    then have "largest_antichain_on P ac" using asm1 largest_antichain_on_def
        using less.prems(1) by presburger
    then have lac_in_P: "lac ⊆ P" 
      using asm1 antichain_on_def largest_antichain_on_def less.prems(1) by presburger
    then have ac_in_P: "ac ⊆ P"
      using ac(1) antichain_on_def by blast
    define p_plus where "p_plus = {x. x ∈ P ∧ (∃ y ∈ ac. y ≤ x)} "  
      ―‹set of all elements greater than or equal to any given element in the largest
 antichain›
    define p_minus where "p_minus = {x. x ∈ P ∧ (∃ y ∈ ac. x ≤ y)}"
      ―‹set of all elements less than or equal to any given element
 in the largest antichain›
    have 1: "ac ⊆ p_plus" 
      ―‹Shows that the largest antichain is a subset of p plus›
      unfolding p_plus_def 
    proof
      fix x
      assume a1: "x ∈ ac"
      then have a2: "x ∈ P"
        using asm1 largest_antichain_on_def antichain_on_def less.prems(1) ac by blast
      then have "x ≤ x" using antichain_def by auto
      then show "x ∈ {x ∈ P. ∃ y ∈ ac. y ≤ x}" using a1 a2 by auto
    qed
    have 2: "ac ⊆ p_minus" 
      ―‹Shows that the largest antichain is a subset of p min›
      unfolding p_minus_def 
    proof
      fix x
      assume a1: "x ∈ ac"
      then have a2: "x ∈ P" 
        using asm1 largest_antichain_on_def antichain_on_def less.prems(1) ac by blast
      then have "x ≤ x" using antichain_def by auto
      then show "x ∈ {x ∈ P. ∃ y ∈ ac. x ≤ y}" using a1 a2 by auto
    qed
    have lac_subset: "ac ⊆ (p_plus ∩ p_minus)" using 1 2 by simp
    have subset_lac: "(p_plus ∩ p_minus) ⊆ ac"
    proof
      fix x
      assume "x ∈ (p_plus ∩ p_minus)"
      then obtain a b where antichain_elems: "a ∈ ac" "b ∈ ac" "a ≤ x" "x ≤ b" 
        using p_plus_def p_minus_def by auto
      then have "a ≤ b" by simp
      then have "a = b" 
        using antichain_elems(1) antichain_elems(2) less.prems
          asm1 largest_antichain_on_def antichain_on_def antichain_def ac by metis
      then have "(a ≤ x) ∧ (x ≤ a)" 
        using antichain_elems(3) antichain_elems(4) by blast
      then have "x = a" by fastforce
      then show "x ∈ ac" using antichain_elems(1) by simp
    qed
    then have lac_pset_eq: "ac = (p_plus ∩ p_minus)" using lac_subset by simp
    have P_PP_PM: "(p_plus ∪ p_minus) = P"
    proof
      show "(p_plus ∪ p_minus) ⊆ P"
      proof
        fix x
        assume "x ∈ (p_plus ∪ p_minus)"
        then have "x ∈ p_plus ∨ x ∈ p_minus" by simp
        then have "x ∈ P" using p_plus_def p_minus_def by auto
        then show "x ∈ P" .
      qed
    next
      show "P ⊆ (p_plus ∪ p_minus)"
      proof
        fix x
        assume x_in: "x ∈ P"
        then have "x ∈ ac ∨ x ∉ ac" by simp
        then have "x ∈ (p_plus ∪ p_minus)"
        proof (cases "x ∈ ac")
          case True
          then show ?thesis using lac_subset by blast
        next
          case False
          then obtain y where "y ∈ ac" "(x ≤ y) ∨ (y ≤ x)" 
            using asm1 False x_in  asm2
             less.prems(1) less.prems(2) 
             ‹largest_antichain_on P ac› x_in x_not_in_ac_rel by blast
          then have "(x ∈ p_plus) ∨ (x ∈ p_minus)" 
            unfolding p_plus_def p_minus_def using x_in by auto
          then show ?thesis by simp
        qed
        then show "x ∈ p_plus ∪ p_minus" by simp
      qed
    qed
    obtain a where a_def: "a ∈ ?min" "a ∉ ac" 
      using asm1 ac True asm3 less.prems(1) less.prems(2) min_e_nIn_lac
      by (metis ‹largest_antichain_on P ac› mem_Collect_eq)
    then have "∀ x ∈ ac. ¬ (x ≤ a)" 
      unfolding is_minimal_in_set_iff using partial_P lac_in_P 
      using ac(1) antichain_on_def 
      using local.nless_le by auto
    then have a_not_in_PP: "a ∉ p_plus" using p_plus_def by simp
    have "a ∈ P" using a_def 
      by (simp add: local.is_minimal_in_set_iff)
    then have ppl: "card p_plus < card P" using P_PP_PM a_not_in_PP
      by (metis Un_upper1 card_mono card_subset_eq less.prems(2) 
          order_le_imp_less_or_eq)
    have p_plus_subset: "p_plus ⊆ P" using p_plus_def by simp
    have antichain_lac: "antichain ac" 
      using assms(1) less.prems ac 
      unfolding largest_antichain_on_def antichain_on_def by simp
    have finite_PP: "finite p_plus" using asm3  p_plus_subset finite_def
      using less.prems(2) rev_finite_subset by blast
    have finite_lac: "finite ac" using ac_in_P asm3 finite_def
      using finite_subset less.prems(2) ac   by auto
    have partial_PP: "partial_order_on p_plus (relation_of (≤) p_plus)" 
      using partial_P p_plus_subset partial_order_on_def
      by (smt (verit, best) local.antisym_conv local.le_less local.order_trans 
          partial_order_on_relation_ofI)
    then have lac_on_PP: "antichain_on p_plus ac" 
      using antichain_on_def 1 antichain_lac by simp
    have card_ac_on_P: "∀ ac. antichain_on P ac ⟶ card ac ≤ card ac"
      using asm1 largest_antichain_on_def less.prems(1) by auto
    then have "∀ ac. antichain_on p_plus ac ⟶ card ac ≤ card ac"
      using p_plus_subset antichain_on_def largest_antichain_on_def
      by (meson partial_P preorder_class.order_trans)
    then have "largest_antichain_on p_plus ac" 
      using lac_on_PP unfolding largest_antichain_on_def 
      by (meson ‹largest_antichain_on P ac› antichain_on_def 
          largest_antichain_on_def p_plus_subset preorder_class.order_trans)
    then have cv_PP: "∃cv. chain_cover_on p_plus cv ∧ card cv = card ac" 
      using less ppl by (metis "1" card.empty chain_cover_null finite_PP subset_empty)
    then obtain cvPP where cvPP_def: "chain_cover_on p_plus cvPP" 
            "card cvPP = card ac"
     using ac(4) by auto
    obtain b where b_def: "b ∈ ?max" "b ∉ ac"
      using asm1 True asm3 less.prems(1) less.prems(2) max_e_nIn_lac 
      using ‹largest_antichain_on P ac› ac(3) by blast 
    then have "∀ x ∈ ac. ¬ (b ≤ x)" 
      unfolding  is_maximal_in_set_iff using partial_P ac_in_P
      nless_le by auto 
    then have b_not_in_PM: "b ∉ p_minus" using p_minus_def by simp
    have "b ∈ P" using b_def is_maximal_in_set_iff  by blast
    then have pml: "card p_minus < card P" using  b_not_in_PM
      by (metis P_PP_PM Un_upper2 card_mono card_subset_eq less.prems(2) nat_less_le)
    have p_min_subset: "p_minus ⊆ P" using p_minus_def by simp
    have finite_PM: "finite p_minus" using asm3 p_min_subset finite_def
      using less.prems(2) rev_finite_subset by blast
    have partial_PM: "partial_order_on p_minus (relation_of (≤) p_minus)"
      by (simp add: partial_order_on_relation_ofI)
    then have lac_on_PM: "antichain_on p_minus ac" 
      using 2 antichain_lac antichain_on_def by simp
    then have "∀ ac. antichain_on p_minus ac ⟶ card ac ≤ card ac"
      using card_ac_on_P P_PP_PM antichain_on_def largest_antichain_on_def
      by (metis partial_P sup.coboundedI2)
    then have "largest_antichain_on p_minus ac" 
      using lac_on_PM ‹largest_antichain_on P ac› antichain_on_def
            largest_antichain_on_def p_min_subset preorder_class.order_trans  
      by meson
    then have cv_PM: "∃cv. chain_cover_on p_minus cv ∧ card cv = card ac" 
      using less pml P_PP_PM ‹a ∈ P› a_not_in_PP finite_PM 
      by blast
    then obtain cvPM where cvPM_def: 
                 "chain_cover_on p_minus cvPM" 
                 "card cvPM = card ac" 
      by auto 
    have lac_minPP: "ac = {x . is_minimal_in_set p_plus x}" (is "ac = ?msPP")
    proof
      show "ac ⊆ {x . is_minimal_in_set p_plus x}"
      proof
        fix x
        assume asm1: "x ∈ ac"
        then have x_in_PP: "x ∈ p_plus" using 1 by auto
        obtain y where y_def: "y ∈ p_plus" "y ≤ x"
          using 1 asm1 by blast
        then obtain a where a_def: "a ∈ ac" "a ≤ y" using p_plus_def by auto
        then have 0: "a ∈ p_plus" using 1 by auto
        then have I: "a ≤ x" using a_def y_def(2) by simp
        then have II: "a = x" using asm1 a_def(1) antichain_lac unfolding antichain_def by simp
        then have III: "y = x" using y_def(2) a_def(2) by simp
        have "∀ p ∈ p_plus. (p ≤ x) ⟶ p = x"
        proof
          fix p
          assume asmP: "p ∈ p_plus"
          show "p ≤ x ⟶ p = x"
          proof
            assume "p ≤ x"
            then show "p = x" 
              using asmP p_plus_def II a_def(1) antichain_def antichain_lac 
                    local.dual_order.antisym local.order.trans mem_Collect_eq
              by (smt (verit))
          qed
        qed
        then have "is_minimal_in_set p_plus x" using is_minimal_in_set_iff 
          using partial_PP 
          using x_in_PP by auto
        then show "x ∈ {x . is_minimal_in_set p_plus x} " 
          using x_in_PP  
          using ‹∀p∈p_plus. p ≤ x ⟶ p = x› local.is_minimal_in_set_iff by force
      qed
    next
      show "{x . is_minimal_in_set p_plus x} ⊆ ac"
      proof
        fix x
        assume asm2: "x ∈ {x . is_minimal_in_set p_plus x}"
        then have I: "∀ a ∈ p_plus. (a ≤ x) ⟶ a = x" 
          using is_minimal_in_set_iff
          by (metis dual_order.not_eq_order_implies_strict  mem_Collect_eq)
        have "x ∈ p_plus" using asm2 
          by (simp add: local.is_minimal_in_set_iff)
        then obtain y where y_def: "y ∈ ac" "y ≤ x" using p_plus_def by auto
        then have "y ∈ p_plus" using 1 by auto
        then have "y = x" using y_def(2) I by simp
        then show "x ∈ ac" using y_def(1) by simp
      qed
    qed
    then have card_msPP: "card ?msPP = card ac" by simp
    then have cvPP_elem_in_lac: "∀ m ∈ ?msPP. ∃ c ∈ cvPP. m ∈ c" 
      using cvPP_def(1) partial_PP asm3 p_plus_subset 
            elem_minset_in_chain elem_ac_in_c 
         lac_on_PP 
      by (simp add: lac_minPP)
    then have cv_for_msPP: "∀ m ∈ ?msPP. ∃ c ∈ cvPP. (∀ a ∈ c. m ≤ a)" 
      using elem_minset_in_chain partial_PP assms(3)
            cvPP_def(1) e_minset_lesseq_e_chain 
      unfolding  chain_cover_on_def[of "p_plus" cvPP] 
      by fastforce
    have lac_elem_in_cvPP: "∀ c ∈ cvPP. ∃ m ∈ ?msPP. m ∈ c" 
      using cvPP_def card_msPP minset_ac card_ac_cv_eq
      by (metis P_PP_PM finite_Un lac_minPP lac_on_PP less.prems(2))
    then have "∀ c ∈ cvPP. ∃ m ∈ ?msPP. (∀ a ∈ c. m ≤ a)" 
      using e_minset_lesseq_e_chain chain_cover_on_def cvPP_def(1) 
      by (metis mem_Collect_eq)
    then have cvPP_lac_rel: "∀ c ∈ cvPP. ∃ x ∈ ac. (∀ a ∈ c. x ≤ a)"
      using lac_minPP by simp
    have lac_maxPM: "ac = {x . is_maximal_in_set p_minus x}" (is "ac = ?msPM")
    proof
      show "ac ⊆ ?msPM"
      proof
        fix x
        assume asm1: "x ∈ ac"
        then have x_in_PM: "x ∈ p_minus" using 2 by auto
        obtain y where y_def: "y ∈ p_minus" "x ≤ y"
          using 2 asm1 by blast
        then obtain a where a_def: "a ∈ ac" "y ≤ a" using p_minus_def by auto
        then have I: "x ≤ a" using y_def(2) by simp
        then have II: "a = x" 
          using asm1 a_def(1) antichain_lac unfolding antichain_def by simp
        then have III: "y = x" using y_def(2) a_def(2) by simp
        have "∀ p ∈ p_minus. (x ≤ p) ⟶ p = x"
        proof
          fix p
          assume asmP: "p ∈ p_minus"
          show "x ≤ p ⟶ p = x"
          proof
            assume "x ≤ p"
            then show "p = x" 
              using p_minus_def  II a_def(1) antichain_def antichain_lac asmP 
                    dual_order.antisym order.trans mem_Collect_eq
              by (smt (verit))
          qed
        qed
        then have "is_maximal_in_set p_minus x" 
          using partial_PM is_maximal_in_set_iff x_in_PM by force
        then show " x ∈ {x. is_maximal_in_set p_minus x}" 
          using x_in_PM  by auto
      qed
    next
      show "?msPM ⊆ ac"
      proof
        fix x
        assume asm2: "x ∈ {x . is_maximal_in_set p_minus x}"
        then have I: "∀ a ∈ p_minus. (x ≤ a) ⟶ a = x" 
          unfolding  is_maximal_in_set_iff by fastforce
        have "x ∈ p_minus" using asm2 
          by (simp add: local.is_maximal_in_set_iff)
        then obtain y where y_def: "y ∈ ac" "x ≤ y" using p_minus_def by auto
        then have "y ∈ p_minus" using 2 by auto
        then have "y = x" using y_def(2) I by simp
        then show "x ∈ ac" using y_def(1) by simp
      qed
    qed
    then have card_msPM: "card ?msPM = card ac" by simp
    then have cvPM_elem_in_lac: "∀ m ∈ ?msPM. ∃ c ∈ cvPM. m ∈ c" 
      using cvPM_def(1) partial_PM asm3 p_min_subset elem_maxset_in_chain 
            elem_ac_in_c lac_maxPM lac_on_PM 
      by presburger
    then have cv_for_msPM: "∀ m ∈ ?msPM. ∃ c ∈ cvPM. (∀ a ∈ c. a ≤ m)"
      using elem_maxset_in_chain partial_PM assms(3) cvPM_def(1) 
            e_chain_lesseq_e_maxset 
      unfolding chain_cover_on_def[of "p_minus" cvPM] 
      by (metis mem_Collect_eq)
    have lac_elem_in_cvPM: "∀ c ∈ cvPM. ∃ m ∈ ?msPM. m ∈ c" 
      using cvPM_def card_msPM 
        maxset_ac card_ac_cv_eq finite_subset lac_maxPM lac_on_PM less.prems(2) 
        p_min_subset partial_PM
        by metis
      then have "∀ c ∈ cvPM. ∃ m ∈ ?msPM. (∀ a ∈ c. a ≤ m)" 
        using e_chain_lesseq_e_maxset chain_cover_on_def cvPM_def(1) 
        by (metis mem_Collect_eq)
    then have cvPM_lac_rel: "∀ c ∈ cvPM. ∃ x ∈ ac. (∀ a ∈ c. a ≤ x)" 
      using lac_maxPM by simp
    obtain x cp cm where x_cp_cm: "x ∈ ac" "cp ∈ cvPP" "(∀ a ∈ cp. x ≤ a)" 
                                  "cm ∈ cvPM" "(∀ a ∈ cm. a ≤ x)"
      using cv_for_msPP cv_for_msPM lac_minPP lac_maxPM assms(1) 
      unfolding largest_antichain_on_def antichain_on_def antichain_def
      by (metis P_PP_PM Sup_empty Un_empty_right all_not_in_conv chain_cover_on_def 
                cvPM_def(1) cvPP_def(1) cvPP_lac_rel lac_elem_in_cvPM less.prems(3))

    have "∃ f. ∀ cp ∈ cvPP. ∃ x ∈ ac. f cp = x ∧ x ∈ cp"
―‹defining a function that maps chains in the p plus chain cover to the element in
 the largest antichain that belongs to the chain.›
      using lac_elem_in_cvPP lac_minPP by metis
    then obtain f where f_def: "∀ cp ∈ cvPP. ∃ x ∈ ac. f cp = x ∧ x ∈ cp" by blast
    have lac_image_f: "f ` cvPP = ac"
    proof
      show "(f ` cvPP) ⊆ ac"
      proof
        fix y
        assume "y ∈ (f ` cvPP)"
        then obtain x where "f x = y" "x ∈ cvPP" using f_def by blast
        then have "y ∈ x" using f_def by blast
        then show "y ∈ ac" using f_def ‹f x = y› ‹x ∈ cvPP› by blast
      qed
    next
      show "ac ⊆ (f ` cvPP)"
      proof
        fix y
        assume y_in_lac: "y ∈ ac"
        then obtain x where "x ∈ cvPP" "y ∈ x" 
          using cvPP_elem_in_lac lac_minPP by auto
        then have "f x = y" using f_def y_in_lac
          by (metis antichain_def antichain_lac cvPP_lac_rel)
        then show "y ∈ (f ` cvPP)" using ‹x ∈ cvPP› by auto
      qed
    qed
    have "∀ x ∈ cvPP. ∀ y ∈ cvPP. f x = f y ⟶ x = y"
    proof (rule ccontr)
      assume "¬ (∀x∈cvPP. ∀y∈cvPP. f x = f y ⟶ x = y)"
      then have "∃ x ∈ cvPP. ∃ y ∈ cvPP. f x = f y ∧ x ≠ y" by blast
      then obtain z x y where z_x_y: "x ∈ cvPP" "y ∈ cvPP" "x ≠ y" "z = f x" "z = f y" 
        by blast
      then have z_in: "z ∈ ac" using f_def by blast
      then have "∀ a ∈ ac. (a ∈ x ∨ a ∈ y) ⟶ a = z" 
        using ac_to_c partial_P asm3 p_plus_subset cvPP_def(1) 
              lac_on_PP z_x_y(1) z_x_y(2)
        by (metis antichain_def antichain_lac cvPP_lac_rel f_def z_x_y(4) z_x_y(5))
      then have "∀ a ∈ ac. a ≠ z ⟶ a ∉ x ∧ a ∉ y" by blast
      then have "∀ a ∈ (ac - {z}). a ∈ ∪ ((cvPP - {x}) - {y})" 
        using cvPP_def(1) 1 unfolding chain_cover_on_def by blast
      then have a: "(ac - {z}) ⊆ ∪ ((cvPP - {x}) - {y})" (is "?lac_z ⊆ ?cvPP_xy") by blast
      have b: "partial_order_on ?cvPP_xy (relation_of (≤) ?cvPP_xy)"
        using partial_PP cvPP_def(1) partial_order_on_def 
              dual_order.eq_iff dual_order.eq_iff 
              dual_order.trans partial_order_on_relation_ofI 
              dual_order.trans partial_order_on_relation_ofI
        by (smt (verit))
      then have ac_on_cvPP_xy: "antichain_on ?cvPP_xy ?lac_z" 
        using a lac_on_PP antichain_on_def unfolding antichain_on_def
        by (metis DiffD1 antichain_def antichain_lac)
      have c: "∀ a ∈ ((cvPP - {x}) - {y}). a ⊆ ?cvPP_xy" by auto
      have d: "∀ a ∈ ((cvPP - {x}) - {y}). Complete_Partial_Order.chain (≤) a" using cvPP_def(1)
        unfolding chain_cover_on_def chain_on_def 
        using z_x_y(2) by blast 
      have e: "∀ a ∈ ((cvPP - {x}) - {y}). chain_on a ?cvPP_xy" 
        using b c d chain_on_def 
        by (metis Diff_iff Sup_upper chain_cover_on_def cvPP_def(1))  
      have f: "finite ?cvPP_xy" using finite_PP cvPP_def(1) 
        unfolding chain_cover_on_def chain_on_def
        by (metis (no_types, opaque_lifting) Diff_eq_empty_iff Diff_subset 
                 Un_Diff_cancel Union_Un_distrib finite_Un)
      have "∪ ((cvPP - {x}) - {y}) = ?cvPP_xy" by blast
      then have cv_on: "chain_cover_on ?cvPP_xy ((cvPP - {x}) - {y})" 
        using chain_cover_on_def[of  ?cvPP_xy " ((cvPP - {x}) - {y}) "] 
              e chain_on_def by argo
      have "card ((cvPP - {x}) - {y}) < card cvPP" 
        using z_x_y(1) z_x_y(2) finite_PP cvPP_def(1) chain_cover_on_def finite_UnionD
        by (metis card_Diff2_less)
      then have "card ((cvPP - {x}) - {y}) < card (ac - {z})" 
        using cvPP_def(2) finite_PP finite_lac cvPP_def(1) chain_cover_on_def 
              finite_UnionD z_x_y(1) z_x_y(2) z_x_y(3) z_in card_Diff2_1_less 
        by metis
      then show False using antichain_card_leq ac_on_cvPP_xy cv_on f by fastforce
    qed
    then have inj_f: "inj_on f cvPP" using inj_on_def by auto
    then have bij_f: "bij_betw f cvPP ac" using lac_image_f bij_betw_def by blast
    have "∃ g. ∀ cm ∈ cvPM. ∃ x ∈ ac. g cm = x ∧ x ∈ cm"
      using lac_elem_in_cvPM lac_maxPM by metis
    then obtain g where g_def: "∀ cm ∈ cvPM. ∃ x ∈ ac. g cm = x ∧ x ∈ cm" by blast
    have lac_image_g: "g ` cvPM = ac"
    proof
      show "g ` cvPM ⊆ ac"
      proof
        fix y 
        assume "y ∈ g ` cvPM"
        then obtain x where x: "g x = y" "x ∈ cvPM" using g_def by blast
        then have "y ∈ x" using g_def by blast
        then show "y ∈ ac" using g_def x by auto
      qed
    next
      show "ac ⊆ g ` cvPM"
      proof
        fix y
        assume y_in_lac: "y ∈ ac"
        then obtain x where x: "x ∈ cvPM" "y ∈ x" 
          using cvPM_elem_in_lac lac_maxPM by auto
        then have "g x = y" using g_def y_in_lac
          by (metis antichain_def antichain_lac cvPM_lac_rel)
        then show "y ∈ g ` cvPM" using x by blast
      qed
    qed
    have "∀ x ∈ cvPM. ∀ y ∈ cvPM. g x = g y ⟶ x = y"
    proof (rule ccontr)
      assume "¬ (∀x∈cvPM. ∀y∈cvPM. g x = g y ⟶ x = y)"
      then have "∃ x ∈ cvPM. ∃ y ∈ cvPM. g x = g y ∧ x ≠ y" by blast
      then obtain z x y where z_x_y: "x ∈ cvPM"  "y ∈ cvPM" 
                                     "x ≠ y" "z = g x" "z = g y" by blast
      then have z_in: "z ∈ ac" using g_def by blast
      then have "∀ a ∈ ac. (a ∈ x ∨ a ∈ y) ⟶ a = z" 
        using ac_to_c partial_P asm3 z_x_y(1) z_x_y(2)
        by (metis antichain_def antichain_lac cvPM_lac_rel g_def z_x_y(4) z_x_y(5))
      then have "∀ a ∈ ac. a ≠ z ⟶ a ∉ x ∧ a ∉ y" by blast
      then have "∀ a ∈ (ac - {z}). a ∈ ∪ ((cvPM - {x}) - {y})" 
        using cvPM_def(1) 2 unfolding chain_cover_on_def by blast
      then have a: "(ac - {z}) ⊆ ∪ ((cvPM - {x}) - {y})" (is "?lac_z ⊆ ?cvPM_xy") 
        by blast
      have b: "partial_order_on ?cvPM_xy (relation_of (≤) ?cvPM_xy)"
        using partial_PP partial_order_on_def
        by (smt (verit) local.dual_order.eq_iff 
            local.dual_order.trans partial_order_on_relation_ofI)
      then have ac_on_cvPM_xy: "antichain_on ?cvPM_xy ?lac_z" 
        using a antichain_on_def unfolding antichain_on_def
        by (metis DiffD1 antichain_def antichain_lac)
      have c: "∀ a ∈ ((cvPM - {x}) - {y}). a ⊆ ?cvPM_xy" by auto
      have d: "∀ a ∈ ((cvPM - {x}) - {y}). Complete_Partial_Order.chain (≤) a" 
        using cvPM_def(1)
        unfolding chain_cover_on_def chain_on_def 
        by (metis DiffD1) 
      have e: "∀ a ∈ ((cvPM - {x}) - {y}). chain_on a ?cvPM_xy" 
        using b c d chain_on_def 
        by (metis Diff_iff Union_upper chain_cover_on_def cvPM_def(1)) 
      have f: "finite ?cvPM_xy" using finite_PM cvPM_def(1) 
        unfolding chain_cover_on_def chain_on_def
        by (metis (no_types, opaque_lifting) Diff_eq_empty_iff Diff_subset
                  Un_Diff_cancel Union_Un_distrib finite_Un)
      have "∪ ((cvPM - {x}) - {y}) = ?cvPM_xy" by blast
      then have cv_on: "chain_cover_on ?cvPM_xy ((cvPM - {x}) - {y})" 
        using chain_cover_on_def e by simp
      have "card ((cvPM - {x}) - {y}) < card cvPM" 
        using z_x_y(1) z_x_y(2) finite_PM cvPM_def(1) chain_cover_on_def finite_UnionD
        by (metis card_Diff2_less)
      then have "card ((cvPM - {x}) - {y}) < card (ac - {z})" 
        using cvPM_def(2) finite_PM finite_lac cvPM_def(1) chain_cover_on_def 
              finite_UnionD z_x_y(1) z_x_y(2) z_x_y(3) z_in card_Diff2_1_less 
        by metis
      then show False using antichain_card_leq ac_on_cvPM_xy cv_on f by fastforce
    qed
    then have inj_g:  "inj_on g cvPM" using inj_on_def by auto
    then have bij_g: "bij_betw g cvPM ac" using lac_image_g bij_betw_def by blast
    define h where "h = inv_into cvPP f"
    then have bij_h: "bij_betw h ac cvPP" 
      using f_def bij_f bij_betw_inv_into by auto
    define i where "i = inv_into cvPM g"
    then have bij_i: "bij_betw i ac cvPM" 
      using g_def bij_f bij_g bij_betw_inv_into by auto
    obtain j where j_def: "∀ x ∈ ac. j x = (h x) ∪ (i x)" 
      using h_def i_def f_def g_def bij_h bij_i
      by (metis sup_apply)
    have "∀ x ∈ ac. ∀ y ∈ ac. j x = j y ⟶ x = y"
    proof (rule ccontr)
      assume "¬ (∀ x ∈ ac. ∀ y ∈ ac. j x = j y ⟶ x = y)"
      then have "∃ x ∈ ac. ∃ y ∈ ac. j x = j y ∧ x ≠ y" by blast
      then obtain z x y where z_x_y: "x ∈ ac" "y ∈ ac" "z = j x" "z = j y" "x ≠ y" 
        by auto 
      then have z_x: "z = (h x) ∪ (i x)" using j_def by simp
      have "z = (h y) ∪ (i y)" using j_def z_x_y by simp
      then have union_eq: "(h x) ∪ (i x) = (h y) ∪ (i y)" using z_x by simp
      have x_hx: "x ∈ (h x)" using h_def f_def bij_f bij_h
        by (metis bij_betw_apply f_inv_into_f lac_image_f z_x_y(1))
      have x_ix: "x ∈ (i x)" using i_def g_def bij_g bij_i
        by (metis bij_betw_apply f_inv_into_f lac_image_g z_x_y(1))
      have "y ∈ (h y)" using h_def f_def bij_f bij_h
        by (metis bij_betw_apply f_inv_into_f lac_image_f z_x_y(2))
      then have "y ∈ (h x) ∪ (i x)" using union_eq by simp
      then have y_in: "y ∈ (h x) ∨ y ∈ (i x)" by simp
      then show False
      proof (cases "y ∈ (h x)")
        case True
        have "∃ c ∈ cvPP. (h x) = c" using h_def f_def bij_h bij_f
          by (simp add: bij_betw_apply z_x_y(1))
        then obtain c where c_def: "c ∈ cvPP" "(h x) = c" by simp
        then have "x ∈ c ∧ y ∈ c" using x_hx True by simp
        then have "x = y" using z_x_y(1) z_x_y(2) asm1 c_def(1) cvPP_def less.prems ac
          unfolding largest_antichain_on_def antichain_on_def antichain_def 
                    chain_cover_on_def chain_on_def chain_def 
          by (metis)
        then show ?thesis using z_x_y(5) by simp
      next
        case False
        then have y_ix: "y ∈ (i x)" using y_in by simp
        have "∃ c ∈ cvPM. (i x) = c" using i_def g_def bij_i bij_g
          by (simp add: bij_betw_apply z_x_y(1))
        then obtain c where c_def: "c ∈ cvPM" "(i x) = c" by simp
        then have "x ∈ c ∧ y ∈ c" using x_ix y_ix by simp
        then have "x = y" 
          using z_x_y(1) z_x_y(2) asm1 ac c_def(1) cvPM_def less.prems 
          unfolding largest_antichain_on_def antichain_on_def antichain_def 
                    chain_cover_on_def chain_on_def chain_def 
          by (metis)
        then show ?thesis using z_x_y(5) by simp
      qed
    qed
    then have inj_j: "inj_on j ac" using inj_on_def by auto
    obtain cvf where cvf_def: "cvf = {j x | x . x ∈ ac}" by simp
    then have "cvf = j ` ac" by blast
    then have bij_j: "bij_betw j ac cvf" using inj_j bij_betw_def by auto
    then have card_cvf: "card cvf = card ac"
      by (metis bij_betw_same_card)
    have j_h_i: "∀ x ∈ ac. ∃ cp ∈ cvPP. ∃ cm ∈ cvPM. (h x = cp) ∧ (i x = cm)
                        ∧ (j x = (cp ∪ cm))"
      using j_def bij_h bij_i by (meson bij_betwE)
    have "∪ cvf = (p_plus ∪ p_minus)"
    proof
      show "∪ cvf ⊆ (p_plus ∪ p_minus)"
      proof
        fix y
        assume "y ∈ ∪ cvf"
        then obtain z where z_def: "z ∈ cvf" "y ∈ z" by blast
        then obtain cp cm where cp_cm: "cp ∈ cvPP" "cm ∈ cvPM" "z = (cp ∪ cm)" 
          using cvf_def h_def i_def j_h_i by blast
        then have "y ∈ cp ∨ y ∈ cm" using z_def(2) by simp
        then show "y ∈ (p_plus ∪ p_minus)" using cp_cm(1) cp_cm(2) cvPP_def cvPM_def
          unfolding chain_cover_on_def chain_on_def by blast
      qed
    next
      show "(p_plus ∪ p_minus) ⊆ ∪ cvf"
      proof
        fix y
        assume "y ∈ (p_plus ∪ p_minus)"
        then have y_in: "y ∈ p_plus ∨ y ∈ p_minus" by simp
        have "p_plus = ∪ cvPP ∧ p_minus = ∪ cvPM" using cvPP_def cvPM_def
          unfolding chain_cover_on_def by simp
        then have "y ∈ (∪ cvPP) ∨ y ∈ (∪ cvPM)" using y_in by simp
        then have "∃ cp ∈ cvPP. ∃ cm ∈ cvPM. (y ∈ cp) ∨ (y ∈ cm)" 
          using cvPP_def cvPM_def
          by (meson Union_iff x_cp_cm(2) x_cp_cm(4))
        then obtain cp cm where cp_cm: "cp ∈ cvPP" "cm ∈ cvPM" "y ∈ (cp ∪ cm)" by blast
        have 1: "∃ cm ∈ cvPM. ∃ x ∈ ac. (x ∈ cp) ∧ (x ∈ cm)"
          using cp_cm(1) f_def cvPM_elem_in_lac lac_maxPM by metis
        have 2: "∃ cp ∈ cvPP. ∃ x ∈ ac. (x ∈ cp) ∧ (x ∈ cm)"
          using cp_cm(2) g_def cvPP_elem_in_lac lac_minPP 
          by meson
        then show "y ∈ ∪ cvf"
        proof (cases "y ∈ cp")
          case True
          obtain x cmc where x_cm: "x ∈ ac" "x ∈ cp" "x ∈ cmc" "cmc ∈ cvPM" 
            using 1 by blast
          have "f cp = x" using cp_cm(1) x_cm(1) f_def
            by (metis antichain_def antichain_lac cvPP_lac_rel x_cm(2))
          then have h_x: "h x = cp" using h_def cp_cm(1) inj_f by auto
          have "g cmc = x" using x_cm(4) x_cm(1) g_def
            by (metis antichain_def antichain_lac cvPM_lac_rel x_cm(3))
          then have i_x: "i x = cmc" using i_def
            by (meson bij_betw_inv_into_left bij_g x_cm(4))
          then have "j x = h x ∪ i x" using j_def x_cm(1) by simp
          then have "(h x ∪ i x) ∈ cvf" using cvf_def x_cm(1) by auto
          then have "(cp ∪ cmc) ∈ cvf" using h_x i_x by simp
          then show ?thesis using True by blast
        next
          case False
          then have y_in: "y ∈ cm" using cp_cm(3) by simp
          obtain x cpc where x_cp: "x ∈ ac" "x ∈ cm" "x ∈ cpc" "cpc ∈ cvPP" 
            using 2 by blast
          have "g cm = x" using cp_cm(2) x_cp(1) x_cp(2) g_def
            by (metis antichain_def antichain_lac cvPM_lac_rel)
          then have x_i: "i x = cm" using i_def x_cp(1)
            by (meson bij_betw_inv_into_left bij_g cp_cm(2))
          have "f cpc = x" using x_cp(4) x_cp(1) x_cp(3) f_def
            by (metis antichain_def antichain_lac cvPP_lac_rel)
          then have x_h: "h x = cpc" using h_def x_cp(1) inj_f x_cp(4) by force
          then have "j x = h x ∪ i x" using j_def x_cp(1) by simp
          then have "(h x ∪ i x) ∈ cvf" using cvf_def x_cp(1) by auto
          then have "(cpc ∪ cm) ∈ cvf" using x_h x_i by simp
          then show ?thesis using y_in by blast
        qed
      qed
    qed
    then have cvf_P: "∪ cvf = P" using P_PP_PM by simp
    have "∀ x ∈ cvf. chain_on x P"
    proof
      fix x
      assume asm1: "x ∈ cvf"
      then obtain a where a_def: "a ∈ ac" "j a = x" using cvf_def by blast
      then obtain cp cm where cp_cm: "cp ∈ cvPP" "cm ∈ cvPM" "h a = cp ∧ i a = cm" 
        using h_def i_def bij_h bij_i j_h_i by blast
      then have x_union: "x = (cp ∪ cm)" using j_def a_def by simp
      then have a_in: "a ∈ cp ∧ a ∈ cm" using cp_cm h_def f_def i_def g_def
        by (metis ‹a ∈ ac› bij_betw_inv_into_right bij_f bij_g)
      then have a_rel_cp: "∀ b ∈ cp. (a ≤ b)" 
        using a_def(1) cp_cm(1) lac_minPP e_minset_lesseq_e_chain 
        by (metis antichain_def antichain_lac cvPP_lac_rel)
      have a_rel_cm: "∀ b ∈ cm. (b ≤ a)"
        using a_def(1) cp_cm(2) lac_maxPM e_chain_lesseq_e_maxset a_in
        by (metis antichain_def antichain_lac cvPM_lac_rel)
      then have "∀ a ∈ cp. ∀ b ∈ cm. (b ≤ a)" using a_rel_cp by fastforce
      then have "∀ x ∈ (cp ∪ cm). ∀ y ∈ (cp ∪ cm). (x ≤ y) ∨ (y ≤ x)"
        using cp_cm(1) cp_cm(2) cvPP_def cvPM_def
        unfolding chain_cover_on_def chain_on_def chain_def 
        by (metis Un_iff) 
      then have "Complete_Partial_Order.chain (≤) (cp ∪ cm)" using chain_def by auto
      then have chain_x: "Complete_Partial_Order.chain (≤) x" using x_union by simp
      have "x ⊆ P" using cvf_P asm1 by blast
      then show "chain_on x P" using chain_x partial_P chain_on_def  by simp
    qed
    then have "chain_cover_on P cvf" using cvf_P  chain_cover_on_def[of P cvf]  by simp
    then show caseTrue: ?thesis using card_cvf ac by auto
  next ―‹the largest antichain is equal to the maximal set or the minimal set›
    case False
    assume "¬ (∃ ac. (antichain_on P ac ∧ ac ≠ ?min ∧ ac ≠ ?max) ∧ card ac = card lac)" 
    then have "¬ ((lac ≠ ?max) ∧ (lac ≠ ?min))" 
      using less(2) unfolding largest_antichain_on_def
      by blast
    then have max_min_asm: "(lac = ?max) ∨ (lac = ?min)" by simp
    then have caseAsm: 
      "∀ ac. (antichain_on P ac ∧ ac ≠ ?min ∧ ac ≠ ?max) ⟶ card ac ≤ card lac"
      using asm1 largest_antichain_on_def less.prems(1) by presburger
    then have case2: "∀ ac. (antichain_on P ac ∧ ac ≠ ?min ∧ ac ≠ ?max) ⟶ card ac < card lac" 
        using False by force
    obtain x where x: "x ∈ ?min" 
      using is_minimal_in_set_iff non_empty_minset partial_P assms(2,3)
      by (metis empty_Collect_eq less.prems(2) less.prems(3) mem_Collect_eq)
    then have "x ∈ P" using is_minimal_in_set_iff by simp
    then obtain y where y: "y ∈ ?max" "x ≤ y" using partial_P max_elem_for_P
        using less.prems(2) by blast
    define PD where PD_def: "PD = P - {x,y}"
    then have finite_PD: "finite PD" using asm3 finite_def
        by (simp add: less.prems(2))
    then have partial_PD: "partial_order_on PD (relation_of (≤) PD)" 
        using partial_P partial_order_on_def
        by (simp add: partial_order_on_relation_ofI)
    then have max_min_nPD: "¬ (?max ⊆ PD) ∧ ¬ (?min ⊆ PD)" 
        using PD_def x y(1) by blast
    have a1: "∀ a ∈ P. (a ≠ x) ∧ (a ≠ y) ⟶ a ∈ PD" 
        using PD_def by blast
      then have "∀ a ∈ ?max. (a ≠ x) ∧ (a ≠ y) ⟶ a ∈ PD" 
        using  is_maximal_in_set_iff  by blast
    then have "(?max - {x, y}) ⊆ PD" (is "?maxPD ⊆ PD") by blast
    have card_maxPD: "card (?max - {x,y}) = (card ?max - 1)" using x y
      proof cases
        assume "x = y"
        then show ?thesis using y(1) by force
      next
        assume "¬ (x = y)"
        then have "x < y" using y(2) by simp
        then have "¬ (is_maximal_in_set P x)" using  x y(1) 
          using ‹x ≠ y› is_maximal_in_set_iff by fastforce
        then have "x ∉ ?max"  by simp
        then show ?thesis using y(1) by auto
      qed
      have "∀ a ∈ ?min. (a ≠ x) ∧ (a ≠ y) ⟶ a ∈ PD" 
        using is_minimal_in_set_iff  a1 
        by (simp add: a1 local.is_minimal_in_set_iff)
    then have "(?min - {x, y}) ⊆ PD" (is "?minPD ⊆ PD") by blast
    have card_minPD: "card (?min - {x,y}) = (card ?min - 1)" using x y
    proof cases
      assume "x = y"
      then show ?thesis using x by auto
    next
      assume "¬ (x = y)"
      then have "x < y" using y(2) by simp
      then have "¬ (is_minimal_in_set P y)" using is_minimal_in_set_iff x y(1) 
          by force
      then have "y ∉ ?min"  by simp
      then show ?thesis using x
          by (metis Diff_insert Diff_insert0 card_Diff_singleton_if)
    qed
    then show ?thesis
    proof cases
      assume asm:"lac = ?max" ―‹ case where the largest antichain is the maximal set›
      then have card_maxPD: "card ?maxPD = (card lac - 1)" using card_maxPD by auto
      then have ac_less: "∀ ac. (antichain_on P ac ∧ ac ≠ ?max ∧ ac ≠ ?min)
                         ⟶ card ac ≤ (card lac - 1)" 
          using case2 by auto
      have PD_sub: "PD ⊂ P" using PD_def
          by (simp add: ‹x ∈ P› subset_Diff_insert subset_not_subset_eq)
      then have PD_less: "card PD < card P" using asm3 card_def
          by (simp add: less.prems(2) psubset_card_mono)
        have maxPD_sub: "?maxPD ⊆ PD" 
          using PD_def  ‹{x. is_maximal_in_set P x} - {x, y} ⊆ PD› by blast  
      have "?maxPD ⊆ ?max" by blast
      then have "antichain ?maxPD" using maxset_ac unfolding antichain_def by blast
      then have ac_maxPD:  "antichain_on PD ?maxPD" 
          using maxPD_sub antichain_on_def partial_PD by simp
      have acPD_nMax_nMin: "∀ ac . (antichain_on PD ac) ⟶ (ac ≠ ?max ∧ ac ≠ ?min)" 
          using max_min_nPD antichain_on_def 
          by auto
      have "∀ ac. (antichain_on PD ac) ⟶ (antichain_on P ac)"
          using antichain_on_def antichain_def
          by (meson PD_sub partial_P psubset_imp_subset subset_trans)
      then have "∀ ac. (antichain_on PD ac) ⟶ card ac ≤ (card lac - 1)" 
          using ac_less PD_sub max_min_nPD acPD_nMax_nMin by blast
      then have maxPD_lac: "largest_antichain_on PD ?maxPD"
          using largest_antichain_on_def ac_maxPD card_maxPD by simp
      then have "∃ cv. chain_cover_on PD cv ∧ card cv = card ?maxPD"
      proof cases
        assume "PD ≠ {}"
        then show ?thesis using less PD_less maxPD_lac finite_PD by blast
      next
        assume "¬ (PD ≠ {})"
        then have PD_empty: "PD = {}" by simp
        then have "?maxPD = {}" using maxPD_sub by auto
        then show ?thesis 
          using maxPD_lac PD_empty largest_antichain_card_eq_empty by simp
      qed
      then obtain cvPD where cvPD_def: "chain_cover_on PD cvPD" 
                                       "card cvPD = card ?maxPD" by blast
      then have "∪ cvPD = PD" unfolding chain_cover_on_def by simp
      then have union_cvPD: "∪ (cvPD ∪ {{x,y}}) = P" using PD_def
          using ‹x ∈ P›  y(1) is_maximal_in_set_iff  by force 
      have chains_cvPD: "∀ x ∈ cvPD. chain_on x P" 
        using chain_on_def cvPD_def(1) PD_sub unfolding chain_cover_on_def
        by (meson subset_not_subset_eq subset_trans)
      have "{x,y} ⊆ P" using x y  
        using union_cvPD by blast
      then have xy_chain_on: "chain_on {x,y} P" 
        using partial_P y(2) chain_on_def chain_def 
        by fast
      define cvf where cvf_def: "cvf = cvPD ∪ {{x,y}}"
      have cv_cvf: "chain_cover_on P cvf" 
        using chains_cvPD union_cvPD xy_chain_on unfolding chain_cover_on_def cvf_def
         by simp
      have "¬ ({x,y} ⊆ PD)" using PD_def by simp
      then have "{x,y} ∉ cvPD" using cvPD_def(1) 
          unfolding chain_cover_on_def chain_on_def by auto
      then have "card (cvPD ∪ {{x,y}}) = (card ?maxPD) + 1" using cvPD_def(2) card_def
          by (simp add: ‹∪ cvPD = PD› finite_PD finite_UnionD)
      then have "card cvf = (card ?maxPD) + 1" using cvf_def by auto
      then have "card cvf = card lac" using card_maxPD asm
        by (metis Diff_infinite_finite Suc_eq_plus1  ‹{x, y} ⊆ P› card_Diff_singleton 
            card_Suc_Diff1 finite_PD finite_subset less.prems(2) maxPD_sub y(1))
      then show ?thesis using cv_cvf by blast
    next
      assume "¬ (lac = ?max)" 
      ―‹ complementary case where the largest antichain is the minimal set›
      then have "lac = ?min" using max_min_asm by simp
      then have card_minPD: "card ?minPD = (card lac - 1)" using card_minPD by simp
      then have ac_less: "∀ ac. (antichain_on P ac ∧ ac ≠ ?max ∧ ac ≠ ?min)
                         ⟶ card ac ≤ (card lac - 1)" 
          using case2 by auto
      have PD_sub: "PD ⊆ P" using PD_def by simp
      then have PD_less: "card PD < card P" using asm3
        using less.prems(2) max_min_nPD is_minimal_in_set_iff psubset_card_mono
        by (metis DiffE PD_def ‹x ∈ P› insertCI psubsetI) 
      have minPD_sub: "?minPD ⊆ PD" using PD_def unfolding  
        is_minimal_in_set_iff by blast
      have "?minPD ⊆ ?min" by blast
      then have "antichain ?minPD" using minset_ac is_minimal_in_set_iff
        unfolding antichain_def 
        by (metis DiffD1) 
      then have ac_minPD:  "antichain_on PD ?minPD" 
          using minPD_sub antichain_on_def partial_PD by simp
      have acPD_nMax_nMin: "∀ ac . (antichain_on PD ac) ⟶ (ac ≠ ?max ∧ ac ≠ ?min)" 
          using max_min_nPD antichain_on_def 
          by metis 
      have "∀ ac. (antichain_on PD ac) ⟶ (antichain_on P ac)"
          using antichain_on_def antichain_def
          by (meson PD_sub partial_P subset_trans)
      then have "∀ ac. (antichain_on PD ac) ⟶ card ac ≤ (card lac - 1)" 
          using ac_less PD_sub max_min_nPD acPD_nMax_nMin by blast
      then have minPD_lac: "largest_antichain_on PD ?minPD" 
        using largest_antichain_on_def ac_minPD card_minPD by simp
      then have "∃ cv. chain_cover_on PD cv ∧ card cv = card ?minPD"
      proof cases
        assume "PD ≠ {}"
        then show ?thesis using less PD_less minPD_lac finite_PD by blast
      next
        assume "¬ (PD ≠ {})"
        then have PD_empty: "PD = {}" by simp
        then have "?minPD = {}" using minPD_sub by auto
        then show ?thesis 
          using minPD_lac PD_empty largest_antichain_card_eq_empty by simp
      qed
      then obtain cvPD where cvPD_def: "chain_cover_on PD cvPD" 
                                       "card cvPD = card ?minPD" by blast
      then have "∪ cvPD = PD" unfolding chain_cover_on_def by simp
      then have union_cvPD: "∪ (cvPD ∪ {{x,y}}) = P" using PD_def
          using ‹x ∈ P›  y(1) 
          using   is_maximal_in_set_iff by force
      have chains_cvPD: "∀ x ∈ cvPD. chain_on x P" 
          using chain_on_def cvPD_def(1) PD_sub unfolding chain_cover_on_def
          by (meson Sup_le_iff partial_P)
      have "{x,y} ⊆ P" using x y  using union_cvPD by blast
      then have xy_chain_on: "chain_on {x,y} P" 
          using partial_P y(2) chain_on_def chain_def by fast
      define cvf where cvf_def: "cvf = cvPD ∪ {{x,y}}"
      then have cv_cvf: "chain_cover_on P cvf" 
          using chains_cvPD union_cvPD xy_chain_on unfolding chain_cover_on_def by simp
      have "¬ ({x,y} ⊆ PD)" using PD_def by simp
      then have "{x,y} ∉ cvPD" using cvPD_def(1) 
          unfolding chain_cover_on_def chain_on_def by auto
      then have "card (cvPD ∪ {{x,y}}) = (card ?minPD) + 1" using cvPD_def(2) card_def
          by (simp add: ‹∪ cvPD = PD› finite_PD finite_UnionD)
      then have "card cvf = (card ?minPD) + 1" using cvf_def by auto
      then have "card cvf = card lac" using card_minPD
        by (metis Diff_infinite_finite Suc_eq_plus1 
            ‹lac = {x. is_minimal_in_set P x}› ‹{x, y} ⊆ P›
            card_Diff_singleton card_Suc_Diff1 finite_PD finite_subset 
            less.prems(2) minPD_sub x)
         then show ?thesis using cv_cvf by blast
    qed
  qed
qed

section "Dilworth's Theorem for Chain Covers: Statement and Proof"

text ‹ We show that in any partially ordered set, the cardinality of
  largest antichain is equal to the cardinality of a smallest chain cover.›

theorem Dilworth: 
  assumes "largest_antichain_on P lac" 
      and "finite P" 
  shows "∃ cv. (smallest_chain_cover_on P cv) ∧ (card cv = card lac)"
proof-
  show ?thesis 
    using antichain_card_leq largest_antichard_card_eq assms largest_antichain_on_def
    by (smt (verit, ccfv_SIG) card.empty chain_cover_null le_antisym le_zero_eq 
            smallest_chain_cover_on_def)
qed


section "Dilworth's Decomposition Theorem"

subsection "Preliminaries"

text  ‹Now we will strengthen the result above to prove that the cardinality of a
  chain decomposition is equal to the cardinality of a largest antichain.
  order to prove that, we construct a preliminary result which states that
  of smallest chain decomposition is equal to the cardinality of smallest
  cover.›

text  ‹We begin by constructing the function make\_disjoint which takes a list of sets
  returns a list of sets which are mutually disjoint, and leaves the union of the
  in the list invariant. This function when acting on a chain cover returns a
  decomposition.›

fun make_disjoint::"_ set list ==> _ "
  where
 "make_disjoint [] = ([])"
|"make_disjoint (s#ls) = (s - (∪ (set ls)))#(make_disjoint ls)"


lemma finite_dist_card_list:
  assumes "finite S"
  shows "∃ls. set ls = S ∧ length ls = card S ∧ distinct ls"
  using assms  distinct_card finite_distinct_list
  by metis

lemma len_make_disjoint:"length xs = length (make_disjoint xs)"
  by (induction xs, simp+)

text  ‹We use the predicate @{term "list_all2 (⊆)"}, which checks if two lists (of sets)
  equal length, and if each element in the first list is a subset of the
  element in the second list.›

lemma subset_make_disjoint: "list_all2 (⊆) (make_disjoint xs) xs"
  by (induction xs, simp, auto)

lemma subslist_union:
 assumes "list_all2 (⊆) xs ys"
 shows "∪ (set xs) ⊆ ∪ (set ys)"
  using assms by(induction, simp, auto)

lemma make_disjoint_union:"∪ (set xs) = ∪ (set (make_disjoint xs))"
proof
  show "∪ (set xs) ⊆ ∪ (set (make_disjoint xs))"
    by (induction xs, auto) 
next
  show "∪ (set (make_disjoint xs)) ⊆ ∪ (set xs)"
    using subslist_union subset_make_disjoint
    by (metis) 
qed

lemma make_disjoint_empty_int:
  assumes "X ∈ set (make_disjoint xs)" "Y ∈ set (make_disjoint xs)"
 and "X ≠ Y"
shows "X ∩ Y = {}"
  using assms
proof(induction xs arbitrary: X Y)
  case (Cons a xs)
  then show ?case
  proof(cases "X ≠ a - (∪ (set xs)) ∧ Y ≠ (a - (∪ (set xs)))")
    case True
    then show ?thesis using Cons(1)[of X Y] Cons(2,3) 
      by (smt (verit, del_insts) Cons.prems(3) Diff_Int_distrib Diff_disjoint 
          Sup_upper make_disjoint.simps(2) make_disjoint_union inf.idem inf_absorb1 
          inf_commute set_ConsD) 
  next
    case False
    hence fa:"X = a - (∪ (set xs)) ∨ Y = a - (∪ (set xs)) " by argo
    then show ?thesis 
    proof(cases "X = a - (∪ (set xs)) ")
      case True
      hence "Y ≠ a - (∪ (set xs)) " using Cons(4) by argo
      hence "Y ∈ set (make_disjoint xs)" using Cons(3) by simp
      hence "Y ⊆ ∪ (set (make_disjoint xs))" by blast
      hence "Y ⊆ ∪ (set xs)" using make_disjoint_union by metis
      hence "X ∩ Y = {}" using True by blast
      then show ?thesis by blast
    next
      case False
      hence Y:"Y = a - (∪ (set xs))" using Cons(4) fa by argo
      hence "X ≠ a - (∪ (set xs))" using False by argo
      hence "X ∈ set (make_disjoint xs)" using Cons(2) by simp
      hence "X ⊆ ∪ (set (make_disjoint xs))" by blast
      hence "X ⊆ ∪ (set xs)" using make_disjoint_union by metis
      hence "X ∩ Y = {}" using Y by blast
      then show ?thesis by blast
    qed
  qed
qed (simp)

lemma chain_subslist:
  assumes "∀i < length xs. Complete_Partial_Order.chain (≤) (xs!i)"
    and "list_all2 (⊆) ys xs"
  shows "∀i < length ys. Complete_Partial_Order.chain (≤) (ys!i)"
  using assms(2,1)
proof(induction)
  case (Cons x xs y ys)
  then have "list_all2 (⊆) xs ys"  by auto
  then have le:" ∀i<length xs. Complete_Partial_Order.chain (≤) (xs ! i)" 
    using Cons by fastforce
  then have "x ⊆ y" using Cons(1) by auto
  then have "Complete_Partial_Order.chain (≤) x" using Cons 
    using chain_subset by fastforce
  then show ?case using le 
    by (metis all_nth_imp_all_set insert_iff list.simps(15) nth_mem) 
qed(argo)

lemma chain_cover_disjoint:
  assumes "chain_cover_on P (set C)"
  shows "chain_cover_on P (set (make_disjoint C))"
proof-
  have "∪ (set (make_disjoint C)) = P" using make_disjoint_union assms(1) 
    unfolding chain_cover_on_def by metis
  moreover have "∀x∈set (make_disjoint C). x ⊆ P"
    using subset_make_disjoint assms unfolding chain_cover_on_def 
    using calculation by blast
  moreover have "∀x∈set (make_disjoint C). Complete_Partial_Order.chain (≤) x" 
    using chain_subslist assms unfolding chain_cover_on_def chain_on_def 
    by (metis in_set_conv_nth subset_make_disjoint)
  ultimately show ?thesis   unfolding chain_cover_on_def chain_on_def by auto
qed

lemma make_disjoint_subset_i:
  assumes "i < length as"
  shows "(make_disjoint (as))!i ⊆ (as!i)" 
  using assms
proof(induct as arbitrary: i)
  case (Cons a as)
  then show ?case
  proof(cases "i = 0")
    case False
    have "i - 1 < length as" using Cons 
      using False by force
    hence "(make_disjoint as)! (i - 1) ⊆ as!(i - 1)" using Cons(1)[of "i - 1"]
      by argo
    then show ?thesis using False by simp
  qed (simp)
qed (simp)

text  ‹Following theorem asserts that the corresponding to the smallest chain cover on
  finite set, there exists a corresponding chain decomposition of the same cardinality.›

lemma chain_cover_decompsn_eq: 
  assumes "finite P"
      and "smallest_chain_cover_on P A"
    shows "∃ B. chain_decomposition P B ∧ card B = card A"
proof-
  obtain As where As:"set As = A" "length As = card A" "distinct As" 
    using assms
    by (metis chain_cover_on_def finite_UnionD finite_dist_card_list 
        smallest_chain_cover_on_def)
  hence ccdas:"chain_cover_on P (set (make_disjoint As))" 
    using assms(2) chain_cover_disjoint[of P As]
    unfolding smallest_chain_cover_on_def by argo
  hence 1:"chain_decomposition P (set (make_disjoint As))" 
    using make_disjoint_empty_int 
    unfolding chain_decomposition_def  by meson
  moreover have 2:"card (set (make_disjoint As)) = card A"
  proof(rule ccontr)
    assume asm:"¬ card (set (make_disjoint As)) = card A"
    have "length (make_disjoint As) = card A" 
      using len_make_disjoint As(2) by metis
    then show False 
      using asm assms(2) card_length ccdas 
            smallest_chain_cover_on_def 
      by metis
  qed
  ultimately show ?thesis by blast
qed
  
  
lemma smallest_cv_cd:
  assumes "smallest_chain_decomposition P cd"
        and "smallest_chain_cover_on P cv"
      shows "card cv ≤ card cd"
  using assms unfolding smallest_chain_decomposition_def chain_decomposition_def
       smallest_chain_cover_on_def by auto

lemma smallest_cv_eq_smallest_cd:
  assumes "finite P"
         and "smallest_chain_decomposition P cd"
        and "smallest_chain_cover_on P cv"
      shows "card cv = card cd"
  using smallest_cv_cd[OF assms(2,3)] chain_cover_decompsn_eq[OF assms(1,3)]
  by (metis assms(2) smallest_chain_decomposition_def)


subsection "Statement and Proof "

text‹We extend the Dilworth's theorem to chain decomposition. The following theorem
  that size of a largest antichain is equal to the size of a smallest chain
 .›

theorem Dilworth_Decomposition: 
  assumes "largest_antichain_on P lac" 
      and "finite P" 
    shows "∃ cd. (smallest_chain_decomposition P cd) ∧ (card cd = card lac)"
  using Dilworth[OF assms] smallest_cv_eq_smallest_cd assms 
  by (metis (mono_tags, lifting) cd_cv chain_cover_decompsn_eq 
       smallest_chain_cover_on_def  smallest_chain_decomposition_def) 
 
end 
(*ends the context*)
end