Theory Matroid

(*
  File:     Matroid.thy
  Author:   Jonas Keinholz
*)
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_remove[OF indep_finite, of ?B⇩1'] y by auto
      also have "… = Suc (Suc (card ?B⇩1))"
        using card.insert_remove[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_remove[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 simp: simp del: card_Diff_insert)
  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_remove)
        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