# Theory Ugraphs

theory Ugraphs
imports
Girth_Chromatic_Misc
begin

section ‹Undirected Simple Graphs›

text ‹
In this section, we define some basics of graph theory needed to formalize
the Chromatic-Girth theorem.
›

text ‹
For readability, we introduce synonyms for the types of vertexes, edges,
graphs and walks.
›
type_synonym uvert = nat
type_synonym uedge = "nat set"
type_synonym ugraph = "uvert set × uedge set"
type_synonym uwalk = "uvert list"

abbreviation uedges :: "ugraph ⇒ uedge set" where
"uedges G ≡ snd G"

abbreviation uverts :: "ugraph ⇒ uvert set" where
"uverts G ≡ fst G"

fun mk_uedge :: "uvert × uvert ⇒ uedge" where
"mk_uedge (u,v) = {u,v}"

text ‹All edges over a set of vertexes @{term S}:›
definition "all_edges S ≡ mk_uedge  {uv ∈ S × S. fst uv ≠ snd uv}"

definition uwellformed :: "ugraph ⇒ bool" where
"uwellformed G ≡ (∀e∈uedges G. card e = 2 ∧ (∀u ∈ e. u ∈ uverts G))"

fun uwalk_edges :: "uwalk ⇒ uedge list" where
"uwalk_edges [] = []"
| "uwalk_edges [x] = []"
| "uwalk_edges (x # y # ys) = {x,y} # uwalk_edges (y # ys)"

definition uwalk_length :: "uwalk ⇒ nat" where
"uwalk_length p ≡ length (uwalk_edges p)"

definition uwalks :: "ugraph ⇒ uwalk set" where
"uwalks G ≡ {p. set p ⊆ uverts G ∧ set (uwalk_edges p) ⊆ uedges G ∧ p ≠ []}"

definition ucycles :: "ugraph ⇒ uwalk set" where
"ucycles G ≡ {p. uwalk_length p ≥ 3 ∧ p ∈ uwalks G ∧ distinct (tl p) ∧ hd p = last p}"

definition remove_vertex :: "ugraph ⇒ nat ⇒ ugraph" ("_ -- _" [60,60] 60) where
"remove_vertex G u ≡ (uverts G - {u}, uedges G - {A ∈ uedges G. u ∈ A})"

subsection ‹Basic Properties›

lemma uwalk_length_conv: "uwalk_length p = length p - 1"
by (induct p rule: uwalk_edges.induct) (auto simp: uwalk_length_def)

lemma all_edges_mono:
"vs ⊆ ws ⟹ all_edges vs ⊆ all_edges ws"
unfolding all_edges_def by auto

lemma all_edges_subset_Pow: "all_edges A ⊆ Pow A"
by (auto simp: all_edges_def)

lemma in_mk_uedge_img: "(a,b) ∈ A ∨ (b,a) ∈ A ⟹ {a,b} ∈ mk_uedge  A"
by (auto intro: rev_image_eqI)

lemma in_mk_uedge_img_iff: "{a,b} ∈ mk_uedge  A ⟷ (a,b) ∈ A ∨ (b,a) ∈ A"
by (auto simp: doubleton_eq_iff intro: rev_image_eqI)

lemma distinct_edgesI:
assumes "distinct p" shows "distinct (uwalk_edges p)"
proof -
from assms have "?thesis" "⋀u. u ∉ set p ⟹ (⋀v. u ≠ v ⟹ {u,v} ∉ set (uwalk_edges p))"
by (induct p rule: uwalk_edges.induct) auto
then show ?thesis by simp
qed

lemma finite_ucycles:
assumes "finite (uverts G)"
shows "finite (ucycles G)"
proof -
have "ucycles G ⊆ {xs. set xs ⊆ uverts G ∧ length xs ≤ Suc (card (uverts G))}"
proof (rule, simp)
fix p assume "p ∈ ucycles G"
then have "distinct (tl p)" and "set p ⊆ uverts G"
unfolding ucycles_def uwalks_def by auto
moreover
then have "set (tl p) ⊆ uverts G"
by (auto simp: list_set_tl)
with assms have "card (set (tl p)) ≤ card (uverts G)"
by (rule card_mono)
then have "length (p) ≤ 1 + card (uverts G)"
using distinct_card[OF ‹distinct (tl p)›] by auto
ultimately show "set p ⊆ uverts G ∧ length p ≤ Suc (card (uverts G))" by auto
qed
moreover
have "finite {xs. set xs ⊆ uverts G ∧ length xs ≤ Suc (card (uverts G))}"
using assms by (rule finite_lists_length_le)
ultimately
show ?thesis by (rule finite_subset)
qed

lemma ucycles_distinct_edges:
assumes "c ∈ ucycles G" shows "distinct (uwalk_edges c)"
proof -
from assms have c_props: "distinct (tl c)" "4 ≤ length c" "hd c = last c"
by (auto simp add: ucycles_def uwalk_length_conv)
then have "{hd c, hd (tl c)} ∉ set (uwalk_edges (tl c))"
proof (induct c rule: uwalk_edges.induct)
case (3 x y ys)
then have "hd ys ≠ last ys" by (cases ys) auto
moreover
from 3 have "uwalk_edges (y # ys) = {y, hd ys} # uwalk_edges ys"
by (cases ys) auto
moreover
{ fix xs have "set (uwalk_edges xs) ⊆ Pow (set xs)"
by (induct xs rule: uwalk_edges.induct) auto }
ultimately
show ?case using 3 by auto
qed simp_all
moreover
from assms have "distinct (uwalk_edges (tl c))"
by (intro distinct_edgesI) (simp add: ucycles_def)
ultimately
show ?thesis by (cases c rule: list_exhaust3) auto
qed

lemma card_left_less_pair:
fixes A :: "('a :: linorder) set"
assumes "finite A"
shows "card {(a,b). a ∈ A ∧ b ∈ A ∧ a < b}
= (card A * (card A - 1)) div 2"
using assms
proof (induct A)
case (insert x A)

show ?case
proof (cases "card A")
case (Suc n)
have "{(a,b). a ∈ insert x A ∧ b ∈ insert x A ∧ a < b}
= {(a,b). a ∈ A ∧ b ∈ A ∧ a < b} ∪ (λa. if a < x then (a,x) else (x,a))  A"
using ‹x ∉ A› by (auto simp: order_less_le)
moreover
have "finite {(a,b). a ∈ A ∧ b ∈ A ∧ a < b}"
using insert by (auto intro: finite_subset[of _ "A × A"])
moreover
have "{(a,b). a ∈ A ∧ b ∈ A ∧ a < b} ∩ (λa. if a < x then (a,x) else (x,a))  A = {}"
using ‹x ∉ A› by auto
moreover have "inj_on (λa. if a < x then (a, x) else (x, a)) A"
by (auto intro: inj_onI split: if_split_asm)
ultimately show ?thesis using insert Suc
by (simp add: card_Un_disjoint card_image del: if_image_distrib)
qed simp

lemma card_all_edges:
assumes "finite A"
shows "card (all_edges A) = card A choose 2"
proof -
have inj_on_mk_uedge: "inj_on mk_uedge {(a,b). a < b}"
by (rule inj_onI) (auto simp: doubleton_eq_iff)
have "all_edges A = mk_uedge  {(a,b). a ∈ A ∧ b ∈ A ∧ a < b}" (is "?L = ?R")
by (auto simp: all_edges_def intro!: in_mk_uedge_img)
then have "card ?L = card ?R" by simp
also have "… = card {(a,b). a ∈ A ∧ b ∈ A ∧ a < b}"
using inj_on_mk_uedge by (blast intro: card_image subset_inj_on)
also have "… = (card A * (card A - 1)) div 2"
using card_left_less_pair using assms by simp
also have "… = (card A choose 2)"
finally show ?thesis .
qed

lemma verts_Gu: "uverts (G -- u) = uverts G - {u}"
unfolding remove_vertex_def by simp

lemma edges_Gu: "uedges (G -- u) ⊆ uedges G"
unfolding remove_vertex_def by auto

subsection ‹Girth, Independence and Vertex Colorings›

definition girth :: "ugraph ⇒ enat" where
"girth G ≡ INF p∈ ucycles G. enat (uwalk_length p)"

definition independent_sets :: "ugraph ⇒ uvert set set" where
"independent_sets Gr ≡ {vs. vs ⊆ uverts Gr ∧ all_edges vs ∩ uedges Gr = {}}"

definition α :: "ugraph ⇒ enat" where
"α G ≡ SUP vs ∈ independent_sets G. enat (card vs)"

definition vertex_colorings :: "ugraph ⇒ uvert set set set" where
"vertex_colorings G ≡ {C. ⋃C = uverts G ∧ (∀c1∈C. ∀c2∈C. c1 ≠ c2 ⟶ c1 ∩ c2 = {}) ∧
(∀c∈C. c ≠ {} ∧ (∀u ∈ c. ∀v ∈ c. {u,v} ∉ uedges G))}"

text ‹The chromatic number $\chi$:›
definition chromatic_number :: "ugraph ⇒ enat" where
"chromatic_number G ≡ INF c∈ (vertex_colorings G). enat (card c)"

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

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

lemma zero_less_α:
assumes "uverts G ≠ {}"
shows "0 < α G"
proof -
from assms obtain a where "a ∈ uverts G" by auto
then have "0 < enat (card {a})" "{a} ∈ independent_sets G"
by (auto simp: independent_sets_def all_edges_def)
then show ?thesis unfolding α_def less_SUP_iff ..
qed

lemma α_le_card:
assumes "finite (uverts G)"
shows "α G ≤ card(uverts G)"
proof -
{ fix x assume "x ∈ independent_sets G"
then have "x ⊆ uverts G" by (auto simp: independent_sets_def) }
with assms show ?thesis unfolding α_def
by (intro SUP_least) (auto intro: card_mono)
qed

lemma α_fin: "finite (uverts G) ⟹ α G ≠ ∞"
using α_le_card[of G] by (cases "α G") auto

lemma α_remove_le:
shows "α (G -- u) ≤ α G"
proof -
have "independent_sets (G -- u) ⊆ independent_sets G" (is "?L ⊆ ?R")
using all_edges_subset_Pow by (simp add: independent_sets_def remove_vertex_def) blast
then show ?thesis unfolding α_def
by (rule SUP_subset_mono) simp
qed

text ‹
A lower bound for the chromatic number of a graph can be given in terms of
the independence number
›
lemma chromatic_lb:
assumes wf_G: "uwellformed G"
and fin_G: "finite (uverts G)"
and neG: "uverts G ≠ {}"
shows "card (uverts G) / α G ≤ chromatic_number G"
proof -
from wf_G have "(λv. {v})  uverts G ∈ vertex_colorings G"
by (auto simp: vertex_colorings_def uwellformed_def)
then have "chromatic_number G ≠ top"
by (simp add: chromatic_number_def) (auto simp: top_enat_def)
then obtain vc where vc_vc: "vc ∈ vertex_colorings G"
and vc_size:"chromatic_number G = card vc"
unfolding chromatic_number_def by (rule enat_in_INF)

have fin_vc_elems: "⋀c. c ∈ vc ⟹ finite c"
using vc_vc by (intro finite_subset[OF _ fin_G]) (auto simp: vertex_colorings_def)

have sum_vc_card: "(∑c ∈ vc. card c) = card (uverts G)"
using fin_vc_elems vc_vc unfolding vertex_colorings_def
by (simp add: card_Union_disjoint[symmetric] pairwise_def disjnt_def)

have "⋀c. c ∈ vc ⟹ c ∈ independent_sets G"
using vc_vc by (auto simp: vertex_colorings_def independent_sets_def all_edges_def)
then have "⋀c. c ∈ vc ⟹ card c ≤ α G"
using vc_vc fin_vc_elems by (subst le_α_iff) (auto simp add: vertex_colorings_def)
then have "(∑c∈vc. card c) ≤ card vc * α G"
using sum_bounded_above[of vc card "α G"]