Theory Dilworth
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
extension 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
is 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
chain 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
some chain it belongs to in a chain cover, we show that, the co-domain of f is a subset of
the 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
cardinality 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
of 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,
the 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
chain 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
in 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,
if the cardinality of the chain cover is equal to the cardinality of the antichain
then for all chains c of the chain cover, there exists an element a of the antichain
such 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
than 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
than 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
the 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
cardinalities 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
from 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
minimal 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
in 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,
then 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,
then there exists an element a in the maximal set such that a does not belong to the
largest 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 (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
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)} "
define p_minus where "p_minus = {x. x ∈ P ∧ (∃ y ∈ ac. x ≤ y)}"
have 1: "ac ⊆ 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"
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"
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
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"
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)"
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
a 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
smallest chain decomposition is equal to the cardinality of a largest antichain.
In order to prove that, we construct a preliminary result which states that
cardinality of smallest chain decomposition is equal to the cardinality of smallest
chain cover.›
text ‹We begin by constructing the function make\_disjoint which takes a list of sets
and returns a list of sets which are mutually disjoint, and leaves the union of the
sets in the list invariant. This function when acting on a chain cover returns a
chain 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)
have equal length, and if each element in the first list is a subset of the
corresponding 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
a 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
asserts that size of a largest antichain is equal to the size of a smallest chain
decomposition.›
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
end