Theory Neighbours

section ‹Background material: the neighbours of vertices›

text ‹Preliminaries for the Book Algorithm›

theory Neighbours imports "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 (XY)"
  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 {XE. finite X} x"
    by (auto simp: Neighbours_def)
  also have "  ({XE. 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 (ST)  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 "YX" "disjnt X Z" "finite X" 
  shows "edge_card C (X-Y) Z = edge_card C X Z - edge_card C Y Z"
proof -
  have "(XY)  Y = X" "disjnt (XY) 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 "YX" 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 "CE" and B: "finite B" "disjnt A B"
  shows "edge_card C A B = (iB. 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 " = (iinsert 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 (AB)"
  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 "(xV. card (Neighbours {e} x)) = 2"
proof -
  obtain u v where uv: "e = {u,v}" "uv"
    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 uv
    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" "CE" 
  shows "(iV. 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" "YX" "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" "YX" "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 eF 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}" "xy"
    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 "2k" "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 CE e wellformed by force
    obtain x y where xy: "e = {x,y}" "xy"
      using CE e by (metis in_mono card_2_iff two_edges)
    define 𝒜 where "𝒜  {A  [V]⇗k. e  A}"
    have "A. A  𝒜  A = e  (Ae)  Ae  [Ve]⇗(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 ` [Ve]⇗(k-2)⇖"
      by auto
    moreover have "inj_on ((∪) e) ([Ve]⇗(k - 2))"
      by (auto simp: inj_on_def nsets_def)
    moreover have "card (Ve) = card V - 2"
      by (metis CE 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 "eE" 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 CE fin_edges finite_subset set_eq_subset)
qed

lemma sum_nsets_Compl:
  assumes "finite A" "k  card A"
  shows "(U[A]⇗k. f (AU)) = (U[A]⇗(card A - k). f U)"
proof -
  have "B  (∖) A ` [A]⇗k⇖" if "B  [A]⇗(card A - k)⇖" for B
  proof -
    have "card (AB) = k"
      using assms that by (simp add: nsets_def card_Diff_subset)
    moreover have "B = A(AB)"
      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. AU) ([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 *: "(xV. yV{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 (VU)) / (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 CE 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)) = (xV. 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 "xV" 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 " = (xV. real (edge_card C {x} (V  {x}))) / (gorder - 1)"
    by (simp add: CE gen_density_def flip: sum_divide_distrib)
  also have " = (iV. 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 CE complete]
    by (simp add: sum_eq_card_Neighbours)
  finally show ?thesis
    using k by simp
next
  case False
  then have K: "gorder > Suc k" "k2" 
    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  vV  wV  vw" 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 (VU) + edge_card C (VU) (VU)"
    (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 (VU)  all_edges_betw_un (VU) (VU)"
      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 CE 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 (VU)))
      = (card V choose k) * card C - real(U[V]⇗k. edge_card C U U + edge_card C (VU) (VU))"
    (is "?L = ?R")
  proof -
    have "?L = (U[V]⇗k. edge_card C V V - real (edge_card C U U + edge_card C (VU) (VU)))"
      unfolding nsets_def by (rule sum.cong) (auto simp: B)
    also have " = ?R"
      using CE complete edge_card_V_V 
      by (simp add: CE 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 (VU) / (real (card U) * card (VU)))
     = (U[V]⇗k. edge_card C U (VU) / (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 (VU)) / (k * (card V - k))"
    by (simp add: sum_divide_distrib)
  finally have *: "(U[V]⇗k. edge_card C U (VU) / (real (card U) * card (VU)))
              = (U[V]⇗k. edge_card C U (VU)) / (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 (VU) (VU))) 
          = (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 CE
    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" "UV" "graph_density C  gen_density C U (VU)"
proof -
  have False if "U. U  [V]⇗k graph_density C > gen_density C U (VU)"
  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