Theory Graph_Triangles

(* Theory: Graph_Triangles.thy 
   Author: Chelsea Edmonds *)

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 "xy" "yz" "xz" 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