Theory Indep_System

(*
  File:     Indep_System.thy
  Author:   Jonas Keinholz

Independence systems
*)
section ‹Independence systems›
theory Indep_System
  imports Main
begin

lemma finite_psubset_inc_induct:
  assumes "finite A" "X ⊆ A"
  assumes "⋀X. (⋀Y. X ⊂ Y ⟹ Y ⊆ A ⟹ P Y) ⟹ P X"
  shows "P X"
proof -
  have wf: "wf {(X,Y). Y ⊂ X ∧ X ⊆ A}"
    by (rule wf_bounded_set[where ub = "λ_. A" and f = id]) (auto simp add: ‹finite A›)
  show ?thesis
  proof (induction X rule: wf_induct[OF wf, case_names step])
    case (step X)
    then show ?case using assms(3)[of X] by blast
  qed
qed

text ‹
  An \emph{independence system} consists of a finite ground set together with an independence
  predicate over the sets of this ground set. At least one set of the carrier is independent and
  subsets of independent sets are also independent.
›

locale indep_system =
  fixes carrier :: "'a set"
  fixes indep :: "'a set ⇒ bool"
  assumes carrier_finite: "finite carrier"
  assumes indep_subset_carrier: "indep X ⟹ X ⊆ carrier"
  assumes indep_ex: "∃X. indep X"
  assumes indep_subset: "indep X ⟹ Y ⊆ X ⟹ indep Y"
begin

lemmas psubset_inc_induct [case_names carrier step] = finite_psubset_inc_induct[OF carrier_finite]
lemmas indep_finite [simp] = finite_subset[OF indep_subset_carrier carrier_finite]

text ‹
  The empty set is independent.
›

lemma indep_empty [simp]: "indep {}"
  using indep_ex indep_subset by auto

subsection ‹Sub-independence systems›

text ‹
  A subset of the ground set induces an independence system.
›

definition indep_in where "indep_in ℰ X ⟷ X ⊆ ℰ ∧ indep X"

lemma indep_inI:
  assumes "X ⊆ ℰ"
  assumes "indep X"
  shows "indep_in ℰ X"
  using assms unfolding indep_in_def by auto

lemma indep_in_subI: "indep_in ℰ X ⟹ indep_in ℰ' (X ∩ ℰ')"
  using indep_subset unfolding indep_in_def by auto

lemma dep_in_subI:
  assumes "X ⊆ ℰ'"
  shows "¬ indep_in ℰ' X ⟹ ¬ indep_in ℰ X"
  using assms unfolding indep_in_def by auto

lemma indep_in_subset_carrier: "indep_in ℰ X ⟹ X ⊆ ℰ"
  unfolding indep_in_def by auto

lemma indep_in_subI_subset:
  assumes "ℰ' ⊆ ℰ"
  assumes "indep_in ℰ' X"
  shows "indep_in ℰ X"
proof -
  have "indep_in ℰ (X ∩ ℰ)" using assms indep_in_subI by auto
  moreover have "X ∩ ℰ = X" using assms indep_in_subset_carrier by auto
  ultimately show ?thesis by auto
qed

lemma indep_in_supI:
  assumes "X ⊆ ℰ'" "ℰ' ⊆ ℰ"
  assumes "indep_in ℰ X"
  shows "indep_in ℰ' X"
proof -
  have "X ∩ ℰ' = X" using assms by auto
  then show ?thesis using assms indep_in_subI[where ℰ = ℰ and ℰ' = ℰ' and X = X] by auto
qed

lemma indep_in_indep: "indep_in ℰ X ⟹ indep X"
  unfolding indep_in_def by auto

lemmas indep_inD = indep_in_subset_carrier indep_in_indep

lemma indep_system_subset [simp, intro]:
  assumes "ℰ ⊆ carrier"
  shows "indep_system ℰ (indep_in ℰ)"
  unfolding indep_system_def indep_in_def
  using finite_subset[OF assms carrier_finite] indep_subset by auto

text ‹
  We will work a lot with different sub structures. Therefore, every definition `foo' will have
  a counterpart `foo\_in' which has the ground set as an additional parameter. Furthermore, every
  result about `foo' will have another result about `foo\_in'. With this, we usually don't have to
  work with @{command interpretation} in proofs.
›

context
  fixes ℰ
  assumes "ℰ ⊆ carrier"
begin

interpretation ℰ: indep_system ℰ "indep_in ℰ"
  using ‹ℰ ⊆ carrier› by auto

lemma indep_in_sub_cong:
  assumes "ℰ' ⊆ ℰ"
  shows "ℰ.indep_in ℰ' X ⟷ indep_in ℰ' X"
  unfolding ℰ.indep_in_def indep_in_def using assms by auto

lemmas indep_in_ex = ℰ.indep_ex
lemmas indep_in_subset = ℰ.indep_subset
lemmas indep_in_empty = ℰ.indep_empty

end

subsection ‹Bases›

text ‹
  A \emph{basis} is a maximal independent set, i.\,e.\ an independent set which becomes dependent on
  inserting any element of the ground set.
›

definition basis where "basis X ⟷ indep X ∧ (∀x ∈ carrier - X. ¬ indep (insert x X))"

lemma basisI:
  assumes "indep X"
  assumes "⋀x. x ∈ carrier - X ⟹ ¬ indep (insert x X)"
  shows "basis X"
  using assms unfolding basis_def by auto

lemma basis_indep: "basis X ⟹ indep X"
  unfolding basis_def by auto

lemma basis_max_indep: "basis X ⟹ x ∈ carrier - X ⟹ ¬ indep (insert x X)"
  unfolding basis_def by auto

lemmas basisD = basis_indep basis_max_indep
lemmas basis_subset_carrier = indep_subset_carrier[OF basis_indep]
lemmas basis_finite [simp] = indep_finite[OF basis_indep]

lemma indep_not_basis:
  assumes "indep X"
  assumes "¬ basis X"
  shows "∃x ∈ carrier - X. indep (insert x X)"
  using assms basisI by auto

lemma basis_subset_eq:
  assumes "basis B⇩1"
  assumes "basis B⇩2"
  assumes "B⇩1 ⊆ B⇩2"
  shows "B⇩1 = B⇩2"
proof (rule ccontr)
  assume "B⇩1 ≠ B⇩2"
  then obtain x where x: "x ∈ B⇩2 - B⇩1" using assms by auto
  then have "insert x B⇩1 ⊆ B⇩2" using assms by auto
  then have "indep (insert x B⇩1)" using assms basis_indep[of B⇩2] indep_subset by auto
  moreover have "x ∈ carrier - B⇩1" using assms x basis_subset_carrier by auto
  ultimately show False using assms basisD by auto
qed

definition basis_in where
  "basis_in ℰ X ⟷ indep_system.basis ℰ (indep_in ℰ) X"

lemma basis_iff_basis_in: "basis B ⟷ basis_in carrier B"
proof -
  interpret ℰ: indep_system carrier "indep_in carrier"
    by auto

  show "basis B ⟷ basis_in carrier B"
    unfolding basis_in_def
  proof (standard, goal_cases LTR RTL)
    case LTR
    show ?case
    proof (rule ℰ.basisI)
      show "indep_in carrier B" using LTR basisD indep_subset_carrier indep_inI by auto
    next
      fix x
      assume "x ∈ carrier - B"
      then have "¬ indep (insert x B)" using LTR basisD by auto
      then show "¬ indep_in carrier (insert x B)" using indep_inD by auto
    qed
  next
    case RTL
    show ?case
    proof (rule basisI)
      show "indep B" using RTL ℰ.basis_indep indep_inD by blast
    next
      fix x
      assume "x ∈ carrier - B"
      then have "¬ indep_in carrier (insert x B)" using RTL ℰ.basisD by auto
      then show "¬ indep (insert x B)" using indep_subset_carrier indep_inI by blast
    qed
  qed
qed

context
  fixes ℰ
  assumes "ℰ ⊆ carrier"
begin

interpretation ℰ: indep_system ℰ "indep_in ℰ"
  using ‹ℰ ⊆ carrier› by auto

lemma basis_inI_aux: "ℰ.basis X ⟹ basis_in ℰ X"
  unfolding basis_in_def by auto

lemma basis_inD_aux: "basis_in ℰ X ⟹ ℰ.basis X"
  unfolding basis_in_def by auto

lemma not_basis_inD_aux: "¬ basis_in ℰ X ⟹ ¬ ℰ.basis X"
  using basis_inI_aux by auto

lemmas basis_inI = basis_inI_aux[OF ℰ.basisI]
lemmas basis_in_indep_in = ℰ.basis_indep[OF basis_inD_aux]
lemmas basis_in_max_indep_in = ℰ.basis_max_indep[OF basis_inD_aux]
lemmas basis_inD = ℰ.basisD[OF basis_inD_aux]
lemmas basis_in_subset_carrier = ℰ.basis_subset_carrier[OF basis_inD_aux]
lemmas basis_in_finite = ℰ.basis_finite[OF basis_inD_aux]
lemmas indep_in_not_basis_in = ℰ.indep_not_basis[OF _ not_basis_inD_aux]
lemmas basis_in_subset_eq = ℰ.basis_subset_eq[OF basis_inD_aux basis_inD_aux]

end

context
  fixes ℰ
  assumes *: "ℰ ⊆ carrier"
begin

interpretation ℰ: indep_system ℰ "indep_in ℰ"
  using * by auto

lemma basis_in_sub_cong:
  assumes "ℰ' ⊆ ℰ"
  shows "ℰ.basis_in ℰ' B ⟷ basis_in ℰ' B"
proof (safe, goal_cases LTR RTL)
  case LTR
  show ?case
  proof (rule basis_inI)
    show "ℰ' ⊆ carrier" using assms * by auto
  next
    show "indep_in ℰ' B"
      using * assms LTR ℰ.basis_in_subset_carrier ℰ.basis_in_indep_in indep_in_sub_cong by auto
  next
    fix x
    assume "x ∈ ℰ' - B"
    then show "¬ indep_in ℰ' (insert x B)"
      using * assms LTR ℰ.basis_in_max_indep_in ℰ.basis_in_subset_carrier indep_in_sub_cong by auto
  qed
next
  case RTL
  show ?case
  proof (rule ℰ.basis_inI)
    show "ℰ' ⊆ ℰ" using assms by auto
  next
    show "ℰ.indep_in ℰ' B"
      using * assms RTL basis_in_subset_carrier basis_in_indep_in indep_in_sub_cong by auto
  next
    fix x
    assume "x ∈ ℰ' - B"
    then show "¬ ℰ.indep_in ℰ' (insert x B)"
      using * assms RTL basis_in_max_indep_in basis_in_subset_carrier indep_in_sub_cong by auto
  qed
qed

end

subsection ‹Circuits›

text ‹
  A \emph{circuit} is a minimal dependent set, i.\,e.\ a set which becomes independent on removing
  any element of the ground set.
›

definition circuit where "circuit X ⟷ X ⊆ carrier ∧ ¬ indep X ∧ (∀x ∈ X. indep (X - {x}))"

lemma circuitI:
  assumes "X ⊆ carrier"
  assumes "¬ indep X"
  assumes "⋀x. x ∈ X ⟹ indep (X - {x})"
  shows "circuit X"
  using assms unfolding circuit_def by auto

lemma circuit_subset_carrier: "circuit X ⟹ X ⊆ carrier"
  unfolding circuit_def by auto
lemmas circuit_finite [simp] = finite_subset[OF circuit_subset_carrier carrier_finite]

lemma circuit_dep: "circuit X ⟹ ¬ indep X"
  unfolding circuit_def by auto

lemma circuit_min_dep: "circuit X ⟹ x ∈ X ⟹ indep (X - {x})"
  unfolding circuit_def by auto

lemmas circuitD = circuit_subset_carrier circuit_dep circuit_min_dep

lemma circuit_nonempty: "circuit X ⟹ X ≠ {}"
  using circuit_dep indep_empty by blast

lemma dep_not_circuit:
  assumes "X ⊆ carrier"
  assumes "¬ indep X"
  assumes "¬ circuit X"
  shows "∃x ∈ X. ¬ indep (X - {x})"
  using assms circuitI by auto

lemma circuit_subset_eq:
  assumes "circuit C⇩1"
  assumes "circuit C⇩2"
  assumes "C⇩1 ⊆ C⇩2"
  shows "C⇩1 = C⇩2"
proof (rule ccontr)
  assume "C⇩1 ≠ C⇩2"
  then obtain x where "x ∉ C⇩1" "x ∈ C⇩2" using assms by auto
  then have "indep C⇩1" using indep_subset ‹C⇩1 ⊆ C⇩2› circuit_min_dep[OF ‹circuit C⇩2›, of x] by auto
  then show False using assms circuitD by auto
qed

definition circuit_in where
  "circuit_in ℰ X ⟷ indep_system.circuit ℰ (indep_in ℰ) X"

context
  fixes ℰ
  assumes "ℰ ⊆ carrier"
begin

interpretation ℰ: indep_system ℰ "indep_in ℰ"
  using ‹ℰ ⊆ carrier› by auto

lemma circuit_inI_aux: "ℰ.circuit X ⟹ circuit_in ℰ X"
  unfolding circuit_in_def by auto

lemma circuit_inD_aux: "circuit_in ℰ X ⟹ ℰ.circuit X"
  unfolding circuit_in_def by auto

lemma not_circuit_inD_aux: "¬ circuit_in ℰ X ⟹ ¬ ℰ.circuit X"
  using circuit_inI_aux by auto

lemmas circuit_inI = circuit_inI_aux[OF ℰ.circuitI]

lemmas circuit_in_subset_carrier = ℰ.circuit_subset_carrier[OF circuit_inD_aux]
lemmas circuit_in_finite = ℰ.circuit_finite[OF circuit_inD_aux]
lemmas circuit_in_dep_in = ℰ.circuit_dep[OF circuit_inD_aux]
lemmas circuit_in_min_dep_in = ℰ.circuit_min_dep[OF circuit_inD_aux]
lemmas circuit_inD = ℰ.circuitD[OF circuit_inD_aux]
lemmas circuit_in_nonempty = ℰ.circuit_nonempty[OF circuit_inD_aux]
lemmas dep_in_not_circuit_in = ℰ.dep_not_circuit[OF _ _ not_circuit_inD_aux]
lemmas circuit_in_subset_eq = ℰ.circuit_subset_eq[OF circuit_inD_aux circuit_inD_aux]

end

lemma circuit_in_subI:
  assumes "ℰ' ⊆ ℰ" "ℰ ⊆ carrier"
  assumes "circuit_in ℰ' C"
  shows "circuit_in ℰ C"
proof (rule circuit_inI)
  show "ℰ ⊆ carrier" using assms by auto
next
  show "C ⊆ ℰ" using assms circuit_in_subset_carrier[of ℰ' C] by auto
next
  show "¬ indep_in ℰ C"
    using assms
      circuit_in_dep_in[where ℰ = ℰ' and X = C]
      circuit_in_subset_carrier dep_in_subI[where ℰ' = ℰ' and ℰ = ℰ]
    by auto
next
  fix x
  assume "x ∈ C"
  then show "indep_in ℰ (C - {x})"
    using assms circuit_in_min_dep_in indep_in_subI_subset by auto
qed

lemma circuit_in_supI:
  assumes "ℰ' ⊆ ℰ" "ℰ ⊆ carrier" "C ⊆ ℰ'"
  assumes "circuit_in ℰ C"
  shows "circuit_in ℰ' C"
proof (rule circuit_inI)
  show "ℰ' ⊆ carrier" using assms by auto
next
  show "C ⊆ ℰ'" using assms by auto
next
  have "¬ indep_in ℰ C" using assms circuit_in_dep_in by auto
  then show "¬ indep_in ℰ' C" using assms dep_in_subI[of C ℰ] by auto
next
  fix x
  assume "x ∈ C"
  then have "indep_in ℰ (C - {x})" using assms circuit_in_min_dep_in by auto
  then have "indep_in ℰ' ((C - {x}) ∩ ℰ')" using indep_in_subI by auto
  moreover have "(C - {x}) ∩ ℰ' = C - {x}" using assms circuit_in_subset_carrier by auto
  ultimately show "indep_in ℰ' (C - {x})" by auto
qed

context
  fixes ℰ
  assumes *: "ℰ ⊆ carrier"
begin

interpretation ℰ: indep_system ℰ "indep_in ℰ"
  using * by auto

lemma circuit_in_sub_cong:
  assumes "ℰ' ⊆ ℰ"
  shows "ℰ.circuit_in ℰ' C ⟷ circuit_in ℰ' C"
proof (safe, goal_cases LTR RTL)
  case LTR
  show ?case
  proof (rule circuit_inI)
    show "ℰ' ⊆ carrier" using assms * by auto
  next
    show "C ⊆ ℰ'"
      using assms LTR ℰ.circuit_in_subset_carrier by auto
  next
    show "¬ indep_in ℰ' C"
      using assms LTR ℰ.circuit_in_dep_in indep_in_sub_cong[OF *] by auto
  next
    fix x
    assume "x ∈ C"
    then show "indep_in ℰ' (C - {x})"
      using assms LTR ℰ.circuit_in_min_dep_in indep_in_sub_cong[OF *] by auto
  qed
next
  case RTL
  show ?case
  proof (rule ℰ.circuit_inI)
    show "ℰ' ⊆ ℰ" using assms * by auto
  next
    show "C ⊆ ℰ'"
      using assms * RTL circuit_in_subset_carrier by auto
  next
    show "¬ ℰ.indep_in ℰ' C"
      using assms * RTL circuit_in_dep_in indep_in_sub_cong[OF *] by auto
  next
    fix x
    assume "x ∈ C"
    then show "ℰ.indep_in ℰ' (C - {x})"
      using assms * RTL circuit_in_min_dep_in indep_in_sub_cong[OF *] by auto
  qed
qed

end

lemma circuit_imp_circuit_in:
  assumes "circuit C"
  shows "circuit_in carrier C"
proof (rule circuit_inI)
  show "C ⊆ carrier" using circuit_subset_carrier[OF assms] .
next
  show "¬ indep_in carrier C" using circuit_dep[OF assms] indep_in_indep by auto
next
  fix x
  assume "x ∈ C"
  then have "indep (C - {x})" using circuit_min_dep[OF assms] by auto
  then show "indep_in carrier (C - {x})" using circuit_subset_carrier[OF assms] by (auto intro: indep_inI)
qed auto

subsection ‹Relation between independence and bases›

text ‹
  A set is independent iff it is a subset of a basis.
›

lemma indep_imp_subset_basis:
  assumes "indep X"
  shows "∃B. basis B ∧ X ⊆ B"
  using assms
proof (induction X rule: psubset_inc_induct)
  case carrier
  show ?case using indep_subset_carrier[OF assms] .
next
  case (step X)
  {
    assume "¬ basis X"
    then obtain x where "x ∈ carrier" "x ∉ X" "indep (insert x X)"
      using step.prems indep_not_basis by auto
    then have ?case using step.IH[of "insert x X"] indep_subset_carrier by auto
  }
  then show ?case by auto
qed

lemmas subset_basis_imp_indep = indep_subset[OF basis_indep]

lemma indep_iff_subset_basis: "indep X ⟷ (∃B. basis B ∧ X ⊆ B)"
  using indep_imp_subset_basis subset_basis_imp_indep by auto

lemma basis_ex: "∃B. basis B"
  using indep_imp_subset_basis[OF indep_empty] by auto

context
  fixes ℰ
  assumes *: "ℰ ⊆ carrier"
begin

interpretation ℰ: indep_system ℰ "indep_in ℰ"
  using * by auto

lemma indep_in_imp_subset_basis_in:
  assumes "indep_in ℰ X"
  shows "∃B. basis_in ℰ B ∧ X ⊆ B"
  unfolding basis_in_def using ℰ.indep_imp_subset_basis[OF assms] .

lemmas subset_basis_in_imp_indep_in = indep_in_subset[OF * basis_in_indep_in[OF *]]

lemma indep_in_iff_subset_basis_in: "indep_in ℰ X ⟷ (∃B. basis_in ℰ B ∧ X ⊆ B)"
  using indep_in_imp_subset_basis_in subset_basis_in_imp_indep_in by auto

lemma basis_in_ex: "∃B. basis_in ℰ B"
  unfolding basis_in_def using ℰ.basis_ex .

lemma basis_in_subI:
  assumes "ℰ' ⊆ ℰ" "ℰ ⊆ carrier"
  assumes "basis_in ℰ' B"
  shows "∃B' ⊆ ℰ - ℰ'. basis_in ℰ (B ∪ B')"
proof -
  have "indep_in ℰ B" using assms basis_in_indep_in indep_in_subI_subset by auto
  then obtain B' where B': "basis_in ℰ B'" "B ⊆ B'"
    using assms indep_in_imp_subset_basis_in[of B] by auto
  show ?thesis
  proof (rule exI)
    have "B' - B ⊆ ℰ - ℰ'"
    proof
      fix x
      assume *: "x ∈ B' - B"
      then have "x ∈ ℰ" "x ∉ B"
        using assms ‹basis_in ℰ B'› basis_in_subset_carrier[of ℰ] by auto
      moreover {
        assume "x ∈ ℰ'"
        moreover have "indep_in ℰ (insert x B)"
          using * assms indep_in_subset[OF _ basis_in_indep_in] B' by auto
        ultimately have "indep_in ℰ' (insert x B)"
          using assms basis_in_subset_carrier unfolding indep_in_def by auto
        then have False using assms * ‹x ∈ ℰ'› basis_in_max_indep_in by auto
      }
      ultimately show "x ∈ ℰ - ℰ'"  by auto
    qed
    moreover have "B ∪ (B' - B) = B'" using ‹B ⊆ B'› by auto
    ultimately show "B' - B ⊆ ℰ - ℰ' ∧ basis_in ℰ (B ∪ (B' - B))"
      using ‹basis_in ℰ B'› by auto
  qed
qed

lemma basis_in_supI:
  assumes "B ⊆ ℰ'" "ℰ' ⊆ ℰ" "ℰ ⊆ carrier"
  assumes "basis_in ℰ B"
  shows "basis_in ℰ' B"
proof (rule basis_inI)
  show "ℰ' ⊆ carrier" using assms by auto
next
  show "indep_in ℰ' B"
  proof -
    have "indep_in ℰ' (B ∩ ℰ')"
      using assms basis_in_indep_in[of ℰ B] indep_in_subI by auto
    moreover have "B ∩ ℰ' = B" using assms by auto
    ultimately show ?thesis by auto
  qed
next
  show "⋀x. x ∈ ℰ' - B ⟹ ¬ indep_in ℰ' (insert x B)"
    using assms basis_in_subset_carrier basis_in_max_indep_in dep_in_subI[of _ ℰ ℰ'] by auto
qed

end

subsection ‹Relation between dependence and circuits›

text ‹
  A set is dependent iff it contains a circuit.
›

lemma dep_imp_supset_circuit:
  assumes "X ⊆ carrier"
  assumes "¬ indep X"
  shows "∃C. circuit C ∧ C ⊆ X"
  using assms
proof (induction X rule: remove_induct)
  case (remove X)
  {
    assume "¬ circuit X"
    then obtain x where "x ∈ X" "¬ indep (X - {x})"
      using remove.prems dep_not_circuit by auto
    then obtain C where "circuit C" "C ⊆ X - {x}"
      using remove.prems remove.IH[of x] by auto
    then have ?case by auto
  }
  then show ?case using remove.prems by auto
qed (auto simp add: carrier_finite finite_subset)

lemma supset_circuit_imp_dep:
  assumes "circuit C ∧ C ⊆ X"
  shows "¬ indep X"
  using assms indep_subset circuit_dep by auto

lemma dep_iff_supset_circuit:
  assumes "X ⊆ carrier"
  shows "¬ indep X ⟷ (∃C. circuit C ∧ C ⊆ X)"
  using assms dep_imp_supset_circuit supset_circuit_imp_dep by auto

context
  fixes ℰ
  assumes "ℰ ⊆ carrier"
begin

interpretation ℰ: indep_system ℰ "indep_in ℰ"
  using ‹ℰ ⊆ carrier› by auto

lemma dep_in_imp_supset_circuit_in:
  assumes "X ⊆ ℰ"
  assumes "¬ indep_in ℰ X"
  shows "∃C. circuit_in ℰ C ∧ C ⊆ X"
  unfolding circuit_in_def using ℰ.dep_imp_supset_circuit[OF assms] .

lemma supset_circuit_in_imp_dep_in:
  assumes "circuit_in ℰ C ∧ C ⊆ X"
  shows "¬ indep_in ℰ X"
  using assms ℰ.supset_circuit_imp_dep unfolding circuit_in_def by auto

lemma dep_in_iff_supset_circuit_in:
  assumes "X ⊆ ℰ"
  shows "¬ indep_in ℰ X ⟷ (∃C. circuit_in ℰ C ∧ C ⊆ X)"
  using assms dep_in_imp_supset_circuit_in supset_circuit_in_imp_dep_in by auto

end

subsection ‹Ranks›

definition lower_rank_of :: "'a set ⇒ nat" where
  "lower_rank_of carrier' ≡ Min {card B | B. basis_in carrier' B}"

definition upper_rank_of :: "'a set ⇒ nat" where
  "upper_rank_of carrier' ≡ Max {card B | B. basis_in carrier' B}"

lemma collect_basis_finite: "finite (Collect basis)"
proof -
  have "Collect basis ⊆ {X. X ⊆ carrier}"
    using basis_subset_carrier by auto
  moreover have "finite …"
    using carrier_finite by auto
  ultimately show ?thesis using finite_subset by auto
qed

context
  fixes ℰ
  assumes *: "ℰ ⊆ carrier"
begin

interpretation ℰ: indep_system ℰ "indep_in ℰ"
  using * by auto

lemma collect_basis_in_finite: "finite (Collect (basis_in ℰ))"
  unfolding basis_in_def using ℰ.collect_basis_finite .

lemma lower_rank_of_le: "lower_rank_of ℰ ≤ card ℰ"
proof -
  have "∃n ∈ {card B | B. basis_in ℰ B}. n ≤ card ℰ"
    using card_mono[OF ℰ.carrier_finite basis_in_subset_carrier[OF *]] basis_in_ex[OF *] by auto
  moreover have "finite {card B | B. basis_in ℰ B}"
    using collect_basis_in_finite by auto
  ultimately show ?thesis
    unfolding lower_rank_of_def using basis_ex Min_le_iff by auto
qed

lemma upper_rank_of_le: "upper_rank_of ℰ ≤ card ℰ"
proof -
  have "∀n ∈ {card B | B. basis_in ℰ B}. n ≤ card ℰ"
    using card_mono[OF ℰ.carrier_finite basis_in_subset_carrier[OF *]] by auto
  then show ?thesis
    unfolding upper_rank_of_def using basis_in_ex[OF *] collect_basis_in_finite by auto
qed

context
  fixes ℰ'
  assumes **: "ℰ' ⊆ ℰ"
begin

interpretation ℰ'⇩1: indep_system ℰ' "indep_in ℰ'"
  using * ** by auto
interpretation ℰ'⇩2: indep_system ℰ' "ℰ.indep_in ℰ'"
  using * ** by auto

lemma lower_rank_of_sub_cong:
  shows "ℰ.lower_rank_of ℰ' = lower_rank_of ℰ'"
proof -
  have "⋀B. ℰ'⇩1.basis B ⟷ ℰ'⇩2.basis B"
    using ** basis_in_sub_cong[OF *, of ℰ']
    unfolding basis_in_def ℰ.basis_in_def by auto
  then show ?thesis
    unfolding lower_rank_of_def ℰ.lower_rank_of_def
    using basis_in_sub_cong[OF * **]
    by auto
qed

lemma upper_rank_of_sub_cong:
  shows "ℰ.upper_rank_of ℰ' = upper_rank_of ℰ'"
proof -
  have "⋀B. ℰ'⇩1.basis B ⟷ ℰ'⇩2.basis B"
    using ** basis_in_sub_cong[OF *, of ℰ']
    unfolding basis_in_def ℰ.basis_in_def by auto
  then show ?thesis
    unfolding upper_rank_of_def ℰ.upper_rank_of_def
    using basis_in_sub_cong[OF * **]
    by auto
qed

end

end

end

end