Theory Undirected_Graph_Theory.Graph_Triangles
section ‹ Triangles in Graph ›
text ‹ Triangles are an important tool in graph theory. This theory presents a number of basic
definitions/lemmas which are useful for general reasoning using triangles. The definitions and lemmas
in this theory are adapted from previous less general work in \<^cite>‹"edmonds_szemeredis"› and \<^cite>‹"edmonds_roths"››
theory Graph_Triangles imports Undirected_Graph_Basics
"HOL-Combinatorics.Multiset_Permutations"
begin
text ‹ Triangles don't make as much sense in a loop context, hence we restrict this to simple graphs ›
context sgraph
begin
definition triangle_in_graph :: "'a ⇒ 'a ⇒ 'a ⇒ bool" where
"triangle_in_graph x y z ≡ ({x,y} ∈ E) ∧ ({y,z} ∈ E) ∧ ({x,z} ∈E)"
lemma triangle_in_graph_edge_empty: "E = {} ⟹ ¬ triangle_in_graph x y z"
using triangle_in_graph_def by auto
definition triangle_triples where
"triangle_triples X Y Z ≡ {(x,y,z) ∈ X × Y × Z. triangle_in_graph x y z }"
definition
"unique_triangles
≡ ∀e ∈ E. ∃!T. ∃x y z. T = {x,y,z} ∧ triangle_in_graph x y z ∧ e ⊆ T"
definition triangle_set :: "'a set set"
where "triangle_set ≡ { {x,y,z} | x y z. triangle_in_graph x y z}"
subsection ‹Preliminaries on Triangles in Graphs›
lemma card_triangle_triples_rotate: "card (triangle_triples X Y Z) = card (triangle_triples Y Z X)"
proof -
have "triangle_triples Y Z X = (λ(x,y,z). (y,z,x)) ` triangle_triples X Y Z"
by (auto simp: triangle_triples_def case_prod_unfold image_iff insert_commute triangle_in_graph_def)
moreover have "inj_on (λ(x, y, z). (y, z, x)) (triangle_triples X Y Z)"
by (auto simp: inj_on_def)
ultimately show ?thesis
by (simp add: card_image)
qed
lemma triangle_commu1:
assumes "triangle_in_graph x y z"
shows "triangle_in_graph y x z"
using assms triangle_in_graph_def by (auto simp add: insert_commute)
lemma triangle_vertices_distinct1:
assumes tri: "triangle_in_graph x y z"
shows "x ≠ y"
proof (rule ccontr)
assume a: "¬ x ≠ y"
have "card {x, y} = 2" using tri triangle_in_graph_def
using wellformed by (simp add: two_edges)
thus False using a by simp
qed
lemma triangle_vertices_distinct2:
assumes "triangle_in_graph x y z"
shows "y ≠ z"
by (metis assms triangle_vertices_distinct1 triangle_in_graph_def)
lemma triangle_vertices_distinct3:
assumes "triangle_in_graph x y z"
shows "z ≠ x"
by (metis assms triangle_vertices_distinct1 triangle_in_graph_def)
lemma triangle_in_graph_edge_point: "triangle_in_graph x y z ⟷ {y, z} ∈ E ∧ vert_adj x y ∧ vert_adj x z"
by (auto simp add: triangle_in_graph_def vert_adj_def)
lemma edge_vertices_not_equal:
assumes "{x,y} ∈ E"
shows "x ≠ y"
using assms two_edges by fastforce
lemma edge_btw_vertices_not_equal:
assumes "(x, y) ∈ all_edges_between X Y"
shows "x ≠ y"
using edge_vertices_not_equal all_edges_between_def
by (metis all_edges_betw_D3 assms)
lemma mk_triangle_from_ss_edges:
assumes "(x, y) ∈ all_edges_between X Y" and "(x, z) ∈ all_edges_between X Z" and "(y, z) ∈ all_edges_between Y Z"
shows "(triangle_in_graph x y z)"
by (meson all_edges_betw_D3 assms triangle_in_graph_def)
lemma triangle_in_graph_verts:
assumes "triangle_in_graph x y z "
shows "x ∈ V" "y ∈ V" "z∈ V"
proof -
show "x ∈ V" using triangle_in_graph_def wellformed_alt_fst assms by blast
show "y ∈ V" using triangle_in_graph_def wellformed_alt_snd assms by blast
show "z ∈ V" using triangle_in_graph_def wellformed_alt_snd assms by blast
qed
lemma convert_triangle_rep_ss:
assumes "X ⊆ V" and "Y ⊆ V" and "Z ⊆ V"
shows "mk_triangle_set ` {(x, y, z) ∈ X × Y × Z . (triangle_in_graph x y z)} ⊆ triangle_set"
by (auto simp add: subsetI triangle_set_def) (auto)
lemma (in fin_sgraph) finite_triangle_set: "finite (triangle_set)"
proof -
have "triangle_set ⊆ Pow V"
using insert_iff wellformed triangle_in_graph_def triangle_set_def by auto
then show ?thesis
by (meson finV finite_Pow_iff infinite_super)
qed
lemma card_triangle_3:
assumes "t ∈ triangle_set"
shows "card t = 3"
using assms by (auto simp: triangle_set_def edge_vertices_not_equal triangle_in_graph_def)
lemma triangle_set_power_set_ss: "triangle_set ⊆ Pow V"
by (auto simp add: triangle_set_def triangle_in_graph_def wellformed_alt_fst wellformed_alt_snd)
lemma triangle_in_graph_ss:
assumes "E' ⊆ E"
assumes "sgraph.triangle_in_graph E' x y z"
shows "triangle_in_graph x y z"
proof -
interpret gnew: sgraph V E'
apply (unfold_locales)
using assms wellformed two_edges by auto
have "{x, y} ∈ E" using assms gnew.triangle_in_graph_def by auto
have "{y, z} ∈ E" using assms gnew.triangle_in_graph_def by auto
have "{x, z} ∈ E" using assms gnew.triangle_in_graph_def by auto
thus ?thesis
by (simp add: ‹{x, y} ∈ E› ‹{y, z} ∈ E› triangle_in_graph_def)
qed
lemma triangle_set_graph_edge_ss:
assumes "E' ⊆ E"
shows "(sgraph.triangle_set E') ⊆ (triangle_set)"
proof (intro subsetI)
interpret gnew: sgraph V E'
using assms wellformed two_edges by (unfold_locales) auto
fix t assume "t ∈ gnew.triangle_set"
then obtain x y z where "t = {x,y,z}" and "gnew.triangle_in_graph x y z"
using gnew.triangle_set_def assms mem_Collect_eq by auto
then have "triangle_in_graph x y z" using assms triangle_in_graph_ss by simp
thus "t ∈ triangle_set" using triangle_set_def assms
using ‹t = {x,y,z}› by auto
qed
lemma (in fin_sgraph) triangle_set_graph_edge_ss_bound:
assumes "E' ⊆ E"
shows "card (triangle_set) ≥ card (sgraph.triangle_set E')"
using triangle_set_graph_edge_ss finite_triangle_set
by (simp add: assms card_mono)
end
locale triangle_free_graph = sgraph +
assumes tri_free: "¬(∃ x y z. triangle_in_graph x y z)"
lemma triangle_free_graph_empty: "E = {} ⟹ triangle_free_graph V E"
apply (unfold_locales, simp_all)
using sgraph.triangle_in_graph_edge_empty
by (metis Int_absorb all_edges_disjoint complete_sgraph)
context fin_sgraph
begin
text ‹Converting between ordered and unordered triples for reasoning on cardinality›
lemma card_convert_triangle_rep:
assumes "X ⊆ V" and "Y ⊆ V" and "Z ⊆ V"
shows "card (triangle_set) ≥ 1/6 * card {(x, y, z) ∈ X × Y × Z . (triangle_in_graph x y z)}"
(is "_ ≥ 1/6 * card ?TT")
proof -
define tofl where "tofl ≡ λl::'a list. (hd l, hd(tl l), hd(tl(tl l)))"
have in_tofl: "(x, y, z) ∈ tofl ` permutations_of_set {x,y,z}" if "x≠y" "y≠z" "x≠z" for x y z
proof -
have "distinct[x,y,z]"
using that by simp
then show ?thesis
unfolding tofl_def image_iff
by (smt (verit, best) list.sel(1) list.sel(3) list.simps(15) permutations_of_setI set_empty)
qed
have "?TT ⊆ {(x, y, z). (triangle_in_graph x y z)}"
by auto
also have "… ⊆ (⋃t ∈ triangle_set. tofl ` permutations_of_set t)"
proof (clarsimp simp: triangle_set_def)
fix u v w
assume t: "triangle_in_graph u v w"
then have "(u, v, w) ∈ tofl ` permutations_of_set {u,v,w}"
by (metis in_tofl triangle_commu1 triangle_vertices_distinct1 triangle_vertices_distinct2)
with t show "∃t. (∃x y z. t = {x, y, z} ∧ triangle_in_graph x y z) ∧ (u, v, w) ∈ tofl ` permutations_of_set t"
by blast
qed
finally have "?TT ⊆ (⋃t ∈ triangle_set. tofl ` permutations_of_set t)" .
then have "card ?TT ≤ card(⋃t ∈ triangle_set. tofl ` permutations_of_set t)"
by (intro card_mono finite_UN_I finite_triangle_set) (auto simp: assms)
also have "… ≤ (∑t ∈ triangle_set. card (tofl ` permutations_of_set t))"
using card_UN_le finV finite_triangle_set wellformed by blast
also have "… ≤ (∑t ∈ triangle_set. card (permutations_of_set t))"
by (meson card_image_le finite_permutations_of_set sum_mono)
also have "… ≤ (∑t ∈ triangle_set. fact 3)"
by(rule sum_mono) (metis card.infinite card_permutations_of_set card_triangle_3 eq_refl nat.simps(3) numeral_3_eq_3)
also have "… = 6 * card (triangle_set)"
by (simp add: eval_nat_numeral)
finally have "card ?TT ≤ 6 * card (triangle_set)" .
then show ?thesis
by (simp add: divide_simps)
qed
lemma card_convert_triangle_rep_bound:
fixes t :: real
assumes "card {(x, y, z) ∈ X × Y × Z . (triangle_in_graph x y z)} ≥ t"
assumes "X ⊆ V" and "Y ⊆ V" and "Z ⊆ V"
shows "card (triangle_set) ≥ 1/6 *t"
proof -
define t' where "t' ≡ card {(x, y, z) ∈ X × Y × Z . (triangle_in_graph x y z)}"
have "t' ≥ t" using assms t'_def by simp
then have tgt: "1/6 * t' ≥ 1/6 * t" by simp
have "card (triangle_set) ≥ 1/6 *t'" using t'_def card_convert_triangle_rep assms by simp
thus ?thesis using tgt by linarith
qed
end
end