# 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
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

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```