Theory Neighbours

section ‹Background material: the neighbours of vertices›

text ‹Preliminaries for the Book Algorithm›

theory Neighbours imports General_Extras "Ramsey_Bounds.Ramsey_Bounds"

begin

abbreviation set_difference :: "['a set,'a set] ⇒ 'a set" (infixl "∖" 65)
  where "A ∖ B ≡ A-B"

subsection ‹Preliminaries on graphs›

context ulgraph
begin

text ‹The set of \emph{undirected} edges between two sets›
definition all_edges_betw_un :: "'a set ⇒ 'a set ⇒ 'a set set" where
  "all_edges_betw_un X Y ≡ {{x, y}| x y. x ∈ X ∧ y ∈ Y ∧ {x, y} ∈ E}"

lemma all_edges_betw_un_commute1: "all_edges_betw_un X Y ⊆ all_edges_betw_un Y X"
  by (smt (verit, del_insts) Collect_mono all_edges_betw_un_def insert_commute)

lemma all_edges_betw_un_commute: "all_edges_betw_un X Y = all_edges_betw_un Y X"
  by (simp add: all_edges_betw_un_commute1 subset_antisym)

lemma all_edges_betw_un_iff_mk_edge: "all_edges_betw_un X Y = mk_edge ` all_edges_between X Y"
  using all_edges_between_set all_edges_betw_un_def by presburger

lemma all_uedges_betw_subset: "all_edges_betw_un X Y ⊆ E"
  by (auto simp: all_edges_betw_un_def)

lemma all_uedges_betw_I: "x ∈ X ⟹ y ∈ Y ⟹ {x, y} ∈ E ⟹ {x, y} ∈ all_edges_betw_un X Y"
  by (auto simp: all_edges_betw_un_def)

lemma all_edges_betw_un_subset: "all_edges_betw_un X Y ⊆ Pow (X∪Y)"
  by (auto simp: all_edges_betw_un_def)

lemma all_edges_betw_un_empty [simp]:
  "all_edges_betw_un {} Z = {}" "all_edges_betw_un Z {} = {}"
  by (auto simp: all_edges_betw_un_def)

lemma card_all_uedges_betw_le: 
  assumes "finite X" "finite Y"
  shows "card (all_edges_betw_un X Y) ≤ card (all_edges_between X Y)"
  by (simp add: all_edges_betw_un_iff_mk_edge assms card_image_le finite_all_edges_between)

lemma all_edges_betw_un_le: 
  assumes "finite X" "finite Y"
  shows "card (all_edges_betw_un X Y) ≤ card X * card Y"
  by (meson assms card_all_uedges_betw_le max_all_edges_between order_trans)

lemma all_edges_betw_un_insert1:
  "all_edges_betw_un (insert v X) Y = ({{v, y}| y. y ∈ Y} ∩ E) ∪ all_edges_betw_un X Y"
  by (auto simp: all_edges_betw_un_def)

lemma all_edges_betw_un_insert2:
  "all_edges_betw_un X (insert v Y) = ({{x, v}| x. x ∈ X} ∩ E) ∪ all_edges_betw_un X Y"
  by (auto simp: all_edges_betw_un_def)

lemma all_edges_betw_un_Un1:
  "all_edges_betw_un (X ∪ Y) Z = all_edges_betw_un X Z ∪ all_edges_betw_un Y Z"
  by (auto simp: all_edges_betw_un_def)

lemma all_edges_betw_un_Un2:
  "all_edges_betw_un X (Y ∪ Z) = all_edges_betw_un X Y ∪ all_edges_betw_un X Z"
  by (auto simp: all_edges_betw_un_def)

lemma finite_all_edges_betw_un:
  assumes "finite X" "finite Y"
  shows "finite (all_edges_betw_un X Y)"
  by (simp add: all_edges_betw_un_iff_mk_edge assms finite_all_edges_between)

lemma all_edges_betw_un_Union1:
  "all_edges_betw_un (Union 𝒳) Y = (⋃X∈𝒳. all_edges_betw_un X Y)"
  by (auto simp: all_edges_betw_un_def)

lemma all_edges_betw_un_Union2:
  "all_edges_betw_un X (Union 𝒴) = (⋃Y∈𝒴. all_edges_betw_un X Y)"
  by (auto simp: all_edges_betw_un_def)

lemma all_edges_betw_un_mono1:
  "Y ⊆ Z ⟹ all_edges_betw_un Y X ⊆ all_edges_betw_un Z X"
  by (auto simp: all_edges_betw_un_def)

lemma all_edges_betw_un_mono2:
  "Y ⊆ Z ⟹ all_edges_betw_un X Y ⊆ all_edges_betw_un X Z"
  by (auto simp: all_edges_betw_un_def)

lemma disjnt_all_edges_betw_un:
  assumes "disjnt X Y" "disjnt X Z"
  shows "disjnt (all_edges_betw_un X Z) (all_edges_betw_un Y Z)"
  using assms by (auto simp: all_edges_betw_un_def disjnt_iff doubleton_eq_iff)

end

subsection ‹Neighbours of a vertex›

definition Neighbours :: "'a set set ⇒ 'a ⇒ 'a set" where
  "Neighbours ≡ λE x. {y. {x,y} ∈ E}"

lemma in_Neighbours_iff: "y ∈ Neighbours E x ⟷ {x,y} ∈ E"
  by (simp add: Neighbours_def)

lemma finite_Neighbours:
  assumes "finite E"
  shows "finite (Neighbours E x)"
proof -
  have "Neighbours E x ⊆ Neighbours {X∈E. finite X} x"
    by (auto simp: Neighbours_def)
  also have "… ⊆ (⋃{X∈E. finite X})"
    by (meson Union_iff in_Neighbours_iff insert_iff subset_iff)
  finally show ?thesis
    using assms finite_subset by fastforce
qed

lemma (in fin_sgraph) not_own_Neighbour: "E' ⊆ E ⟹ x ∉ Neighbours E' x"
  by (force simp: Neighbours_def singleton_not_edge)

context fin_sgraph
begin

declare singleton_not_edge [simp]

text ‹"A graph on vertex set @{term"S ∪ T"}  that contains all edges incident to @{term"S"}"
  (page 3). In fact, @{term S} is a clique and every vertex in @{term T} 
  has an edge into @{term S}.›
definition book :: "'a set ⇒ 'a set ⇒ 'a set set ⇒ bool" where
  "book ≡ λS T F. disjnt S T ∧ all_edges_betw_un S (S∪T) ⊆ F"

text ‹Cliques of a given number of vertices; the definition of clique from Ramsey is used›

definition size_clique :: "nat ⇒ 'a set ⇒ 'a set set ⇒ bool" where
  "size_clique p K F ≡ card K = p ∧ clique K F ∧ K ⊆ V"

lemma size_clique_smaller: "⟦size_clique p K F; p' < p⟧ ⟹ ∃K'. size_clique p' K' F"
  unfolding size_clique_def
  by (meson card_Ex_subset order.trans less_imp_le_nat smaller_clique)

subsection ‹Density: for calculating the parameter p›

definition "edge_card ≡ λC X Y. card (C ∩ all_edges_betw_un X Y)"

definition "gen_density ≡ λC X Y. edge_card C X Y / (card X * card Y)"

lemma edge_card_empty [simp]: "edge_card C {} X = 0" "edge_card C X {} = 0"
  by (auto simp: edge_card_def)

lemma edge_card_commute: "edge_card C X Y = edge_card C Y X"
  using all_edges_betw_un_commute edge_card_def by presburger

lemma edge_card_le: 
  assumes "finite X" "finite Y"
  shows "edge_card C X Y ≤ card X * card Y"
proof -
  have "edge_card C X Y ≤ card (all_edges_betw_un X Y)"
    by (simp add: assms card_mono edge_card_def finite_all_edges_betw_un)
  then show ?thesis
    by (meson all_edges_betw_un_le assms le_trans)
qed

text ‹the assumption that @{term Z} is disjoint from @{term X} (or @{term Y}) is necessary›
lemma edge_card_Un:
  assumes "disjnt X Y" "disjnt X Z" "finite X" "finite Y"
  shows "edge_card C (X ∪ Y) Z = edge_card C X Z + edge_card C Y Z"
proof -
  have [simp]: "finite (all_edges_betw_un U Z)" for U
    by (meson all_uedges_betw_subset fin_edges finite_subset)
  have "disjnt (C ∩ all_edges_betw_un X Z) (C ∩ all_edges_betw_un Y Z)"
    using assms by (meson Int_iff disjnt_all_edges_betw_un disjnt_iff)
  then show ?thesis
    by (simp add: edge_card_def card_Un_disjnt all_edges_betw_un_Un1 Int_Un_distrib)
qed

lemma edge_card_diff:
  assumes "Y⊆X" "disjnt X Z" "finite X" 
  shows "edge_card C (X-Y) Z = edge_card C X Z - edge_card C Y Z"
proof -
  have "(X∖Y) ∪ Y = X" "disjnt (X∖Y) Y"
    by (auto simp: Un_absorb2 assms disjnt_iff)
  then show ?thesis
    by (metis add_diff_cancel_right' assms disjnt_Un1 edge_card_Un finite_Diff finite_subset)
qed

lemma edge_card_mono:
  assumes "Y⊆X" shows "edge_card C Y Z ≤ edge_card C X Z"
  unfolding edge_card_def
proof (intro card_mono)
  show "finite (C ∩ all_edges_betw_un X Z)"
    by (meson all_uedges_betw_subset fin_edges finite_Int finite_subset)
  show "C ∩ all_edges_betw_un Y Z ⊆ C ∩ all_edges_betw_un X Z"
    by (meson Int_mono all_edges_betw_un_mono1 assms subset_refl)
qed

lemma edge_card_eq_sum_Neighbours:
  assumes "C⊆E" and B: "finite B" "disjnt A B"
  shows "edge_card C A B = (∑i∈B. card (Neighbours C i ∩ A))"
  using B
proof (induction B)
  case empty
  then show ?case
    by (auto simp: edge_card_def)
next
  case (insert b B)
  have "finite C"
    using assms(1) fin_edges finite_subset by blast
  have bij: "bij_betw (λe. the_elem(e-{b})) (C ∩ {{x, b} |x. x ∈ A}) (Neighbours C b ∩ A)"
    unfolding bij_betw_def
  proof
    have [simp]: "the_elem ({x, b} - {b}) = x" if "x ∈ A" for x
      using insert.prems by (simp add: disjnt_iff insert_Diff_if that)
    show "inj_on (λe. the_elem (e - {b})) (C ∩ {{x, b} |x. x ∈ A})"
      by (auto simp: inj_on_def)
    show "(λe. the_elem (e - {b})) ` (C ∩ {{x, b} |x. x ∈ A}) = Neighbours C b ∩ A"
      by (fastforce simp: Neighbours_def insert_commute image_iff Bex_def)
  qed
  have "(C ∩ all_edges_betw_un A (insert b B)) = (C ∩ ({{x, b} |x. x ∈ A} ∪ all_edges_betw_un A B))"
    using ‹C ⊆ E› by (auto simp: all_edges_betw_un_insert2)
  then have "edge_card C A (insert b B) = card ((C ∩ ({{x,b} |x. x ∈ A}) ∪ (C ∩ all_edges_betw_un A B)))"
    by (simp add: edge_card_def Int_Un_distrib)
  also have "… = card (C ∩ {{x,b} |x. x ∈ A}) + card (C ∩ all_edges_betw_un A B)"
  proof (rule card_Un_disjnt)
    show "disjnt (C ∩ {{x, b} |x. x ∈ A}) (C ∩ all_edges_betw_un A B)"
      using insert by (auto simp: disjnt_iff all_edges_betw_un_def doubleton_eq_iff)
  qed (use ‹finite C› in auto)
  also have "… = card (Neighbours C b ∩ A) + card (C ∩ all_edges_betw_un A B)"
    using bij_betw_same_card [OF bij] by simp
  also have "… = (∑i∈insert b B. card (Neighbours C i ∩ A))"
    using insert by (simp add: edge_card_def)
  finally show ?case .
qed

lemma sum_eq_card: "finite A ⟹ (∑x ∈ A. if x ∈ B then 1 else 0) = card (A∩B)"
  by (metis (no_types, lifting) card_eq_sum sum.cong sum.inter_restrict)

lemma sum_eq_card_Neighbours:
  assumes "x ∈ V" "C ⊆ E"
  shows "(∑y ∈ V∖{x}. if {x,y} ∈ C then 1 else 0) = card (Neighbours C x)"
proof -
  have "Neighbours C x = (V ∖ {x}) ∩ {y. {x, y} ∈ C}"
    using assms wellformed by (auto simp: Neighbours_def)
  with finV sum_eq_card [of _ "{y. {x,y}∈C}"] show ?thesis by simp
qed

lemma Neighbours_insert_NO_MATCH: "NO_MATCH {} C ⟹ Neighbours (insert e C) x = Neighbours {e} x ∪ Neighbours C x"
  by (auto simp: Neighbours_def)

lemma Neighbours_sing_2:
  assumes "e ∈ E"
  shows "(∑x∈V. card (Neighbours {e} x)) = 2"
proof -
  obtain u v where uv: "e = {u,v}" "u≠v"
    by (meson assms card_2_iff two_edges)
  then have "u ∈ V" "v ∈ V"
    using assms wellformed uv by blast+
  have *: "Neighbours {e} x = (if x=u then {v} else if x=v then {u} else {})" for x
    by (auto simp: Neighbours_def uv doubleton_eq_iff)
  show ?thesis
    using ‹u≠v›
    by (simp add: * if_distrib [of card] finV sum.delta_remove ‹u ∈ V› ‹v ∈ V› cong: if_cong)
qed

lemma sum_Neighbours_eq_card:
  assumes "finite C" "C⊆E" 
  shows "(∑i∈V. card (Neighbours C i)) = card C * 2"
  using assms
proof (induction C)
  case empty
  then show ?case
    by (auto simp: Neighbours_def)
next
  case (insert e C)
  then have [simp]: "Neighbours {e} x ∩ Neighbours C x = {}" for x
    by (auto simp: Neighbours_def)
  with insert show ?case
    by (auto simp: card_Un_disjoint finite_Neighbours Neighbours_insert_NO_MATCH sum.distrib Neighbours_sing_2)
qed

lemma gen_density_empty [simp]: "gen_density C {} X = 0" "gen_density C X {} = 0"
  by (auto simp: gen_density_def)

lemma gen_density_commute: "gen_density C X Y = gen_density C Y X"
  by (simp add: edge_card_commute gen_density_def)

lemma gen_density_ge0: "gen_density C X Y ≥ 0"
  by (auto simp: gen_density_def)

lemma gen_density_gt0: 
  assumes "finite X" "finite Y" "{x,y} ∈ C" "x ∈ X" "y ∈ Y" "C ⊆ E"
  shows "gen_density C X Y > 0"
proof -
  have xy: "{x,y} ∈ all_edges_betw_un X Y"
    using assms by (force simp: all_edges_betw_un_def)
  moreover have "finite (all_edges_betw_un X Y)"
    by (simp add: assms finite_all_edges_betw_un)
  ultimately have "edge_card C X Y > 0"
    by (metis IntI assms(3) card_0_eq edge_card_def emptyE finite_Int gr0I)
  with xy show ?thesis
    using assms gen_density_def less_eq_real_def by fastforce
qed

lemma gen_density_le1: "gen_density C X Y ≤ 1"
  unfolding gen_density_def
  by (smt (verit) card.infinite divide_le_eq_1 edge_card_le mult_eq_0_iff of_nat_le_0_iff of_nat_mono)

lemma gen_density_le_1_minus: 
  shows "gen_density C X Y ≤ 1 - gen_density (E-C) X Y"
proof (cases "finite X ∧ finite Y")
  case True
  have "C ∩ all_edges_betw_un X Y ∪ (E - C) ∩ all_edges_betw_un X Y = all_edges_betw_un X Y"
    by (auto simp: all_edges_betw_un_def)
  with True have "(edge_card C X Y) + (edge_card (E - C) X Y) ≤ card (all_edges_betw_un X Y)"
    unfolding edge_card_def
    by (metis Diff_Int_distrib2 Diff_disjoint card_Un_disjoint card_Un_le finite_Int finite_all_edges_betw_un)
  with True show ?thesis
    apply (simp add: gen_density_def divide_simps)
    by (smt (verit) all_edges_betw_un_le of_nat_add of_nat_mono of_nat_mult)
qed (auto simp: gen_density_def)

lemma gen_density_lt1: 
  assumes "{x,y} ∈ E-C" "x ∈ X" "y ∈ Y" "C ⊆ E"
  shows "gen_density C X Y < 1"
proof (cases "finite X ∧ finite Y")
  case True
  then have "0 < gen_density (E - C) X Y"
    using assms gen_density_gt0 by auto
  have "gen_density C X Y ≤ 1 - gen_density (E - C) X Y"
    by (intro gen_density_le_1_minus)
  then show ?thesis
    using ‹0 < gen_density (E - C) X Y› by linarith
qed (auto simp: gen_density_def)

lemma gen_density_le_iff:
  assumes "disjnt X Z" "finite X" "Y⊆X" "Y ≠ {}" "finite Z"
  shows "gen_density C X Z ≤ gen_density C Y Z ⟷ 
        edge_card C X Z / card X ≤ edge_card C Y Z / card Y"
  using assms by (simp add: gen_density_def divide_simps mult_less_0_iff zero_less_mult_iff)

text ‹"Removing vertices whose degree is less than the average can only increase the density 
from the remaining set" (page 17) ›
lemma gen_density_below_avg_ge:
  assumes "disjnt X Z" "finite X" "Y⊂X" "finite Z" 
    and genY: "gen_density C Y Z ≤ gen_density C X Z"
  shows "gen_density C (X-Y) Z ≥ gen_density C X Z"
proof -
  have "real (edge_card C Y Z) / card Y ≤ real (edge_card C X Z) / card X"
    using assms
    by (force simp: gen_density_def divide_simps zero_less_mult_iff split: if_split_asm)
  have "card Y < card X"
    by (simp add: assms psubset_card_mono)
  have *: "finite Y" "Y ⊆ X" "X≠{}"
    using assms finite_subset by blast+
  then
  have "card X * edge_card C Y Z ≤ card Y * edge_card C X Z"
    using genY assms
    by (simp add: gen_density_def field_split_simps card_eq_0_iff flip: of_nat_mult split: if_split_asm)
  with assms * ‹card Y < card X› show ?thesis
    by (simp add: gen_density_le_iff field_split_simps edge_card_diff card_Diff_subset 
        edge_card_mono flip: of_nat_mult)
qed

lemma edge_card_insert:
  assumes "NO_MATCH {} F" and "e ∉ F"
    shows  "edge_card (insert e F) X Y = edge_card {e} X Y + edge_card F X Y"
proof -
  have fin: "finite (all_edges_betw_un X Y)"
    by (meson all_uedges_betw_subset fin_edges finite_subset)
  have "insert e F ∩ all_edges_betw_un X Y 
      = {e} ∩ all_edges_betw_un X Y ∪ F ∩ all_edges_betw_un X Y"
    by auto
  with ‹e∉F› show ?thesis
    by (auto simp: edge_card_def card_Un_disjoint disjoint_iff fin)
qed

lemma edge_card_sing:
  assumes "e ∈ E"
  shows "edge_card {e} U U = (if e ⊆ U then 1 else 0)"
proof (cases "e ⊆ U")
  case True
  obtain x y where xy: "e = {x,y}" "x≠y"
    using assms by (metis card_2_iff two_edges)
  with True assms have "{e} ∩ all_edges_betw_un U U = {e}"
    by (auto simp: all_edges_betw_un_def)
  with True show ?thesis
    by (simp add: edge_card_def)
qed (auto simp: edge_card_def all_edges_betw_un_def)

lemma sum_edge_card_choose: 
  assumes "2≤k" "C ⊆ E"
  shows "(∑U∈[V]⇗k⇖. edge_card C U U) = (card V - 2 choose (k-2)) * card C"
proof -
  have *: "card {A ∈ [V]⇗k⇖. e ⊆ A} = card V - 2 choose (k-2)" if e: "e ∈ C" for e
  proof -
    have "e ⊆ V"
      using ‹C⊆E› e wellformed by force
    obtain x y where xy: "e = {x,y}" "x≠y"
      using ‹C⊆E› e by (metis in_mono card_2_iff two_edges)
    define 𝒜 where "𝒜 ≡ {A ∈ [V]⇗k⇖. e ⊆ A}"
    have "⋀A. A ∈ 𝒜 ⟹ A = e ∪ (A∖e) ∧ A∖e ∈ [V∖e]⇗(k - 2)⇖"
      by (auto simp: 𝒜_def nsets_def xy)
    moreover have "⋀xa. ⟦xa ∈ [V ∖ e]⇗(k - 2)⇖⟧ ⟹ e ∪ xa ∈ 𝒜"
      using ‹e ⊆ V› assms
      by (auto simp: 𝒜_def nsets_def xy card_insert_if)
    ultimately have "𝒜 = (∪)e ` [V∖e]⇗(k-2)⇖"
      by auto
    moreover have "inj_on ((∪) e) ([V∖e]⇗(k - 2)⇖)"
      by (auto simp: inj_on_def nsets_def)
    moreover have "card (V∖e) = card V - 2"
      by (metis ‹C⊆E› ‹e ∈ C› subsetD card_Diff_subset finV finite_subset two_edges wellformed)
    ultimately show ?thesis
      using assms by (simp add: card_image 𝒜_def)
  qed
  have "(∑U∈[V]⇗k⇖. edge_card R U U) = ((card V - 2) choose (k-2)) * card R"
    if "finite R" "R ⊆ C" for R
    using that
  proof (induction R)
    case empty
    then show ?case
      by (simp add: edge_card_def)
  next
    case (insert e R)
    with assms have "e∈E" by blast
    with insert show ?case
      by (simp add: edge_card_insert * sum.distrib edge_card_sing Ramsey.finite_imp_finite_nsets 
           finV flip: sum.inter_filter)
  qed
  then show ?thesis
    by (meson ‹C⊆E› fin_edges finite_subset set_eq_subset)
qed

lemma sum_nsets_Compl:
  assumes "finite A" "k ≤ card A"
  shows "(∑U∈[A]⇗k⇖. f (A∖U)) = (∑U∈[A]⇗(card A - k)⇖. f U)"
proof -
  have "B ∈ (∖) A ` [A]⇗k⇖" if "B ∈ [A]⇗(card A - k)⇖" for B
  proof -
    have "card (A∖B) = k"
      using assms that by (simp add: nsets_def card_Diff_subset)
    moreover have "B = A∖(A∖B)"
      using that by (auto simp: nsets_def)
    ultimately show ?thesis
      using assms unfolding nsets_def image_iff by blast
  qed
  then have "bij_betw (λU. A∖U) ([A]⇗k⇖) ([A]⇗(card A - k)⇖)"
    using assms by (auto simp: nsets_def bij_betw_def inj_on_def card_Diff_subset)
  then show ?thesis
    using sum.reindex_bij_betw by blast
qed

subsection ‹Lemma 9.2 preliminaries›

text ‹Equation (45) in the text, page 30, is seemingly a huge gap.
   The development below relies on binomial coefficient identities.›

definition "graph_density ≡ λC. card C / card E"

lemma graph_density_Un:
  assumes "disjnt C D" "C ⊆ E" "D ⊆ E" 
  shows "graph_density (C ∪ D) = graph_density C + graph_density D"
proof (cases "card E > 0")
  case True
  with assms obtain "finite C" "finite D"
    by (metis card_ge_0_finite finite_subset)
  with assms show ?thesis
    by (auto simp: graph_density_def card_Un_disjnt divide_simps)
qed (auto simp: graph_density_def)

text ‹Could be generalised to any complete graph›
lemma density_eq_average:
  assumes "C ⊆ E" and complete: "E = all_edges V"
  shows "graph_density C =
    real (∑x ∈ V. ∑y ∈ V∖{x}. if {x,y} ∈ C then 1 else 0) / (card V * (card V - 1))"
proof -
  have cardE: "card E = card V choose 2"
    using card_all_edges complete finV by blast
  have "finite C"
    using assms fin_edges finite_subset by blast
  then have *: "(∑x∈V. ∑y∈V∖{x}. if {x, y} ∈ C then 1 else 0) = card C * 2"
    using assms by (simp add: sum_eq_card_Neighbours sum_Neighbours_eq_card)
  show ?thesis
    by (auto simp: graph_density_def divide_simps cardE choose_two_real *)
qed

lemma edge_card_V_V: 
  assumes "C ⊆ E" and complete: "E = all_edges V"
  shows "edge_card C V V = card C"
proof -
  have "C ⊆ all_edges_betw_un V V"
    using assms clique_iff complete subset_refl
    by (metis all_uedges_betw_I all_uedges_betw_subset clique_def)
  then show ?thesis
    by (metis Int_absorb2 edge_card_def)
qed

text ‹Bhavik's statement; own proof›
proposition density_eq_average_partition:
  assumes k: "0 < k" "k < card V" and "C ⊆ E" and complete: "E = all_edges V"
  shows "graph_density C = (∑U∈[V]⇗k⇖. gen_density C U (V∖U)) / (card V choose k)"
proof (cases "k=1 ∨ gorder = Suc k")
  case True
  then have [simp]: "gorder choose k = gorder" by auto
  have eq: "(C ∩ {{x, y} |y. y ∈ V ∧ y ≠ x ∧ {x, y} ∈ E}) 
           = (λy. {x,y}) ` {y. {x,y} ∈ C}" for x
    using ‹C⊆E› wellformed by fastforce
  have "V ≠ {}"
    using assms by force
  then have nontriv: "E ≠ {}"
    using assms card_all_edges finV by force
  have "(∑U∈[V]⇗k⇖. gen_density C U (V ∖ U)) = (∑x∈V. gen_density C {x} (V ∖ {x}))"
    using True
  proof
    assume "k = 1"
    then show ?thesis
      by (simp add: sum_nsets_one)
  next
    assume §: "gorder = Suc k"
    then have  "V-A ≠ {}" if "card A = k" "finite A" for A
      using that
      by (metis assms(2) card.empty card_less_sym_Diff finV less_nat_zero_code)
    then have bij: "bij_betw (λx. V ∖ {x}) V ([V]⇗k⇖)"
      using finV § 
      by (auto simp: inj_on_def bij_betw_def nsets_def image_iff)
        (metis Diff_insert_absorb card.insert card_subset_eq insert_subset subsetI)
    moreover have "V∖(V∖{x}) = {x}" if "x∈V" for x
      using that by auto
    ultimately show ?thesis
      using sum.reindex_bij_betw [OF bij] gen_density_commute 
      by (metis (no_types, lifting) sum.cong) 
  qed
  also have "… = (∑x∈V. real (edge_card C {x} (V ∖ {x}))) / (gorder - 1)"
    by (simp add: ‹C⊆E› gen_density_def flip: sum_divide_distrib)
  also have "… = (∑i∈V. card (Neighbours C i)) / (gorder - 1)"
    unfolding edge_card_def Neighbours_def all_edges_betw_un_def
    by (simp add: eq card_image inj_on_def doubleton_eq_iff)
  also have "… = graph_density C * gorder"
    using assms density_eq_average [OF ‹C⊆E› complete]
    by (simp add: sum_eq_card_Neighbours)
  finally show ?thesis
    using k by simp
next
  case False
  then have K: "gorder > Suc k" "k≥2" 
    using assms by auto
  then have "gorder - Suc (Suc (gorder - Suc (Suc k))) = k"
    using assms by auto
  then have [simp]: "gorder - 2 choose (gorder - Suc (Suc k)) = (gorder - 2 choose k)"
    using binomial_symmetric [of "(gorder - Suc (Suc k))"]
    by simp
  have cardE: "card E = card V choose 2"
    using card_all_edges complete finV by blast
  have "card E > 0"
    using k cardE by auto
  have in_E_iff [iff]: "{v,w} ∈ E ⟷ v∈V ∧ w∈V ∧ v≠w" for v w
    by (auto simp: complete all_edges_alt doubleton_eq_iff)

  have B: "edge_card C V V = edge_card C U U + edge_card C U (V∖U) + edge_card C (V∖U) (V∖U)"
    (is "?L = ?R")
    if "U ⊆ V" for U
  proof -
    have fin: "finite (all_edges_betw_un U U')" for U'
      by (meson all_uedges_betw_subset fin_edges finite_subset)
    have dis: "all_edges_betw_un U U ∩ all_edges_betw_un U (V ∖ U) = {}"
      by (auto simp: all_edges_betw_un_def doubleton_eq_iff)
    have "all_edges_betw_un V V = all_edges_betw_un U U ∪ all_edges_betw_un U (V∖U) ∪ all_edges_betw_un (V∖U) (V∖U)"
      by (smt (verit) that Diff_partition Un_absorb Un_assoc all_edges_betw_un_Un2 all_edges_betw_un_commute)
    with that have "?L = card (C ∩ all_edges_betw_un U U ∪ C ∩ all_edges_betw_un U (V ∖ U)
                             ∪ C ∩ all_edges_betw_un (V ∖ U) (V ∖ U))"
      by (simp add: edge_card_def Int_Un_distrib)
    also have "… = ?R"
      using fin dis ‹C⊆E› fin_edges finite_subset
      by ((subst card_Un_disjoint)?, fastforce simp: edge_card_def all_edges_betw_un_def doubleton_eq_iff)+
    finally show ?thesis .
  qed
  have C: "(∑U∈[V]⇗k⇖. real (edge_card C U (V∖U)))
      = (card V choose k) * card C - real(∑U∈[V]⇗k⇖. edge_card C U U + edge_card C (V∖U) (V∖U))"
    (is "?L = ?R")
  proof -
    have "?L = (∑U∈[V]⇗k⇖. edge_card C V V - real (edge_card C U U + edge_card C (V∖U) (V∖U)))"
      unfolding nsets_def by (rule sum.cong) (auto simp: B)
    also have "… = ?R"
      using ‹C⊆E› complete edge_card_V_V 
      by (simp add: ‹C⊆E› sum_subtractf edge_card_V_V)
    finally show ?thesis .
  qed

  have "(gorder-2 choose k) + (gorder-2 choose (k-2)) + 2 * (gorder-2 choose (k-1)) = (gorder choose k)"
    using assms K by (auto simp: choose_reduce_nat [of "gorder"] choose_reduce_nat [of "gorder-Suc 0"] eval_nat_numeral)
  moreover
  have "(gorder - 1) * (gorder-2 choose (k-1)) = (gorder-k) * (gorder-1 choose (k-1))"
    by (metis Suc_1 Suc_diff_1 binomial_absorb_comp diff_Suc_eq_diff_pred ‹k>0›)
  ultimately have F: "(gorder - 1) * (gorder-2 choose k) + (gorder - 1) * (gorder-2 choose (k-2)) + 2 * (gorder-k) * (gorder-1 choose (k-1)) 
      = (gorder - 1) * (gorder choose k)"
    by (smt (verit) add_mult_distrib2 mult.assoc mult.left_commute)

  have "(∑U∈[V]⇗k⇖. edge_card C U (V∖U) / (real (card U) * card (V∖U)))
     = (∑U∈[V]⇗k⇖. edge_card C U (V∖U) / (real k * (card V - k)))"
    using card_Diff_subset by (intro sum.cong) (auto simp: nsets_def)
  also have "… = (∑U∈[V]⇗k⇖. edge_card C U (V∖U)) / (k * (card V - k))"
    by (simp add: sum_divide_distrib)
  finally have *: "(∑U∈[V]⇗k⇖. edge_card C U (V∖U) / (real (card U) * card (V∖U)))
              = (∑U∈[V]⇗k⇖. edge_card C U (V∖U)) / (k * (card V - k))" .

  have choose_m1: "gorder * (gorder - 1 choose (k - 1)) = k * (gorder choose k)"
    using ‹k>0› times_binomial_minus1_eq by presburger 
  have **: "(real k * (real gorder - real k) * real (gorder choose k)) =
        (real (gorder choose k) - (real (gorder - 2 choose (k - 2)) + real (gorder - 2 choose k))) *
        real (gorder choose 2)"
    using assms K arg_cong [OF F, of "λu. real gorder * real u"] arg_cong [OF choose_m1, of real]
    apply (simp add: choose_two_real ring_distribs)
    by (smt (verit) distrib_right mult.assoc mult_2_right mult_of_nat_commute)
  have eq: "(∑U∈[V]⇗k⇖. real (edge_card C (V∖U) (V∖U))) 
          = (∑U∈[V]⇗(gorder-k)⇖. real (edge_card C U U))"
    using K finV by (subst sum_nsets_Compl, simp_all)
  show ?thesis
    unfolding graph_density_def gen_density_def
    using K ‹card E > 0› ‹C⊆E›
    apply (simp add: eq divide_simps B C sum.distrib *)
    apply (simp add: ** sum_edge_card_choose cardE flip: of_nat_sum)
    by argo
qed

lemma exists_density_edge_density:
  assumes k: "0 < k" "k < card V" and "C ⊆ E" and complete: "E = all_edges V"
  obtains U where "card U = k" "U⊆V" "graph_density C ≤ gen_density C U (V∖U)"
proof -
  have False if "⋀U. U ∈ [V]⇗k⇖ ⟹ graph_density C > gen_density C U (V∖U)"
  proof -
    have "card([V]⇗k⇖) > 0"
      using assms by auto
    then have "(∑U∈[V]⇗k⇖. gen_density C U (V ∖ U)) < card([V]⇗k⇖) * graph_density C"
      by (meson sum_bounded_above_strict that)
    with density_eq_average_partition assms show False by force
  qed
  with that show thesis
    unfolding nsets_def by fastforce
qed

end  (*fin_sgraph*)

end