Theory Foldes_Hammer

theory Foldes_Hammer
  imports "Undirected_Graph_Theory.Undirected_Graphs_Root"
begin

context fin_sgraph
begin

definition is_clique :: "'a set ⇒ bool" where
  "is_clique C ⟷ C ⊆ V ∧ induced_edges C = all_edges C"

definition cliques :: "'a set set" where
  "cliques = {C. is_clique C}"

definition maximum_clique :: "'a set ⇒ bool" where
  "maximum_clique K ⟷ K ∈ cliques ∧ (∀C∈cliques. card C ≤ card K)"

definition outside_edge_count :: "'a set ⇒ nat" where
  "outside_edge_count K = card (induced_edges (V - K))"

definition is_split_partition :: "'a set ⇒ 'a set ⇒ bool" where
  "is_split_partition C I ⟷ C ∩ I = {} ∧ C ∪ I = V ∧ is_clique C ∧ is_independent_set I"

definition is_split_graph :: bool where
  "is_split_graph ⟷ (∃C I. is_split_partition C I)"

definition induces_2K2 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool" where
  "induces_2K2 a b c d ⟷
     distinct [a, b, c, d] ∧
     vert_adj a b ∧ vert_adj c d ∧
     ¬ vert_adj a c ∧ ¬ vert_adj a d ∧ ¬ vert_adj b c ∧ ¬ vert_adj b d"

definition induces_C4 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool" where
  "induces_C4 a b c d ⟷
     distinct [a, b, c, d] ∧
     vert_adj a b ∧ vert_adj b c ∧ vert_adj c d ∧ vert_adj d a ∧
     ¬ vert_adj a c ∧ ¬ vert_adj b d"

definition induces_C5 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool" where
  "induces_C5 a b c d e ⟷
     distinct [a, b, c, d, e] ∧
     vert_adj a b ∧ vert_adj b c ∧ vert_adj c d ∧ vert_adj d e ∧ vert_adj e a ∧
     ¬ vert_adj a c ∧ ¬ vert_adj a d ∧ ¬ vert_adj b d ∧ ¬ vert_adj b e ∧ ¬ vert_adj c e"

definition has_induced_2K2 :: bool where
  "has_induced_2K2 ⟷ (∃a b c d. induces_2K2 a b c d)"

definition has_induced_C4 :: bool where
  "has_induced_C4 ⟷ (∃a b c d. induces_C4 a b c d)"

definition has_induced_C5 :: bool where
  "has_induced_C5 ⟷ (∃a b c d e. induces_C5 a b c d e)"

definition foldes_hammer_free :: bool where
  "foldes_hammer_free ⟷ ¬ has_induced_2K2 ∧ ¬ has_induced_C4 ∧ ¬ has_induced_C5"

lemma is_clique_alt:
  "is_clique C ⟷ C ⊆ V ∧ (∀u∈C. ∀v∈C. u ≠ v ⟶ vert_adj u v)"
proof
  assume H: "is_clique C"
  then have "C ⊆ V" by (simp add: is_clique_def)
  moreover have "∀u∈C. ∀v∈C. u ≠ v ⟶ vert_adj u v"
  proof (intro ballI impI)
    fix u v
    assume uC: "u ∈ C" and vC: "v ∈ C" and uv: "u ≠ v"
    from H have eq: "induced_edges C = all_edges C"
      by (simp add: is_clique_def)
    have "{u, v} ∈ all_edges C"
      using uC vC uv by (auto simp: all_edges_alt)
    with eq have "{u, v} ∈ induced_edges C" by simp
    then show "vert_adj u v"
      by (auto simp: induced_edges_def vert_adj_def)
  qed
  ultimately show "C ⊆ V ∧ (∀u∈C. ∀v∈C. u ≠ v ⟶ vert_adj u v)"
    by simp
next
  assume H: "C ⊆ V ∧ (∀u∈C. ∀v∈C. u ≠ v ⟶ vert_adj u v)"
  then have Csub: "C ⊆ V"
    and adj: "∀u∈C. ∀v∈C. u ≠ v ⟶ vert_adj u v"
    by auto
  have "induced_edges C = all_edges C"
  proof (rule subset_antisym)
    show "induced_edges C ⊆ all_edges C"
      using induced_edges_alt by auto
  next
    show "all_edges C ⊆ induced_edges C"
    proof
      fix e
      assume eC: "e ∈ all_edges C"
      then obtain u v where e: "e = {u, v}" and uC: "u ∈ C" and vC: "v ∈ C" and uv: "u ≠ v"
        by (auto simp: all_edges_alt)
      from adj uC vC uv have "vert_adj u v" by blast
      then have "e ∈ E"
        by (simp add: e vert_adj_def)
      moreover from eC have "e ⊆ C"
        by (auto simp: all_edges_def)
      ultimately show "e ∈ induced_edges C"
        by (simp add: induced_edges_def)
    qed
  qed
  with Csub show "is_clique C"
    by (simp add: is_clique_def)
qed

lemma clique_pair_adj:
  assumes "is_clique C" "u ∈ C" "v ∈ C" "u ≠ v"
  shows "vert_adj u v"
  using assms by (auto simp: is_clique_alt)

lemma clique_mono:
  assumes "is_clique C" "D ⊆ C"
  shows "is_clique D"
  using assms by (auto simp: is_clique_alt)

lemma vert_adj_neq:
  assumes "vert_adj u v"
  shows "u ≠ v"
proof
  assume uv_eq: "u = v"
  from assms have card2: "card {u, v} = 2"
    unfolding vert_adj_def using two_edges by blast
  from uv_eq have "card {u, v} = 1"
    by simp
  with card2 show False
    by simp
qed

lemma empty_clique: "is_clique {}"
  by (simp add: is_clique_alt)

lemma singleton_clique:
  assumes "v ∈ V"
  shows "is_clique {v}"
  using assms by (auto simp: is_clique_alt)

lemma finite_cliques: "finite cliques"
proof -
  have "cliques ⊆ Pow V"
    by (auto simp: cliques_def is_clique_def)
  moreover have "finite (Pow V)"
    using finV by simp
  ultimately show ?thesis
    by (rule finite_subset)
qed

lemma cliques_nonempty: "{} ∈ cliques"
  by (simp add: cliques_def empty_clique)

lemma maximum_clique_exists:
  obtains K where "maximum_clique K"
proof -
  have fin: "finite (card ` cliques)"
    using finite_cliques by simp
  have ne: "card ` cliques ≠ {}"
    using cliques_nonempty by auto
  let ?m = "Max (card ` cliques)"
  have m_in: "?m ∈ card ` cliques"
    using Max_in[OF fin ne] .
  then obtain K where K_in: "K ∈ cliques" and K_card: "card K = ?m"
    by auto
  have maxK: "∀C∈cliques. card C ≤ card K"
  proof
    fix C
    assume C_in: "C ∈ cliques"
    then have "card C ∈ card ` cliques"
      by auto
    then have "card C ≤ ?m"
      using Max_ge[OF fin] by blast
    then show "card C ≤ card K"
      by (simp add: K_card)
  qed
  have "maximum_clique K"
    using K_in maxK by (simp add: maximum_clique_def)
  then show ?thesis
    using that by blast
qed

lemma maximum_clique_finite:
  assumes "maximum_clique K"
  shows "finite K"
  using assms finV finite_subset
  by (auto simp: maximum_clique_def cliques_def is_clique_def)

lemma finite_induced_edges_subset_V:
  assumes "S ⊆ V"
  shows "finite (induced_edges S)"
proof -
  have finS: "finite S"
    using assms finV finite_subset by blast
  have "induced_edges S ⊆ Pow S"
    by (auto simp: induced_edges_def)
  moreover have "finite (Pow S)"
    using finS by simp
  ultimately show ?thesis
    by (rule finite_subset)
qed

lemma obtain_best_clique:
  obtains K where "maximum_clique K"
    and "∀L. maximum_clique L ⟶ outside_edge_count K ≤ outside_edge_count L"
proof -
  let ?M = "{K. maximum_clique K}"
  have finM: "finite ?M"
  proof (rule finite_subset[of ?M cliques])
    show "?M ⊆ cliques"
      by (auto simp: maximum_clique_def)
    show "finite cliques"
      using finite_cliques .
  qed
  have neM: "?M ≠ {}"
    using maximum_clique_exists by blast
  have finImg: "finite (outside_edge_count ` ?M)"
    using finM by simp
  have neImg: "outside_edge_count ` ?M ≠ {}"
    using neM by auto
  let ?m = "Min (outside_edge_count ` ?M)"
  have mIn: "?m ∈ outside_edge_count ` ?M"
    using Min_in[OF finImg neImg] .
  then obtain K where Kmax: "maximum_clique K" and Kmin: "outside_edge_count K = ?m"
    by auto
  have Kbest: "∀L. maximum_clique L ⟶ outside_edge_count K ≤ outside_edge_count L"
    using Kmin finImg neImg
    by (simp add: Min_le)
  show ?thesis
    using that Kmax Kbest by blast
qed

lemma insert_clique_if_all_adj:
  assumes C: "is_clique C"
    and vV: "v ∈ V"
    and vnot: "v ∉ C"
    and adj: "∀u∈C. vert_adj u v"
  shows "is_clique (insert v C)"
proof -
  from C have Csub: "C ⊆ V"
    and Cadj: "∀u∈C. ∀w∈C. u ≠ w ⟶ vert_adj u w"
    by (auto simp: is_clique_alt)
  have "insert v C ⊆ V"
    using Csub vV by auto
  moreover have "∀u∈insert v C. ∀w∈insert v C. u ≠ w ⟶ vert_adj u w"
  proof (intro ballI impI)
    fix u w
    assume uin: "u ∈ insert v C" and win: "w ∈ insert v C" and uw: "u ≠ w"
    show "vert_adj u w"
    proof (cases "u = v")
      case u_eq_v: True
      with win vnot uw have "w ∈ C" by auto
      then have "vert_adj w v"
        using adj by simp
      then show ?thesis
        using u_eq_v by (simp add: vert_adj_sym)
    next
      case u_ne_v: False
      show ?thesis
      proof (cases "w = v")
        case w_eq_v: True
        with uin vnot uw u_ne_v have "u ∈ C" by auto
        then have "vert_adj u v"
          using adj by simp
        then show ?thesis
          using w_eq_v by simp
      next
        case w_ne_v: False
        from uin win u_ne_v w_ne_v have "u ∈ C" "w ∈ C" by auto
        with Cadj uw show ?thesis by blast
      qed
    qed
  qed
  ultimately show ?thesis
    by (simp add: is_clique_alt)
qed

lemma maximum_clique_outside_has_nonneighbor:
  assumes maxK: "maximum_clique K"
    and vV: "v ∈ V"
    and vnot: "v ∉ K"
  shows "∃u∈K. ¬ vert_adj u v"
proof (rule ccontr)
  assume neg: "¬ (∃u∈K. ¬ vert_adj u v)"
  then have all_adj: "∀u∈K. vert_adj u v"
    by auto
  from maxK have K_clique: "is_clique K"
    by (auto simp: maximum_clique_def cliques_def)
  have ins_clique: "is_clique (insert v K)"
    using insert_clique_if_all_adj[OF K_clique vV vnot all_adj] .
  then have ins_in: "insert v K ∈ cliques"
    by (simp add: cliques_def)
  from maxK have bound: "∀C∈cliques. card C ≤ card K"
    by (auto simp: maximum_clique_def)
  from maxK have Ksub: "K ⊆ V"
    by (auto simp: maximum_clique_def cliques_def is_clique_def)
  then have finK: "finite K"
    using finV finite_subset by blast
  from ins_in bound have "card (insert v K) ≤ card K"
    by blast
  with finK vnot show False
    by simp
qed

lemma split_graph_alt:
  "is_split_graph ⟷ (∃C. is_clique C ∧ is_independent_set (V - C))"
proof
  assume H: "is_split_graph"
  then obtain C I where sp: "is_split_partition C I"
    by (auto simp: is_split_graph_def)
  then have "I = V - C"
    by (auto simp: is_split_partition_def is_clique_def)
  with sp show "∃C. is_clique C ∧ is_independent_set (V - C)"
    by (auto simp: is_split_partition_def)
next
  assume H: "∃C. is_clique C ∧ is_independent_set (V - C)"
  then obtain C where C: "is_clique C" "is_independent_set (V - C)"
    by blast
  have "is_split_partition C (V - C)"
    using C by (auto simp: is_split_partition_def is_clique_def)
  then show "is_split_graph"
    by (auto simp: is_split_graph_def)
qed

lemma independent_pair_not_adj:
  assumes "is_independent_set I" "u ∈ I" "v ∈ I"
  shows "¬ vert_adj u v"
  using assms by (auto simp: is_independent_alt)

lemma split_partition_edge_hits_clique:
  assumes sp: "is_split_partition C I"
    and uv: "vert_adj u v"
  shows "u ∈ C ∨ v ∈ C"
proof (rule ccontr)
  assume notC: "¬ (u ∈ C ∨ v ∈ C)"
  from uv have uV: "u ∈ V" and vV: "v ∈ V"
    using vert_adj_imp_inV by auto
  from sp uV vV notC have uI: "u ∈ I" and vI: "v ∈ I"
    by (auto simp: is_split_partition_def)
  from sp have indep: "is_independent_set I"
    by (simp add: is_split_partition_def)
  from independent_pair_not_adj[OF indep uI vI] uv show False
    by contradiction
qed

lemma split_partition_nonedge_not_both_clique:
  assumes sp: "is_split_partition C I"
    and uV: "u ∈ V"
    and vV: "v ∈ V"
    and uv: "u ≠ v"
    and not_adj: "¬ vert_adj u v"
  shows "¬ (u ∈ C ∧ v ∈ C)"
proof
  assume uvC: "u ∈ C ∧ v ∈ C"
  then have uC: "u ∈ C" and vC: "v ∈ C"
    by auto
  from sp have clique: "is_clique C"
    by (simp add: is_split_partition_def)
  from clique_pair_adj[OF clique uC vC uv] not_adj show False
    by contradiction
qed

lemma induces_2K2_inV:
  assumes "induces_2K2 a b c d"
  shows "a ∈ V" "b ∈ V" "c ∈ V" "d ∈ V"
  using assms vert_adj_imp_inV by (auto simp: induces_2K2_def)

lemma induces_C4_inV:
  assumes "induces_C4 a b c d"
  shows "a ∈ V" "b ∈ V" "c ∈ V" "d ∈ V"
  using assms vert_adj_imp_inV by (auto simp: induces_C4_def)

lemma induces_C5_inV:
  assumes "induces_C5 a b c d e"
  shows "a ∈ V" "b ∈ V" "c ∈ V" "d ∈ V" "e ∈ V"
  using assms vert_adj_imp_inV by (auto simp: induces_C5_def)

lemma split_partition_forbids_2K2:
  assumes sp: "is_split_partition C I"
    and H: "induces_2K2 a b c d"
  shows False
proof -
  from H have ab: "vert_adj a b" and cd: "vert_adj c d"
    and aV: "a ∈ V" and bV: "b ∈ V" and cV: "c ∈ V" and dV: "d ∈ V"
    and ac: "a ≠ c" and ad: "a ≠ d" and bc: "b ≠ c" and bd: "b ≠ d"
    and nac: "¬ vert_adj a c" and nad: "¬ vert_adj a d" and nbc: "¬ vert_adj b c" and nbd: "¬ vert_adj b d"
    using induces_2K2_inV[OF H] by (auto simp: induces_2K2_def)
  have "a ∈ C ∨ b ∈ C"
    using split_partition_edge_hits_clique[OF sp ab] .
  moreover have "c ∈ C ∨ d ∈ C"
    using split_partition_edge_hits_clique[OF sp cd] .
  moreover have "¬ (a ∈ C ∧ c ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp aV cV ac nac] .
  moreover have "¬ (a ∈ C ∧ d ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp aV dV ad nad] .
  moreover have "¬ (b ∈ C ∧ c ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp bV cV bc nbc] .
  moreover have "¬ (b ∈ C ∧ d ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp bV dV bd nbd] .
  ultimately show False
    by blast
qed

lemma split_partition_forbids_C4:
  assumes sp: "is_split_partition C I"
    and H: "induces_C4 a b c d"
  shows False
proof -
  from H have ab: "vert_adj a b" and bc: "vert_adj b c" and cd: "vert_adj c d" and da: "vert_adj d a"
    and aV: "a ∈ V" and bV: "b ∈ V" and cV: "c ∈ V" and dV: "d ∈ V"
    and ac: "a ≠ c" and bd: "b ≠ d"
    and nac: "¬ vert_adj a c" and nbd: "¬ vert_adj b d"
    using induces_C4_inV[OF H] by (auto simp: induces_C4_def)
  have "a ∈ C ∨ b ∈ C"
    using split_partition_edge_hits_clique[OF sp ab] .
  moreover have "b ∈ C ∨ c ∈ C"
    using split_partition_edge_hits_clique[OF sp bc] .
  moreover have "c ∈ C ∨ d ∈ C"
    using split_partition_edge_hits_clique[OF sp cd] .
  moreover have "d ∈ C ∨ a ∈ C"
    using split_partition_edge_hits_clique[OF sp da] .
  moreover have "¬ (a ∈ C ∧ c ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp aV cV ac nac] .
  moreover have "¬ (b ∈ C ∧ d ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp bV dV bd nbd] .
  ultimately show False
    by blast
qed

lemma split_partition_forbids_C5:
  assumes sp: "is_split_partition C I"
    and H: "induces_C5 a b c d e"
  shows False
proof -
  from H have ab: "vert_adj a b" and bc: "vert_adj b c" and cd: "vert_adj c d" and de: "vert_adj d e" and ea: "vert_adj e a"
    and aV: "a ∈ V" and bV: "b ∈ V" and cV: "c ∈ V" and dV: "d ∈ V" and eV: "e ∈ V"
    and ac: "a ≠ c" and ad: "a ≠ d" and bd: "b ≠ d" and be: "b ≠ e" and ce: "c ≠ e"
    and nac: "¬ vert_adj a c" and nad: "¬ vert_adj a d" and nbd: "¬ vert_adj b d" and nbe: "¬ vert_adj b e" and nce: "¬ vert_adj c e"
    using induces_C5_inV[OF H] by (auto simp: induces_C5_def)
  have "a ∈ C ∨ b ∈ C"
    using split_partition_edge_hits_clique[OF sp ab] .
  moreover have "b ∈ C ∨ c ∈ C"
    using split_partition_edge_hits_clique[OF sp bc] .
  moreover have "c ∈ C ∨ d ∈ C"
    using split_partition_edge_hits_clique[OF sp cd] .
  moreover have "d ∈ C ∨ e ∈ C"
    using split_partition_edge_hits_clique[OF sp de] .
  moreover have "e ∈ C ∨ a ∈ C"
    using split_partition_edge_hits_clique[OF sp ea] .
  moreover have "¬ (a ∈ C ∧ c ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp aV cV ac nac] .
  moreover have "¬ (a ∈ C ∧ d ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp aV dV ad nad] .
  moreover have "¬ (b ∈ C ∧ d ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp bV dV bd nbd] .
  moreover have "¬ (b ∈ C ∧ e ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp bV eV be nbe] .
  moreover have "¬ (c ∈ C ∧ e ∈ C)"
    using split_partition_nonedge_not_both_clique[OF sp cV eV ce nce] .
  ultimately show False
    by blast
qed

lemma split_graph_imp_foldes_hammer_free:
  assumes "is_split_graph"
  shows "foldes_hammer_free"
proof -
  obtain C I where sp: "is_split_partition C I"
    using assms by (auto simp: is_split_graph_def)
  have "¬ has_induced_2K2"
    using sp split_partition_forbids_2K2 by (auto simp: has_induced_2K2_def)
  moreover have "¬ has_induced_C4"
    using sp split_partition_forbids_C4 by (auto simp: has_induced_C4_def)
  moreover have "¬ has_induced_C5"
    using sp split_partition_forbids_C5 by (auto simp: has_induced_C5_def)
  ultimately show ?thesis
    by (simp add: foldes_hammer_free_def)
qed

lemma outside_adjacent_nonneighbor_sets_nested:
  assumes fh: "foldes_hammer_free"
    and Kmax: "maximum_clique K"
    and uO: "u ∈ V - K"
    and vO: "v ∈ V - K"
    and uv: "vert_adj u v"
  shows "{x∈K. ¬ vert_adj x u} ⊆ {x∈K. ¬ vert_adj x v} ∨
         {x∈K. ¬ vert_adj x v} ⊆ {x∈K. ¬ vert_adj x u}"
proof (rule ccontr)
  let ?A = "{x∈K. ¬ vert_adj x u}"
  let ?B = "{x∈K. ¬ vert_adj x v}"
  assume not_nested: "¬ (?A ⊆ ?B ∨ ?B ⊆ ?A)"
  then obtain a b where aA: "a ∈ ?A" and aB: "a ∉ ?B" and bB: "b ∈ ?B" and bA: "b ∉ ?A"
    by blast
  have aK: "a ∈ K" and aNu: "¬ vert_adj a u"
    using aA by auto
  have bK: "b ∈ K" and bNv: "¬ vert_adj b v"
    using bB by auto
  have av: "vert_adj a v"
    using aB aK by auto
  have bu: "vert_adj b u"
    using bA bK by auto
  have ab_ne: "a ≠ b"
    using aA bA by auto
  have uv_ne: "u ≠ v"
    using vert_adj_neq[OF uv] .
  have Kclq: "is_clique K"
    using Kmax by (auto simp: maximum_clique_def cliques_def)
  have ab: "vert_adj a b"
    using clique_pair_adj[OF Kclq aK bK ab_ne] .
  have vu: "vert_adj v u"
    using uv by (simp add: vert_adj_sym)
  have ub: "vert_adj u b"
    using bu by (simp add: vert_adj_sym)
  have ba: "vert_adj b a"
    using ab by (simp add: vert_adj_sym)
  have vNb: "¬ vert_adj v b"
    using bNv by (simp add: vert_adj_sym)
  have dist: "distinct [a, v, u, b]"
    using aK bK uO vO ab_ne uv_ne by auto
  have "induces_C4 a v u b"
    using dist av vu ub ba aNu vNb
    by (simp add: induces_C4_def)
  then have "has_induced_C4"
    by (auto simp: has_induced_C4_def)
  with fh show False
    by (simp add: foldes_hammer_free_def)
qed

lemma outside_adjacent_smaller_nonneighbor_set_singleton:
  assumes fh: "foldes_hammer_free"
    and Kmax: "maximum_clique K"
    and uO: "u ∈ V - K"
    and vO: "v ∈ V - K"
    and uv: "vert_adj u v"
    and AB: "{x∈K. ¬ vert_adj x u} ⊆ {x∈K. ¬ vert_adj x v}"
  obtains a where "{x∈K. ¬ vert_adj x u} = {a}" and "a ∈ K" and "¬ vert_adj a u" and "¬ vert_adj a v"
proof -
  have uV: "u ∈ V" and unotK: "u ∉ K"
    using uO by auto
  obtain a where aK: "a ∈ K" and aNu: "¬ vert_adj a u"
    using maximum_clique_outside_has_nonneighbor[OF Kmax uV unotK] by blast
  have aA: "a ∈ {x∈K. ¬ vert_adj x u}"
    using aK aNu by auto
  have aB: "a ∈ {x∈K. ¬ vert_adj x v}"
    using AB aA by blast
  have aNv: "¬ vert_adj a v"
    using aB by auto
  have Aeq: "{x∈K. ¬ vert_adj x u} = {a}"
  proof (rule subset_antisym)
    show "{x∈K. ¬ vert_adj x u} ⊆ {a}"
    proof
      fix b
      assume bA: "b ∈ {x∈K. ¬ vert_adj x u}"
      show "b ∈ {a}"
      proof (rule ccontr)
        assume bneq: "b ∉ {a}"
        then have ab_ne: "a ≠ b"
          by auto
        have bK: "b ∈ K" and bNu: "¬ vert_adj b u"
          using bA by auto
        have bB: "b ∈ {x∈K. ¬ vert_adj x v}"
          using AB bA by blast
        have bNv: "¬ vert_adj b v"
          using bB by auto
        have uv_ne: "u ≠ v"
          using vert_adj_neq[OF uv] .
        have Kclq: "is_clique K"
          using Kmax by (auto simp: maximum_clique_def cliques_def)
        have ab: "vert_adj a b"
          using clique_pair_adj[OF Kclq aK bK ab_ne] .
        have dist: "distinct [a, b, u, v]"
          using aK bK uO vO ab_ne uv_ne by auto
        have "induces_2K2 a b u v"
          using dist ab uv aNu aNv bNu bNv
          by (simp add: induces_2K2_def)
        then have "has_induced_2K2"
          by (auto simp: has_induced_2K2_def)
        with fh show False
          by (simp add: foldes_hammer_free_def)
      qed
    qed
  next
    show "{a} ⊆ {x∈K. ¬ vert_adj x u}"
      using aK aNu by auto
  qed
  show thesis
    using that Aeq aK aNu aNv by blast
qed

lemma orient_outside_edge_for_swap:
  assumes fh: "foldes_hammer_free"
    and Kmax: "maximum_clique K"
    and uO: "u ∈ V - K"
    and vO: "v ∈ V - K"
    and uv: "vert_adj u v"
  obtains u' v' a where
      "{u', v'} = {u, v}"
    and "u' ∈ V - K"
    and "v' ∈ V - K"
    and "vert_adj u' v'"
    and "{x∈K. ¬ vert_adj x u'} = {a}"
    and "a ∈ K"
    and "¬ vert_adj a u'"
    and "¬ vert_adj a v'"
proof -
  have nested:
    "{x∈K. ¬ vert_adj x u} ⊆ {x∈K. ¬ vert_adj x v} ∨
     {x∈K. ¬ vert_adj x v} ⊆ {x∈K. ¬ vert_adj x u}"
    using outside_adjacent_nonneighbor_sets_nested[OF fh Kmax uO vO uv] .
  then show thesis
  proof
    assume AB: "{x∈K. ¬ vert_adj x u} ⊆ {x∈K. ¬ vert_adj x v}"
    obtain a where Aeq: "{x∈K. ¬ vert_adj x u} = {a}" and aK: "a ∈ K"
      and aNu: "¬ vert_adj a u" and aNv: "¬ vert_adj a v"
      using outside_adjacent_smaller_nonneighbor_set_singleton[OF fh Kmax uO vO uv AB] by blast
    show thesis
      using that[of u v a] uO vO uv Aeq aK aNu aNv by simp
  next
    assume BA: "{x∈K. ¬ vert_adj x v} ⊆ {x∈K. ¬ vert_adj x u}"
    have vu: "vert_adj v u"
      using uv by (simp add: vert_adj_sym)
    obtain a where Beq: "{x∈K. ¬ vert_adj x v} = {a}" and aK: "a ∈ K"
      and aNv: "¬ vert_adj a v" and aNu: "¬ vert_adj a u"
      using outside_adjacent_smaller_nonneighbor_set_singleton[OF fh Kmax vO uO vu BA] by blast
    show thesis
      using that[of v u a] vO uO vu Beq aK aNv aNu by auto
  qed
qed

lemma replace_unique_nonneighbor_maximum_clique:
  assumes Kmax: "maximum_clique K"
    and uO: "u ∈ V - K"
    and Au: "{x∈K. ¬ vert_adj x u} = {a}"
  shows "maximum_clique (insert u (K - {a}))"
proof -
  have Kclq: "is_clique K"
    using Kmax by (auto simp: maximum_clique_def cliques_def)
  have aK: "a ∈ K" and aNu: "¬ vert_adj a u"
    using Au by auto
  have uV: "u ∈ V" and unotK: "u ∉ K"
    using uO by auto
  have Ksub: "K - {a} ⊆ K"
    by auto
  have Kminclq: "is_clique (K - {a})"
    using clique_mono[OF Kclq Ksub] .
  have uadj: "∀x∈K - {a}. vert_adj x u"
  proof
    fix x
    assume xK: "x ∈ K - {a}"
    have xK0: "x ∈ K" and xnea: "x ≠ a"
      using xK by auto
    have "x ∉ {x∈K. ¬ vert_adj x u}"
      using Au xnea by auto
    then show "vert_adj x u"
      using xK0 by auto
  qed
  have newclq: "is_clique (insert u (K - {a}))"
    using insert_clique_if_all_adj[OF Kminclq uV] unotK uadj by auto
  have finK: "finite K"
    using maximum_clique_finite[OF Kmax] .
  have newcard: "card (insert u (K - {a})) = card K"
  proof -
    have u_not_Ka: "u ∉ K - {a}"
      using unotK by auto
    have "card (insert u (K - {a})) = Suc (card (K - {a}))"
      using finK u_not_Ka by simp
    also have "... = Suc (card K - 1)"
      using finK aK by simp
    also have "... = card K"
    proof -
      have "K ≠ {}"
        using aK by auto
      have "0 < card K"
        using finK ‹K ≠ {}› by (simp add: card_gt_0_iff)
      then show ?thesis
        by arith
    qed
    finally show ?thesis .
  qed
  have newin: "insert u (K - {a}) ∈ cliques"
    using newclq by (simp add: cliques_def)
  have newbound: "∀C∈cliques. card C ≤ card (insert u (K - {a}))"
  proof
    fix C
    assume Cin: "C ∈ cliques"
    from Kmax have "∀C∈cliques. card C ≤ card K"
      by (simp add: maximum_clique_def)
    then show "card C ≤ card (insert u (K - {a}))"
      using Cin newcard by simp
  qed
  show ?thesis
    using newin newbound by (simp add: maximum_clique_def)
qed

lemma replacement_edge_transfer:
  assumes fh: "foldes_hammer_free"
    and Kmax: "maximum_clique K"
    and uO: "u ∈ V - K"
    and vO: "v ∈ V - K"
    and uv: "vert_adj u v"
    and Au: "{x∈K. ¬ vert_adj x u} = {a}"
    and aNv: "¬ vert_adj a v"
    and zO: "z ∈ V - K"
    and zne: "z ≠ u"
    and az: "vert_adj a z"
  shows "vert_adj u z"
proof (rule ccontr)
  assume uz: "¬ vert_adj u z"
  have aK: "a ∈ K" and aNu: "¬ vert_adj a u"
    using Au by auto
  have uv_ne: "u ≠ v"
    using vert_adj_neq[OF uv] .
  have vz: "vert_adj v z"
  proof (rule ccontr)
    assume vz_not: "¬ vert_adj v z"
    have zv_ne: "z ≠ v"
      using az aNv by auto
    have dist: "distinct [a, z, u, v]"
      using aK uO vO zO uv_ne zne az zv_ne by auto
    have zNu: "¬ vert_adj z u"
      using uz by (simp add: vert_adj_sym)
    have zNv: "¬ vert_adj z v"
      using vz_not by (simp add: vert_adj_sym)
    have "induces_2K2 a z u v"
      using dist az uv aNu aNv zNu zNv
      by (simp add: induces_2K2_def)
    then have "has_induced_2K2"
      by (auto simp: has_induced_2K2_def)
    with fh show False
      by (simp add: foldes_hammer_free_def)
  qed
  have zv: "vert_adj z v"
    using vz by (simp add: vert_adj_sym)
  have nested:
    "{x∈K. ¬ vert_adj x z} ⊆ {x∈K. ¬ vert_adj x v} ∨
     {x∈K. ¬ vert_adj x v} ⊆ {x∈K. ¬ vert_adj x z}"
    using outside_adjacent_nonneighbor_sets_nested[OF fh Kmax zO vO zv] .
  have zV: "z ∈ V" and znotK: "z ∉ K"
    using zO by auto
  obtain c where cK: "c ∈ K" and cNz: "¬ vert_adj c z"
    using maximum_clique_outside_has_nonneighbor[OF Kmax zV znotK] by blast
  have CsubB: "{x∈K. ¬ vert_adj x z} ⊆ {x∈K. ¬ vert_adj x v}"
  proof -
    from nested show ?thesis
    proof
      assume h: "{x∈K. ¬ vert_adj x z} ⊆ {x∈K. ¬ vert_adj x v}"
      show ?thesis by fact
    next
      assume h: "{x∈K. ¬ vert_adj x v} ⊆ {x∈K. ¬ vert_adj x z}"
      have "a ∈ {x∈K. ¬ vert_adj x z}"
        using h aK aNv by auto
      then have aNz: "¬ vert_adj a z"
        by auto
      then have False
        using az by contradiction
      then show ?thesis
        by blast
    qed
  qed
  have cNv: "¬ vert_adj c v"
    using CsubB cK cNz by auto
  have ca_ne: "c ≠ a"
    using az cK cNz by auto
  have cu: "vert_adj c u"
  proof -
    have "c ∉ {x∈K. ¬ vert_adj x u}"
      using Au ca_ne by auto
    then show ?thesis
      using cK by auto
  qed
  have Kclq: "is_clique K"
    using Kmax by (auto simp: maximum_clique_def cliques_def)
  have ac: "vert_adj a c"
    using clique_pair_adj[OF Kclq aK cK ca_ne[symmetric]] .
  have zv: "vert_adj z v"
    using vz by (simp add: vert_adj_sym)
  have vu: "vert_adj v u"
    using uv by (simp add: vert_adj_sym)
  have uc: "vert_adj u c"
    using cu by (simp add: vert_adj_sym)
  have ca: "vert_adj c a"
    using ac by (simp add: vert_adj_sym)
  have zNu: "¬ vert_adj z u"
    using uz by (simp add: vert_adj_sym)
  have zNc: "¬ vert_adj z c"
    using cNz by (simp add: vert_adj_sym)
  have vNc: "¬ vert_adj v c"
    using cNv by (simp add: vert_adj_sym)
  have dist: "distinct [a, z, v, u, c]"
    using aK cK uO vO zO uv_ne zne az ca_ne aNv by auto
  have "induces_C5 a z v u c"
    using dist az zv vu uc ca aNv aNu zNu zNc vNc
    by (simp add: induces_C5_def)
  then have "has_induced_C5"
    unfolding has_induced_C5_def by blast
  with fh show False
    by (simp add: foldes_hammer_free_def)
qed

lemma outside_set_after_swap:
  assumes uO: "u ∈ V - K"
    and aV: "a ∈ V"
    and aK: "a ∈ K"
  shows "V - insert u (K - {a}) = insert a ((V - K) - {u})"
  using assms by auto

lemma swap_outside_edges_inj:
  assumes uO: "u ∈ V - K"
    and aK: "a ∈ K"
  shows "inj_on (%e. if a ∈ e then insert u (e - {a}) else e)
      (induced_edges (V - insert u (K - {a})))"
proof (rule inj_onI)
  let ?I' = "V - insert u (K - {a})"
  let ?f = "%e. if a ∈ e then insert u (e - {a}) else e"
  fix e1 e2
  assume e1I: "e1 ∈ induced_edges ?I'"
    and e2I: "e2 ∈ induced_edges ?I'"
    and eq: "?f e1 = ?f e2"
  have u_not_I': "u ∉ ?I'"
    using uO by auto
  have e1ss: "e1 ⊆ ?I'" and e2ss: "e2 ⊆ ?I'"
    using e1I e2I by (auto simp: induced_edges_def)
  show "e1 = e2"
  proof (cases "a ∈ e1")
    case False
    then have f1: "?f e1 = e1"
      by simp
    show ?thesis
    proof (cases "a ∈ e2")
      case False
      with eq f1 show ?thesis
        by simp
    next
      case True
      then have "u ∈ ?f e2"
        by simp
      then have "u ∈ e1"
        using eq f1 by simp
      with e1ss u_not_I' show ?thesis
        by blast
    qed
  next
    case e1_has_a: True
    show ?thesis
    proof (cases "a ∈ e2")
      case False
      then have f2: "?f e2 = e2"
        by simp
      have "u ∈ ?f e1"
        using e1_has_a by simp
      then have "u ∈ e2"
        using eq f2 by simp
      with e2ss u_not_I' show ?thesis
        by blast
    next
      case e2_has_a: True
      have u_not_e1: "u ∉ e1 - {a}" and u_not_e2: "u ∉ e2 - {a}"
        using e1ss e2ss u_not_I' by blast+
      have "insert u (e1 - {a}) = insert u (e2 - {a})"
        using eq e1_has_a e2_has_a by simp
      then have diff_eq: "e1 - {a} = e2 - {a}"
      proof -
        have "(insert u (e1 - {a})) - {u} = (insert u (e2 - {a})) - {u}"
          using ‹insert u (e1 - {a}) = insert u (e2 - {a})› by simp
        then show ?thesis
          using u_not_e1 u_not_e2 by auto
      qed
      have "e1 = insert a (e1 - {a})"
        using e1_has_a by blast
      moreover have "e2 = insert a (e2 - {a})"
        using e2_has_a by blast
      ultimately show ?thesis
        using diff_eq by simp
    qed
  qed
qed

lemma swap_outside_edges_image_subset:
  assumes fh: "foldes_hammer_free"
    and Kmax: "maximum_clique K"
    and uO: "u ∈ V - K"
    and vO: "v ∈ V - K"
    and uv: "vert_adj u v"
    and Au: "{x∈K. ¬ vert_adj x u} = {a}"
    and aNv: "¬ vert_adj a v"
  shows "(%e. if a ∈ e then insert u (e - {a}) else e) `
      induced_edges (V - insert u (K - {a}))
      ⊆ induced_edges (V - K)"
proof
  let ?I = "V - K"
  let ?I' = "V - insert u (K - {a})"
  let ?f = "%e. if a ∈ e then insert u (e - {a}) else e"
  have aK: "a ∈ K"
    using Au by auto
  have aV: "a ∈ V"
    using Kmax aK by (auto simp: maximum_clique_def cliques_def is_clique_def)
  have Ieq: "?I' = insert a (?I - {u})"
    using outside_set_after_swap[OF uO aV aK] .
  fix x
  assume xin: "x ∈ ?f ` induced_edges ?I'"
  then obtain e where eI: "e ∈ induced_edges ?I'" and xeq: "x = ?f e"
    by blast
  have ess: "e ⊆ ?I'" and eE: "e ∈ E"
    using eI by (auto simp: induced_edges_def)
  show "x ∈ induced_edges ?I"
  proof (cases "a ∈ e")
    case False
    then have xeqe: "x = e"
      using xeq by simp
    have "e ⊆ ?I"
    proof
      fix y
      assume "y ∈ e"
      with ess False show "y ∈ ?I"
        by (auto simp: Ieq)
    qed
    with eE xeqe show ?thesis
      by (auto simp: induced_edges_def)
  next
    case True
    from eE have ecard: "card e = 2"
      using two_edges by auto
    from True ecard obtain z where e: "e = {a, z}" and zne: "z ≠ a"
      by (auto simp: card_2_iff)
    have zI: "z ∈ ?I - {u}"
      using ess True e zne by (auto simp: Ieq)
    then have zO: "z ∈ V - K" and zne_u: "z ≠ u"
      by auto
    have az: "vert_adj a z"
      using eE e by (simp add: vert_adj_def)
    have uz: "vert_adj u z"
      using replacement_edge_transfer[OF fh Kmax uO vO uv Au aNv zO zne_u az] .
    have xeqz: "x = {u, z}"
      using xeq True e zne by simp
    have uzE: "{u, z} ∈ E"
      using uz by (simp add: vert_adj_def)
    have uz_sub: "{u, z} ⊆ ?I"
      using uO zO by auto
    show ?thesis
      using xeqz uzE uz_sub by (auto simp: induced_edges_def)
  qed
qed

lemma swap_outside_edges_missing_uv:
  assumes uO: "u ∈ V - K"
    and vO: "v ∈ V - K"
    and uv: "vert_adj u v"
    and aK: "a ∈ K"
    and aNv: "¬ vert_adj a v"
  shows "{u, v} ∈ induced_edges (V - K)"
    and "{u, v} ∉ (%e. if a ∈ e then insert u (e - {a}) else e) `
      induced_edges (V - insert u (K - {a}))"
proof -
  have uv_in: "{u, v} ∈ induced_edges (V - K)"
    using uO vO uv by (auto simp: induced_edges_def vert_adj_def)
  show "{u, v} ∈ induced_edges (V - K)"
    using uv_in .
  show "{u, v} ∉ (%e. if a ∈ e then insert u (e - {a}) else e) `
      induced_edges (V - insert u (K - {a}))"
  proof
    let ?I' = "V - insert u (K - {a})"
    let ?f = "%e. if a ∈ e then insert u (e - {a}) else e"
    assume img: "{u, v} ∈ ?f ` induced_edges ?I'"
    then obtain e where eI: "e ∈ induced_edges ?I'" and eq: "{u, v} = ?f e"
      by blast
    have u_not_I': "u ∉ ?I'"
      using uO by auto
    have ess: "e ⊆ ?I'" and eE: "e ∈ E"
      using eI by (auto simp: induced_edges_def)
    have uv_ne: "u ≠ v"
      using vert_adj_neq[OF uv] .
    show False
    proof (cases "a ∈ e")
      case False
      then have "{u, v} = e"
        using eq by simp
      then have "u ∈ e"
        by auto
      with ess u_not_I' show False
        by blast
    next
      case True
      from eE have ecard: "card e = 2"
        using two_edges by auto
      from True ecard obtain z where e: "e = {a, z}" and zne: "z ≠ a"
        by (auto simp: card_2_iff)
      have zI': "z ∈ ?I'"
        using ess True e zne by auto
      then have zne_u: "z ≠ u"
        using u_not_I' by auto
      have "{u, v} = {u, z}"
        using eq True e zne by simp
      then have zeqv: "z = v"
        using uv_ne zne_u by auto
      have "vert_adj a z"
        using eE e by (simp add: vert_adj_def)
      with aNv zeqv show False
        by simp
    qed
  qed
qed

lemma outside_edge_count_swap_strict:
  assumes fh: "foldes_hammer_free"
    and Kmax: "maximum_clique K"
    and uO: "u ∈ V - K"
    and vO: "v ∈ V - K"
    and uv: "vert_adj u v"
    and Au: "{x∈K. ¬ vert_adj x u} = {a}"
    and aNv: "¬ vert_adj a v"
  shows "outside_edge_count (insert u (K - {a})) < outside_edge_count K"
proof -
  let ?I = "V - K"
  let ?I' = "V - insert u (K - {a})"
  let ?f = "%e. if a ∈ e then insert u (e - {a}) else e"
  have aK: "a ∈ K"
    using Au by auto
  have inj: "inj_on ?f (induced_edges ?I')"
    using swap_outside_edges_inj[OF uO aK] .
  have imgsub: "?f ` induced_edges ?I' ⊆ induced_edges ?I"
    using swap_outside_edges_image_subset[OF fh Kmax uO vO uv Au aNv] .
  have uv_in: "{u, v} ∈ induced_edges ?I"
    using swap_outside_edges_missing_uv[OF uO vO uv aK aNv] by blast
  have uv_not_img: "{u, v} ∉ ?f ` induced_edges ?I'"
    using swap_outside_edges_missing_uv[OF uO vO uv aK aNv] by blast
  have psub: "?f ` induced_edges ?I' ⊂ induced_edges ?I"
    using imgsub uv_in uv_not_img by blast
  have finI': "finite (induced_edges ?I')"
    by (rule finite_induced_edges_subset_V) auto
  have finI: "finite (induced_edges ?I)"
    by (rule finite_induced_edges_subset_V) auto
  have card_img: "card (?f ` induced_edges ?I') = card (induced_edges ?I')"
    by (rule card_image[OF inj])
  have "card (induced_edges ?I') = card (?f ` induced_edges ?I')"
    using card_img by simp
  also have "... < card (induced_edges ?I)"
    using finI psub by (rule psubset_card_mono)
  finally show ?thesis
    by (simp add: outside_edge_count_def)
qed

theorem foldes_hammer_converse:
  assumes fh: "foldes_hammer_free"
  shows "is_split_graph"
proof -
  obtain K where Kmax: "maximum_clique K"
    and Kbest: "∀L. maximum_clique L ⟶ outside_edge_count K ≤ outside_edge_count L"
    using obtain_best_clique by blast
  have Kclq: "is_clique K"
    using Kmax by (auto simp: maximum_clique_def cliques_def)
  have indep: "is_independent_set (V - K)"
  proof (rule ccontr)
    assume not_indep: "¬ is_independent_set (V - K)"
    then obtain u v where uO: "u ∈ V - K" and vO: "v ∈ V - K" and uv: "vert_adj u v"
      by (auto simp: is_independent_alt)
    obtain u' v' a where uvset: "{u', v'} = {u, v}"
      and u'O: "u' ∈ V - K" and v'O: "v' ∈ V - K" and uv': "vert_adj u' v'"
      and Au': "{x∈K. ¬ vert_adj x u'} = {a}"
      and aK: "a ∈ K" and aNu': "¬ vert_adj a u'" and aNv': "¬ vert_adj a v'"
      using orient_outside_edge_for_swap[OF fh Kmax uO vO uv] by blast
    let ?K' = "insert u' (K - {a})"
    have K'max: "maximum_clique ?K'"
      using replace_unique_nonneighbor_maximum_clique[OF Kmax u'O Au'] .
    have dec: "outside_edge_count ?K' < outside_edge_count K"
      using outside_edge_count_swap_strict[OF fh Kmax u'O v'O uv' Au' aNv'] .
    have "outside_edge_count K ≤ outside_edge_count ?K'"
      using Kbest K'max by blast
    with dec show False
      by simp
  qed
  show ?thesis
    using Kclq indep by (auto simp: split_graph_alt)
qed

theorem foldes_hammer:
  "is_split_graph ⟷ foldes_hammer_free"
  using foldes_hammer_converse split_graph_imp_foldes_hammer_free by blast

end

end