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 add: card_eq_0_iff insert) 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)" by (simp add: n_choose_2_nat) 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"] by (simp add: of_nat_eq_enat[symmetric] of_nat_sum) then have "ereal_of_enat (card (uverts G)) ≤ ereal_of_enat (α G) * ereal_of_enat (card vc)" by (simp add: sum_vc_card ereal_of_enat_pushout ac_simps del: ereal_of_enat_simps) with zero_less_α[OF neG] α_fin[OF fin_G] vc_size show ?thesis by (simp add: ereal_divide_le_pos) qed end