Theory Turan
theory Turan
imports
"Girth_Chromatic.Ugraphs"
"Random_Graph_Subgraph_Threshold.Ugraph_Lemmas"
begin
section ‹Basic facts on graphs›
lemma wellformed_uverts_0 :
assumes "uwellformed G" and "uverts G = {}"
shows "card (uedges G) = 0" using assms
by (metis uwellformed_def card.empty ex_in_conv zero_neq_numeral)
lemma finite_verts_edges :
assumes "uwellformed G" and "finite (uverts G)"
shows "finite (uedges G)"
proof -
have sub_pow: "uwellformed G ⟹ uedges G ⊆ {S. S ⊆ uverts G}"
by (cases G, auto simp add: uwellformed_def)
then have "finite {S. S ⊆ uverts G}" using assms
by auto
with sub_pow assms show "finite (uedges G)"
using finite_subset by blast
qed
lemma ugraph_max_edges :
assumes "uwellformed G" and "card (uverts G) = n" and "finite (uverts G)"
shows "card (uedges G) ≤ n * (n-1)/2"
using assms wellformed_all_edges [OF assms(1)] card_all_edges [OF assms(3)] Binomial.choose_two [of "card(uverts G)"]
by (smt (verit, del_insts) all_edges_finite card_mono dbl_simps(3) dbl_simps(5) div_times_less_eq_dividend le_divide_eq_numeral1(1) le_square nat_mult_1_right numerals(1) of_nat_1 of_nat_diff of_nat_mono of_nat_mult of_nat_numeral right_diff_distrib')
lemma subgraph_verts_finite : "⟦ finite (uverts G); subgraph G' G ⟧ ⟹ finite (uverts G')"
using rev_finite_subset subgraph_def by auto
section ‹Cliques›
text ‹In this section a straightforward definition of cliques for simple, undirected graphs is introduced.
Besides fundamental facts about cliques, also more specialized lemmata are proved in subsequent subsections.›
definition uclique :: "ugraph ⇒ ugraph ⇒ nat ⇒ bool" where
"uclique C G p ≡ p = card (uverts C) ∧ subgraph C G ∧ C = complete (uverts C)"
lemma clique_any_edge :
assumes "uclique C G p" and "x ∈ uverts C" and "y ∈ uverts C" and "x ≠ y"
shows "{x,y} ∈ uedges G"
using assms
apply (simp add: uclique_def complete_def all_edges_def subgraph_def)
by (smt (verit, best) SigmaI fst_conv image_iff mem_Collect_eq mk_uedge.simps snd_conv subset_eq)
lemma clique_exists : "∃ C p. uclique C G p ∧ p ≤ card (uverts G)"
using bex_imageD card.empty emptyE gr_implies_not0 le_neq_implies_less
by (auto simp add: uclique_def complete_def subgraph_def all_edges_def)
lemma clique_exists1 :
assumes "uverts G ≠ {}" and "finite (uverts G)"
shows "∃ C p. uclique C G p ∧ 0 < p ∧ p ≤ card (uverts G)"
proof -
obtain x where x: "x ∈ uverts G"
using assms
by auto
show ?thesis
apply (rule exI [of _ "({x},{})"], rule exI [of _ 1])
using x assms(2)
by (simp add: uclique_def subgraph_def complete_def all_edges_def Suc_leI assms(1) card_gt_0_iff)
qed
lemma clique_max_size : "uclique C G p ⟹ finite (uverts G) ⟹ p ≤ card (uverts G)"
by (auto simp add: uclique_def subgraph_def Finite_Set.card_mono)
lemma clique_exists_gt0 :
assumes "finite (uverts G)" "card (uverts G) > 0"
shows "∃ C p. uclique C G p ∧ p ≤ card (uverts G) ∧ (∀C q. uclique C G q ⟶ q ≤ p)"
proof -
have 1: "finite (uverts G) ⟹ finite {p. ∃C. uclique C G p}"
using clique_max_size
by (smt (verit, best) finite_nat_set_iff_bounded_le mem_Collect_eq)
have 2: "⋀A::nat set. finite A ⟹ ∃x. x∈A ⟹ ∃x∈A.∀y∈A. y ≤ x"
using Max_ge Max_in by blast
have "∃C p. uclique C G p ∧ (∀C q. uclique C G q ⟶ q ≤ p)"
using 2 [OF 1 [OF ‹finite (uverts G)›]] clique_exists [of G]
by (smt (z3) mem_Collect_eq)
then show ?thesis
using ‹finite (uverts G)› clique_max_size
by blast
qed
text ‹If there exists a $(p+1)$-clique @{term C} in a graph @{term G}
then we can obtain a $p$-clique in @{term G} by removing an arbitrary vertex from @{term C}›
lemma clique_size_jumpfree :
assumes "finite (uverts G)" and "uwellformed G"
and "uclique C G (p+1)"
shows "∃C'. uclique C' G p"
proof -
have "card(uverts G) > p"
using assms by (simp add: uclique_def subgraph_def card_mono less_eq_Suc_le)
obtain x where x: "x ∈ uverts C"
using assms by (fastforce simp add: uclique_def)
have "mk_uedge ` {uv ∈ uverts C × uverts C. fst uv ≠ snd uv} - {A ∈ uedges C. x ∈ A} =
mk_uedge ` {uv ∈ (uverts C - {x}) × (uverts C - {x}). fst uv ≠ snd uv}"
proof -
have "⋀y. y ∈ mk_uedge ` {uv ∈ uverts C × uverts C. fst uv ≠ snd uv} - {A ∈ uedges C. x ∈ A} ⟹
y ∈ mk_uedge ` {uv ∈ (uverts C - {x}) × (uverts C - {x}). fst uv ≠ snd uv}"
using assms(3)
apply (simp add: uclique_def complete_def all_edges_def)
by (smt (z3) DiffI SigmaE SigmaI image_iff insertCI mem_Collect_eq mk_uedge.simps singleton_iff snd_conv)
moreover have "⋀y. y ∈ mk_uedge ` {uv ∈ (uverts C - {x}) × (uverts C - {x}). fst uv ≠ snd uv}
⟹ y ∈ mk_uedge ` {uv ∈ uverts C × uverts C. fst uv ≠ snd uv} - {A ∈ uedges C. x ∈ A}"
apply (simp add: uclique_def complete_def all_edges_def)
by (smt (z3) DiffE SigmaE SigmaI image_iff insert_iff mem_Collect_eq mk_uedge.simps singleton_iff)
ultimately show ?thesis
by blast
qed
then have 1: "(uverts C - {x}, uedges C - {A ∈ uedges C. x ∈ A}) = Ugraph_Lemmas.complete (uverts C - {x})"
using assms(3)
apply (simp add: uclique_def complete_def all_edges_def)
by (metis (no_types, lifting) snd_eqD)
show ?thesis
apply (rule exI [of _ "C -- x"])
using assms x
apply (simp add: uclique_def remove_vertex_def subgraph_def)
apply (simp add: 1)
by (auto simp add: complete_def all_edges_def)
qed
text ‹The next lemma generalises the lemma @{thm [source] clique_size_jumpfree} to a proof of
the existence of a clique of any size smaller than the size of the original clique.›
lemma clique_size_decr :
assumes "finite (uverts G)" and "uwellformed G"
and "uclique C G p"
shows "q ≤ p ⟹ ∃C. uclique C G q" using assms
proof (induction q rule: measure_induct [of "λx. p - x"])
case (1 x)
then show ?case
proof (cases "x = p")
case True
then show ?thesis
using ‹uclique C G p›
by blast
next
case False
with 1(2) have "x < p"
by auto
from ‹x < p› have "p - Suc x < p - x"
by auto
then show ?thesis
using 1(1) assms(1,2,3) ‹x < p›
using clique_size_jumpfree [OF ‹finite (uverts G)› ‹uwellformed G› _]
by (metis "1.prems"(4) add.commute linorder_not_le not_less_eq plus_1_eq_Suc)
qed
qed
text ‹With this lemma we can easily derive by contradiction that
if there is no $p$-clique then there cannot exist a clique of a size greater than @{term p}›
corollary clique_size_neg_max :
assumes "finite (uverts G)" and "uwellformed G"
and "¬(∃C. uclique C G p)"
shows "∀C q. uclique C G q ⟶ q < p"
proof (rule ccontr)
assume 1: "¬ (∀C q. uclique C G q ⟶ q < p)"
show False
proof -
obtain C q where C: "uclique C G q"
and q: "q ≥ p"
using 1 linorder_not_less
by blast
show ?thesis
using assms(3) q clique_size_decr [OF ‹finite (uverts G)› ‹uwellformed G› C ]
using order_less_imp_le by blast
qed
qed
corollary clique_complete :
assumes "finite V" and "x ≤ card V"
shows "∃C. uclique C (complete V) x"
proof -
have "uclique (complete V) (complete V) (card V)"
by (simp add: uclique_def complete_def subgraph_def)
then show ?thesis
using clique_size_decr [OF _ complete_wellformed [of V] _ assms(2)] assms(1)
by (simp add: complete_def)
qed
lemma subgraph_clique :
assumes "uwellformed G" "subgraph C G" "C = complete (uverts C)"
shows "{e ∈ uedges G. e ⊆ uverts C} = uedges C"
proof -
from assms complete_wellformed [of "uverts C"] have "uedges C ⊆ {e ∈ uedges G. e ⊆ uverts C}"
by (auto simp add: subgraph_def uwellformed_def)
moreover from assms(1) complete_wellformed [of "uverts C"] have "{e ∈ uedges G. e ⊆ uverts C} ⊆ uedges C"
apply (simp add: subgraph_def uwellformed_def complete_def card_2_iff all_edges_def)
using assms(3)[unfolded complete_def all_edges_def] in_mk_uedge_img
by (smt (verit, ccfv_threshold) SigmaI fst_conv insert_subset mem_Collect_eq snd_conv subsetI)
ultimately show ?thesis
by auto
qed
text ‹Next, we prove that in a graph @{term G} with a $p$-clique @{term C} and some vertex @{term v} outside of this clique,
there exists a $(p+1)$-clique in @{term G} if @{term v} is connected to all nodes in @{term C}.
The next lemma is an abstracted version that does not explicitly mention cliques:
If a vertex @{term n} has as many edges to a set of nodes @{term N} as there are nodes in @{term N}
then @{term n} is connected to all vertices in @{term N}.›
lemma card_edges_nodes_all_edges :
fixes G :: "ugraph" and N :: "nat set" and E :: "nat set set" and n :: nat
assumes "uwellformed G"
and "finite N"
and "N ⊆ uverts G" and "E ⊆ uedges G"
and "n ∈ uverts G" and "n ∉ N"
and "∀e ∈ E. ∃x ∈ N. {n,x} = e"
and "card E = card N"
shows "∀x ∈ N. {n,x} ∈ E"
proof (rule ccontr)
assume "¬(∀x ∈ N. {n,x} ∈ E)"
show False
proof -
obtain x where x: "x ∈ N" and e: "{n,x} ∉ E"
using ‹¬(∀x ∈ N. {n,x} ∈ E)›
by auto
have "E ⊆ (λy. {n,y}) ` (N - {x})"
using Set.image_diff_subset ‹∀e ∈ E. ∃x ∈ N. {n,x} = e› x e
by auto
then show ?thesis
using ‹finite N› ‹card E = card N› x
using surj_card_le [of "N - {x}" E "(λy. {n,y})"]
by (simp, metis card_gt_0_iff diff_less emptyE lessI linorder_not_le)
qed
qed
subsection ‹Partitioning edges along a clique›
text ‹Tur\'{a}n's proof partitions the edges of a graph into three partitions for a $(p-1)$-clique @{term C}:
All edges within @{term C}, all edges outside of @{term C}, and all edges between a vertex in @{term C} and a
vertex not in @{term C}.
We prove a generalized lemma that partitions the edges along some arbitrary set of vertices
which does not necessarily need to induce a clique.
Furthermore, in Tur\'{a}n's graph theorem we only argue about the cardinality of the partitions
so that we restrict this proof to showing that
the sum of the cardinalities of the partitions is equal to number of all edges.›
lemma graph_partition_edges_card :
assumes "finite (uverts G)" and "uwellformed G" and "A ⊆ (uverts G)"
shows "card (uedges G) = card {e ∈ uedges G. e ⊆ A} + card {e ∈ uedges G. e ⊆ uverts G - A} + card {e ∈ uedges G. e ∩ A ≠ {} ∧ e ∩ (uverts G - A) ≠ {}}"
using assms
proof -
have "uedges G = {e ∈ uedges G. e ⊆ A} ∪ {e ∈ uedges G. e ⊆ (uverts G) - A} ∪ {e ∈ uedges G. e ∩ A ≠ {} ∧ e ∩ ((uverts G) - A) ≠ {}}"
using assms uwellformed_def
by blast
moreover have "{e ∈ uedges G. e ⊆ A} ∩ {e ∈ uedges G. e ⊆ uverts G - A} = {}"
using assms uwellformed_def
by (smt (verit, ccfv_SIG) Diff_disjoint Int_subset_iff card.empty disjoint_iff mem_Collect_eq nat.simps(3) nat_1_add_1 plus_1_eq_Suc prod.sel(2) subset_empty)
moreover have "({e ∈ uedges G. e ⊆ A} ∪ {e ∈ uedges G. e ⊆ uverts G - A}) ∩ {e ∈ uedges G. e ∩ A ≠ {} ∧ e ∩ (uverts G - A) ≠ {}} = {}"
by blast
moreover have "finite {e ∈ uedges G. e ⊆ A}" using assms
by (simp add: finite_subset)
moreover have "finite {e ∈ uedges G. e ⊆ uverts G - A}" using assms
by (simp add: finite_subset)
moreover have "finite {e ∈ uedges G. e ∩ A ≠ {} ∧ e ∩ (uverts G - A) ≠ {}}"
using assms finite_verts_edges
by auto
ultimately show ?thesis
using assms Finite_Set.card_Un_disjoint
by (smt (verit, best) finite_UnI)
qed
text ‹Now, we turn to the problem of calculating the cardinalities of these partitions
when they are induced by the biggest clique in the graph.
First, we consider the number of edges in a $p$-clique.›
lemma clique_edges_inside :
assumes G1: "uwellformed G" and G2: "finite (uverts G)"
and p: "p ≤ card (uverts G)" and n: "n = card(uverts G)"
and C: "uclique C G p"
shows "card {e ∈ uedges G. e ⊆ uverts C} = p * (p-1) / 2"
proof -
have "2 dvd (card (uverts C) * (p - 1))"
using C uclique_def
by auto
have "2 = real 2"
by simp
then show ?thesis
using C uclique_def [of C G p] complete_def [of "uverts C"]
using subgraph_clique [OF G1, of C] subgraph_verts_finite [OF assms(2), of C]
using Real.real_of_nat_div [OF ‹2 dvd (card (uverts C) * (p - 1))›] Binomial.choose_two [of " card (uverts G)"]
by (smt (verit, del_insts) One_nat_def approximation_preproc_nat(5) card_all_edges diff_self_eq_0 eq_imp_le left_diff_distrib' left_diff_distrib' linorder_not_less mult_le_mono2 choose_two not_gr0 not_less_eq_eq of_nat_1 of_nat_diff snd_eqD)
qed
text ‹Next, we turn to the number of edges that connect a node inside of the biggest clique with
a node outside of said clique. For that we start by calculating a bound for the number of
edges from one single node outside of the clique into the clique.›
lemma clique_edges_inside_to_node_outside :
assumes "uwellformed G" and "finite (uverts G)"
assumes "0 < p" and "p ≤ card (uverts G)"
assumes "uclique C G p" and "(∀C p'. uclique C G p' ⟶ p' ≤ p)"
assumes y: "y ∈ uverts G - uverts C"
shows "card {{x,y}| x. x ∈ uverts C ∧ {x,y} ∈ uedges G} ≤ p - 1"
proof (rule ccontr)
txt ‹For effective proof automation we use a local function definition to compute this
set of edges into the clique from any node @{term y}:›
define S where "S ≡ λy. {{x,y}| x. x ∈ uverts C ∧ {x,y} ∈ uedges G}"
assume "¬ card {{x, y} |x. x ∈ uverts C ∧ {x, y} ∈ uedges G} ≤ p - 1"
then have Sy: "card (S y) > p - 1"
using S_def y by auto
have "uclique ({y} ∪ (uverts C),S y ∪ uedges C) G (Suc p)"
proof -
have "card ({y} ∪ uverts C) = Suc p"
using assms(3,5,7) uclique_def
by (metis DiffD2 card_gt_0_iff card_insert_disjoint insert_is_Un)
moreover have "subgraph ({y} ∪ uverts C, (S y) ∪ uedges C) G"
using assms(5,7)
by (auto simp add: uclique_def subgraph_def S_def)
moreover have "({y} ∪ (uverts C),(S y) ∪ uedges C) = complete ({y} ∪ (uverts C))"
proof -
have "(S y) ∪ uedges C ⊆ all_edges ({y} ∪ (uverts C))"
using y assms(5) S_def all_edges_def uclique_def complete_def
by (simp, smt (z3) SigmaE SigmaI fst_conv image_iff in_mk_uedge_img insertCI mem_Collect_eq snd_conv subsetI)
moreover have "all_edges ({y} ∪ (uverts C)) ⊆ (S y) ∪ uedges C"
proof -
have "∀x∈uverts C. {y, x} ∈ S y"
proof -
have "card (S y) = card (uverts C)"
using Sy assms(2,3,5,7) S_def uclique_def card_gt_0_iff
using Finite_Set.surj_card_le [of "uverts C" "S y" "λx. {x, y}"]
by (smt (verit, del_insts) Suc_leI Suc_pred' image_iff le_antisym mem_Collect_eq subsetI)
then show ?thesis
using card_edges_nodes_all_edges [OF assms(1), of "uverts C" "S y" y] assms(1,2,5,7) S_def uclique_def
by (smt (verit, ccfv_threshold) DiffE insert_commute mem_Collect_eq subgraph_def subgraph_verts_finite subsetI)
qed
then show ?thesis
using assms(5) all_edges_def S_def uclique_def complete_def mk_uedge.simps in_mk_uedge_img
by (smt (z3) insert_commute SigmaI fst_conv mem_Collect_eq snd_conv SigmaE UnCI image_iff insert_iff insert_is_Un subsetI)
qed
ultimately show ?thesis
by (auto simp add: complete_def)
qed
ultimately show ?thesis
by (simp add: uclique_def complete_def)
qed
then show False
using assms(6)
by fastforce
qed
text ‹Now, that we have this upper bound for the number of edges from a single vertex into the largest clique
we can calculate the upper bound for all such vertices and edges:›
lemma clique_edges_inside_to_outside :
assumes G1: "uwellformed G" and G2: "finite (uverts G)"
and p0: "0 < p" and pn: "p ≤ card (uverts G)" and "card(uverts G) = n"
and C: "uclique C G p" and C_max: "(∀C p'. uclique C G p' ⟶ p' ≤ p)"
shows "card {e ∈ uedges G. e ∩ uverts C ≠ {} ∧ e ∩ (uverts G - uverts C) ≠ {}} ≤ (p - 1) * (n - p)"
proof -
define S where "S ≡ λy. {{x,y}| x. x ∈ uverts C ∧ {x,y} ∈ uedges G}"
have "card (uverts G - uverts C) = n - p"
using pn C ‹card(uverts G) = n› G2
apply (simp add: uclique_def)
by (meson card_Diff_subset subgraph_def subgraph_verts_finite)
moreover have "{e ∈ uedges G. e ∩ uverts C ≠ {} ∧ e ∩ (uverts G - uverts C) ≠ {}} = {{x,y}| x y. x ∈ uverts C ∧ y ∈ (uverts G - uverts C) ∧ {x,y} ∈ uedges G}"
proof -
have "e ∈ {e ∈ uedges G. e ∩ uverts C ≠ {} ∧ e ∩ (uverts G - uverts C) ≠ {}}
⟹ ∃x y. e = {x,y} ∧ x ∈ uverts C ∧ y ∈ uverts G - uverts C" for e
using G1
apply (simp add: uwellformed_def)
by (smt (z3) DiffD2 card_2_iff disjoint_iff_not_equal insert_Diff insert_Diff_if insert_iff)
then show ?thesis
by auto
qed
moreover have "card {{x,y}| x y. x ∈ uverts C ∧ y ∈ (uverts G - uverts C) ∧ {x,y} ∈ uedges G} ≤ card (uverts G - uverts C) * (p-1)"
proof -
have "card {{x,y}| x y. x ∈ uverts C ∧ y ∈ (uverts G - uverts C) ∧ {x,y} ∈ uedges G}
≤ (∑y ∈ (uverts G - uverts C). card (S y))"
proof -
have "finite (uverts G - uverts C)"
using ‹finite (uverts G)› by auto
have "{{x,y}| x y. x ∈ uverts C ∧ y ∈ (uverts G - uverts C) ∧ {x,y} ∈ uedges G}
= (⋃y ∈ (uverts G - uverts C). {{x,y}| x. x ∈ uverts C ∧ {x,y} ∈ uedges G})"
by auto
then show ?thesis
using Groups_Big.card_UN_le [OF ‹finite (uverts G - uverts C)›,
of "λy. {{x, y} |x. x ∈ uverts C ∧ {x, y} ∈ uedges G}"]
using S_def
by auto
qed
moreover have "(∑y∈uverts G - uverts C. card (S y)) ≤ card (uverts G - uverts C) * (p-1)"
proof -
have "card (S y) ≤ p - 1" if y: "y ∈ uverts G - uverts C" for y
using clique_edges_inside_to_node_outside [OF assms(1,2,3,4) C C_max y] S_def y
by simp
then show ?thesis
by (metis id_apply of_nat_eq_id sum_bounded_above)
qed
ultimately show ?thesis
using order_trans
by blast
qed
ultimately show ?thesis
by (smt (verit, ccfv_SIG) mult.commute)
qed
text ‹Lastly, we need to argue about the number of edges which are located entirely outside of
the greatest clique. Note that this is in the inductive step case in the overarching proof
of Tur\'{a}n's graph theorem. That is why we have access to the inductive hypothesis as an
assumption in the following lemma:›
lemma clique_edges_outside :
assumes "uwellformed G" and "finite (uverts G)"
and p2: "2 ≤ p" and pn: "p ≤ card (uverts G)" and n: "n = card(uverts G)"
and C: "uclique C G (p-1)" and C_max: "(∀C q. uclique C G q ⟶ q ≤ p-1)"
and IH: "⋀G y. y < n ⟹ finite (uverts G) ⟹ uwellformed G ⟹ ∀C p'. uclique C G p' ⟶ p' < p
⟹ 2 ≤ p ⟹ card (uverts G) = y ⟹ real (card (uedges G)) ≤ (1 - 1 / real (p - 1)) * real (y⇧2) / 2"
shows "card {e ∈ uedges G. e ⊆ uverts G - uverts C} ≤ (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2"
proof -
have "n - card (uverts C) < n"
using C pn p2 n
by (metis Suc_pred' diff_less less_2_cases_iff linorder_not_less not_gr0 uclique_def)
have GC1: "finite (uverts (uverts G - uverts C, {e ∈ uedges G. e ⊆ uverts G - uverts C}))"
using assms(2)
by simp
have GC2: "uwellformed (uverts G - uverts C, {e ∈ uedges G. e ⊆ uverts G - uverts C})"
using assms(1)
by (auto simp add: uwellformed_def)
have GC3: "∀C' p'. uclique C' (uverts G - uverts C, {e ∈ uedges G. e ⊆ uverts G - uverts C}) p' ⟶ p' < p"
proof (rule ccontr)
assume "¬(∀C' p'. uclique C' (uverts G - uverts C, {e ∈ uedges G. e ⊆ uverts G - uverts C}) p' ⟶ p' < p)"
then obtain C' p' where C': "uclique C' (uverts G - uverts C, {e ∈ uedges G. e ⊆ uverts G - uverts C}) p'" and p': "p' ≥ p"
by auto
then have "uclique C' G p'"
using uclique_def subgraph_def
by auto
then show False
using p' p2 C_max
by fastforce
qed
have GC4: "card (uverts (uverts G - uverts C,{e ∈ uedges G. e ⊆ uverts G - uverts C})) = n - card (uverts C)"
using C n assms(2) uclique_def subgraph_def
by (simp, meson card_Diff_subset infinite_super)
show ?thesis
using C GC3 IH [OF ‹n - card (uverts C) < n› GC1 GC2 GC3 ‹2 ≤ p› GC4] assms(2) n uclique_def
by (simp, smt (verit, best) C One_nat_def Suc_1 Suc_leD clique_max_size of_nat_1 of_nat_diff p2)
qed
subsection ‹Extending the size of the biggest clique› text_raw ‹\label{sec:extend_clique}›
text ‹In this section, we want to prove that we can add edges to a graph so that we augment the biggest clique
to some greater clique with a specific number of vertices. For that, we need the following lemma:
When too many edges have been added to a graph so that there exists a $(p+1)$-clique
then we can remove at least one of the added edges while also retaining a p-clique›
lemma clique_union_size_decr :
assumes "finite (uverts G)" and "uwellformed (uverts G, uedges G ∪ E)"
and "uclique C (uverts G, uedges G ∪ E) (p+1)"
and "card E ≥ 1"
shows "∃C' E'. card E' < card E ∧ uclique C' (uverts G, uedges G ∪ E') p ∧ uwellformed (uverts G, uedges G ∪ E')"
proof (cases "∃x ∈ uverts C. ∃e ∈ E. x ∈ e")
case True
then obtain x where x1: "x ∈ uverts C" and x2: "∃e ∈ E. x ∈ e"
by auto
show ?thesis
proof (rule exI [of _ "C -- x"], rule exI [of _ "{e ∈ E. x ∉ e}"])
have "card {e ∈ E. x ∉ e} < card E"
using x2 assms(4)
by (smt (verit) One_nat_def card.infinite diff_is_0_eq mem_Collect_eq minus_nat.diff_0 not_less_eq psubset_card_mono psubset_eq subset_eq)
moreover have "uclique (C -- x) (uverts G, uedges G ∪ {e ∈ E. x ∉ e}) p"
proof -
have "p = card (uverts (C -- x))"
using x1 assms(3)
by (auto simp add: uclique_def remove_vertex_def)
moreover have "subgraph (C -- x) (uverts G, uedges G ∪ {e ∈ E. x ∉ e})"
using assms(3)
by (auto simp add: uclique_def subgraph_def remove_vertex_def)
moreover have "C -- x = Ugraph_Lemmas.complete (uverts (C -- x))"
proof -
have 1: "⋀y. y ∈ mk_uedge ` {uv ∈ uverts C × uverts C. fst uv ≠ snd uv} - {A ∈ uedges C. x ∈ A} ⟹
y ∈ mk_uedge ` {uv ∈ (uverts C - {x}) × (uverts C - {x}). fst uv ≠ snd uv}"
by (smt (z3) DiffE DiffI SigmaE SigmaI Ugraph_Lemmas.complete_def all_edges_def assms(3) empty_iff image_iff insert_iff mem_Collect_eq mk_uedge.simps snd_conv uclique_def)
have 2: "⋀y. y ∈ mk_uedge ` {uv ∈ (uverts C - {x}) × (uverts C - {x}). fst uv ≠ snd uv} ⟹
y ∈ mk_uedge ` {uv ∈ uverts C × uverts C. fst uv ≠ snd uv} - {A ∈ uedges C. x ∈ A}"
by (smt (z3) DiffE DiffI SigmaE SigmaI image_iff insert_iff mem_Collect_eq mk_uedge.simps singleton_iff)
show ?thesis
using assms(3)
apply (simp add: remove_vertex_def complete_def all_edges_def uclique_def)
using 1 2
by (smt (verit, ccfv_SIG) split_pairs subset_antisym subset_eq)
qed
ultimately show ?thesis
by (simp add: uclique_def)
qed
moreover have "uwellformed (uverts G, uedges G ∪ {e ∈ E. x ∉ e})"
using assms(2)
by (auto simp add: uwellformed_def)
ultimately show "card {e ∈ E. x ∉ e} < card E ∧
uclique (C -- x) (uverts G, uedges G ∪ {e ∈ E. x ∉ e}) p ∧
uwellformed (uverts G, uedges G ∪ {e ∈ E. x ∉ e})"
by auto
qed
next
case False
then have "⋀x. x ∈ uedges C ⟹ x ∉ E"
using assms(2)
by (metis assms(3) card_2_iff' complete_wellformed uclique_def uwellformed_def)
then have "uclique C G (p+1)"
using assms(3)
by (auto simp add: uclique_def subgraph_def uwellformed_def)
show ?thesis
using assms(2,4) clique_size_jumpfree [OF assms(1) _ ‹uclique C G (p+1)›]
apply (simp add: uwellformed_def)
by (metis Suc_le_eq UnCI Un_empty_right card.empty prod.exhaust_sel)
qed
text ‹We use this preceding lemma to prove the next result. In this lemma we assume that we have
added too many edges. The goal is then to remove some of the new edges appropriately so
that it is indeed guaranteed that there is no bigger clique.
Two proofs of this lemma will be described in the following.
Both fundamentally come down to the same core idea:
In essence, both proofs apply the well-ordering principle.
In the first proof we do so immediately by obtaining the minimum of a set:›
lemma clique_union_make_greatest :
fixes p n :: nat
assumes "finite (uverts G)" and "uwellformed G"
and "uwellformed (uverts G, uedges G ∪ E)" and "card(uverts G) ≥ p"
and "uclique C (uverts G, uedges G ∪ E) p"
and "∀C' q'. uclique C' G q' ⟶ q' < p" and "1 ≤ card E"
shows "∃C' E'. uwellformed (uverts G, uedges G ∪ E')
∧ (uclique C' (uverts G, uedges G ∪ E') p)
∧ (∀C'' q'. uclique C'' (uverts G, uedges G ∪ E') q' ⟶ q' ≤ p)"
using assms
proof (induction "card E" arbitrary: C E rule: less_induct)
case (less E)
then show ?case
proof (cases "∃A. uclique A (uverts G, uedges G ∪ E) (p+1)")
case True
then obtain A where A: "uclique A (uverts G, uedges G ∪ E) (p+1)"
by auto
obtain C' E' where E'1: "card E' < card E"
and E'2: "uclique C' (uverts G, uedges G ∪ E') p"
and E'3: "uwellformed (uverts G, uedges G ∪ E')"
and E'4: "1 ≤ card E'"
using less(7)
using clique_union_size_decr [OF assms(1) ‹uwellformed (uverts G, uedges G ∪ E)› A less(8)]
by (metis One_nat_def Suc_le_eq Un_empty_right card_gt_0_iff finite_Un finite_verts_edges fst_conv less.prems(1) less_not_refl prod.collapse snd_conv)
show ?thesis
using less(1) [OF E'1 assms(1,2) E'3 less(5) E'2 less(7) E'4]
using E'1 less(8)
by (meson less_or_eq_imp_le order_le_less_trans)
next
case False
show ?thesis
apply (rule exI [of _ C], rule exI [of _ E])
using clique_size_neg_max [OF _ less(4) False]
using less(2,4,6)
by fastforce
qed
qed
text ‹In this second, alternative proof the well-ordering principle is used through complete induction.›
lemma clique_union_make_greatest_alt :
fixes p n :: nat
assumes "finite (uverts G)" and "uwellformed G"
and "uwellformed (uverts G, uedges G ∪ E)" and "card(uverts G) ≥ p"
and "uclique C (uverts G, uedges G ∪ E) p"
and "∀C' q'. uclique C' G q' ⟶ q' < p" and "1 ≤ card E"
shows "∃C' E'. uwellformed (uverts G, uedges G ∪ E')
∧ (uclique C' (uverts G, uedges G ∪ E') p)
∧ (∀C'' q'. uclique C'' (uverts G, uedges G ∪ E') q' ⟶ q' ≤ p)"
proof -
define P where "P ≡ λE. uwellformed (uverts G, uedges G ∪ E) ∧ (∃C. uclique C (uverts G, uedges G ∪ E) p)"
have "finite {y. ∃E. P E ∧ card E = y}"
proof -
have "⋀E. P E ⟹ E ⊆ Pow (uverts G)"
by (auto simp add: P_def uwellformed_def)
then have "finite {E. P E}"
using assms(1)
by (metis Collect_mono Pow_def finite_Pow_iff rev_finite_subset)
then show ?thesis
by simp
qed
obtain F where F1: "P F"
and F2: "card F = Min {y. ∃E. P E ∧ card E = y}"
and F3: "card F > 0"
using assms(1,3,4,5,6) Min_in ‹finite {y. ∃E. P E ∧ card E = y}› P_def CollectD Collect_empty_eq
by (smt (verit, ccfv_threshold) Un_empty_right card_gt_0_iff finite_Un finite_verts_edges fst_conv le_refl linorder_not_le prod.collapse snd_conv)
have "p > 0"
using assms(6) clique_exists bot_nat_0.not_eq_extremum
by blast
then show ?thesis
proof (cases "∃C. uclique C (uverts G, uedges G ∪ F) (p + 1)")
case True
then obtain F' where F'1 : "P F'" and F'2: "card F' < card F"
using F1 F2 F3 clique_union_size_decr [OF assms(1), of F _ p] P_def
by (smt (verit) One_nat_def Suc_eq_plus1 Suc_leI add_2_eq_Suc' assms(1) clique_size_jumpfree fst_conv)
then show ?thesis
using F2 ‹finite {y. ∃F. P F ∧ card F = y}› Min_gr_iff
by fastforce
next
case False
then show ?thesis
using clique_size_neg_max [OF _ _ False]
using assms(1) F1 P_def
by (smt (verit, ccfv_SIG) Suc_eq_plus1 Suc_leI fst_conv linorder_not_le)
qed
qed
text ‹Finally, with this lemma we can turn to this section's main challenge of increasing the
greatest clique size of a graph by adding edges.›
lemma clique_add_edges_max :
fixes p :: nat
assumes "finite (uverts G)"
and "uwellformed G" and "card(uverts G) > p"
and "∃C. uclique C G p" and "(∀C q'. uclique C G q' ⟶ q' ≤ p)"
and "q ≤ card(uverts G)" and "p ≤ q"
shows "∃E. uwellformed (uverts G, uedges G ∪ E) ∧ (∃C. uclique C (uverts G, uedges G ∪ E) q)
∧ (∀C q'. uclique C (uverts G, uedges G ∪ E) q' ⟶ q' ≤ q)"
proof (cases "p < q")
case True
then show ?thesis
proof -
have "∃E. uwellformed (uverts G, uedges G ∪ E) ∧ (∃C. uclique C (uverts G, uedges G ∪ E) q) ∧ card E ≥ 1"
apply (rule exI [of _ "all_edges (uverts G)"])
using Set.Un_absorb1 [OF wellformed_all_edges [OF assms(2)]]
using complete_wellformed [of "uverts G"] clique_complete [OF assms(1,6)]
using all_edges_def assms(1,5)
apply (simp add: complete_def)
by (metis Suc_leI True Un_empty_right all_edges_finite card_gt_0_iff linorder_not_less prod.collapse)
then obtain E C where E1: "uwellformed (uverts G, uedges G ∪ E)"
and E2: "uclique C (uverts G, uedges G ∪ E) q"
and E3: "card E ≥ 1"
by auto
show ?thesis
using clique_union_make_greatest [OF assms(1,2) E1 assms(6) E2 _ E3] assms(5) True
using order_le_less_trans
by blast
qed
next
case False
show ?thesis
apply (rule exI [of _ "{}"])
using False assms(2,4,5,7)
by simp
qed
section ‹Properties of the upper edge bound›
text ‹In this section we prove results about the upper edge bound in Tur\'{a}n's theorem.
The first lemma proves that upper bounds of the sizes of the partitions sum up exactly to the overall upper bound.›
lemma turan_sum_eq :
fixes n p :: nat
assumes "p ≥ 2" and "p ≤ n"
shows "(p-1) * (p-2) / 2 + (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2 + (p - 2) * (n - p + 1) = (1 - 1 / (p-1)) * n^2 / 2"
proof -
have "a * (a-1) / 2 + (1 - 1 / a) * (n - a) ^ 2 / 2 + (a - 1) * (n - a) = (1 - 1 / a) * n^2 / 2"
if a1: "a ≥ 1" and a2: "n ≥ a"
for a :: nat
proof -
have "a⇧2 + (n - a)⇧2 + a * (n - a) * 2 = n⇧2"
using a2
apply (simp flip: Groups.ab_semigroup_mult_class.mult.commute [of 2 "a * (n - a)"])
apply (simp add: Semiring_Normalization.comm_semiring_1_class.semiring_normalization_rules(18) [of 2 a "(n - a)"])
by (simp flip: Power.comm_semiring_1_class.power2_sum [of a "n-a"])
then have "((a - 1) / a) * (a ^ 2 + (n - a) ^ 2 + a * (n - a) * 2) = ((a - 1) / a) * n^2"
by presburger
then have "(((a - 1) / a) * a ^ 2 + ((a - 1) / a) * (n - a) ^ 2 + ((a - 1) / a) * a * (n - a) * 2) = ..."
using Rings.semiring_class.distrib_left [of "(a - 1) / a" "a⇧2 + (n - a)⇧2" "a * (n - a) * 2"]
using Rings.semiring_class.distrib_left [of "(a - 1) / a" "a⇧2" "(n - a)⇧2"]
by auto
moreover have "((a - 1) / a) * a ^ 2 = a * (a-1)"
by (simp add: power2_eq_square)
ultimately have "a * (a-1) + ((a - 1) / a) * (n - a) ^ 2 + (a - 1) * (n - a) * 2 = ((a - 1) / a) * n^2"
using a1 a2
by auto
moreover have "1 - 1 / a = (a - 1) / a"
by (smt (verit, del_insts) One_nat_def Suc_pred diff_divide_distrib diff_is_0_eq of_nat_1 of_nat_diff of_nat_le_0_iff of_nat_le_iff of_nat_less_iff right_inverse_eq that)
ultimately have "a * (a-1) + (1 - 1 / a) * (n - a) ^ 2 + (a - 1) * (n - a) * 2 = (1 - 1 / a) * n^2"
by simp
then show ?thesis
by simp
qed
moreover have "p - 1 ≥ 1"
using ‹p ≥ 2› by auto
moreover have "n ≥ p - 1"
using assms(2) by auto
ultimately show ?thesis
by (smt (verit) assms Nat.add_diff_assoc2 Nat.diff_diff_right diff_diff_left le_eq_less_or_eq less_Suc_eq_le linorder_not_less nat_1_add_1 plus_1_eq_Suc)
qed
text ‹The next fact proves that the upper bound of edges is monotonically increasing with the size of the biggest clique.›
lemma turan_mono :
fixes n p q :: nat
assumes "0 < q" and "q < p" and "p ≤ n"
shows "(1 - 1 / q) * n^2 / 2 ≤ (1 - 1 / (p-1)) * n^2 / 2"
using assms
by (simp add: Extended_Nonnegative_Real.divide_right_mono_ennreal Real.inverse_of_nat_le)
section ‹Tur\'{a}n's Graph Theorem›
text ‹In this section we turn to the direct adaptation of Tur\'{a}n's original proof as presented by Aigner and Ziegler \cite{Aigner2018}›
theorem turan :
fixes p n :: nat
assumes "finite (uverts G)"
and "uwellformed G" and "∀C p'. uclique C G p' ⟶ p' < p" and "p ≥ 2" and "card(uverts G) = n"
shows "card (uedges G) ≤ (1 - 1 / (p-1)) * n^2 / 2" using assms
proof (induction n arbitrary: G rule: less_induct)
case (less n)
then show ?case
proof (cases "n < p")
case True
show ?thesis
proof (cases "n")
case 0
with less True show ?thesis
by (auto simp add: wellformed_uverts_0)
next
case (Suc n')
with True have "(1 - 1 / real n) ≤ (1 - 1 / real (p - 1))"
by (metis diff_Suc_1 diff_left_mono inverse_of_nat_le less_Suc_eq_le linorder_not_less list_decode.cases not_add_less1 plus_1_eq_Suc)
moreover have "real (card (uedges G)) ≤ (1 - 1 / real n) * real (n⇧2) / 2"
using ugraph_max_edges [OF less(3,6,2)]
by (smt (verit, ccfv_SIG) left_diff_distrib mult.right_neutral mult_of_nat_commute nonzero_mult_div_cancel_left of_nat_1 of_nat_mult power2_eq_square times_divide_eq_left)
ultimately show ?thesis
using Rings.ordered_semiring_class.mult_right_mono divide_less_eq_numeral1(1) le_less_trans linorder_not_less of_nat_0_le_iff
by (smt (verit, ccfv_threshold) divide_nonneg_nonneg times_divide_eq_right)
qed
next
case False
show ?thesis
proof -
obtain C q where C: "uclique C G q"
and C_max: "(∀C q'. uclique C G q' ⟶ q' ≤ q)"
and q: "q < card (uverts G)"
using clique_exists_gt0 [OF ‹finite (uverts G)›] False ‹p ≥ 2› less.prems(1,3,5)
by (metis card.empty card_gt_0_iff le_eq_less_or_eq order_less_le_trans pos2)
obtain E C' where E: "uwellformed (uverts G, uedges G ∪ E)"
and C': "(uclique C' (uverts G, uedges G ∪ E) (p-1))"
and C'_max: "(∀C q'. uclique C (uverts G, uedges G ∪ E) q' ⟶ q' ≤ p-1)"
using clique_add_edges_max [OF ‹finite (uverts G)› ‹uwellformed G› q _ C_max, of "p-1"]
using C less(4) less(5) False ‹card (uverts G) = n›
by (smt (verit) One_nat_def Suc_leD Suc_pred less_Suc_eq_le linorder_not_less order_less_le_trans pos2)
have "card {e ∈ uedges G ∪ E. e ⊆ uverts C'} = (p-1) * (p-2) / 2"
using clique_edges_inside [OF E _ _ _ C'] False less(2) less.prems(4) C'
by (smt (verit, del_insts) Collect_cong Suc_1 add_leD1 clique_max_size fst_conv of_nat_1 of_nat_add of_nat_diff of_nat_mult plus_1_eq_Suc snd_conv)
moreover have "card {e ∈ uedges G ∪ E. e ⊆ uverts G - uverts C'} ≤ (1 - 1 / (p-1)) * (n - p + 1) ^ 2 / 2"
proof -
have "real(card{e ∈ uedges (uverts G, uedges G ∪ E). e ⊆ uverts (uverts G, uedges G ∪ E) - uverts C'})
≤ (1 - 1 / (real p - 1)) * (real n - real p + 1)⇧2 / 2"
using clique_edges_outside [OF E _ less(5) _ _ C' C'_max, of n] linorder_class.leI [OF False] less(1,2,6)
by (metis (no_types, lifting) fst_conv)
then show ?thesis
by (simp, smt (verit, best) False One_nat_def Suc_1 Suc_leD add.commute leI less.prems(4) of_nat_1 of_nat_diff)
qed
moreover have "card {e ∈ uedges G ∪ E. e ∩ uverts C' ≠ {} ∧ e ∩ (uverts G - uverts C') ≠ {}} ≤ (p - 2) * (n - p + 1)"
using clique_edges_inside_to_outside [OF E _ _ _ _ C' C'_max, of n] less(2,5,6)
by (simp, metis (no_types, lifting) C' False Nat.add_diff_assoc Nat.add_diff_assoc2 One_nat_def Suc_1 clique_max_size fst_conv leI mult_Suc_right plus_1_eq_Suc)
ultimately have "real (card (uedges G ∪ E)) ≤ (1 - 1 / real (p - 1)) * real (n⇧2) / 2"
using graph_partition_edges_card [OF _ E, of "uverts C'"]
using less(2) turan_sum_eq [OF ‹2 ≤ p›, of n] False C' uclique_def subgraph_def
by (smt (verit) Collect_cong fst_eqD linorder_not_le of_nat_add of_nat_mono snd_eqD)
then show ?thesis
using less(2) E finite_verts_edges Finite_Set.card_mono [OF _ Set.Un_upper1 [of "uedges G" E]]
by force
qed
qed
qed
section ‹A simplified proof of Tur\'{a}n's Graph Theorem›
text ‹In this section we discuss a simplified proof of Tur\'{a}n's Graph Theorem which uses an idea put forward by the author:
Instead of increasing the size of the biggest clique it is also possible to use the fact that
the expression in Tur\'{a}n's graph theorem is monotonically increasing in the size of the biggest clique (Lemma @{thm [source] turan_mono}).
Hence, it suffices to prove the upper bound for the actual biggest clique size in the graph.
Afterwards, the monotonicity provides the desired inequality.
The simplifications in the proof are annotated accordingly.›
theorem turan' :
fixes p n :: nat
assumes "finite (uverts G)"
and "uwellformed G" and "∀C p'. uclique C G p' ⟶ p' < p" and "p ≥ 2" and "card(uverts G) = n"
shows "card (uedges G) ≤ (1 - 1 / (p-1)) * n^2 / 2" using assms
proof (induction n arbitrary: p G rule: less_induct)
txt ‹In the simplified proof we also need to generalize over the biggest clique size @{term p}
so that we can leverage the induction hypothesis in the proof
for the already pre-existing biggest clique size which might be smaller than @{term "p-1"}.›
case (less n)
then show ?case
proof (cases "n < p")
case True
show ?thesis
proof (cases "n")
case 0
with less True show ?thesis
by (auto simp add: wellformed_uverts_0)
next
case (Suc n')
with True have "(1 - 1 / real n) ≤ (1 - 1 / real (p - 1))"
by (metis diff_Suc_1 diff_left_mono inverse_of_nat_le less_Suc_eq_le linorder_not_less list_decode.cases not_add_less1 plus_1_eq_Suc)
moreover have "real (card (uedges G)) ≤ (1 - 1 / real n) * real (n⇧2) / 2"
using ugraph_max_edges [OF less(3,6,2)]
by (smt (verit, ccfv_SIG) left_diff_distrib mult.right_neutral mult_of_nat_commute nonzero_mult_div_cancel_left of_nat_1 of_nat_mult power2_eq_square times_divide_eq_left)
ultimately show ?thesis
using Rings.ordered_semiring_class.mult_right_mono divide_less_eq_numeral1(1) le_less_trans linorder_not_less of_nat_0_le_iff
by (smt (verit, ccfv_threshold) divide_nonneg_nonneg times_divide_eq_right)
qed
next
case False
show ?thesis
proof -
from False ‹p ≥ 2›
obtain C q where C: "uclique C G q"
and C_max: "(∀C q'. uclique C G q' ⟶ q' ≤ q)"
and q1: "q < card (uverts G)" and q2: "0 < q"
and pq: "q < p"
using clique_exists_gt0 [OF ‹finite (uverts G)›] clique_exists1 less.prems(1,3,5)
by (metis card.empty card_gt_0_iff le_eq_less_or_eq order_less_le_trans pos2)
txt ‹In the unsimplified proof we extend this existing greatest clique C to a clique of size @{term "p-1"}.
This part is made superfluous in the simplified proof.
In particular, also Section \ref{sec:extend_clique} is unneeded for this simplified proof.
From here on the proof is analogous to the unsimplified proof
with the potentially smaller clique of size @{term q} in place of the extended clique.›
have "card {e ∈ uedges G. e ⊆ uverts C} = q * (q-1) / 2"
using clique_edges_inside [OF less(3,2) _ _ C] q1 less(6)
by auto
moreover have "card {e ∈ uedges G. e ⊆ uverts G - uverts C} ≤ (1 - 1 / q) * (n - q) ^ 2 / 2"
proof -
have "real (card {e ∈ uedges G. e ⊆ uverts G - uverts C})
≤ (1 - 1 / (real (q + 1) - 1)) * (real n - real (q + 1) + 1)⇧2 / 2"
using clique_edges_outside [OF less(3,2) _ _ , of "q+1" n C] C C_max q1 q2 linorder_class.leI [OF False] less(1,6)
by (smt (verit, ccfv_threshold) Suc_1 Suc_eq_plus1 Suc_leI diff_add_inverse2 zero_less_diff)
then show ?thesis
using less.prems(5) q1
by (simp add: of_nat_diff)
qed
moreover have "card {e ∈ uedges G. e ∩ uverts C ≠ {} ∧ e ∩ (uverts G - uverts C) ≠ {}} ≤ (q - 1) * (n - q)"
using clique_edges_inside_to_outside [OF less(3,2) q2 _ less(6) C C_max] q1
by simp
ultimately have "real (card (uedges G)) ≤ (1 - 1 / real q) * real (n⇧2) / 2"
using graph_partition_edges_card [OF less(2,3), of "uverts C"]
using C uclique_def subgraph_def q1 q2 less.prems(5) turan_sum_eq [of "Suc q" n]
by (smt (verit) Nat.add_diff_assoc Suc_1 Suc_le_eq Suc_le_mono add.commute add.right_neutral diff_Suc_1 diff_Suc_Suc of_nat_add of_nat_mono plus_1_eq_Suc)
then show ?thesis
txt ‹The final statement can then easily be derived with the monotonicity (Lemma @{thm [source] turan_mono}).›
using turan_mono [OF q2 pq, of n] False
by linarith
qed
qed
qed
end