Theory Girth_Chromatic.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 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: choose_two)
  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