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  (euedges 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  (c1C. c2C. c1  c2  c1  c2 = {}) 
    (cC. 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 "(cvc. 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