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 B1"
  assumes "basis B2"
  shows "card B1 = card B2"
proof (rule ccontr, goal_cases False)
  case False
  then have "card B1 < card B2  card B2 < card B1" by auto
  moreover {
    fix B1 B2
    assume "basis B1" "basis B2" "card B1 < card B2"
    then obtain x where "x  B2 - B1" "indep (insert x B1)"
      using augment basisD by blast
    then have "x  carrier - B1"
      using basis B1 basisD indep_subset_carrier by blast
    then have "¬ indep (insert x B1)" using basis B1 basisD by auto
    then have "False" using indep (insert x B1) 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 B1" "basis B2" "x  B1 - B2"
  shows "y  B2 - B1. basis (insert y (B1 - {x}))"
proof -
  let ?B1 = "B1 - {x}"
  have "card ?B1 < card B2"
    using assms basis_card[of B1 B2] card_Diff1_less[OF basis_finite, of B1] by auto
  moreover have "indep ?B1" using assms basis_indep[of B1] indep_subset[of B1 ?B1] by auto
  ultimately obtain y where y: "y  B2 - ?B1" "indep (insert y ?B1)"
    using assms augment[of B2 ?B1] basis_indep by auto
  let ?B1' = "insert y ?B1"
  have "basis ?B1'" using indep ?B1'
  proof (rule basisI, goal_cases "insert")
    case (insert x)
    have "card (insert x ?B1') > card B1"
    proof -
      have "card (insert x ?B1') = Suc (card ?B1')"
        using insert card.insert_remove[OF indep_finite, of ?B1'] y by auto
      also have " = Suc (Suc (card ?B1))"
        using card.insert_remove[OF indep_finite, of ?B1] indep ?B1 y by auto
      also have " = Suc (card B1)"
        using assms basis_finite[of B1] card.remove[of B1] by auto
      finally show ?thesis by auto
    qed
    then have "¬indep (insert x (insert y ?B1))"
      using assms basis_indep_card[of "insert x (insert y ?B1)" B1] by auto
    moreover have "insert x (insert y ?B1)  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  B1" "basis_in  B2" "x  B1 - B2"
  shows "y  B2 - B1. basis_in  (insert y (B1 - {x}))"
  using assms ℰ.basis_augment unfolding basis_in_def by auto

end

subsection ‹Circuits›

lemma circuit_elim:
  assumes "circuit C1" "circuit C2" "C1  C2" "x  C1  C2"
  shows "C3  (C1  C2) - {x}. circuit C3"
proof -
  let ?C = "(C1  C2) - {x}"
  let ?carrier = "C1  C2"

  have assms': "circuit_in carrier C1" "circuit_in carrier C2"
    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  C2" "y  C1" using assms circuit_subset_eq by blast
    then have "indep_in ?carrier (C2 - {y})"
      using assms' circuit_in_min_dep_in[OF * circuit_in_supI[OF *, of C2]] by auto
    then obtain B where B: "basis_in ?carrier B" "C2 - {y}  B"
      using * assms indep_in_imp_subset_basis_in[of ?carrier "C2 - {y}"] by auto

    have "y  B"
    proof (rule ccontr, goal_cases False)
      case False
      then have "C2  B" using B by auto
      moreover have "circuit_in ?carrier C2" 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 "C1 - B  {}"
    proof (rule ccontr, goal_cases False)
      case False
      then have "C1 - (C1  B) = {}" by auto
      then have "C1 = C1  B" using assms circuit_subset_eq by auto
      moreover have "indep (C1  B)"
        using assms B basis_in_indep_in[OF *] indep_in_subset[OF *, of B "C1  B"] indep_in_indep
        by auto
      ultimately show ?case using assms circuitD by auto
    qed
    then obtain z where z: "z  C1" "z  B" by auto

    have "y  z" using y z by auto
    have "x  C1" "x  C2" 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 (C1  C2 - {y, z})" using finite ?carrier by auto
    next
      show "B  C1  C2 - {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  C2 z  C1 y  z card_Diff_subset_Int by auto
    also have " < card ?carrier - 1"
    proof -
      have "card ?carrier = card C1 + card C2 - card (C1  C2)"
        using assms finite ?carrier card_Un_Int[of C1 C2] by auto
      also have " = card C1 + (card C2 - card (C1  C2))"
        using assms finite ?carrier card_mono[of C2] by auto
      also have " = card C1 + card (C2 - C1)"
      proof -
        have "card (C2 - C1) = card C2 - card (C2  C1)"
          using assms finite ?carrier card_Diff_subset_Int[of C2 C1] by auto
        also have " = card C2 - card (C1  C2)" by (simp add: inf_commute)
        finally show ?thesis by auto
      qed
      finally have "card (C1  C2) = card C1 + card (C2 - C1)" .
      moreover have "card C1 > 0" using assms circuit_nonempty finite ?carrier by auto
      moreover have "card (C2 - C1) > 0" using assms finite ?carrier y  C2 y  C1 by auto
      ultimately show ?thesis by auto
    qed
    also have " = card ?C"
      using finite ?carrier card_Diff_singleton x  C1 x  C2 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  C1" "circuit_in  C2" "C1  C2" "x  C1  C2"
  shows "C3  (C1  C2) - {x}. circuit_in  C3"
  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 BX where BX: "basis_in X  BX" using assms basis_in_ex[of X] by auto
  moreover obtain BY where BY: "basis_in Y BY" using assms basis_in_ex[of Y] by auto
  moreover have "card BX  card BY"
    using assms basis_in_indep_in_card[OF _ _ BY] basis_in_indep_in[OF _ BX] 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 BX where BX: "basis_in X BX" using assms basis_in_ex[of X] by auto

    have "basis_in (insert x X) BX"
    proof -
      have "rank_of BX = card BX  rank_of BX = rank_of (insert x X)"
      proof -
        have "rank_of BX = card BX  rank_of BX = rank_of X"
          using assms BX
            basis_in_subset_carrier[where= X and X = BX]
            basis_in_iff_rank_of[where= X and X = BX]
          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 _ BX] x  carrier basis_in_iff_rank_of[of "insert x X" BX]
        by auto
    qed

    have "indep_in (insert x Y) BX"
      using assms basis_in_indep_in[OF _ BX] indep_in_subI_subset[of X "insert x Y"] by auto
    then obtain BY where BY: "basis_in (insert x Y) BY" "BX  BY"
      using assms x  carrier indep_in_iff_subset_basis_in[of "insert x Y" BX] by auto

    have "basis_in Y BY"
    proof -
      have "x  BY"
      proof (rule ccontr, goal_cases False)
        case False
        then have "insert x BX  BY" using BX  BY by auto
        then have "indep_in (insert x Y) (insert x BX)"
          using assms x  carrier
            BY basis_in_indep_in[where= "insert x Y" and X = BY]
            indep_in_subset[where= "insert x Y" and X = BY and Y = "insert x BX"]
          by auto
        then have "indep_in (insert x X) (insert x BX)"
          using assms BX
            basis_in_subset_carrier[where= X and X = BX]
            indep_in_supI[where= "insert x Y" and ℰ' = "insert x X" and X = "insert x BX"]
          by auto
        moreover have "x  insert x X - BX"
          using assms x  X BX basis_in_subset_carrier[where= X and X = BX] by auto
        ultimately show ?case
          using assms x  carrier basis_in (insert x X) BX
            basis_in_max_indep_in[where= "insert x X" and X = BX and x = x]
          by auto
      qed
      then show ?thesis
      using assms x  carrier BY basis_in_subset_carrier[of "insert x Y" BY]
        basis_in_supI[where= "insert x Y" and ℰ' = Y and B = BY] by auto
    qed

    show "rank_of (insert x Y) = rank_of Y"
    proof -
      have "rank_of (insert x Y) = card BY"
        using assms x  carrier basis_in (insert x Y) BY basis_in_subset_carrier
        using basis_in_iff_rank_of[where= "insert x Y" and X = BY]
        by auto
      also have " = rank_of Y"
        using assms x  carrier basis_in Y BY basis_in_subset_carrier
        using basis_in_iff_rank_of[where= Y and X = BY]
        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  (xX. x  cl (X - {x})))"
begin

lemma I_mono: "I Y" if "Y  X" "I X" for X Y :: "'a set"
proof -
  have "xY. 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 "xY. 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  (xY-X. ¬I (insert x X)))"
  proof
    assume *: "X Y. I X  I Y  card X < card Y  (xY-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 "xY - 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