section ‹Matroids›
theory Matroid
imports Indep_System
begin
lemma card_subset_ex:
assumes "finite A" "n ≤ card A"
shows "∃B ⊆ A. card B = n"
using assms
proof (induction A arbitrary: n rule: finite_induct)
case (insert x A)
show ?case
proof (cases n)
case 0
then show ?thesis using card_empty by blast
next
case (Suc k)
then have "∃B ⊆ A. card B = k" using insert by auto
then obtain B where "B ⊆ A" "card B = k" by auto
moreover from this have "finite B" using insert.hyps finite_subset by auto
ultimately have "card (insert x B) = n"
using Suc insert.hyps card_insert_disjoint by fastforce
then show ?thesis using ‹B ⊆ A› by blast
qed
qed auto
locale matroid = indep_system +
assumes augment_aux:
"indep X ⟹ indep Y ⟹ card X = Suc (card Y) ⟹ ∃x ∈ X - Y. indep (insert x Y)"
begin
lemma augment:
assumes "indep X" "indep Y" "card Y < card X"
shows "∃x ∈ X - Y. indep (insert x Y)"
proof -
obtain X' where "X' ⊆ X" "card X' = Suc (card Y)"
using assms card_subset_ex[of X "Suc (card Y)"] indep_finite by auto
then obtain x where "x ∈ X' - Y" "indep (insert x Y)"
using assms augment_aux[of X' Y] indep_subset by auto
then show ?thesis using ‹X' ⊆ X› by auto
qed
lemma augment_psubset:
assumes "indep X" "indep Y" "Y ⊂ X"
shows "∃x ∈ X - Y. indep (insert x Y)"
using assms augment psubset_card_mono indep_finite by blast
subsection ‹Minors›
text ‹
A subset of the ground set induces a matroid.
›
lemma matroid_subset [simp, intro]:
assumes "ℰ ⊆ carrier"
shows "matroid ℰ (indep_in ℰ)"
unfolding matroid_def matroid_axioms_def
proof (safe, goal_cases indep_system augment)
case indep_system
then show ?case using indep_system_subset[OF assms] .
next
case (augment X Y)
then show ?case using augment_aux[of X Y] unfolding indep_in_def by auto
qed
context
fixes ℰ
assumes "ℰ ⊆ carrier"
begin
interpretation ℰ: matroid ℰ "indep_in ℰ"
using ‹ℰ ⊆ carrier› by auto
lemmas augment_aux_indep_in = ℰ.augment_aux
lemmas augment_indep_in = ℰ.augment
lemmas augment_psubset_indep_in = ℰ.augment_psubset
end
subsection ‹Bases›
lemma basis_card:
assumes "basis B⇩1"
assumes "basis B⇩2"
shows "card B⇩1 = card B⇩2"
proof (rule ccontr, goal_cases False)
case False
then have "card B⇩1 < card B⇩2 ∨ card B⇩2 < card B⇩1" by auto
moreover {
fix B⇩1 B⇩2
assume "basis B⇩1" "basis B⇩2" "card B⇩1 < card B⇩2"
then obtain x where "x ∈ B⇩2 - B⇩1" "indep (insert x B⇩1)"
using augment basisD by blast
then have "x ∈ carrier - B⇩1"
using ‹basis B⇩1› basisD indep_subset_carrier by blast
then have "¬ indep (insert x B⇩1)" using ‹basis B⇩1› basisD by auto
then have "False" using ‹indep (insert x B⇩1)› by auto
}
ultimately show ?case using assms by auto
qed
lemma basis_indep_card:
assumes "indep X"
assumes "basis B"
shows "card X ≤ card B"
proof -
obtain B' where "basis B'" "X ⊆ B'" using assms indep_imp_subset_basis by auto
then show ?thesis using assms basis_finite basis_card[of B B'] by (auto intro: card_mono)
qed
lemma basis_augment:
assumes "basis B⇩1" "basis B⇩2" "x ∈ B⇩1 - B⇩2"
shows "∃y ∈ B⇩2 - B⇩1. basis (insert y (B⇩1 - {x}))"
proof -
let ?B⇩1 = "B⇩1 - {x}"
have "card ?B⇩1 < card B⇩2"
using assms basis_card[of B⇩1 B⇩2] card_Diff1_less[OF basis_finite, of B⇩1] by auto
moreover have "indep ?B⇩1" using assms basis_indep[of B⇩1] indep_subset[of B⇩1 ?B⇩1] by auto
ultimately obtain y where y: "y ∈ B⇩2 - ?B⇩1" "indep (insert y ?B⇩1)"
using assms augment[of B⇩2 ?B⇩1] basis_indep by auto
let ?B⇩1' = "insert y ?B⇩1"
have "basis ?B⇩1'" using ‹indep ?B⇩1'›
proof (rule basisI, goal_cases "insert")
case (insert x)
have "card (insert x ?B⇩1') > card B⇩1"
proof -
have "card (insert x ?B⇩1') = Suc (card ?B⇩1')"
using insert card_insert[OF indep_finite, of ?B⇩1'] y by auto
also have "… = Suc (Suc (card ?B⇩1))"
using card_insert[OF indep_finite, of ?B⇩1] ‹indep ?B⇩1› y by auto
also have "… = Suc (card B⇩1)"
using assms basis_finite[of B⇩1] card.remove[of B⇩1] by auto
finally show ?thesis by auto
qed
then have "¬indep (insert x (insert y ?B⇩1))"
using assms basis_indep_card[of "insert x (insert y ?B⇩1)" B⇩1] by auto
moreover have "insert x (insert y ?B⇩1) ⊆ carrier"
using assms insert y basis_finite indep_subset_carrier by auto
ultimately show ?case by auto
qed
then show ?thesis using assms y by auto
qed
context
fixes ℰ
assumes *: "ℰ ⊆ carrier"
begin
interpretation ℰ: matroid ℰ "indep_in ℰ"
using ‹ℰ ⊆ carrier› by auto
lemmas basis_in_card = ℰ.basis_card[OF basis_inD_aux[OF *] basis_inD_aux[OF *]]
lemmas basis_in_indep_in_card = ℰ.basis_indep_card[OF _ basis_inD_aux[OF *]]
lemma basis_in_augment:
assumes "basis_in ℰ B⇩1" "basis_in ℰ B⇩2" "x ∈ B⇩1 - B⇩2"
shows "∃y ∈ B⇩2 - B⇩1. basis_in ℰ (insert y (B⇩1 - {x}))"
using assms ℰ.basis_augment unfolding basis_in_def by auto
end
subsection ‹Circuits›
lemma circuit_elim:
assumes "circuit C⇩1" "circuit C⇩2" "C⇩1 ≠ C⇩2" "x ∈ C⇩1 ∩ C⇩2"
shows "∃C⇩3 ⊆ (C⇩1 ∪ C⇩2) - {x}. circuit C⇩3"
proof -
let ?C = "(C⇩1 ∪ C⇩2) - {x}"
let ?carrier = "C⇩1 ∪ C⇩2"
have assms': "circuit_in carrier C⇩1" "circuit_in carrier C⇩2"
using assms circuit_imp_circuit_in by auto
have "?C ⊆ carrier" using assms circuit_subset_carrier by auto
show ?thesis
proof (cases "indep ?C")
case False
then show ?thesis using dep_iff_supset_circuit ‹?C ⊆ carrier› by auto
next
case True
then have "indep_in ?carrier ?C" using ‹?C ⊆ carrier› by (auto intro: indep_inI)
have *: "?carrier ⊆ carrier" using assms circuit_subset_carrier by auto
obtain y where y: "y ∈ C⇩2" "y ∉ C⇩1" using assms circuit_subset_eq by blast
then have "indep_in ?carrier (C⇩2 - {y})"
using assms' circuit_in_min_dep_in[OF * circuit_in_supI[OF *, of C⇩2]] by auto
then obtain B where B: "basis_in ?carrier B" "C⇩2 - {y} ⊆ B"
using * assms indep_in_imp_subset_basis_in[of ?carrier "C⇩2 - {y}"] by auto
have "y ∉ B"
proof (rule ccontr, goal_cases False)
case False
then have "C⇩2 ⊆ B" using B by auto
moreover have "circuit_in ?carrier C⇩2" using * assms' circuit_in_supI by auto
ultimately have "¬ indep_in ?carrier B"
using B basis_in_subset_carrier[OF *] supset_circuit_in_imp_dep_in[OF *] by auto
then show False using assms B basis_in_indep_in[OF *] by auto
qed
have "C⇩1 - B ≠ {}"
proof (rule ccontr, goal_cases False)
case False
then have "C⇩1 - (C⇩1 ∩ B) = {}" by auto
then have "C⇩1 = C⇩1 ∩ B" using assms circuit_subset_eq by auto
moreover have "indep (C⇩1 ∩ B)"
using assms B basis_in_indep_in[OF *] indep_in_subset[OF *, of B "C⇩1 ∩ B"] indep_in_indep
by auto
ultimately show ?case using assms circuitD by auto
qed
then obtain z where z: "z ∈ C⇩1" "z ∉ B" by auto
have "y ≠ z" using y z by auto
have "x ∈ C⇩1" "x ∈ C⇩2" using assms by auto
have "finite ?carrier" using assms carrier_finite finite_subset by auto
have "card B ≤ card (?carrier - {y, z})"
proof (rule card_mono)
show "finite (C⇩1 ∪ C⇩2 - {y, z})" using ‹finite ?carrier› by auto
next
show "B ⊆ C⇩1 ∪ C⇩2 - {y, z}"
using B basis_in_subset_carrier[OF *, of B] ‹y ∉ B› ‹z ∉ B› by auto
qed
also have "… = card ?carrier - 2"
using ‹finite ?carrier› ‹y ∈ C⇩2› ‹z ∈ C⇩1› ‹y ≠ z› card_Diff_subset_Int by auto
also have "… < card ?carrier - 1"
proof -
have "card ?carrier = card C⇩1 + card C⇩2 - card (C⇩1 ∩ C⇩2)"
using assms ‹finite ?carrier› card_Un_Int[of C⇩1 C⇩2] by auto
also have "… = card C⇩1 + (card C⇩2 - card (C⇩1 ∩ C⇩2))"
using assms ‹finite ?carrier› card_mono[of C⇩2] by auto
also have "… = card C⇩1 + card (C⇩2 - C⇩1)"
proof -
have "card (C⇩2 - C⇩1) = card C⇩2 - card (C⇩2 ∩ C⇩1)"
using assms ‹finite ?carrier› card_Diff_subset_Int[of C⇩2 C⇩1] by auto
also have "… = card C⇩2 - card (C⇩1 ∩ C⇩2)" by (simp add: inf_commute)
finally show ?thesis by auto
qed
finally have "card (C⇩1 ∪ C⇩2) = card C⇩1 + card (C⇩2 - C⇩1)" .
moreover have "card C⇩1 > 0" using assms circuit_nonempty ‹finite ?carrier› by auto
moreover have "card (C⇩2 - C⇩1) > 0" using assms ‹finite ?carrier› ‹y ∈ C⇩2› ‹y ∉ C⇩1› by auto
ultimately show ?thesis by auto
qed
also have "… = card ?C"
using ‹finite ?carrier› card_Diff_singleton ‹x ∈ C⇩1› ‹x ∈ C⇩2› by auto
finally have "card B < card ?C" .
then have False
using basis_in_indep_in_card[OF *, of ?C B] B ‹indep_in ?carrier ?C› by auto
then show ?thesis by auto
qed
qed
lemma min_dep_imp_supset_circuit:
assumes "indep X"
assumes "circuit C"
assumes "C ⊆ insert x X"
shows "x ∈ C"
proof (rule ccontr)
assume "x ∉ C"
then have "C ⊆ X" using assms by auto
then have "indep C" using assms indep_subset by auto
then show False using assms circuitD by auto
qed
lemma min_dep_imp_ex1_supset_circuit:
assumes "x ∈ carrier"
assumes "indep X"
assumes "¬ indep (insert x X)"
shows "∃!C. circuit C ∧ C ⊆ insert x X"
proof -
obtain C where C: "circuit C" "C ⊆ insert x X"
using assms indep_subset_carrier dep_iff_supset_circuit by auto
show ?thesis
proof (rule ex1I, goal_cases ex unique)
show "circuit C ∧ C ⊆ insert x X" using C by auto
next
{
fix C'
assume C': "circuit C'" "C' ⊆ insert x X"
have "C' = C"
proof (rule ccontr)
assume "C' ≠ C"
moreover have "x ∈ C' ∩ C" using C C' assms min_dep_imp_supset_circuit by auto
ultimately have "¬ indep (C' ∪ C - {x})"
using circuit_elim[OF C(1) C'(1), of x] supset_circuit_imp_dep[of _ "C' ∪ C - {x}"] by auto
moreover have "C' ∪ C - {x} ⊆ X" using C C' by auto
ultimately show False using assms indep_subset by auto
qed
}
then show "⋀C'. circuit C' ∧ C' ⊆ insert x X ⟹ C' = C"
by auto
qed
qed
lemma basis_ex1_supset_circuit:
assumes "basis B"
assumes "x ∈ carrier - B"
shows "∃!C. circuit C ∧ C ⊆ insert x B"
using assms min_dep_imp_ex1_supset_circuit basisD by auto
definition fund_circuit :: "'a ⇒ 'a set ⇒ 'a set" where
"fund_circuit x B ≡ (THE C. circuit C ∧ C ⊆ insert x B)"
lemma circuit_iff_fund_circuit:
"circuit C ⟷ (∃x B. x ∈ carrier - B ∧ basis B ∧ C = fund_circuit x B)"
proof (safe, goal_cases LTR RTL)
case LTR
then obtain x where "x ∈ C" using circuit_nonempty by auto
then have "indep (C - {x})" using LTR unfolding circuit_def by auto
then obtain B where B: "basis B" "C - {x} ⊆ B" using indep_imp_subset_basis by auto
then have "x ∈ carrier" using LTR circuit_subset_carrier ‹x ∈ C› by auto
moreover have "x ∉ B"
proof (rule ccontr, goal_cases False)
case False
then have "C ⊆ B" using ‹C - {x} ⊆ B› by auto
then have "¬ indep B" using LTR B basis_subset_carrier supset_circuit_imp_dep by auto
then show ?case using B basis_indep by auto
qed
ultimately show ?case
unfolding fund_circuit_def
using LTR B theI_unique[OF basis_ex1_supset_circuit[of B x], of C] by auto
next
case (RTL x B)
then have "∃!C. circuit C ∧ C ⊆ insert x B"
using min_dep_imp_ex1_supset_circuit basisD[of B] by auto
then show ?case
unfolding fund_circuit_def
using theI[of "λC. circuit C ∧ C ⊆ insert x B"] by fastforce
qed
lemma fund_circuitI:
assumes "basis B"
assumes "x ∈ carrier - B"
assumes "circuit C"
assumes "C ⊆ insert x B"
shows "fund_circuit x B = C"
unfolding fund_circuit_def
using assms theI_unique[OF basis_ex1_supset_circuit, of B x C] by auto
definition fund_circuit_in where "fund_circuit_in ℰ x B ≡ matroid.fund_circuit ℰ (indep_in ℰ) x B"
context
fixes ℰ
assumes *: "ℰ ⊆ carrier"
begin
interpretation ℰ: matroid ℰ "indep_in ℰ"
using ‹ℰ ⊆ carrier› by auto
lemma fund_circuit_inI_aux: "ℰ.fund_circuit x B = fund_circuit_in ℰ x B"
unfolding fund_circuit_in_def by auto
lemma circuit_in_elim:
assumes "circuit_in ℰ C⇩1" "circuit_in ℰ C⇩2" "C⇩1 ≠ C⇩2" "x ∈ C⇩1 ∩ C⇩2"
shows "∃C⇩3 ⊆ (C⇩1 ∪ C⇩2) - {x}. circuit_in ℰ C⇩3"
using assms ℰ.circuit_elim unfolding circuit_in_def by auto
lemmas min_dep_in_imp_supset_circuit_in = ℰ.min_dep_imp_supset_circuit[OF _ circuit_inD_aux[OF *]]
lemma min_dep_in_imp_ex1_supset_circuit_in:
assumes "x ∈ ℰ"
assumes "indep_in ℰ X"
assumes "¬ indep_in ℰ (insert x X)"
shows "∃!C. circuit_in ℰ C ∧ C ⊆ insert x X"
using assms ℰ.min_dep_imp_ex1_supset_circuit unfolding circuit_in_def by auto
lemma basis_in_ex1_supset_circuit_in:
assumes "basis_in ℰ B"
assumes "x ∈ ℰ - B"
shows "∃!C. circuit_in ℰ C ∧ C ⊆ insert x B"
using assms ℰ.basis_ex1_supset_circuit unfolding circuit_in_def basis_in_def by auto
lemma fund_circuit_inI:
assumes "basis_in ℰ B"
assumes "x ∈ ℰ - B"
assumes "circuit_in ℰ C"
assumes "C ⊆ insert x B"
shows "fund_circuit_in ℰ x B = C"
using assms ℰ.fund_circuitI
unfolding basis_in_def circuit_in_def fund_circuit_in_def by auto
end
context
fixes ℰ
assumes *: "ℰ ⊆ carrier"
begin
interpretation ℰ: matroid ℰ "indep_in ℰ"
using ‹ℰ ⊆ carrier› by auto
lemma fund_circuit_in_sub_cong:
assumes "ℰ' ⊆ ℰ"
assumes "x ∈ ℰ' - B"
assumes "basis_in ℰ' B"
shows "ℰ.fund_circuit_in ℰ' x B = fund_circuit_in ℰ' x B"
proof -
obtain C where C: "circuit_in ℰ' C" "C ⊆ insert x B"
using * assms basis_in_ex1_supset_circuit_in[of ℰ' B x] by auto
then have "fund_circuit_in ℰ' x B = C"
using * assms fund_circuit_inI by auto
also have "… = ℰ.fund_circuit_in ℰ' x B"
using * assms C ℰ.fund_circuit_inI basis_in_sub_cong[of ℰ] circuit_in_sub_cong[of ℰ] by auto
finally show ?thesis by auto
qed
end
subsection ‹Ranks›
abbreviation rank_of where "rank_of ≡ lower_rank_of"
lemmas rank_of_def = lower_rank_of_def
lemmas rank_of_sub_cong = lower_rank_of_sub_cong
lemmas rank_of_le = lower_rank_of_le
context
fixes ℰ
assumes *: "ℰ ⊆ carrier"
begin
interpretation ℰ: matroid ℰ "indep_in ℰ"
using * by auto
lemma lower_rank_of_eq_upper_rank_of: "lower_rank_of ℰ = upper_rank_of ℰ"
proof -
obtain B where "basis_in ℰ B" using basis_in_ex[OF *] by auto
then have "{card B | B. basis_in ℰ B} = {card B}"
by safe (auto dest: basis_in_card[OF *])
then show ?thesis unfolding lower_rank_of_def upper_rank_of_def by auto
qed
lemma rank_of_eq_card_basis_in:
assumes "basis_in ℰ B"
shows "rank_of ℰ = card B"
proof -
have "{card B | B. basis_in ℰ B} = {card B}" using assms by safe (auto dest: basis_in_card[OF *])
then show ?thesis unfolding rank_of_def by auto
qed
lemma rank_of_indep_in_le:
assumes "indep_in ℰ X"
shows "card X ≤ rank_of ℰ"
proof -
{
fix B
assume "basis_in ℰ B"
moreover obtain B' where "basis_in ℰ B'" "X ⊆ B'"
using assms indep_in_imp_subset_basis_in[OF *] by auto
ultimately have "card X ≤ card B"
using card_mono[OF basis_in_finite[OF *]] basis_in_card[OF *, of B B'] by auto
}
moreover have "finite {card B | B. basis_in ℰ B}"
using collect_basis_in_finite[OF *] by auto
ultimately show ?thesis
unfolding rank_of_def using basis_in_ex[OF *] by auto
qed
end
lemma rank_of_mono:
assumes "X ⊆ Y"
assumes "Y ⊆ carrier"
shows "rank_of X ≤ rank_of Y"
proof -
obtain B⇩X where B⇩X: "basis_in X B⇩X" using assms basis_in_ex[of X] by auto
moreover obtain B⇩Y where B⇩Y: "basis_in Y B⇩Y" using assms basis_in_ex[of Y] by auto
moreover have "card B⇩X ≤ card B⇩Y"
using assms basis_in_indep_in_card[OF _ _ B⇩Y] basis_in_indep_in[OF _ B⇩X] indep_in_subI_subset
by auto
ultimately show ?thesis using assms rank_of_eq_card_basis_in by auto
qed
lemma rank_of_insert_le:
assumes "X ⊆ carrier"
assumes "x ∈ carrier"
shows "rank_of (insert x X) ≤ Suc (rank_of X)"
proof -
obtain B where B: "basis_in X B" using assms basis_in_ex[of X] by auto
have "basis_in (insert x X) B ∨ basis_in (insert x X) (insert x B)"
proof -
obtain B' where B': "B' ⊆ insert x X - X" "basis_in (insert x X) (B ∪ B')"
using assms B basis_in_subI[of "insert x X" X B] by auto
then have "B' = {} ∨ B' = {x}" by auto
then show ?thesis
proof
assume "B' = {}"
then have "basis_in (insert x X) B" using B' by auto
then show ?thesis by auto
next
assume "B' = {x}"
then have "basis_in (insert x X) (insert x B)" using B' by auto
then show ?thesis by auto
qed
qed
then show ?thesis
proof
assume "basis_in (insert x X) B"
then show ?thesis
using assms B rank_of_eq_card_basis_in by auto
next
assume "basis_in (insert x X) (insert x B)"
then have "rank_of (insert x X) = card (insert x B)"
using assms rank_of_eq_card_basis_in by auto
also have "… = Suc (card (B - {x}))"
using assms card_insert[of B x] using B basis_in_finite by auto
also have "… ≤ Suc (card B)"
using assms B basis_in_finite card_Diff1_le[of B] by auto
also have "… = Suc (rank_of X)"
using assms B rank_of_eq_card_basis_in by auto
finally show ?thesis .
qed
qed
lemma rank_of_Un_Int_le:
assumes "X ⊆ carrier"
assumes "Y ⊆ carrier"
shows "rank_of (X ∪ Y) + rank_of (X ∩ Y) ≤ rank_of X + rank_of Y"
proof -
obtain B_Int where B_Int: "basis_in (X ∩ Y) B_Int" using assms basis_in_ex[of "X ∩ Y"] by auto
then have "indep_in (X ∪ Y) B_Int"
using assms indep_in_subI_subset[OF _ basis_in_indep_in[of "X ∩ Y" B_Int], of "X ∪ Y"] by auto
then obtain B_Un where B_Un: "basis_in (X ∪ Y) B_Un" "B_Int ⊆ B_Un"
using assms indep_in_imp_subset_basis_in[of "X ∪ Y" B_Int] by auto
have "card (B_Un ∩ (X ∪ Y)) + card (B_Un ∩ (X ∩ Y)) = card ((B_Un ∩ X) ∪ (B_Un ∩ Y)) + card ((B_Un ∩ X) ∩ (B_Un ∩ Y))"
by (simp add: inf_assoc inf_left_commute inf_sup_distrib1)
also have "… = card (B_Un ∩ X) + card (B_Un ∩ Y)"
proof -
have "finite (B_Un ∩ X)" "finite (B_Un ∩ Y)"
using assms finite_subset[OF _ carrier_finite] by auto
then show ?thesis using card_Un_Int[of "B_Un ∩ X" "B_Un ∩ Y"] by auto
qed
also have "… ≤ rank_of X + rank_of Y"
proof -
have "card (B_Un ∩ X) ≤ rank_of X"
proof -
have "indep_in X (B_Un ∩ X)" using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI by auto
then show ?thesis using assms rank_of_indep_in_le by auto
qed
moreover have "card (B_Un ∩ Y) ≤ rank_of Y"
proof -
have "indep_in Y (B_Un ∩ Y)" using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI by auto
then show ?thesis using assms rank_of_indep_in_le by auto
qed
ultimately show ?thesis by auto
qed
finally have "rank_of X + rank_of Y ≥ card (B_Un ∩ (X ∪ Y)) + card (B_Un ∩ (X ∩ Y))" .
moreover have "B_Un ∩ (X ∪ Y) = B_Un" using assms basis_in_subset_carrier[OF _ B_Un(1)] by auto
moreover have "B_Un ∩ (X ∩ Y) = B_Int"
proof -
have "card (B_Un ∩ (X ∩ Y)) ≤ card B_Int"
proof -
have "indep_in (X ∩ Y) (B_Un ∩ (X ∩ Y))"
using assms basis_in_indep_in[OF _ B_Un(1)] indep_in_subI by auto
then show ?thesis using assms basis_in_indep_in_card[of "X ∩ Y" _ B_Int] B_Int by auto
qed
moreover have "finite (B_Un ∩ (X ∩ Y))"
using assms carrier_finite finite_subset[of "B_Un ∩ (X ∩ Y)"] by auto
moreover have "B_Int ⊆ B_Un ∩ (X ∩ Y)"
using assms B_Un B_Int basis_in_subset_carrier[of "X ∩ Y" B_Int] by auto
ultimately show ?thesis using card_seteq by blast
qed
ultimately have "rank_of X + rank_of Y ≥ card B_Un + card B_Int" by auto
moreover have "card B_Un = rank_of (X ∪ Y)"
using assms rank_of_eq_card_basis_in[OF _ B_Un(1)] by auto
moreover have "card B_Int = rank_of (X ∩ Y)"
using assms rank_of_eq_card_basis_in[OF _ B_Int] by fastforce
ultimately show "rank_of X + rank_of Y ≥ rank_of (X ∪ Y) + rank_of (X ∩ Y)" by auto
qed
lemma rank_of_Un_absorbI:
assumes "X ⊆ carrier" "Y ⊆ carrier"
assumes "⋀y. y ∈ Y - X ⟹ rank_of (insert y X) = rank_of X"
shows "rank_of (X ∪ Y) = rank_of X"
proof -
have "finite (Y - X)" using finite_subset[OF ‹Y ⊆ carrier›] carrier_finite by auto
then show ?thesis using assms
proof (induction "Y - X" arbitrary: Y rule: finite_induct )
case empty
then have "X ∪ Y = X" by auto
then show ?case by auto
next
case (insert y F)
have "rank_of (X ∪ Y) + rank_of X ≤ rank_of X + rank_of X"
proof -
have "rank_of (X ∪ Y) + rank_of X = rank_of ((X ∪ (Y - {y})) ∪ (insert y X)) + rank_of ((X ∪ (Y - {y})) ∩ (insert y X))"
proof -
have "X ∪ Y = (X ∪ (Y - {y})) ∪ (insert y X)" "X = (X ∪ (Y - {y})) ∩ (insert y X)" using insert by auto
then show ?thesis by auto
qed
also have "… ≤ rank_of (X ∪ (Y - {y})) + rank_of (insert y X)"
proof (rule rank_of_Un_Int_le)
show "X ∪ (Y - {y}) ⊆ carrier" using insert by auto
next
show "insert y X ⊆ carrier" using insert by auto
qed
also have "… = rank_of (X ∪ (Y - {y})) + rank_of X"
proof -
have "y ∈ Y - X" using insert by auto
then show ?thesis using insert by auto
qed
also have "… = rank_of X + rank_of X"
proof -
have "F = (Y - {y}) - X" "Y - {y} ⊆ carrier" using insert by auto
then show ?thesis using insert insert(3)[of "Y - {y}"] by auto
qed
finally show ?thesis .
qed
moreover have "rank_of (X ∪ Y) + rank_of X ≥ rank_of X + rank_of X"
using insert rank_of_mono by auto
ultimately show ?case by auto
qed
qed
lemma indep_iff_rank_of:
assumes "X ⊆ carrier"
shows "indep X ⟷ rank_of X = card X"
proof (standard, goal_cases LTR RTL)
case LTR
then have "indep_in X X" by (auto intro: indep_inI)
then have "basis_in X X" by (auto intro: basis_inI[OF assms])
then show ?case using rank_of_eq_card_basis_in[OF assms] by auto
next
case RTL
obtain B where B: "basis_in X B" using basis_in_ex[OF assms] by auto
then have "card B = card X" using RTL rank_of_eq_card_basis_in[OF assms] by auto
then have "B = X"
using basis_in_subset_carrier[OF assms B] card_seteq[OF finite_subset[OF assms carrier_finite]]
by auto
then show ?case using basis_in_indep_in[OF assms B] indep_in_indep by auto
qed
lemma basis_iff_rank_of:
assumes "X ⊆ carrier"
shows "basis X ⟷ rank_of X = card X ∧ rank_of X = rank_of carrier"
proof (standard, goal_cases LTR RTL)
case LTR
then have "rank_of X = card X" using assms indep_iff_rank_of basis_indep by auto
moreover have "… = rank_of carrier"
using LTR rank_of_eq_card_basis_in[of carrier X] basis_iff_basis_in by auto
ultimately show ?case by auto
next
case RTL
show ?case
proof (rule basisI)
show "indep X" using assms RTL indep_iff_rank_of by blast
next
fix x
assume x: "x ∈ carrier - X"
show "¬ indep (insert x X)"
proof (rule ccontr, goal_cases False)
case False
then have "card (insert x X) ≤ rank_of carrier"
using assms x indep_inI rank_of_indep_in_le by auto
also have "… = card X" using RTL by auto
finally show ?case using finite_subset[OF assms carrier_finite] x by auto
qed
qed
qed
lemma circuit_iff_rank_of:
assumes "X ⊆ carrier"
shows "circuit X ⟷ X ≠ {} ∧ (∀x ∈ X. rank_of (X - {x}) = card (X - {x}) ∧ card (X - {x}) = rank_of X)"
proof (standard, goal_cases LTR RTL)
case LTR
then have "X ≠ {}" using circuit_nonempty by auto
moreover have indep_remove: "⋀x. x ∈ X ⟹ rank_of (X - {x}) = card (X - {x})"
proof -
fix x
assume "x ∈ X"
then have "indep (X - {x})" using circuit_min_dep[OF LTR] by auto
moreover have "X - {x} ⊆ carrier" using assms by auto
ultimately show "rank_of (X - {x}) = card (X - {x})" using indep_iff_rank_of by auto
qed
moreover have "⋀x. x ∈ X ⟹ rank_of (X - {x}) = rank_of X"
proof -
fix x
assume *: "x ∈ X"
have "rank_of X ≤ card X" using assms rank_of_le by auto
moreover have "rank_of X ≠ card X" using assms LTR circuitD indep_iff_rank_of[of X] by auto
ultimately have "rank_of X < card X" by auto
then have "rank_of X ≤ card (X - {x})" using * finite_subset[OF assms] carrier_finite by auto
also have "… = rank_of (X - {x})" using indep_remove ‹x ∈ X› by auto
finally show "rank_of (X - {x}) = rank_of X" using assms rank_of_mono[of "X - {x}" X] by auto
qed
ultimately show ?case by auto
next
case RTL
then have "X ≠ {}"
and indep_remove: "⋀x. x ∈ X ⟹ rank_of (X - {x}) = card (X - {x})"
and dep: "⋀x. x ∈ X ⟹ rank_of (X - {x}) = rank_of X"
by auto
show ?case using assms
proof (rule circuitI)
obtain x where x: "x ∈ X" using ‹X ≠ {}› by auto
then have "rank_of X = card (X - {x})" using dep indep_remove by auto
also have "… < card X" using card_Diff1_less[OF finite_subset[OF assms carrier_finite] x] .
finally show "¬ indep X" using indep_iff_rank_of[OF assms] by auto
next
fix x
assume "x ∈ X"
then show "indep (X - {x})" using assms indep_remove[of x] indep_iff_rank_of[of "X - {x}"]
by auto
qed
qed
context
fixes ℰ
assumes *: "ℰ ⊆ carrier"
begin
interpretation ℰ: matroid ℰ "indep_in ℰ"
using * by auto
lemma indep_in_iff_rank_of:
assumes "X ⊆ ℰ"
shows "indep_in ℰ X ⟷ rank_of X = card X"
using assms ℰ.indep_iff_rank_of rank_of_sub_cong[OF * assms] by auto
lemma basis_in_iff_rank_of:
assumes "X ⊆ ℰ"
shows "basis_in ℰ X ⟷ rank_of X = card X ∧ rank_of X = rank_of ℰ"
using ℰ.basis_iff_rank_of[OF assms] rank_of_sub_cong[OF *] assms
unfolding basis_in_def by auto
lemma circuit_in_iff_rank_of:
assumes "X ⊆ ℰ"
shows "circuit_in ℰ X ⟷ X ≠ {} ∧ (∀x ∈ X. rank_of (X - {x}) = card (X - {x}) ∧ card (X - {x}) = rank_of X)"
proof -
have "circuit_in ℰ X ⟷ ℰ.circuit X" unfolding circuit_in_def ..
also have "… ⟷ X ≠ {} ∧ (∀x ∈ X. ℰ.rank_of (X - {x}) = card (X - {x}) ∧ card (X - {x}) = ℰ.rank_of X)"
using ℰ.circuit_iff_rank_of[OF assms] .
also have "… ⟷ X ≠ {} ∧ (∀x ∈ X. rank_of (X - {x}) = card (X - {x}) ∧ card (X - {x}) = rank_of X)"
proof -
{
fix x
have "ℰ.rank_of (X - {x}) = rank_of (X - {x})" "ℰ.rank_of X = rank_of X"
using assms rank_of_sub_cong[OF *, of "X - {x}"] rank_of_sub_cong[OF *, of X] by auto
then have "ℰ.rank_of (X - {x}) = card (X - {x}) ∧ card (X - {x}) = ℰ.rank_of X ⟷ rank_of (X - {x}) = card (X - {x}) ∧ card (X - {x}) = rank_of X"
by auto
}
then show ?thesis by auto
qed
finally show ?thesis .
qed
end
subsection ‹Closure›
definition cl :: "'a set ⇒ 'a set" where
"cl X ≡ {x ∈ carrier. rank_of (insert x X) = rank_of X}"
lemma clI:
assumes "x ∈ carrier"
assumes "rank_of (insert x X) = rank_of X"
shows "x ∈ cl X"
unfolding cl_def using assms by auto
lemma cl_altdef:
assumes "X ⊆ carrier"
shows "cl X = ⋃{Y ∈ Pow carrier. X ⊆ Y ∧ rank_of Y = rank_of X}"
proof -
{
fix x
assume *: "x ∈ cl X"
have "x ∈ ⋃{Y ∈ Pow carrier. X ⊆ Y ∧ rank_of Y = rank_of X}"
proof
show "insert x X ∈ {Y ∈ Pow carrier. X ⊆ Y ∧ rank_of Y = rank_of X}"
using assms * unfolding cl_def by auto
qed auto
}
moreover {
fix x
assume *: "x ∈ ⋃{Y ∈ Pow carrier. X ⊆ Y ∧ rank_of Y = rank_of X}"
then obtain Y where Y: "x ∈ Y" "Y ⊆ carrier" "X ⊆ Y" "rank_of Y = rank_of X" by auto
have "rank_of (insert x X) = rank_of X"
proof -
have "rank_of (insert x X) ≤ rank_of X"
proof -
have "insert x X ⊆ Y" using Y by auto
then show ?thesis using rank_of_mono[of "insert x X" Y] Y by auto
qed
moreover have "rank_of X ≤ rank_of (insert x X)" using Y by (auto intro: rank_of_mono)
ultimately show ?thesis by auto
qed
then have "x ∈ cl X" using * unfolding cl_def by auto
}
ultimately show ?thesis by blast
qed
lemma cl_rank_of: "x ∈ cl X ⟹ rank_of (insert x X) = rank_of X"
unfolding cl_def by auto
lemma cl_subset_carrier: "cl X ⊆ carrier"
unfolding cl_def by auto
lemmas clD = cl_rank_of cl_subset_carrier
lemma cl_subset:
assumes "X ⊆ carrier"
shows "X ⊆ cl X"
using assms using insert_absorb[of _ X] by (auto intro!: clI)
lemma cl_mono:
assumes "X ⊆ Y"
assumes "Y ⊆ carrier"
shows "cl X ⊆ cl Y"
proof
fix x
assume "x ∈ cl X"
then have "x ∈ carrier" using cl_subset_carrier by auto
have "insert x X ⊆ carrier"
using assms ‹x ∈ cl X› cl_subset_carrier[of X] by auto
then interpret X_insert: matroid "insert x X" "indep_in (insert x X)" by auto
have "insert x Y ⊆ carrier"
using assms ‹x ∈ cl X› cl_subset_carrier[of X] by auto
then interpret Y_insert: matroid "insert x Y" "indep_in (insert x Y)" by auto
show "x ∈ cl Y" using ‹x ∈ carrier›
proof (rule clI, cases "x ∈ X")
case True
then show "rank_of (insert x Y) = rank_of Y" using assms insert_absorb[of x Y] by auto
next
case False
obtain B⇩X where B⇩X: "basis_in X B⇩X" using assms basis_in_ex[of X] by auto
have "basis_in (insert x X) B⇩X"
proof -
have "rank_of B⇩X = card B⇩X ∧ rank_of B⇩X = rank_of (insert x X)"
proof -
have "rank_of B⇩X = card B⇩X ∧ rank_of B⇩X = rank_of X"
using assms B⇩X
basis_in_subset_carrier[where ℰ = X and X = B⇩X]
basis_in_iff_rank_of[where ℰ = X and X = B⇩X]
by blast
then show ?thesis using cl_rank_of[OF ‹x ∈ cl X›] by auto
qed
then show ?thesis
using assms basis_in_subset_carrier[OF _ B⇩X] ‹x ∈ carrier› basis_in_iff_rank_of[of "insert x X" B⇩X]
by auto
qed
have "indep_in (insert x Y) B⇩X"
using assms basis_in_indep_in[OF _ B⇩X] indep_in_subI_subset[of X "insert x Y"] by auto
then obtain B⇩Y where B⇩Y: "basis_in (insert x Y) B⇩Y" "B⇩X ⊆ B⇩Y"
using assms ‹x ∈ carrier› indep_in_iff_subset_basis_in[of "insert x Y" B⇩X] by auto
have "basis_in Y B⇩Y"
proof -
have "x ∉ B⇩Y"
proof (rule ccontr, goal_cases False)
case False
then have "insert x B⇩X ⊆ B⇩Y" using ‹B⇩X ⊆ B⇩Y› by auto
then have "indep_in (insert x Y) (insert x B⇩X)"
using assms ‹x ∈ carrier›
B⇩Y basis_in_indep_in[where ℰ = "insert x Y" and X = B⇩Y]
indep_in_subset[where ℰ = "insert x Y" and X = B⇩Y and Y = "insert x B⇩X"]
by auto
then have "indep_in (insert x X) (insert x B⇩X)"
using assms B⇩X
basis_in_subset_carrier[where ℰ = X and X = B⇩X]
indep_in_supI[where ℰ = "insert x Y" and ℰ' = "insert x X" and X = "insert x B⇩X"]
by auto
moreover have "x ∈ insert x X - B⇩X"
using assms ‹x ∉ X› B⇩X basis_in_subset_carrier[where ℰ = X and X = B⇩X] by auto
ultimately show ?case
using assms ‹x ∈ carrier› ‹basis_in (insert x X) B⇩X›
basis_in_max_indep_in[where ℰ = "insert x X" and X = B⇩X and x = x]
by auto
qed
then show ?thesis
using assms ‹x ∈ carrier› B⇩Y basis_in_subset_carrier[of "insert x Y" B⇩Y]
basis_in_supI[where ℰ = "insert x Y" and ℰ' = Y and B = B⇩Y] by auto
qed
show "rank_of (insert x Y) = rank_of Y"
proof -
have "rank_of (insert x Y) = card B⇩Y"
using assms ‹x ∈ carrier› ‹basis_in (insert x Y) B⇩Y› basis_in_subset_carrier
using basis_in_iff_rank_of[where ℰ = "insert x Y" and X = B⇩Y]
by auto
also have "… = rank_of Y"
using assms ‹x ∈ carrier› ‹basis_in Y B⇩Y› basis_in_subset_carrier
using basis_in_iff_rank_of[where ℰ = Y and X = B⇩Y]
by auto
finally show ?thesis .
qed
qed
qed
lemma cl_insert_absorb:
assumes "X ⊆ carrier"
assumes "x ∈ cl X"
shows "cl (insert x X) = cl X"
proof
show "cl (insert x X) ⊆ cl X"
proof (standard, goal_cases elem)
case (elem y)
then have *: "x ∈ carrier" "y ∈ carrier" using assms cl_subset_carrier by auto
have "rank_of (insert y X) = rank_of (insert y (insert x X))"
proof -
have "rank_of (insert y X) ≤ rank_of (insert y (insert x X))"
using assms * by (auto intro: rank_of_mono)
moreover have "rank_of (insert y (insert x X)) = rank_of (insert y X)"
proof -
have "insert y (insert x X) = insert x (insert y X)" by auto
then have "rank_of (insert y (insert x X)) = rank_of (insert x (insert y X))" by auto
also have "… = rank_of (insert y X)"
proof -
have "cl X ⊆ cl (insert y X)" by (rule cl_mono) (auto simp add: assms ‹y ∈ carrier›)
then have "x ∈ cl (insert y X)" using assms by auto
then show ?thesis unfolding cl_def by auto
qed
finally show ?thesis .
qed
ultimately show ?thesis by auto
qed
also have "… = rank_of (insert x X)" using elem using cl_rank_of by auto
also have "… = rank_of X" using assms cl_rank_of by auto
finally show "y ∈ cl X" using * by (auto intro: clI)
qed
next
have "insert x X ⊆ carrier" using assms cl_subset_carrier by auto
moreover have "X ⊆ insert x X" using assms by auto
ultimately show "cl X ⊆ cl (insert x X)" using assms cl_subset_carrier cl_mono by auto
qed
lemma cl_cl_absorb:
assumes "X ⊆ carrier"
shows "cl (cl X) = cl X"
proof
show "cl (cl X) ⊆ cl X"
proof (standard, goal_cases elem)
case (elem x)
then have "x ∈ carrier" using cl_subset_carrier by auto
then show ?case
proof (rule clI)
have "rank_of (insert x X) ≥ rank_of X"
using assms ‹x ∈ carrier› rank_of_mono[of X "insert x X"] by auto
moreover have "rank_of (insert x X) ≤ rank_of X"
proof -
have "rank_of (insert x X) ≤ rank_of (insert x (cl X))"
using assms ‹x ∈ carrier› cl_subset_carrier cl_subset[of X]
rank_of_mono[of "insert x X" "insert x (cl X)"] by auto
also have "… = rank_of (cl X)" using elem cl_rank_of by auto
also have "… = rank_of (X ∪ (cl X - X))"
using Diff_partition[OF cl_subset[OF assms]] by auto
also have "… = rank_of X" using ‹X ⊆ carrier›
proof (rule rank_of_Un_absorbI)
show "cl X - X ⊆ carrier" using assms cl_subset_carrier by auto
next
fix y
assume "y ∈ cl X - X - X"
then show "rank_of (insert y X) = rank_of X" unfolding cl_def by auto
qed
finally show ?thesis .
qed
ultimately show "rank_of (insert x X) = rank_of X" by auto
qed
qed
next
show "cl X ⊆ cl (cl X)" using cl_subset[OF cl_subset_carrier] by auto
qed
lemma cl_augment:
assumes "X ⊆ carrier"
assumes "x ∈ carrier"
assumes "y ∈ cl (insert x X) - cl X"
shows "x ∈ cl (insert y X)"
using ‹x ∈ carrier›
proof (rule clI)
have "rank_of (insert y X) ≤ rank_of (insert x (insert y X))"
using assms cl_subset_carrier by (auto intro: rank_of_mono)
moreover have "rank_of (insert x (insert y X)) ≤ rank_of (insert y X)"
proof -
have "rank_of (insert x (insert y X)) = rank_of (insert y (insert x X))"
proof -
have "insert x (insert y X) = insert y (insert x X)" by auto
then show ?thesis by auto
qed
also have "rank_of (insert y (insert x X)) = rank_of (insert x X)"
using assms cl_def by auto
also have "… ≤ Suc (rank_of X)"
using assms cl_subset_carrier by (auto intro: rank_of_insert_le)
also have "… = rank_of (insert y X)"
proof -
have "rank_of (insert y X) ≤ Suc (rank_of X)"
using assms cl_subset_carrier by (auto intro: rank_of_insert_le)
moreover have "rank_of (insert y X) ≠ rank_of X"
using assms cl_def by auto
moreover have "rank_of X ≤ rank_of (insert y X)"
using assms cl_subset_carrier by (auto intro: rank_of_mono)
ultimately show ?thesis by auto
qed
finally show ?thesis .
qed
ultimately show "rank_of (insert x (insert y X)) = rank_of (insert y X)" by auto
qed
lemma clI_insert:
assumes "x ∈ carrier"
assumes "indep X"
assumes "¬ indep (insert x X)"
shows "x ∈ cl X"
using ‹x ∈ carrier›
proof (rule clI)
have *: "X ⊆ carrier" using assms indep_subset_carrier by auto
then have **: "insert x X ⊆ carrier" using assms by auto
have "indep_in (insert x X) X" using assms by (auto intro: indep_inI)
then obtain B where B: "basis_in (insert x X) B" "X ⊆ B"
using assms indep_in_iff_subset_basis_in[OF **] by auto
have "x ∉ B"
proof (rule ccontr, goal_cases False)
case False
then have "indep_in (insert x X) (insert x X)"
using B indep_in_subset[OF ** basis_in_indep_in[OF **]] by auto
then show ?case using assms indep_in_indep by auto
qed
have "basis_in X B" using *
proof (rule basis_inI, goal_cases indep max_indep)
case indep
show ?case
proof (rule indep_in_supI[where ℰ = "insert x X"])
show "B ⊆ X" using B basis_in_subset_carrier[OF **] ‹x ∉ B› by auto
next
show "indep_in (insert x X) B" using basis_in_indep_in[OF ** B(1)] .
qed auto
next
case (max_indep y)
then have "¬ indep_in (insert x X) (insert y B)"
using B basis_in_max_indep_in[OF **] by auto
then show ?case by (auto intro: indep_in_subI_subset)
qed
then show "rank_of (insert x X) = rank_of X"
using B rank_of_eq_card_basis_in[OF *] rank_of_eq_card_basis_in[OF **] by auto
qed
lemma indep_in_carrier [simp]: "indep_in carrier = indep"
using indep_subset_carrier by (auto simp: indep_in_def fun_eq_iff)
context
fixes I
defines "I ≡ (λX. X ⊆ carrier ∧ (∀x∈X. x ∉ cl (X - {x})))"
begin
lemma I_mono: "I Y" if "Y ⊆ X" "I X" for X Y :: "'a set"
proof -
have "∀x∈Y. x ∉ cl (Y - {x})"
proof (intro ballI)
fix x assume x: "x ∈ Y"
with that have "cl (Y - {x}) ⊆ cl (X - {x})"
by (intro cl_mono) (auto simp: I_def)
with that and x show "x ∉ cl (Y - {x})" by (auto simp: I_def)
qed
with that show ?thesis by (auto simp: I_def)
qed
lemma clI':
assumes "I X" "x ∈ carrier" "¬I (insert x X)"
shows "x ∈ cl X"
proof -
from assms have x: "x ∉ X" by (auto simp: insert_absorb)
from assms obtain y where y: "y ∈ insert x X" "y ∈ cl (insert x X - {y})"
by (force simp: I_def)
show "x ∈ cl X"
proof (cases "x = y")
case True
thus ?thesis using assms x y by (auto simp: I_def)
next
case False
have "y ∈ cl (insert x X - {y})" by fact
also from False have "insert x X - {y} = insert x (X - {y})" by auto
finally have "y ∈ cl (insert x (X - {y})) - cl (X - {y})"
using assms False y unfolding I_def by blast
hence "x ∈ cl (insert y (X - {y}))"
using cl_augment[of "X - {y}" x y] assms False y by (auto simp: I_def)
also from y and False have "insert y (X - {y}) = X" by auto
finally show ?thesis .
qed
qed
lemma matroid_I: "matroid carrier I"
proof (unfold_locales, goal_cases)
show "finite carrier" by (rule carrier_finite)
next
case (4 X Y)
have "∀x∈Y. x ∉ cl (Y - {x})"
proof (intro ballI)
fix x assume x: "x ∈ Y"
with 4 have "cl (Y - {x}) ⊆ cl (X - {x})"
by (intro cl_mono) (auto simp: I_def)
with 4 and x show "x ∉ cl (Y - {x})" by (auto simp: I_def)
qed
with 4 show ?case by (auto simp: I_def)
next
case (5 X Y)
have "~(∃X Y. I X ∧ I Y ∧ card X < card Y ∧ (∀x∈Y-X. ¬I (insert x X)))"
proof
assume *: "∃X Y. I X ∧ I Y ∧ card X < card Y ∧ (∀x∈Y-X. ¬I (insert x X))" (is "∃X Y. ?P X Y")
define n where "n = Max ((λ(X, Y). card (X ∩ Y)) ` {(X, Y). ?P X Y})"
have "{(X, Y). ?P X Y} ⊆ Pow carrier × Pow carrier"
by (auto simp: I_def)
hence finite: "finite {(X, Y). ?P X Y}"
by (rule finite_subset) (insert carrier_finite, auto)
hence "n ∈ ((λ(X, Y). card (X ∩ Y)) ` {(X, Y). ?P X Y})"
unfolding n_def using * by (intro Max_in finite_imageI) auto
then obtain X Y where XY: "?P X Y" "n = card (X ∩ Y)"
by auto
hence finite': "finite X" "finite Y"
using finite_subset[OF _ carrier_finite] XY by (auto simp: I_def)
from XY finite' have "~(Y ⊆ X)"
using card_mono[of X Y] by auto
then obtain y where y: "y ∈ Y - X" by blast
have False
proof (cases "X ⊆ cl (Y - {y})")
case True
from y XY have [simp]: "y ∈ carrier" by (auto simp: I_def)
assume "X ⊆ cl (Y - {y})"
hence "cl X ⊆ cl (cl (Y - {y}))"
by (intro cl_mono cl_subset_carrier)
also have "… = cl (Y - {y})"
using XY by (intro cl_cl_absorb) (auto simp: I_def)
finally have "cl X ⊆ cl (Y - {y})" .
moreover have "y ∉ cl (Y - {y})"
using y I_def XY(1) by blast
ultimately have "y ∉ cl X" by blast
thus False unfolding I_def
using XY y clI' ‹y ∈ carrier› by blast
next
case False
with y XY have [simp]: "y ∈ carrier" by (auto simp: I_def)
assume "¬(X ⊆ cl (Y - {y}))"
then obtain t where t: "t ∈ X" "t ∉ cl (Y - {y})"
by auto
with XY have [simp]: "t ∈ carrier" by (auto simp: I_def)
have "t ∈ X - Y"
using t y clI[of t "Y - {y}"] by (cases "t = y") (auto simp: insert_absorb)
moreover have "I (Y - {y})" using XY(1) I_mono[of "Y - {y}" Y] by blast
ultimately have *: "I (insert t (Y - {y}))"
using clI'[of "Y - {y}" t] t by auto
from XY have "finite Y"
by (intro finite_subset[OF _ carrier_finite]) (auto simp: I_def)
moreover from y have "Y ≠ {}" by auto
ultimately have [simp]: "card (insert t (Y - {y})) = card Y" using ‹t ∈ X - Y› y
by (simp add: Suc_diff_Suc card_gt_0_iff)
have "∃x∈Y - X. I (insert x X)"
proof (rule ccontr)
assume "¬?thesis"
hence "?P X (insert t (Y - {y}))" using XY * ‹t ∈ X - Y›
by auto
hence "card (X ∩ insert t (Y - {y})) ≤ n"
unfolding n_def using finite by (intro Max_ge) auto
also have "X ∩ insert t (Y - {y}) = insert t ((X ∩ Y) - {y})"
using y ‹t ∈ X - Y› by blast
also have "card … = Suc (card (X ∩ Y))"
using y ‹t ∈ X - Y› ‹finite Y› by (simp add: card_insert)
finally show False using XY by simp
qed
with XY show False by blast
qed
thus False .
qed
with 5 show ?case by auto
qed (auto simp: I_def)
end
definition cl_in where "cl_in ℰ X = matroid.cl ℰ (indep_in ℰ) X"
lemma cl_eq_cl_in:
assumes "X ⊆ carrier"
shows "cl X = cl_in carrier X"
proof -
interpret ℰ: matroid carrier "indep_in carrier"
by (intro matroid_subset) auto
have "cl X = {x ∈ carrier. rank_of (insert x X) = rank_of X}"
unfolding cl_def by auto
also have "… = {x ∈ carrier. ℰ.rank_of (insert x X) = ℰ.rank_of X}"
using rank_of_sub_cong[of carrier] assms by auto
also have "… = cl_in carrier X"
unfolding cl_in_def ℰ.cl_def by auto
finally show ?thesis .
qed
context
fixes ℰ
assumes *: "ℰ ⊆ carrier"
begin
interpretation ℰ: matroid ℰ "indep_in ℰ"
using * by auto
lemma cl_inI_aux: "x ∈ ℰ.cl X ⟹ x ∈ cl_in ℰ X"
unfolding cl_in_def by auto
lemma cl_inD_aux: "x ∈ cl_in ℰ X ⟹ x ∈ ℰ.cl X"
unfolding cl_in_def by auto
lemma cl_inI:
assumes "X ⊆ ℰ"
assumes "x ∈ ℰ"
assumes "rank_of (insert x X) = rank_of X"
shows "x ∈ cl_in ℰ X"
proof -
have "ℰ.rank_of (insert x X) = rank_of (insert x X)" "ℰ.rank_of X = rank_of X"
using assms rank_of_sub_cong[OF *] by auto
then show ?thesis unfolding cl_in_def using assms by (auto intro: ℰ.clI)
qed
lemma cl_in_altdef:
assumes "X ⊆ ℰ"
shows "cl_in ℰ X = ⋃{Y ∈ Pow ℰ. X ⊆ Y ∧ rank_of Y = rank_of X}"
unfolding cl_in_def
proof (safe, goal_cases LTR RTL)
case (LTR x)
then have "x ∈ ⋃{Y ∈ Pow ℰ. X ⊆ Y ∧ ℰ.rank_of Y = ℰ.rank_of X}"
using ℰ.cl_altdef[OF assms] by auto
then obtain Y where Y: "x ∈ Y" "Y ∈ Pow ℰ" "X ⊆ Y" "ℰ.rank_of Y = ℰ.rank_of X" by auto
then show ?case using rank_of_sub_cong[OF *] by auto
next
case (RTL x Y)
then have "x ∈ ⋃{Y ∈ Pow ℰ. X ⊆ Y ∧ ℰ.rank_of Y = ℰ.rank_of X}"
using rank_of_sub_cong[OF *, of X] rank_of_sub_cong[OF *, of Y] by auto
then show ?case using ℰ.cl_altdef[OF assms] by auto
qed
lemma cl_in_subset_carrier: "cl_in ℰ X ⊆ ℰ"
using ℰ.cl_subset_carrier unfolding cl_in_def .
lemma cl_in_rank_of:
assumes "X ⊆ ℰ"
assumes "x ∈ cl_in ℰ X"
shows "rank_of (insert x X) = rank_of X"
proof -
have "ℰ.rank_of (insert x X) = ℰ.rank_of X"
using assms ℰ.cl_rank_of unfolding cl_in_def by auto
moreover have "ℰ.rank_of (insert x X) = rank_of (insert x X)"
using assms rank_of_sub_cong[OF *, of "insert x X"] cl_in_subset_carrier by auto
moreover have "ℰ.rank_of X = rank_of X"
using assms rank_of_sub_cong[OF *] by auto
ultimately show ?thesis by auto
qed
lemmas cl_inD = cl_in_rank_of cl_in_subset_carrier
lemma cl_in_subset:
assumes "X ⊆ ℰ"
shows "X ⊆ cl_in ℰ X"
using ℰ.cl_subset[OF assms] unfolding cl_in_def .
lemma cl_in_mono:
assumes "X ⊆ Y"
assumes "Y ⊆ ℰ"
shows "cl_in ℰ X ⊆ cl_in ℰ Y"
using ℰ.cl_mono[OF assms] unfolding cl_in_def .
lemma cl_in_insert_absorb:
assumes "X ⊆ ℰ"
assumes "x ∈ cl_in ℰ X"
shows "cl_in ℰ (insert x X) = cl_in ℰ X"
using assms ℰ.cl_insert_absorb unfolding cl_in_def by auto
lemma cl_in_augment:
assumes "X ⊆ ℰ"
assumes "x ∈ ℰ"
assumes "y ∈ cl_in ℰ (insert x X) - cl_in ℰ X"
shows "x ∈ cl_in ℰ (insert y X)"
using assms ℰ.cl_augment unfolding cl_in_def by auto
lemmas cl_inI_insert = cl_inI_aux[OF ℰ.clI_insert]
end
lemma cl_in_subI:
assumes "X ⊆ ℰ'" "ℰ' ⊆ ℰ" "ℰ ⊆ carrier"
shows "cl_in ℰ' X ⊆ cl_in ℰ X"
proof (safe, goal_cases elem)
case (elem x)
then have "x ∈ ℰ'" "rank_of (insert x X) = rank_of X"
using assms cl_inD[where ℰ = ℰ' and X = X] by auto
then show "x ∈ cl_in ℰ X" using assms by (auto intro: cl_inI)
qed
context
fixes ℰ
assumes *: "ℰ ⊆ carrier"
begin
interpretation ℰ: matroid ℰ "indep_in ℰ"
using * by auto
lemma cl_in_sub_cong:
assumes "X ⊆ ℰ'" "ℰ' ⊆ ℰ"
shows "ℰ.cl_in ℰ' X = cl_in ℰ' X"
proof (safe, goal_cases LTR RTL)
case (LTR x)
then have "x ∈ ℰ'" "ℰ.rank_of (insert x X) = ℰ.rank_of X"
using assms
ℰ.cl_in_rank_of[where ℰ = ℰ' and X = X and x = x]
ℰ.cl_in_subset_carrier[where ℰ = ℰ']
by auto
moreover have "ℰ.rank_of X = rank_of X"
using assms rank_of_sub_cong[OF *] by auto
moreover have "ℰ.rank_of (insert x X) = rank_of (insert x X)"
using assms rank_of_sub_cong[OF *, of "insert x X"] ‹x ∈ ℰ'› by auto
ultimately show ?case using assms * by (auto intro: cl_inI)
next
case (RTL x)
then have "x ∈ ℰ'" "rank_of (insert x X) = rank_of X"
using * assms cl_inD[where ℰ = ℰ' and X = X] by auto
moreover have "ℰ.rank_of X = rank_of X"
using assms rank_of_sub_cong[OF *] by auto
moreover have "ℰ.rank_of (insert x X) = rank_of (insert x X)"
using assms rank_of_sub_cong[OF *, of "insert x X"] ‹x ∈ ℰ'› by auto
ultimately show ?case using assms by (auto intro: ℰ.cl_inI)
qed
end
end
end