Theory Undirected_Graph_Theory.Girth_Independence

theory Girth_Independence imports Connectivity
begin

section ‹ Girth and Independence ›
text ‹ We translate and extend on a number of definitions and lemmas on girth and independence
from Noschinski's ugraph representation \<^cite>‹"noschinski_2012"›. ›

context sgraph
begin

definition girth :: "enat" where
  "girth ≡ INF p∈ cycles. enat (walk_length p)"

lemma girth_acyclic: "cycles = {} ⟹ girth = ∞"
  unfolding girth_def using top_enat_def by simp

lemma girth_lte: "c ∈ cycles ⟹ girth ≤ walk_length c"
  using girth_def INF_lower by auto

lemma girth_obtains: 
  assumes "girth ≠ top"
  obtains c where "c ∈ cycles" and "walk_length c = girth"
  using enat_in_INF girth_def assms by (metis (full_types) the_enat.simps)

lemma girthI:
  assumes "c' ∈ cycles"
  assumes "⋀ c . c ∈ cycles ⟹ walk_length c' ≤ walk_length c"
  shows "girth = walk_length c'"
proof (rule ccontr)
  assume "girth ≠ walk_length c'"
  then have "girth < walk_length c'"
    using  assms girth_lte by fastforce
  then obtain c where "c ∈ cycles" and "walk_length c < walk_length c'"
    using girth_def by (metis enat_ord_simps(2) girth_obtains infinity_ilessE top_enat_def) 
  thus False using assms(2) less_imp_le_nat le_antisym
    by fastforce
qed

lemma (in fin_sgraph) girth_min_alt: 
  assumes "cycles ≠ {}"
  shows "girth = Min ((λ c . enat (walk_length c)) ` cycles)" (is "girth = Min ?A")
  unfolding girth_def using finite_cycles assms Min_Inf
  by (metis (full_types) INF_le_SUP bot_enat_def ccInf_empty ccSup_empty enat_ord_code(5) finite_imageI top_enat_def zero_enat_def) 

definition is_independent_set :: "'a set ⇒ bool" where
"is_independent_set vs ≡ vs ⊆ V ∧ (all_edges vs) ∩ E = {}"

text ‹ A More mathematical way of thinking about it ›
lemma is_independent_alt: "is_independent_set vs ⟷ vs ⊆ V ∧ (∀ v ∈ vs. ∀ u ∈ vs. ¬ vert_adj v u)"
  unfolding is_independent_set_def
proof (auto)
  fix v u assume ss: "vs ⊆ V" and inter: "all_edges vs ∩ E = {}" and vin: "v ∈ vs" and uin: "u ∈ vs" and adj: "vert_adj v u"
  then have inE: "{v, u} ∈ E" using vert_adj_def by simp
  then have imp: "{v, u} ∈ all_edges vs" using vin uin e_in_all_edges_ss vin uin
    by (simp add: ss)
  then show False
    using inE inter by blast 
next
  fix x assume "vs ⊆ V" "∀v∈vs. ∀u∈vs. ¬ vert_adj v u"  "x ∈ all_edges vs" "x ∈ E"
  then have "⋀ u v. {u, v} ⊆ vs ⟹ {u, v} ∉ E" by (simp add: vert_adj_def)
  then have "⋀ x . x ⊆ vs ⟹ card x = 2 ⟹ x ∉ E" by (metis card_2_iff) 
  then show False using all_edges_def
    by (metis (mono_tags, lifting) ‹x ∈ E› ‹x ∈ all_edges vs› mem_Collect_eq) 
qed

lemma singleton_independent_set: "v ∈ V ⟹ is_independent_set {v}"
  by (metis empty_subsetI insert_absorb2 insert_subset is_independent_alt
      singletonD singleton_not_edge vert_adj_def) 

definition independent_sets :: "'a set set" where
  "independent_sets ≡ {vs. is_independent_set vs}"

definition independence_number :: "enat"  where
   "independence_number ≡ SUP vs ∈ independent_sets. enat (card vs)"

abbreviation "α ≡ independence_number"

lemma independent_sets_mono:
  "vs ∈ independent_sets  ⟹ us ⊆ vs ⟹ us ∈ independent_sets "
  using Int_mono[OF all_edges_mono, of us vs "E" "E"]
  unfolding independent_sets_def is_independent_set_def by auto

lemma le_independence_iff:
  assumes "0 < k"
  shows "k ≤ α ⟷ k ∈ card ` independent_sets " (is "?L ⟷ ?R")
proof
  assume ?L
  then obtain vs where "vs ∈ independent_sets " and klt: "k ≤ card vs"
    using assms unfolding independence_number_def enat_le_Sup_iff by auto
  moreover
  obtain us where "us ⊆ vs" and "k = card us"
    using card_Ex_subset  klt by auto
  ultimately
  have "us ∈ independent_sets "  by (auto intro: independent_sets_mono)
  then show ?R using ‹k = card us› by auto
qed (auto intro: SUP_upper simp: independence_number_def)

lemma zero_less_independence:
  assumes "V ≠ {}"
  shows "0 < α"
proof -
  from assms obtain a where "a ∈ V" by auto
  then have "0 < enat (card {a})" "{a} ∈ independent_sets"
    using independent_sets_def is_independent_set_def all_edges_def singleton_independent_set by simp_all
  then show ?thesis unfolding independence_number_def less_SUP_iff ..
qed

end

context fin_sgraph
begin
lemma fin_independent_sets: "finite (independent_sets)" 
  unfolding independent_sets_def is_independent_set_def using finV by auto

lemma independence_le_card:
  shows "α  ≤ card V"
proof -
  { fix x assume "x ∈ independent_sets "
    then have "x ⊆ V" by (auto simp: independent_sets_def is_independent_set_def) }
  with finV show ?thesis unfolding independence_number_def
    by (intro SUP_least) (auto intro: card_mono)
qed

lemma independence_fin: "α ≠ ∞"
  using independence_le_card by (cases "α") auto

lemma independence_max_alt: "V ≠ {} ⟹ α = Max ((λ vs . enat (card vs)) ` independent_sets)"
  unfolding independence_number_def using Sup_enat_def zero_less_independence
  by (metis i0_less independence_fin independence_number_def)

lemma independent_sets_ne: 
  assumes "V ≠ {}"
  shows "independent_sets ≠ {}"
proof - 
  from assms obtain a where "a ∈ V" by auto
  then have "{a} ∈ independent_sets" using independent_sets_def singleton_independent_set by simp
  thus ?thesis by blast
qed

lemma independence_obtains: 
  assumes "V ≠ {}"
  obtains vs where "is_independent_set vs" and "card vs = α"
proof -
  have "α = Max ((λ vs . enat (card vs)) ` independent_sets)" using independence_max_alt assms by simp
  then obtain vs where "vs ∈ independent_sets" and "enat (card vs) = α" 
    using obtains_MIN[of "independent_sets" "λ vs . enat (card vs)"] assms fin_independent_sets independent_sets_ne
    by (metis (no_types, lifting) Max_in finite_imageI imageE image_is_empty) 
  thus ?thesis using independent_sets_def that by simp
qed
end
end