# Theory Girth_Chromatic

Up to index of Isabelle/HOL/HOL-Multivariate_Analysis/HOL-Probability/Girth_Chromatic

theory Girth_Chromatic
imports Ugraphs Probability Approximation
`theory Girth_Chromaticimports  Ugraphs  Girth_Chromatic_Misc  "~~/src/HOL/Probability/Probability"  "~~/src/HOL/Library/Binomial"  "~~/src/HOL/Decision_Procs/Approximation"beginsection {* Probability Space on Sets of Edges *}definition cylinder :: "'a set => 'a set => 'a set => 'a set set" where  "cylinder S A B = {T ∈ Pow S. A ⊆ T ∧ B ∩ T = {}}"lemma full_sum:  fixes p :: real  assumes "finite S"  shows "(∑A∈Pow S. p^card A * (1 - p)^card (S - A)) = 1"using assmsproof induct  case (insert s S)  have "inj_on (insert s) (Pow S)"      and "!!x. S - insert s x = S - x"      and "Pow S ∩ insert s ` Pow S = {}"      and "!!x. x ∈ Pow S ==> card (insert s S - x) = Suc (card (S - x))"    using insert(1-2) by (auto simp: insert_Diff_if intro!: inj_onI)  moreover have "!!x. x ⊆ S ==> card (insert s x) = Suc (card x)"    using insert(1-2) by (subst card.insert) (auto dest: finite_subset)  ultimately show ?case    by (simp add: setsum_reindex setsum_right_distrib[symmetric] ac_simps                  insert.hyps setsum_Un_disjoint Pow_insert)qed simptext {* Definition of the probability space on edges: *}locale edge_space =  fixes n :: nat and p :: real  assumes p_prob: "0 ≤ p" "p ≤ 1"begindefinition S_verts :: "nat set" where  "S_verts ≡ {1..n}"definition S_edges :: "uedge set" where  "S_edges = all_edges S_verts"definition edge_ugraph :: "uedge set => ugraph" where  "edge_ugraph es ≡ (S_verts, es ∩ S_edges)"definition "P = point_measure (Pow S_edges) (λs. p^card s * (1 - p)^card (S_edges - s))"lemma finite_verts[intro!]: "finite S_verts"  by (auto simp: S_verts_def)lemma finite_edges[intro!]: "finite S_edges"  by (auto simp: S_edges_def all_edges_def finite_verts)lemma finite_graph[intro!]: "finite (uverts (edge_ugraph es))"  unfolding edge_ugraph_def by autolemma uverts_edge_ugraph[simp]: "uverts (edge_ugraph es) = S_verts"  by (simp add: edge_ugraph_def)lemma uedges_edge_ugraph[simp]: "uedges (edge_ugraph es) = es ∩ S_edges"  unfolding edge_ugraph_def by simplemma space_eq: "space P = Pow S_edges" by (simp add: P_def space_point_measure)lemma sets_eq: "sets P = Pow (Pow S_edges)" by (simp add: P_def sets_point_measure)lemma emeasure_eq:  "emeasure P A = (if A ⊆ Pow S_edges then (∑edges∈A. p^card edges * (1 - p)^card (S_edges - edges)) else 0)"  using finite_edges p_prob  by (simp add: P_def space_point_measure emeasure_point_measure_finite zero_le_mult_iff                zero_le_power_iff sets_point_measure emeasure_notin_sets)lemma integrable_P[intro, simp]: "integrable P f"  using finite_edges by (simp add: integrable_point_measure_finite P_def)lemma borel_measurable_P[measurable]: "f ∈ borel_measurable P"  unfolding P_def by simp  lemma prob_space_P: "prob_space P"proof  show "emeasure P (space P) = 1" -- {* Sum of probabilities equals 1 *}    using finite_edges by (simp add: emeasure_eq full_sum one_ereal_def space_eq)qedendsublocale edge_space ⊆ prob_space P  by (rule prob_space_P)context edge_spacebeginlemma prob_eq:  "prob A = (if A ⊆ Pow S_edges then (∑edges∈A. p^card edges * (1 - p)^card (S_edges - edges)) else 0)"  using emeasure_eq[of A] unfolding emeasure_eq_measure by simplemma integral_finite_singleton: "integral⇡L P f = (∑x∈Pow S_edges. f x * measure P {x})"  using p_prob prob_eq unfolding P_def  by (subst lebesgue_integral_point_measure_finite) (auto intro!: setsum_cong mult_nonneg_nonneg)text {* Probability of cylinder sets: *}lemma cylinder_prob:  assumes "A ⊆ S_edges" "B ⊆ S_edges" "A ∩ B = {}"  shows "prob (cylinder S_edges A B) = p ^ (card A) * (1 - p) ^ (card B)" (is "_ = ?pp A B")proof -  have "Pow S_edges ∩ cylinder S_edges A B = cylinder S_edges A B"       "!!x. x ∈ cylinder S_edges A B ==> A ∪ x = x"       "!!x. x ∈ cylinder S_edges A B ==> finite x"       "!!x. x ∈ cylinder S_edges A B ==> B ∩ (S_edges - B - x) = {}"       "!!x. x ∈ cylinder S_edges A B ==> B ∪ (S_edges - B - x) = S_edges - x"       "finite A" "finite B"    using assms by (auto simp add: cylinder_def intro: finite_subset)  then have "(∑T∈cylinder S_edges A B. ?pp T (S_edges - T))      = (∑T ∈ cylinder S_edges A B. p^(card A + card (T - A)) * (1 - p)^(card B + card ((S_edges - B) - T)))"    using finite_edges by (simp add: card_Un_Int)  also have "… = ?pp A B * (∑T∈cylinder S_edges A B. ?pp (T - A) (S_edges - B - T))"    by (simp add: power_add setsum_right_distrib ac_simps)  also have "… = ?pp A B"  proof -    have "!!T. T ∈ cylinder S_edges A B ==> S_edges - B - T = (S_edges - A) - B - (T - A)"         "Pow (S_edges - A - B) = (λx. x - A) ` cylinder S_edges A B"         "inj_on (λx. x - A) (cylinder S_edges A B)"         "finite (S_edges - A - B)"      using assms by (auto simp: cylinder_def intro!: inj_onI)    with full_sum[of "S_edges - A - B"] show ?thesis by (simp add: setsum_reindex)  qed  finally show ?thesis by (auto simp add: prob_eq cylinder_def)qedlemma Markov_inequality:  fixes a :: real and X :: "uedge set => real"  assumes "0 < c" "!!x. 0 ≤ f x"  shows "prob {x ∈ space P. c ≤ f x} ≤ (\<integral>x. f x ∂ P) / c"proof -  from assms have "(\<integral>⇡+ x. ereal (f x) ∂P) = (\<integral>x. f x ∂P)"    by (intro positive_integral_eq_integral) auto  with assms show ?thesis    using positive_integral_Markov_inequality[of f P "space P" "1 / c"]    by (simp cong: positive_integral_cong add: emeasure_eq_measure one_ereal_def)qedendsubsection {* Graph Probabilities outside of @{term Edge_Space} locale*}text {* These abbreviations allow a compact expression of probabilities about random graphs outside of the @{term Edge_Space} locale. We also transfer a few of the lemmas we need from the locale into the toplevel theory.*}abbreviation MGn :: "(nat => real) => nat => (uedge set) measure" where  "MGn p n ≡ (edge_space.P n (p n))"abbreviation probGn :: "(nat => real) => nat => (uedge set => bool) => real" where  "probGn p n P ≡ measure (MGn p n) {es ∈ space (MGn p n). P es}"lemma probGn_le:  assumes p_prob: "0 < p n" "p n < 1"  assumes sub: "!!n es. es ∈ space (MGn p n) ==> P n es ==> Q n es"  shows "probGn p n (P n) ≤ probGn p n (Q n)"proof -  from p_prob interpret E: edge_space n "p n" by unfold_locales auto  show ?thesis    by (auto intro!: E.finite_measure_mono sub simp: E.space_eq E.sets_eq)qedsection {* Short cycles *}definition short_cycles :: "ugraph => nat => uwalk set" where  "short_cycles G k ≡ {p ∈ ucycles G. uwalk_length p ≤ k}"text {* obtains a vertex in a short cycle: *}definition choose_v :: "ugraph => nat => uvert" where  "choose_v G k ≡ SOME u. ∃p. p ∈ short_cycles G k ∧ u ∈ set p"partial_function (tailrec) kill_short :: "ugraph => nat => ugraph" where  "kill_short G k = (if short_cycles G k = {} then G else (kill_short (G -- (choose_v G k)) k))"lemma ksc_simps[simp]:  "short_cycles G k = {} ==> kill_short G k = G"  "short_cycles G k ≠ {}  ==> kill_short G k = kill_short (G -- (choose_v G k)) k"  by (auto simp: kill_short.simps)lemma  assumes "short_cycles G k ≠ {}"  shows choose_v__in_uverts: "choose_v G k ∈ uverts G" (is ?t1)    and choose_v__in_short: "∃p. p ∈ short_cycles G k ∧ choose_v G k ∈ set p" (is ?t2)proof -  from assms obtain p where "p ∈ ucycles G" "uwalk_length p ≤ k"    unfolding short_cycles_def by auto  moreover  then obtain u where "u ∈ set p" unfolding ucycles_def    by (cases p) (auto simp: uwalk_length_conv)  ultimately have "∃u p. p ∈ short_cycles G k ∧ u ∈ set p"    by (auto simp: short_cycles_def)  then show ?t2 by (auto simp: choose_v_def intro!: someI_ex)  then show ?t1 by (auto simp: short_cycles_def ucycles_def uwalks_def)qedlemma kill_step_smaller:  assumes "short_cycles G k ≠ {}"  shows "short_cycles (G -- (choose_v G k)) k ⊂ short_cycles G k"proof -  let ?cv = "choose_v G k"  from assms obtain p where "p ∈ short_cycles G k" "?cv ∈ set p"    by atomize_elim (rule choose_v__in_short)  have "short_cycles (G -- ?cv) k ⊆ short_cycles G k"  proof    fix p assume "p ∈ short_cycles (G -- ?cv) k"    then show "p ∈ short_cycles G k"      unfolding short_cycles_def ucycles_def uwalks_def      using edges_Gu[of G ?cv] by (auto simp: verts_Gu)  qed  moreover have "p ∉ short_cycles (G -- ?cv) k"    using `?cv ∈ set p` by (auto simp: short_cycles_def ucycles_def uwalks_def verts_Gu)  ultimately show ?thesis using `p ∈ short_cycles G k` by autoqedtext {* Induction rule for @{term kill_short}: *}lemma kill_short_induct[consumes 1, case_names empty kill_vert]:  assumes fin: "finite (uverts G)"  assumes a_empty: "!!G. short_cycles G k = {} ==> P G k"  assumes a_kill: "!!G. finite (short_cycles G k) ==> short_cycles G k ≠ {}    ==> P (G -- (choose_v G k)) k ==> P G k"  shows "P G k"proof -  have "finite (short_cycles G k)"    using finite_ucycles[OF fin] by (auto simp: short_cycles_def)  then show ?thesis    by (induct "short_cycles G k" arbitrary: G rule: finite_psubset_induct)      (metis kill_step_smaller a_kill a_empty)qedtext {* Large Girth (after @{term kill_short}): *}lemma kill_short_large_girth:  assumes "finite (uverts G)"  shows "k < girth (kill_short G k)"using assmsproof (induct G k rule: kill_short_induct)  case (empty G)  then have "!!p. p ∈ ucycles G ==> k < enat (uwalk_length p)"    by (auto simp: short_cycles_def)  with empty show ?case by (auto simp: girth_def intro: enat_less_INF_I)qed simptext {* Order of graph (after @{term kill_short}): *}lemma kill_short_order_of_graph:  assumes "finite (uverts G)"  shows "card (uverts G) - card (short_cycles G k) ≤ card (uverts (kill_short G k))"using assms assmsproof (induct G k rule: kill_short_induct)  case (kill_vert G)  let ?oG = "G -- (choose_v G k)"  have "finite (uverts ?oG)"    using kill_vert by (auto simp: remove_vertex_def)  moreover  have "uverts (kill_short G k) = uverts (kill_short ?oG k)"    using kill_vert by simp  moreover  have "card (uverts G) = Suc (card (uverts ?oG))"    using choose_v__in_uverts kill_vert    by (simp add: remove_vertex_def card_Suc_Diff1 del: card_Diff_insert)  moreover  have "card (short_cycles ?oG k) < card (short_cycles G k)"    by (intro psubset_card_mono kill_vert.hyps kill_step_smaller)  ultimately show ?case using kill_vert.hyps by presburgerqed simptext {* Independence number (after @{term kill_short}): *}lemma kill_short_α:  assumes "finite (uverts G)"  shows "α (kill_short G k) ≤ α G"using assmsproof (induct G k rule: kill_short_induct)  case (kill_vert G)  note kill_vert(3)  also have "α (G -- (choose_v G k)) ≤ α G" by (rule α_remove_le)  finally show ?case using kill_vert by simpqed simptext {* Wellformedness (after @{term kill_short}): *}lemma kill_short_uwellformed:  assumes "finite (uverts G)" "uwellformed G"  shows "uwellformed (kill_short G k)"using assmsproof (induct G k rule: kill_short_induct)  case (kill_vert G)  from kill_vert.prems have "uwellformed (G -- (choose_v G k))"    by (auto simp: uwellformed_def remove_vertex_def)  with kill_vert.hyps show ?case by simpqed simpsection {* The Chromatic-Girth Theorem *}text {* Probability of Independent Edges: *}lemma (in edge_space) random_prob_independent:  assumes "n ≥ k" "k ≥ 2"  shows "prob {es ∈ space P. k ≤ α (edge_ugraph es)}    ≤ (n choose k)*(1-p)^(k choose 2)"proof -  let "?k_sets" = "{vs. vs ⊆ S_verts ∧ card vs = k}"  { fix vs assume A: "vs ∈ ?k_sets"    then have B: "all_edges vs ⊆ S_edges"      unfolding all_edges_def S_edges_def by blast    have "{es ∈ space P. vs ∈ independent_sets (edge_ugraph es)}        = cylinder S_edges {} (all_edges vs)" (is "?L = _")      using A by (auto simp: independent_sets_def edge_ugraph_def space_eq cylinder_def)    then have "prob ?L = (1-p)^(k choose 2)"      using A B finite by (auto simp: cylinder_prob card_all_edges dest: finite_subset)  }  note prob_k_indep = this    -- "probability that a fixed set of k vertices is independent in a random graph"  have "{es ∈ space P. k ∈ card ` independent_sets (edge_ugraph es)}    = (\<Union>vs ∈ ?k_sets. {es ∈ space P. vs ∈ independent_sets (edge_ugraph es)})" (is "?L = ?R")    unfolding image_def space_eq independent_sets_def by auto  then have "prob ?L ≤ (∑vs ∈ ?k_sets. prob {es ∈ space P. vs ∈ independent_sets (edge_ugraph es)})"    by (auto intro!: finite_measure_subadditive_finite simp: space_eq sets_eq)  also have "… = (n choose k)*((1 - p) ^ (k choose 2))"    by (simp add: prob_k_indep real_eq_of_nat S_verts_def n_subsets)  finally show ?thesis using `k ≥ 2` by (simp add: le_α_iff)qedtext {* Almost never many independent edges: *}lemma almost_never_le_α:  fixes k :: nat    and p :: "nat => real"  assumes p_prob: "∀⇡∞ n. 0 < p n ∧ p n < 1"  assumes [arith]: "k > 0"  assumes N_prop: "∀⇡∞ n. (6 * k * ln n)/n ≤ p n"  shows "(λn. probGn p n (λes. 1/2*n/k ≤ α (edge_space.edge_ugraph n es))) ----> 0"    (is "(λn. ?prob_fun n) ----> 0")proof -  let "?prob_fun_raw n" = "probGn p n (λes. natceiling (1/2*n/k) ≤ α (edge_space.edge_ugraph n es))"  def r ≡ "λ(n :: nat). (1 / 2 * n / k)"  let "?nr n" = "natceiling (r n)"  have r_pos: "!!n. 0 < n ==> 0 < r n " by (auto simp: r_def field_simps)  have nr_bounds: "∀⇡∞ n. 2 ≤ ?nr n ∧ ?nr n ≤ n"    by (intro eventually_sequentiallyI[of "4 * k"])      (simp add: r_def natceiling_le le_natceiling_iff field_simps)  from nr_bounds p_prob have ev_prob_fun_raw_le:    "∀⇡∞ n. probGn p n (λes. ?nr n≤ α (edge_space.edge_ugraph n es))      ≤ (n * exp (- p n * (real (?nr n) - 1) / 2)) powr ?nr n"    (is "∀⇡∞ n. ?prob_fun_raw_le n")  proof (rule eventually_elim2)    fix n :: nat assume A: "2 ≤ ?nr n ∧ ?nr n ≤ n" "0 < p n ∧p n < 1"    then interpret pG: edge_space n "p n" by unfold_locales auto    have r: "real (?nr n - 1) = real (?nr n) - 1" using A by auto    have "probGn p n (λes. ?nr n ≤ α (edge_space.edge_ugraph n es))        ≤ (n choose ?nr n) * (1 - p n)^(?nr n choose 2)"      using A by (auto intro: pG.random_prob_independent)    also have "… ≤ n powr ?nr n * (1 - p n) powr (?nr n choose 2)"      using A      by (simp add: powr_realpow power_real_of_nat binomial_le_pow del: real_of_nat_power)    also have "… = n powr ?nr n * (1 - p n) powr (?nr n * (?nr n - 1) / 2)"      by (cases "even (?nr n - 1)")         (auto simp: n_choose_2_nat nat_even_iff_2_dvd[symmetric] real_of_nat_div)    also have "… = n powr ?nr n * ((1 - p n) powr ((?nr n - 1) / 2)) powr ?nr n"      by (auto simp: powr_powr algebra_simps)    also have "… ≤ (n * exp (- p n * (?nr n - 1) / 2)) powr ?nr n"    proof -      have "(1 - p n) powr ((?nr n - 1) / 2) ≤ exp (- p n) powr ((?nr n - 1) / 2)"        using A by (auto simp: powr_mono2 ab_diff_minus)      also have "… = exp (- p n * (?nr n - 1) / 2)" by (auto simp: powr_def)      finally show ?thesis        using A by (auto simp: mult_pos_pos powr_mono2 powr_mult)    qed    finally show "probGn p n (λes. ?nr n ≤ α (edge_space.edge_ugraph n es))      ≤ (n * exp (- p n * (real (?nr n) - 1) / 2)) powr ?nr n"      using A r by simp  qed  from p_prob N_prop  have ev_expr_bound: "∀⇡∞ n. n * exp (-p n * (real (?nr n) - 1) / 2) ≤ (exp 1 / n) powr (1 / 2)"  proof (elim eventually_rev_mp, intro eventually_sequentiallyI conjI impI)    fix n assume n_bound[arith]: "2 ≤ n"      and p_bound: "0 < p n ∧ p n < 1" "(6 * k * ln n) / n ≤ p n"    have r_bound: "r n ≤ ?nr n" by (rule real_natceiling_ge)    have "n * exp (-p n * (real (?nr n)- 1) / 2) ≤ n * exp (- 3 / 2 * ln n + p n / 2)"    proof -      have "0 < ln n" using "n_bound" by auto      then have "(3 / 2) * ln n ≤ ((6 * k * ln n) / n) * (?nr n / 2)"        using r_bound by (simp add: r_def field_simps del: ln_gt_zero_iff)      also have "… ≤ p n * (?nr n / 2)"        using n_bound p_bound r_bound r_pos[of n] by (auto simp: field_simps)      finally show ?thesis using r_bound by (auto simp: field_simps)    qed    also have "… ≤ n * n powr (- 3 / 2) * exp 1 powr (1 / 2)"      using p_bound by (simp add: powr_def exp_add)    also have "… ≤ n powr (-1 / 2) * exp 1 powr (1 / 2)" by (simp add: powr_mult_base)    also have "… = (exp 1 / n) powr (1/2)"      by (simp add: powr_divide powr_minus_divide)    finally show "n * exp (- p n * (real (?nr n) - 1) / 2) ≤ (exp 1 / n) powr (1 / 2)" .  qed  have ceil_bound: "!!G n. 1/2*n/k ≤ α G <-> natceiling (1/2*n/k) ≤ α G"    by (case_tac "α G") (auto simp: natceiling_le_eq)  show ?thesis  proof (unfold ceil_bound, rule real_tendsto_sandwich)    show "(λn. 0) ----> 0"        "(λn. (exp 1 / n) powr (1 / 2)) ----> 0"        "∀⇡∞ n. 0 ≤ ?prob_fun_raw n"      using p_prob by (auto intro: measure_nonneg LIMSEQ_inv_powr elim: eventually_elim1)  next    from nr_bounds ev_expr_bound ev_prob_fun_raw_le    show "∀⇡∞ n. ?prob_fun_raw n ≤ (exp 1 / n) powr (1 / 2)"    proof (elim eventually_rev_mp, intro eventually_sequentiallyI impI conjI)      fix n assume A: "3 ≤ n"        and nr_bounds: "2 ≤ ?nr n ∧ ?nr n ≤ n"        and prob_fun_raw_le: "?prob_fun_raw_le n"        and expr_bound: "n * exp (- p n * (real (natceiling (r n)) - 1) / 2) ≤ (exp 1 / n) powr (1 / 2)"      have "exp 1 < (3 :: real)" by (approximation 5)      then have "(exp 1 / n) powr (1 / 2) ≤ 1 powr (1 / 2)"        using A by (intro powr_mono2) (auto simp: field_simps)      then have ep_bound: "(exp 1 / n) powr (1 / 2) ≤ 1" by simp      have "?prob_fun_raw n ≤ (n * exp (- p n * (real (?nr n) - 1) / 2)) powr (?nr n)"        using prob_fun_raw_le by (simp add: r_def)      also have "… ≤ ((exp 1 / n) powr (1 / 2)) powr ?nr n"        using expr_bound A by (auto simp: powr_mono2 mult_pos_pos)      also have "… ≤ ((exp 1 / n) powr (1 / 2))"        using nr_bounds ep_bound by (auto simp: powr_le_one_le)      finally show "?prob_fun_raw n ≤ (exp 1 / n) powr (1 / 2)" .    qed  qedqedtext {* Mean number of k-cycles in a graph. (Or rather of paths describing a circle of length @{term k}): *}lemma (in edge_space) mean_k_cycles:  assumes "3 ≤ k" "k < n"  shows "(\<integral>es. card {c ∈ ucycles (edge_ugraph es). uwalk_length c = k} ∂ P)    = (fact n div fact (n - k)) * p ^ k"proof -  let ?k_cycle = "λes c k. c ∈ ucycles (edge_ugraph es) ∧ uwalk_length c = k"  def C ≡ "λk. {c. ?k_cycle S_edges c k}"    -- {* @{term "C k"} is the set of all possible cycles of size @{term k} in @{term "edge_ugraph S_edges"} *}  def XG ≡ "λes. {c. ?k_cycle es c k}"    -- {* @{term "XG es"} is the set of cycles contained in a @{term "edge_ugraph es"} *}  def XC ≡ "λc. {es ∈ space P. ?k_cycle es c k}"    -- {* "@{term "XC c"} is the set of graphs (edge sets) containing a cycle c" *}  then have XC_in_sets: "!!c. XC c ∈ sets P"      and XC_cyl: "!!c. c ∈ C k ==> XC c = cylinder S_edges (set (uwalk_edges c)) {}"    by (auto simp: ucycles_def space_eq uwalks_def C_def cylinder_def sets_eq)  have "(\<integral>es. card {c ∈ ucycles (edge_ugraph es). uwalk_length c = k} ∂ P)      =  (∑x∈space P. card (XG x) * prob {x})"    by (simp add: XG_def integral_finite_singleton space_eq)  also have "… = (∑c∈C k. prob (cylinder S_edges (set (uwalk_edges c)) {}))"  proof -    have XG_Int_C: "!!s. s ∈ space P ==> C k ∩ XG s = XG s"      unfolding XG_def C_def ucycles_def uwalks_def edge_ugraph_def by auto    have fin_XC: "!!k. finite (XC k)" and fin_C: "finite (C k)"      unfolding C_def XC_def by (auto simp: finite_edges space_eq intro!: finite_ucycles)    have "(∑x∈space P. card (XG x) * prob {x}) = (∑x∈space P. (∑c ∈ XG x. prob {x}))"      by (simp add: real_eq_of_nat)    also have "… = (∑x∈space P. (∑c ∈ C k. if c ∈ XG x then prob {x} else 0))"      using fin_C by (simp add: setsum_cases) (simp add: XG_Int_C)    also have "… = (∑c ∈ C k. (∑ x ∈ space P ∩ XC c. prob {x}))"      using finite_edges by (subst setsum_commute) (simp add: setsum_restrict_set XG_def XC_def space_eq)    also have "… = (∑c ∈ C k. prob (XC c))"      using fin_XC XC_in_sets      by (auto simp add: prob_eq sets_eq space_eq intro!: setsum_cong)    finally show ?thesis by (simp add: XC_cyl)  qed  also have "… = (∑c∈C k. p ^ k)"  proof -    have "!!x. x ∈ C k ==> card (set (uwalk_edges x)) = uwalk_length x"      by (auto simp: uwalk_length_def C_def ucycles_distinct_edges intro: distinct_card)    then show ?thesis by (auto simp: C_def ucycles_def uwalks_def cylinder_prob)  qed  also have "… = (fact n div fact (n - k)) * p ^ k"  proof -    have inj_last_Cons: "!!A. inj_on (λes. last es # es) A" by (rule inj_onI) simp    { fix xs A assume "3 ≤ length xs - Suc 0" "hd xs = last xs"      then have "xs ∈ (λxs. last xs # xs) ` A <-> tl xs ∈ A"        by (cases xs) (auto simp: inj_image_mem_iff[OF inj_last_Cons] split: split_if_asm) }    note image_mem_iff_inst = this    { fix xs have "xs ∈ uwalks (edge_ugraph S_edges) ==> set (tl xs) ⊆ S_verts"        unfolding uwalks_def by (induct xs) auto }    moreover    { fix xs assume "set xs ⊆ S_verts" "2 ≤ length xs" "distinct xs"      then have "(last xs # xs) ∈ uwalks (edge_ugraph S_edges)"      proof (induct xs rule: uwalk_edges.induct)        case (3 x y ys)        have S_edges_memI: "!!x y. x ∈ S_verts ==> y ∈ S_verts ==> x ≠ y ==> {x, y} ∈ S_edges"          unfolding S_edges_def all_edges_def image_def by auto        have "ys ≠ [] ==> set ys ⊆ S_verts ==> last ys ∈ S_verts"  by auto        with 3 show ?case          by (auto simp add: uwalks_def Suc_le_eq intro: S_edges_memI)      qed simp_all}    moreover note `3 ≤ k`    ultimately    have "C k = (λxs. last xs # xs) ` {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ S_verts}"      by (auto simp: C_def ucycles_def uwalk_length_conv image_mem_iff_inst)    moreover have "card S_verts = n" by (simp add: S_verts_def)    ultimately have "card (C k) = fact n div fact (n - k)"      using `k < n`      by (simp add: card_image[OF inj_last_Cons] card_lists_distinct_length_eq fact_div_fact)    then show ?thesis by (simp add: real_eq_of_nat)  qed                                      finally show ?thesis by simpqedtext {* Girth-Chromatic number theorem: *}theorem girth_chromatic:  fixes l :: nat  shows "∃G. uwellformed G ∧ l < girth G ∧ l < chromatic_number G"proof -  def k ≡ "max 3 l"   def ε ≡ "1 / (2 * k)"  def p ≡ "λ(n :: nat). real n powr (ε - 1)"  let ?ug = edge_space.edge_ugraph  def short_count ≡ "λg. card (short_cycles g k)"    -- {* This random variable differs from the one used in the proof of theorem 11.2.2,          as we count the number of paths describing a circle, not the circles themselves *}  from k_def have "3 ≤ k" "l ≤ k" by auto  from ε_def `3 ≤ k` have ε_props: "0 < ε" "ε < 1 / k" "ε < 1" by (auto simp: field_simps)  have ev_p: "∀⇡∞ n. 0 < p n ∧ p n < 1"  proof (rule eventually_sequentiallyI)    fix n :: nat assume "2 ≤ n"    with `ε < 1` have "n powr (ε - 1) < 1" by (auto intro!: powr_less_one)    then show "0 < p n ∧ p n < 1" by (auto simp: p_def)  qed  then  have prob_short_count_le: "∀⇡∞ n. probGn p n (λes. (real n/2) ≤ short_count (?ug n es))      ≤ 2 * (k - 2) * n powr (ε * k - 1)"  (is "∀⇡∞ n. ?P n")  proof (elim eventually_rev_mp, intro eventually_sequentiallyI impI)    fix n :: nat assume A: "Suc k ≤ n" "0 < p n ∧ p n < 1"    then interpret pG: edge_space n "p n" by unfold_locales auto    have "1 ≤ n" using A by auto      def mean_short_count ≡ "\<integral>es. short_count (?ug n es) ∂ pG.P"      have mean_short_count_le: "mean_short_count ≤ (k - 2) * n powr (ε * k)"    proof -      have small_empty: "!!es k. k ≤ 2 ==> short_cycles (edge_space.edge_ugraph n es) k = {}"          by (auto simp add: short_cycles_def ucycles_def)      have short_count_conv: "!!es. short_count (?ug n es) = (∑i=3..k. real (card {c ∈ ucycles (?ug n es). uwalk_length c = i}))"      proof (unfold short_count_def, induct k)        case 0 with small_empty show ?case by auto      next        case (Suc k)        show ?case proof (cases "Suc k ≤ 2")          case True with small_empty show ?thesis by auto        next          case False          have "{c ∈ ucycles (?ug n es). uwalk_length c ≤ Suc k}              = {c ∈ ucycles (?ug n es). uwalk_length c ≤ k} ∪ {c ∈ ucycles (?ug n es). uwalk_length c = Suc k}"            by auto          moreover          have "finite (uverts (edge_space.edge_ugraph n es))" by auto          ultimately          have "card {c ∈ ucycles (?ug n es). uwalk_length c ≤ Suc k}            = card {c ∈ ucycles (?ug n es). uwalk_length c ≤ k} + card {c ∈ ucycles (?ug n es). uwalk_length c = Suc k}"            using finite_ucycles by (subst card_Un_disjoint[symmetric]) auto          then show ?thesis            using Suc False unfolding short_cycles_def by (auto simp: not_le)        qed      qed        have "mean_short_count = (∑i=3..k. \<integral>es. card {c ∈ ucycles (?ug n es). uwalk_length c = i} ∂ pG.P)"        unfolding mean_short_count_def short_count_conv        by (subst integral_setsum) (auto intro: pG.integral_finite_singleton)      also have "… = (∑i∈{3..k}. (fact n div fact (n - i)) * p n ^ i)"        using A by (simp add: pG.mean_k_cycles)      also have "… ≤ (∑ i∈{3..k}. n ^ i * p n ^ i)"        using A fact_div_fact_le_pow        by (auto intro: setsum_mono simp del: real_of_nat_power)      also have "... ≤ (∑ i∈{3..k}. n powr (ε * k))"        using `1 ≤ n` `0 < ε` A        by (intro setsum_mono) (auto simp: p_def field_simps powr_mult_base powr_powr          powr_realpow[symmetric] powr_mult[symmetric] powr_add[symmetric])      finally show ?thesis by (simp add: real_eq_of_nat)    qed      have "pG.prob {es ∈ space pG.P. n/2 ≤ short_count (?ug n es)} ≤ mean_short_count / (n/2)"      unfolding mean_short_count_def using `1 ≤ n`      by (intro pG.Markov_inequality) (auto simp: short_count_def)    also have "… ≤ 2 * (k - 2) * n powr (ε * k - 1)"    proof -      have "mean_short_count / (n / 2) ≤ 2 * (k - 2) * (1 / n powr 1) * n powr (ε * k)"        using mean_short_count_le `1 ≤ n` by (simp add: field_simps)      then show ?thesis by (simp add: powr_divide2[symmetric] algebra_simps)    qed    finally show "?P n" .  qed  def pf_short_count ≡ "λn. probGn p n (λes. n/2 ≤ short_count (?ug n es))"    and pf_α ≡ "λn. probGn p n (λes. 1/2 * n/k ≤ α (edge_space.edge_ugraph n es))"  have ev_short_count_le: "∀⇡∞ n. pf_short_count n < 1 / 2"  proof -    have "ε * k - 1 < 0"      using ε_props `3 ≤ k` by (auto simp: field_simps)    then have "(λn. 2 * (k - 2) * n powr (ε * k - 1)) ----> 0" (is "?bound ----> 0")      by (intro tendsto_mult_right_zero LIMSEQ_neg_powr)    then have "∀⇡∞ n. dist (?bound n) 0  < 1 / 2"      by (rule tendstoD) simp    with prob_short_count_le show ?thesis      by (rule eventually_elim2) (auto simp: dist_real_def pf_short_count_def)  qed  have lim_α: "pf_α ----> 0"  proof -    have "0 < k" using `3 ≤ k` by simp    have "∀⇡∞ n. (6*k) * ln n / n ≤ p n <-> (6*k) * ln n * n powr - ε ≤ 1"    proof (rule eventually_sequentiallyI)     fix n :: nat assume "1 ≤ n"      then have "(6 * k) * ln n / n ≤ p n <-> (6*k) * ln n * (n powr - 1) ≤ n powr (ε - 1)"        by  (subst powr_minus) (simp add: divide_inverse p_def)      also have "… <-> (6*k) * ln n * ((n powr - 1) / (n powr (ε - 1))) ≤ n powr (ε - 1) / (n powr (ε - 1))"        by auto      also have "… <-> (6*k) * ln n * n powr - ε ≤ 1"        by (simp add: powr_divide2)      finally show "(6*k) * ln n / n ≤ p n <-> (6*k) * ln n * n powr - ε ≤ 1" .    qed    then have "(∀⇡∞ n. (6 * k) * ln n / real n ≤ p n)        <-> (∀⇡∞ n. (6*k) * ln n * n powr - ε ≤ 1)"      by (rule eventually_subst)    also have "∀⇡∞ n. (6*k) * ln n * n powr - ε ≤ 1"    proof -      { fix n :: nat assume "0 < n"        have "ln (real n) ≤ n powr (ε/2) / (ε/2)"          using `0 < n` `0 < ε` by (intro ln_powr_bound) auto        also have "… ≤ 2/ε * n powr (ε/2)" by (auto simp: field_simps)        finally have "(6*k) * ln n * (n powr - ε)  ≤ (6*k) * (2/ε * n powr (ε/2)) * (n powr - ε)"          using `0 < n` `0 < k` by (intro mult_right_mono mult_left_mono) auto        also have "… = 12*k/ε * n powr (-ε/2)"          unfolding divide_inverse          by (auto simp: field_simps powr_minus[symmetric] powr_add[symmetric])        finally have "(6*k) * ln n * (n powr - ε) ≤ 12*k/ε * n powr (-ε/2)" .      }      then have "∀⇡∞ n. (6*k) * ln n * (n powr - ε) ≤ 12*k/ε * n powr (-ε/2)"        by (intro eventually_sequentiallyI[of 1]) auto      also have "∀⇡∞ n. 12*k/ε * n powr (-ε/2) ≤ 1"      proof -        have "(λn. 12*k/ε * n powr (-ε/2)) ----> 0"          using `0 < ε` by (intro tendsto_mult_right_zero LIMSEQ_neg_powr) auto        then show ?thesis          using `0 < ε` by (auto elim: eventually_elim1 simp: dist_real_def dest!: tendstoD[where e=1])      qed      finally (eventually_le_le) show ?thesis .    qed    finally have "∀⇡∞ n. real (6 * k) * ln (real n) / real n ≤ p n" .    with ev_p `0 < k` show ?thesis unfolding pf_α_def by (rule almost_never_le_α)  qed  from ev_short_count_le lim_α[THEN tendstoD, of "1/2"] ev_p  have "∀⇡∞ n. 0 < p n ∧ p n < 1 ∧ pf_short_count n < 1/2 ∧ pf_α n < 1/2"    by simp (elim eventually_rev_mp, auto simp: eventually_sequentially dist_real_def)  then obtain n where "0 < p n" "p n < 1" and [arith]: "0 < n"      and probs: "pf_short_count n < 1/2" "pf_α n < 1/2"    by (auto simp: eventually_sequentially)  then interpret ES: edge_space n "(p n)" by unfold_locales auto  have rest_compl: "!!A P. A - {x∈A. P x} = {x∈A. ¬P x}" by blast  from probs have "ES.prob ({es ∈ space ES.P. n/2 ≤ short_count (?ug n es)}      ∪ {es ∈ space ES.P. 1/2 * n/k ≤ α (?ug n es)}) ≤ pf_short_count n + pf_α n"    unfolding pf_short_count_def pf_α_def  by (subst ES.finite_measure_subadditive) auto  also have "… < 1" using probs by auto  finally have "0 < ES.prob (space ES.P - ({es ∈ space ES.P. n/2 ≤ short_count (?ug n es)}      ∪ {es ∈ space ES.P. 1/2 * n/k ≤ α (?ug n es)}))" (is "0 < ES.prob ?S")    by (subst ES.prob_compl) auto  also have "?S = {es ∈ space ES.P. short_count (?ug n es) < n/2 ∧ α (?ug n es) < 1/2* n/k}" (is "… = ?C")    by (auto simp: not_less rest_compl)  finally have "?C ≠ {}" by (intro notI) (simp only:, auto)  then obtain es where es_props: "es ∈ space ES.P"      "short_count (?ug n es) < n/2" "α (?ug n es) < 1/2 * n/k"    by auto    -- "now we obtained a high colored graph (few independent nodes) with almost no short cycles"  def G ≡ "?ug n es"  def H ≡ "kill_short G k"  have G_props: "uverts G = {1..n}" "finite (uverts G)" "short_count G < n/2" "α G < 1/2 * n/k"    unfolding G_def using es_props by (auto simp: ES.S_verts_def)  have "uwellformed G" by (auto simp: G_def uwellformed_def all_edges_def ES.S_edges_def)  with G_props have T1: "uwellformed H" unfolding H_def by (intro kill_short_uwellformed)  have "enat l ≤ enat k" using `l ≤ k` by simp  also have "… < girth H" using G_props by (auto simp: kill_short_large_girth H_def)  finally have T2: "l < girth H" .  have card_H: "n/2 ≤ card (uverts H)"    using G_props es_props kill_short_order_of_graph[of G k] by (simp add: short_count_def H_def)  then have uverts_H: "uverts H ≠ {}" "0 < card (uverts H)" by auto  then have "0 < α H" using zero_less_α uverts_H by auto  have α_HG: "α H ≤ α G"    unfolding H_def G_def by (auto intro: kill_short_α)  have "enat l ≤ ereal k" using `l ≤ k` by auto  also have "… < (n/2) / α G" using G_props `3 ≤ k`    by (cases "α G") (auto simp: real_of_nat_def[symmetric] field_simps)  also have "… ≤ (n/2) / α H" using α_HG `0 < α H`    by (auto simp: ereal_of_enat_pushout intro!: ereal_divide_left_mono)  also have "… ≤ card (uverts H) / α H" using card_H `0 < α H`    by (auto intro!: ereal_divide_right_mono)  also have "… ≤ chromatic_number H" using uverts_H T1 by (intro chromatic_lb) auto  finally have T3: "l < chromatic_number H"    by (simp add: ereal_of_enat_less_iff del: ereal_of_enat_simps)  from T1 T2 T3 show ?thesis by fastqedend`